# LTL -> Büchi Automata

LTL formula:
Enable new optimizations (e.g. direct simulation, reverse simulation, bdds)

The LTL formulas themselves are defined with the operators and connectives below.

## Accepted temporal logic operators are:

```
G    (Always)
F    (Eventually)
U    (Strong Until)
W    (Weak Until) (p W q) == ((p U q) || G p)
R    (Release) (p R q) == !(!p U !q)
M    (The Dual of Weak Until) (p M q) == !(!p W !q)
X    (Next)
```

## Boolean Operators:

```
&&   (And)
||   (Or)
!    (Negation)
->   (Implication)
<->  (IFF)
```

All operators are left-associative, except the operator "->"

## Boolean Predicates:

```
true, false
any lowercase string
```

## Precedence:

Sorted in order from least to greatest, the operator precedences are:
```
<->, -> , ||,  &&
W,  U,  M,  R,  F , G
X , !
```

## Examples:

```
G p
!( F !q )
p U q
p U (G (q U r))
Fp && F!p
!(G F p1 && G F p2 -> G(q -> F r))
G(q -> ((!p U (s || r)) || G !p))
G((q && Fr) -> (!p U (s || r)))
!(p1 U (p2 U (p3 U p4)))
F r -> (p -> (!r U (s && !r))) U r
G((q && F r) -> (p -> (!r U (s && !r && !z && X((!r && !z) U t)))) U r)
((p1 U q1) || (t1 R p1)) && ((p2 U q2) || (t2 R p2))
```

Last updated Jul 22 2002 by Leonardo de Moura