Checking that finite state concurrent programs satisfy their linear specification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Checking that finite state concurrent programs satisfy their linear specification

Full text

Pdf (1.03 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages table of contents

New Orleans, Louisiana, United States

Pages: 97 - 107

Year of Publication: 1985

ISBN:0-89791-147-4

Authors

Orna Lichtenstein	Tel Aviv University, Ramat Aviv, Tel Aviv, Israel 69978
Amir Pnueli	The Weizmann Institute of Science, Rehovot, 76100 Israel

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 15, Downloads (12 Months): 117, Citation Count: 89

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/318593.318622 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	[BK] H. Barringer and R. Kuiper, A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, (1983).
	2	[BMP] M. Ben-Ari, Z. Manna, A. Pnueli, The Temporal Logic of Branching Time, Acta Informatica 20 (1983) pp. 207-226.
	3	Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
	4	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
	5	E. Allen Emerson , Joseph Y. Halpern, "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report), Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.127-140, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567081]
	6	E. A Emerson , Chin L Lei, Model Checking Under Generalized Fairness Constraints, University of Texas at Austin, Austin, TX, 1984
	7	Ron Koymans , Jan Vytopil , Willem P. de Roever, Real-time programming and asynchronous message passing, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.187-197, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806721]
	8	Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
	9	[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.
	10	Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
	11	Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
	12	Zohar Manna , Amir Pnueli, Proving Precedence Properties: The Temporal Way, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.491-512, July 18-22, 1983
	13	[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.
	14	Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
	15	Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
	16	[QS2] J. P. Quelle, J. Sifakis, Fairness and Related Properties in Transition Systems, IMAG Research Report 292, Grenoble, March 1982.
	17	A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.159-168, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802189]
	18	[SP] R. Sherman and A. Pnueli, Semantic Tableau for Temporal Logic, Technical Report, CS81- 21, Weizmann Institute of Science, September (1981).
	19	[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.

CITED BY 89

	Michael Wooldridge, Semantic Issues in the Verification of Agent Communication Languages, Autonomous Agents and Multi-Agent Systems, v.3 n.1, p.9-31, March 2000
	Steven M. German , A. Prasad Sistla, Reasoning about systems with many processes, Journal of the ACM (JACM), v.39 n.3, p.675-735, July 1992
	Karen Yorav , Orna Grumberg, Static Analysis for State-Space Reductions Preserving Temporal Logics, Formal Methods in System Design, v.25 n.1, p.67-96, July 2004
	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States
	James C. Corbett, Constructing compact models of concurrent Java programs, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.1-10, March 1998
	M. Y. Vardi, A temporal fixpoint calculus, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-259, January 10-13, 1988, San Diego, California, United States
	Costas Courcoubetis , Mihalis Yannakakis, The complexity of probabilistic verification, Journal of the ACM (JACM), v.42 n.4, p.857-907, July 1995
	P. -Y. Schobbens , J. -F. Raskin , T. A. Henzinger, Axioms for real-time logics, Theoretical Computer Science, v.274 n.1-2, p.151-182, March 6, 2002
	Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996
	Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France
	Bowen Alpern , Fred B. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.147-167, Jan. 1989
	Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000
	Christos H. Papadimitriou , Mihalis Yannakakis, On the complexity of database queries (extended abstract), Proceedings of the sixteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.12-19, May 11-15, 1997, Tucson, Arizona, United States
	Rajeev Alur , Kousha Etessami , Salvatore La Torre , Doron Peled, Parametric temporal logic for “model measuring”, ACM Transactions on Computational Logic (TOCL), v.2 n.3, p.388-407, July 2001
	Stéphane Demri , Philippe Schnoebelen, The complexity of propositional linear temporal logics in simple cases, Information and Computation, v.174 n.1, p.84-103, April 10, 2002
	Shmuel Katz , Hillel Miller, Saving Space by Fully Exploiting Invisible Transitions, Formal Methods in System Design, v.14 n.3, p.311-332, May 1999
	Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.124-133, March 1998
	James C. Corbett, Using shape analysis to reduce finite-state models of concurrent Java programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.51-93, Jan. 2000
	E M Clarke , O Grumberg , M C Browne, Reasoning about networks with many identical finite-state processes, Proceedings of the fifth annual ACM symposium on Principles of distributed computing, p.240-248, August 11-13, 1986, Calgary, Alberta, Canada
	Orna Kupferman , Moshe Y. Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.87-128, Jan. 2000
	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994
	S. Aggarwal , C. Courcoubetis , P. Wolper, Adding liveness properties to coupled finite-state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.303-339, April 1990
	Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.273-303, May 2001
	P. David Stotts , Richard Furuta , Cyrano Ruiz Cabarrus, Hyperdocuments as automata: verification of trace-based browsing properties by model checking, ACM Transactions on Information Systems (TOIS), v.16 n.1, p.1-30, Jan. 1998
	E. M. Clarke , O. Grumberg, Avoiding the state explosion problem in temporal logic model checking, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.294-303, August 10-12, 1987, Vancouver, British Columbia, Canada
	Frank Huch, Verification of Erlang programs using abstract interpretation and model checking, ACM SIGPLAN Notices, v.34 n.9, p.261-272, Sept. 1999
	Miguel J. Hornos , Manuel I. Capel, On-the-fly model checking from interval logic specifications, ACM SIGPLAN Notices, v.37 n.12, December 2002
	E. M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997
	F. Kabanza , J.-M. Stevenne , P. Wolper, Handling infinite temporal data, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.392-403, April 02-04, 1990, Nashville, Tennessee, United States
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997
	Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994
	Michael Dekhtyar , Alexander Dikovsky , Mars Valiev, On feasible cases of checking multi-agent systems behavior, Theoretical Computer Science, v.303 n.1, p.63-81, 28 June 2003
	Michael R. Fellows, Parameterized complexity: the main ideas and connections to practical computing, Experimental algorithmics: from algorithm design to robust and efficient software, Springer-Verlag New York, Inc., New York, NY, 2002
	Beata Konikowska , Wojciech Penczek, Model checking for multi-valued computation tree logics, Beyond two: theory and applications of multiple-valued logic, Physica-Verlag GmbH, Heidelberg, Germany, 2003
	Rajeev Alur , Salvatore La Torre, Deterministic generators and games for Ltl fragments, ACM Transactions on Computational Logic (TOCL), v.5 n.1, p.1-25, January 2004
	Jianer Chen , Iyad A. Kanj, Constrained minimum vertex cover in bipartite graphs: complexity and parameterized algorithms, Journal of Computer and System Sciences, v.67 n.4, p.833-847, December 2003
	C Courcoubetis , M Y Vardi , P Wolper, Reasoning about fair concurrent programs, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.283-294, May 28-30, 1986, Berkeley, California, United States
	Rajeev Alur , Thomas A. Henzinger, A really temporal logic, Journal of the ACM (JACM), v.41 n.1, p.181-203, Jan. 1994
	Allen Emerson , Jai Srinivasan, A decidable temporal logic to reason about many processes, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.233-246, August 22-24, 1990, Quebec City, Quebec, Canada
	Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002
	Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996
	David Harel , Orna Kupferman , Moshe Y. Vardi, On the complexity of verifying concurrent transition systems, Information and Computation, v.173 n.2, p.143-161, March 15, 2002
	Martin Grohe, Parameterized complexity for the database theorist, ACM SIGMOD Record, v.31 n.4, December 2002
	Orna Kupferman , Moshe Y. Vardi, From linear time to branching time, ACM Transactions on Computational Logic (TOCL), v.6 n.2, p.273-294, April 2005
	Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
	Saddek Bensalem , Yassine Lakhnech, Automatic Generation of Invariants, Formal Methods in System Design, v.15 n.1, p.75-92, July 1999
	Sérgio Campos , Edmund M. Clarke , Orna Grumberg, Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System, Formal Methods in System Design, v.17 n.2, p.163-192, Oct. 2000
	Christel Baier , Marta Kwiatkowska, Model checking for a probabilistic branching time logic with fairness, Distributed Computing, v.11 n.3, p.125-155, August 1998
	S. Chouali , J. Julliand , P.-A. Masson , F. Bellegarde, PLTL-partitioned model checking for reactive systems under fairness assumptions, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.267-301, May 2005
	Ji Zhang , Betty H. C. Cheng, Specifying adaptation semantics, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	R. H. Hardin , R. P. Kurshan , S. K. Shukla , M. Y. Vardi, A New Heuristic for Bad Cycle Detection Using BDDs, Formal Methods in System Design, v.18 n.2, p.131-140, March 1, 2001
	Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, v.10 n.1, p.47-71, February 1997
	Pierre Wolper, Expressing interesting properties of programs in propositional temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.184-193, January 01, 1986, St. Petersburg Beach, Florida
	Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
	Orna Grumberg , Tamir Heyman , Assaf Schuster, Distributed Symbolic Model Checking for μ-Calculus, Formal Methods in System Design, v.26 n.2, p.197-219, March 2005
	Stavros Tripakis , Sergio Yovine , Ahmed Bouajjani, Checking Timed Büchi Automata Emptiness Efficiently, Formal Methods in System Design, v.26 n.3, p.267-292, May 2005
	Chao Wang , Roderick Bloem , Gary D. Hachtel , Kavita Ravi , Fabio Somenzi, Compositional SCC Analysis for Language Emptiness, Formal Methods in System Design, v.28 n.1, p.5-36, January 2006
	Yonit Kesten , Amir Pnueli , Li-On Raviv , Elad Shahar, Model Checking with Strong Fairness, Formal Methods in System Design, v.28 n.1, p.57-84, January 2006
	Bernard Boigelot , Patrice Godefroid, Symbolic Verification of Communication Protocols with Infinite StateSpaces using QDDs, Formal Methods in System Design, v.14 n.3, p.237-255, May 1999
	S. Demri , F. Laroussinie , Ph. Schnoebelen, A parametric analysis of the state-explosion problem in model checking, Journal of Computer and System Sciences, v.72 n.4, p.547-575, June 2006
	Mark Lawford , Vera Pantelic , Hong Zhang, Towards integrated verification of timed transition models, Fundamenta Informaticae, v.70 n.1, p.75-110, March 2006
	E. A. Emerson , A. P. Sistla, Utilizing symmetry when model-checking under fairness assumptions: an automata-theoretic approach, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.4, p.617-638, July 1997
	Sezer Gören , F. Joel Ferguson, Test sequence generation for controller verification and test with high coverage, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.11 n.4, p.916-938, October 2006
	Yonit Kesten , Amir Pnueli, A compositional approach to CTL^* verification, Theoretical Computer Science, v.331 n.2-3, p.397-428, 25 February 2005
	Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage metrics for temporal logic model checking, Formal Methods in System Design, v.28 n.3, p.189-212, May 2006
	Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
	Hana Chockler , Eitan Farchi , Ziv Glazberg , Benny Godlin , Yarden Nir-Buchbinder , Ishai Rabinovitz, Formal verification of concurrent software: two case studies, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA
	Ji Zhang , Betty H. C. Cheng, Model-based development of dynamically adaptive software, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Krishnendu Chatterjee , Thomas A. Henzinger , Marcin Jurdziński, Games with secure equilibria, Theoretical Computer Science, v.365 n.1, p.67-82, 10 November 2006
	Tobias Schuele , Klaus Schneider, Bounded model checking of infinite state systems, Formal Methods in System Design, v.30 n.1, p.51-81, February 2007
	Jianer Chen , Yang Liu , Songjian Lu , Barry O'Sullivan , Igor Razgon, A fixed-parameter algorithm for the directed feedback vertex set problem, Proceedings of the 40th annual ACM symposium on Theory of computing, May 17-20, 2008, Victoria, British Columbia, Canada
	Walter Dosch , Pornsiri Muenchaisri , Wuttipong Ruanthong , Annette Stümpel, Model checking for input/output properties of a black-box model, Proceedings of the third conference on IASTED International Conference: Advances in Computer Science and Technology, p.120-127, April 02-04, 2007, Phuket, Thailand
	Tomohiro Yoneda , Bernd--Holger Schlingloff, Efficient Verification of Parallel Real–Time Systems, Formal Methods in System Design, v.11 n.2, p.187-215, Aug. 1997
	J. Frossl , T. Kropf, Verifying real-time properties of MOS-transistor circuits, Proceedings of the 1995 European conference on Design and Test, p.314, March 06-09, 1995
	Rajeev Alur , Ken McMillan , Doron Peled, Deciding Global Partial-Order Properties, Formal Methods in System Design, v.26 n.1, p.7-25, January 2005
	Abhik Roychoudhury , I. V. Ramakrishnan, Inductively Verifying Invariant Properties of Parameterized Systems, Automated Software Engineering, v.11 n.2, p.101-139, April 2004
	Z. Manna , A. Pnueli, Specification and verification of concurrent programs by A∀automata, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-2, January 21-23, 1987, Munich, West Germany
	Sharon Shoham , Orna Grumberg, A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.1-es, December 2007
	Tristan M. Behrens , Jürgen Dix, Model checking multi-agent systems with logic based Petri nets, Annals of Mathematics and Artificial Intelligence, v.51 n.2-4, p.81-121, December 2007
	Jianer Chen , Yang Liu , Songjian Lu , Barry O'sullivan , Igor Razgon, A fixed-parameter algorithm for the directed feedback vertex set problem, Journal of the ACM (JACM), v.55 n.5, p.1-19, October 2008
	Hana Chockler , Ofer Strichman, Before and after vacuity, Formal Methods in System Design, v.34 n.1, p.37-58, February 2009
	Ji Zhang , Heather J. Goldsby , Betty H.C. Cheng, Modular verification of dynamically adaptive systems, Proceedings of the 8th ACM international conference on Aspect-oriented software development, March 02-06, 2009, Charlottesville, Virginia, USA
	Robert M. Hierons , Kirill Bogdanov , Jonathan P. Bowen , Rance Cleaveland , John Derrick , Jeremy Dick , Marian Gheorghe , Mark Harman , Kalpesh Kapoor , Paul Krause , Gerald Lüttgen , Anthony J. H. Simons , Sergiy Vilkomir , Martin R. Woodward , Hussein Zedan, Using formal specifications to support testing, ACM Computing Surveys (CSUR), v.41 n.2, p.1-76, February 2009
	Hana Chockler , Arie Gurfinkel , Ofer Strichman, Beyond vacuity: towards the strongest passing formula, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
	Kaile Su, Model checking temporal logics of knowledge in distributed systems, Proceedings of the 19th national conference on Artifical intelligence, p.98-103, July 25-29, 2004, San Jose, California
	J. Julliand , P. -A. Masson , E. Oudot, Partitioned PLTL model-checking for refined transition systems, Information and Computation, v.207 n.6, p.681-698, June, 2009
	Anand S. Rao , Michael P. Georgeff, A model-theoretic approach to the verification of situated reasoning systems, Proceedings of the 13th international joint conference on Artifical intelligence, p.318-324, August 28-September 03, 1993, Chambery, France
	Moshe Y. Vardi, Automated verification: graphs, logic, and automata, Proceedings of the 18th international joint conference on Artificial intelligence, p.1603-1606, August 09-15, 2003, Acapulco, Mexico