×

zbMATH — the first resource for mathematics

A quick axiomatisation of LTL with past. (English) Zbl 1058.03023
Summary: The paper defines focus games for satisfiability of linear time temporal logic with past operators. The games are defined in such a way that a complete axiomatisation can easily be obtained from the game rules.

MSC:
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] and The temporal analysis of fairness. In: Proc. 7th Symp. on Principles of Programming Languages (POPL’80), pp. 163-173 (ACM, January 1980).
[2] On tense logic and the theory of order. PhD thesis, Univ. of California, 1968.
[3] and Focus games for satisfiability and completeness of temporal logic. In: Proc. 16th Symp. on Logic in Computer Science (LICS’01), Boston (MA), June 2001 (IEEE).
[4] The temporal logic of programs. In: Proc. 18th Symp. on Foundations of Computer Science (FOCS’77), pp. 46-57 (IEEE, Providence, RI, 1977).
[5] Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels. In: Proc. 5th Int. Congress of Mathematicians, volume II, pp. 501-504 (Cambridge University Press, Cambridge 1913).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.