Syntax of Temporal Formulae

The Büch Store follows the same syntax as used in GOAL. Below we summarize the input formats and the precedence of operators. A few examples are also provided.

Temporal Operators

Both future operators and past operators are supported.
Future Operators
Format 1 Format 2
Next () X
Eventually (Sometime) <> F
Henceforth (Always) [] G
Until U  
Wait-for (Unless) W  
Release R V

Past Operators
Format 1 Format 2
Previous (-) Y
Before (~) Z
Once <-> O
So-for [-] H
Since S  
Back-to B  
Trigger T


Boolean Operators

Format 1 Format 2
Not ~ !
And /\ &
Or \/ |
Implication --> ->
Equivalence <-->  


Quantifiers

Format
ForallA
ExistsE

Note: like in GOAL, quantifiers may not appear within the scope of a temporal operator.



Operator Precedence

The Büch Store assumes the following order of precedence:
Unary Operator > Temporal Binary Operator > Boolean Binary Operator



Examples

  • <> p or F p
  • []<> p or GF p or G(F p)
  • [](p--> <> q) or G(p-->F q) or G(p--> (F q))
  • [](p--> <-> q) or G(p-->O q) or G(p--> (O q))
  • [](~p \/ ()q) or G(~p \/ X q) or G(~p \/ (X q))
  • []p S q or G p S q or (G p)S q
  • [](p --> p S q) or G(p --> p S q) or G(p-->(p S q))
  • E t : t /\ [] ((t --> p) /\ (t <--> () (~ t)))


Bibliographic Notes

The Quantified Propositional Temporal Logic (QPTL) [1] is an extension of the Propositional Temporal Logic (PTL) with quantification over atomic propositions. PTL is one of the simplest kinds and most commonly used of linear temporal logic, where temporal formulae are constructed by applying boolean connectives and temporal operators to atomic propositions drawn from a predefined universe. People in the model checking community often refer to PTL as LTL, considering it as a sublogic of the generalized Computation Tree Logic (CTL*) [2]. The term LTL has also been used to denote the full linear temporal logic of Manna and Pnueli [3]. So, PTL can also be seen as the pure propositional restriction of Manna and Pnueli's LTL, particularly when past temporal operators are included in the logic. PTL is simple and convenient enough for expressing many common, interesting safety and liveness properties. Yet, situations had arisen that called for a more expressive but still decidable logic. For example, PTL is incapable of expressing the fact that a proposition holds exactly at every other state of a sequence [4], which is an omega-regular property. QPTL was one of the decidable extensions to PTL, achieving omega-regularity. It was originally introduced by Sistla [1] and further studied by Sistla et al. [5] and by Kesten and Pnueli [6].

  1. A.P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. Ph.D. Thesis, Harvard University, 1983.
  2. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999.
  3. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
  4. P. Wolper. Temporal Logic Can Be More Expressive. Information and Computation, 56(1-2):72-99, 1983.
  5. A.P. Sistla, M.Y. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic. Throretical Computer Science, 49:217-237, 1987.
  6. Y. Kesten and A. Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation, 12(5):701-745, 2002.