ABSTRACT
We present an algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program. The running time of the algorithm is exponential in the size of the formula but linear in the size of the checked program. The algorithm yields also a formal proof in case the formula is valid over the program. The algorithm has four versions that check satisfiability by unrestricted, impartial, just and fair computations of the given program.
- [BK] H. Barringer and R. Kuiper, A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, (1983).Google Scholar
- [BMP] M. Ben-Ari, Z. Manna, A. Pnueli, The Temporal Logic of Branching Time, Acta Informatica 20 (1983) pp. 207-226.Google ScholarDigital Library
- [CE] E. M. Clarke, E. A. Emerson, Synthesis of Synchronization Skeletons for Branching Time Temporal Logic, Proc. of the Workshop on Logic of Programs, Yorktown Heights, NY, Springer Verlag LNCS Vol. 131 (1982). Google ScholarDigital Library
- [CES] E. M. Clarke, E. A. Emerson and A. P. Sistla, Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, 10th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1983. Google ScholarDigital Library
- [EH] E. A. Emerson, J. Y. Halpern, Sometimes and Not Never Revisited: On Branching Time Versus Linear Time, 10th ACM Symposium on Principles of Programming Languages, Austin, Texas, 1983. Google ScholarDigital Library
- [EL] E. A. Emerson and C. L. Lei, Temporal Model Checking Under Generalieed Fairness Constraints, University of Texas, Austin July (1984). Google ScholarDigital Library
- [KVR] R. Koymans, J. Vytopil and W. P. de Roever, Real-time Programming and Asynchronous Message Passing, 2nd ACM Symposium on Principles of Distributed Computing, Montreal, Canada (1983) 187-197. Google ScholarDigital Library
- [L1] L. Lamport, 'Sometime' is Sometimes 'Not Never' A Tutorial on the Temporal Logic of Programs, Proc. of the 7th Annual ACM Symposium on Principles of Programming Languages , Jan. 1980. Google ScholarDigital Library
- [L2] L. Lamport, What good is Temporal Logic? Information Processing 1983, Proc. of the 9th IFIP Congress, R.E.A. Mason Editor, North Holland, pp. 657-668.Google Scholar
- [LPS] D. Lehmann, A. Pnueli, J. Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Automata, Languages and Programming, Springer Verlag LNCS 115 (1981) pp. 265-277. Google ScholarDigital Library
- [MP1] Z. Manna, A. Pnueli, Verification of Concurrent Programs: The Temporal Framework, in the Correctness Problem in Computer Science, R. S. Boyer, J. S. Moore Editors, International Lecture Series in Computer Science, Academic Press (1981). Google ScholarDigital Library
- [MP2] Z. Manna, A. Pnueli, Proving Precedence Properties: The Temporal Way, Technical Report CS84-04, The Weiemann Institute February 1984, also a shorter version in Automata, Languages and Programming 10th Colloquium Barcelona, July, 1983, Springer Verlag LNCS 154, pp. 491-512. Google ScholarDigital Library
- [MP3] Z. Manna, A. Pnueli, Verification of Concurrent Programs: A Temporal Proof System, Foundations of Computer Science IV, Distributed Systems: Part 2, Semantics and Logic, J. W. DeBakker, J. Van Leeuwen Editors, Mathematical Centre Tracts 159 Amsterdam 1983, pp. 163-255.Google Scholar
- [MP4] Z. Manna, A. Pnueli, How to Cook a Temporal Proof System for Your Pet Language, Symposium on Principles of Programming Languages , Austin, Texas (1983). Google ScholarDigital Library
- [QS1] J. P. Quelle, J. Sifakis, Specification and Verification of Concurrent Systems in CESAR, Proc. of the 5th International Symposium on Programming, 1981. Google ScholarDigital Library
- [QS2] J. P. Quelle, J. Sifakis, Fairness and Related Properties in Transition Systems, IMAG Research Report 292, Grenoble, March 1982.Google Scholar
- [SC] A. P. Sistla, E. M. Clarke, The Complexity of Propositional Temporal Logic, 14th ACM Symaposium on Theory of Computing, May 1982, pp. 159-167. Google ScholarDigital Library
- [SP] R. Sherman and A. Pnueli, Semantic Tableau for Temporal Logic, Technical Report, CS81- 21, Weizmann Institute of Science, September (1981).Google Scholar
- [ZWRCB] P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand, Towards Analyzing and Synthesizing Protocols, IEEE Transactions on Communications , Vol. COM-28, No. 4, April 1980, pp. 651-671.Google Scholar
Index Terms
- Checking that finite state concurrent programs satisfy their linear specification
Recommendations
Model-Checking parameterized concurrent programs using linear interfaces
CAV'10: Proceedings of the 22nd international conference on Computer Aided VerificationWe consider the verification of parameterized Boolean programs— abstractions of shared-memory concurrent programs with an unbounded number of threads We propose that such programs can be model-checked by iteratively considering the program under k-round ...
Efficient Verification of Sequential and Concurrent C Programs
There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
From Two-Way to One-Way Finite State Transducers
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer ScienceAny two-way finite state automaton is equivalent to some one-way finite state automaton. This well-known result, shown by Rabin and Scott and independently by Shepherd son, states that two-way finite state automata (even non-deterministic) characterize ...
Comments