A. Prasad Sistla
Abstract
Abstract
In this paper we present syntactic characterization of temporal formulas that express various properties of interest in the verification of concurrent programs. Such a characterization helps us in choosing the right techniques for proving correctness with respect to these properties. The properties that we consider include safety properties, liveness properties and fairness properties. We also present algorithms for checking if a given temporal formula expresses any of these properties.
- [ADS86] Alpern, B., Deemers, A.J. and Schneider, F.B.: Safety without Stuttering, Information Processing Letters 23(4):177–180.Google Scholar
- [AlS85] Alpern, B. and Schneider, F.: Defining Liveness, Information Processing Letters, 21:181–185.Google Scholar
- [AlS86] Alpern, B. and Schneider, F.B.: Recognizing Safety and Liveness, TR 86-727, Computer Science Department, Cornell University, Jan 1986.Google Scholar
- [CES86] Clarke, E.M., Emerson, E.A. and Sistla, A.P.: Automatic Verification of finite-state Concurrent Systems using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems 8(2):244–263.Google Scholar
- [Eme83] Alternative Semantics for Temporal LogicTheoretical Computer Science198326121130Google ScholarCross Ref
- [EmL87] Modalities for Modelchecking: Branching Time Strikes BackScience of Computer Programming19878275306Google ScholarDigital Library
- [Fra86] Francez, N.: Fairness, Texts and Monographs in Computer Science, Springer-Verlag 1986.Google Scholar
- [Lam77] Proving Correctness of Multiprocess ProgramsIEEE Transactions on Software Engineering, SE-319772125143Google ScholarDigital Library
- [Lam85] Lamport, L.: Logical Foundation, Distributed Systems-Methods and Tools for Specification, Vol 190, Lecture Notes in Computer Science, Springer-Verlag, Berlin,Google Scholar
- [LPZ85] Lichtenstein, O., Pnueli, A. and Zuck, L.: The Glory of the Past, Lecture Notes in Computer Science, 193, Proceedings of the workshop on Logics of Programs, Brookline College, June 1985.Google Scholar
- [MaP89] Completing the Temporal Picture, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, 1989Theoretical Computer Science199183197130Google ScholarDigital Library
- [MaP90] Manna, Z. and Pnueli, A.: A hierarchy of Temporal Properties, Proceedings of the 9th ACM Symposium on Principles of Distributed Computing, 1990, pp 377–408.Google Scholar
- [MaP92] Manna, Z. and Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems—Specification, Springer-Verlag, 1992.Google Scholar
- [OwL82] Owicki, S. Lamport, L.: Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems 4,No.3, 1982.Google Scholar
- [Pnu77] Pnueli, A.: The Temporal Logic of Programs, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, Providence, RI(1977).Google Scholar
- [SCFM] Sistla, A.P., Clarke, E.M., Francez, N. and Meyer, A.R.: Can Message Buffers be Axiomatized in Temporal Logic?, Information and Computation, 63(1,2):88–112.Google Scholar
- [SiC85] Sistla, A.P. and Clarke, E.M.: Complexity of Prepositional Temporal Logics, Journal of the Association for Computing Machinery, Vol.32,No.3, July 1985.Google Scholar
- [Sis83] Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed Systems, Ph.D. thesis 1983, Harvard University.Google Scholar
- [Sis85] Sistla, A.P.: On Characterization of Safety and Liveness Properties in Temporal Logic, Proceedings of the 4th ACM Symposium on Principles of Distributed Computing, August, 1985, Minaki, Canada.Google Scholar
- [Sis86] Sistla, A.P.: Characterization of Safety and Liveness Properties in Temporal Logic, GTE Laboratories Technical Report, 1986.Google Scholar
- [Tho86] Thomas, W.: Safety and Liveness Properties in Propositional Temporal Logic: Characterization and Decidability, Schriften Zur Informatik, Bericht Nr. 116. April 1986.Google Scholar
Recommendations
From liveness to promptness
Liveness temporal properties state that something "good" eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the "wait time" for an eventuality to be fulfilled. That is, F ...
Deciding safety and liveness in TPTL
We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented by ...
Comments