Abstract
An extension of propositional temporal logic that includes operators referring to a bounded past is considered. An exponential time decision procedure and a complete axiomatic system are presented. A suggested normal form leads to a syntactic classification of safety and liveness formulae. The adequacy of temporal logic to modular verification is examined. Finally we present the notion of α-fairness which is proved to fully capture the behavior of probabilistic finite state programs.
The work of this author was supported by the Eshkol Fund.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Alpern, B., Schneider, F.B., — Defining Liveness, Cornell University, (Oct. 1984).
Barringer, H., Kuiper R., — A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, (Nov. 1983).
Barringer, H., Kuiper, R., Pnueli, A. — Now You May Compose Temporal Logic Specifications, 16th Symposium on Theory of Computing (April 84), 51–63.
Büchi, J.R., — On a Decision Method in Restricted Second Order Arithmetic, Proc. Intern. Congr. Logic, and Philos. Sci. 1960, 1960, Stanford University Press (1962) 1–11.
Büchi, J.R., — Weak Second Order Arithmetics and Finite Automata, Z. Math. Logik Grundlagen Math 6 (1960) 66–92.
Burgess, J., — Basic Tense Logic, in Handbook of Philosophical Logic, Vol. 2 (D. Gabbay and F. Guenthner eds.) D. Reidel Pub. Co., (1984).
Choueka, Y., — Theories of Automata on ω-Tapes: A Simplified Approach, Journal of Computers and Systems Sciences 8 (1974) 117–141.
Chen, Z.C., Hoare, C.A.R., — Partial Correctness of Communicating Processes and Protocols, Technical Monograph, PRG-20 Oxford University Computing Laboratory (May 1981).
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J., — On the Temporal Analysis of Fairness, Proc of the 7th ACM Symp. on Principles of Programming Languages (1980) 163–173.
Hoare, C.A.R., — A Calculus of Total Correctness for Communicating Precesses, Technical Monograph, RPG-23 Oxford University Computing Laboratory (May 1981).
Hailpern, B., Owicki, S., — Modular Verification of Computer Communication Protocols, IEEE Trans. on Communications, COM-31, 1 (Jan. 1983) 56–68.
Kamp, H.W., — Tense Logic and the Theory of Linear Order, Ph.D. Thesis, University of California Los Angeles (1968).
Koymans, R., Vytopil, J., DeRoever, W.P., — Real Time Programming and Asynchronous Message Passing, 2nd ACM Symp. of Distributed Computing, Montreal (1983) 187–197.
Lamport, L., — What is Good in Temporal Logic?, Proceeding IFIP (1983) 657–668.
Lichtenstein, O., — Decidability and Completeness of a Temporal Proof System for Finite State Programs, M.Sc. Thesis, Tel Aviv University (1984).
Lichtenstein, O., Pnueli, A., — Checking That Finite State Concurrent Programs Satisfy Their Linear Specification, ACM Symp. on Principles of Programming Languages (1985).
Misra, J., Chandy, K.M., — Proofs of Networks of Processes, IEEE Trans. on Software Engineering 5E-7, 4 (July 1981).
McNaughton, R., Papert, S., — Counter Free Automata, MIT press, Cambridge, Mass (1971).
Manna, Z., Pnueli, A., — Verification of Concurrent Programs: A Temporal Proof System, Proc. 4th School on Advanced Programming, Amsterdam (June 1982) 163–255.
Manna, Z., Pnueli, A., — How to Cook a Temporal Proof System for your Pet Programming Language Proc of the 10th ACM Symp. on Principles of Programming Languages (1983).
Manna, Z., Pnueli, A., — Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, Science and Computer Programming, Forthcoming.
Nguyen, V., Gries, D., Owicki, S., — A Model and Temporal Proof System for Networks of Processes, Proc of the 12th ACM Symp. on Principles of Programming Languages (1985).
Owicki, S., Gries, D., — An axiomatic Proof Technique for Parallel Programs, Acta Informatica 6 (1976) 319–340.
Owicki, S., Lamport, L., — Proving Liveness Properties of Concurrent Programs, ACM TOPLAS 4,3 (July 1982) 455–495.
Peikert, R., — Propositional Temporal Logic and ω-regular Languages, Manuscript, ETH-Zürich.
Pnueli, A., — The Temporal Logic of Programs, 18th Annual Symp. on Foundation of Computer Science (1977) 46–57.
Pnueli, A., — In Transition from Global to Modular Temporal Reasoning about Programs, Proc. Advanced NATO Institute on Logic and Models for Verification and Specification of Concurrent Systems, La Colle-Sur-Loupe (Oct. 1984).
Pnueli, A., — On the Extremely Fair Treatment of Probabilistic Algorithms, Proc. of the 15th Annual ACM Symp. on Theory of Computing (1983).
Prior, — Past Present and Future, Oxford Press.
Rescher, N., Urquhart, A., — Temporal Logic, Springer Verlag (1971).
Sistla, A.P., — Characterization of Safety and Liveness Properties in Temporal Logic, University of Massachusetts, Amherst (Nov. 1984).
A.P. Sistla, E.M. Carke, The Complexity of Propositional Temporal Logic, 14th ACM Symposium on Thoery of Computing, (May 1982) 159–167.
Thomas, W., — A Combinatorial Approach to the Theory of ω-Automata, Information and Control 48,3 (March 1981) 261–283.
Vardi, M.Y., Wolper, P., — Expressiveness and Complexity of Languages for Describing Sequences, Stanford University.
Wolper, P., — Temporal Logic can be More Expressive, Proc. of the 22nd Annual Symp. on Foundation of Computer Science (1981) 340–348.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lichtenstein, O., Pnueli, A., Zuck, L. (1985). The glory of the past. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_16
Download citation
DOI: https://doi.org/10.1007/3-540-15648-8_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15648-2
Online ISBN: 978-3-540-39527-0
eBook Packages: Springer Book Archive