Abstract
This paper defines a generalization of Lamport’s Temporal Logic of Actions.We prove that our logic is stuttering-invariant and give an axiomatization of its propositional fragment. We also show that standard TLA is as expressive as our extension once quantification over flexible propositions is added.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Martín Abadi. An axiomatization of Lamport’s Temporal Logic of Actions. In Jos C. M. Baeten and Jan W. Klop, editors, CONCUR’ 90, Theories of Concurrency: Unification and Extension, volume 458 of Lecture Notes in Computer Science, pages 57–69, Berlin, 1990. Springer-Verlag. A revised version is available on the Web at http://www.research.digital. com/SRC/personal/Martin Abadi/allpapers.html.
Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 81(2):253–284, May 1991.
Martín Abadi and Leslie Lamport. An old-fashioned recipe for real time. Research Report 91, Digital Equipment Corporation, Systems Research Center, 1992. An earlier version, without proofs, appeared in [7, pages 1–27].
Martín Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.
Martín Abadi and Stephan Merz. An abstract account of composition. In Jiří Wiedermann and Petr Hajek, editors, Mathematical Foundations of Computer Science, volume 969 of Lecture Notes in Computer Science, pages 499–508, Berlin, 1995. Springer-Verlag.
Martín Abadi and Stephan Merz. On TLA as a logic. In Manfred Broy, editor, Deductive Program Design, NATO ASI series F, pages 235–272. Springer-Verlag, Berlin, 1996.
J.W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors. Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992. Proceedings of a REX Real-TimeWorkshop, held in The Netherlands in June, 1991.
Dov Gabbay, Amir Pnueli, S. Shelah, and Jonathan Stavi. On the temporal analysis of fairness. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pages 163–173. ACM, 1980.
Fred Kröger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1987.
Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657–668, Paris, September 1983. IFIP, North-Holland.
Leslie Lamport. Hybrid systems in TLA+. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 77–102. Springer-Verlag, 1993.
Leslie Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Leslie Lamport. Refinement in state-based formalisms. Technical Note 1996-001, Digital Equipment Corporation, Systems Research Center, Palo Alto, California, December 1996.
Stephan Merz. A more complete TLA. Technical Report, Institut für Informatik, Universität München. Available on the WWW at URL http://www.pst.informatik.uni-muenchen.de/~merz/papers/gtla.html, 1999.
Stephan Merz. Isabelle/TLA. Available on the WWW at URL http://www.pst.informatik.uni-muenchen. de/~merz/isabelle/, 1997. Revised 1999.
Abdelillah Mokkedem and Dominique Méry. A stuttering closed temporal logic for modular reasoning about concurrent programs. In Temporal Logic (ICTL’ 94), volume 827 of Lecture Notes in Computer Science, pages 382–397, Bonn, 1994. Springer-Verlag.
Amir Pnueli. System specification and refinement in temporal logic. In R.K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 1–38. Springer-Verlag, 1992.
Alexander Rabinovich. Expressive completeness of temporal logic of action. In L. Brim, J. Gruska, and J. Zlatuska, editors, Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, Brno, Czech Republic, August 1998. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Merz, S. (1999). A more complete TLA. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_15
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive