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