LTL -> Büchi Automata
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