Modalities for model checking (extended abstract)

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Modalities for model checking (extended abstract): branching time strikes back

Full text

Pdf (1.19 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: 84 - 96

Year of Publication: 1985

ISBN:0-89791-147-4

Authors

E. Allen Emerson	Department of Computer Sciences, University of Texas at Austin, Austin, Texas
Chin-Laung Lei	Department of Computer Sciences, University of Texas at Austin, Austin, Texas

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): 8, Downloads (12 Months): 39, Citation Count: 35

Additional Information:

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.318620 What is a DOI?

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	[AE83] Antila, M., Erikkson, H., Ikonen, J., Kujansuu, R., Ojala, L., Tuominen, H., Tools and Studies of Formal Techniques - Petri Nets and Temporal Logic, Protocol Specification, Testing, and Verification III, H. Rudin and C. West (editors), Elsevier North-Holland, IFIP, 1983.
	2	Karl Raymond Abrahamson, Decidability and expressiveness of logics of processes, University of Washington, 1980
	3	K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
	4	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
	5	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]
	6	Edmund M. Clarke , Bud Mishra, Automatic Verification of Asynchronous Circuits, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.101-115, June 06-08, 1983
	7	E. Allen Emerson , Edmund M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.169-181, July 14-18, 1980
	8	[EC82] Emerson, E. A., and Clarke, E. M., Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Tech. Report TR-208, Univ. of Texas, 1982.
	9	E. Allen Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.169-180, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802190]
	10	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]
	11	E. Allen Emerson , A. Prasad Sistla, Deciding branching time logic, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.14-24, December 1984 [doi>10.1145/800057.808661]
	12	[FL79] Fischer, M. J., and Ladner, R. E, Propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194-211, 1979.
	13	Nissim Francez , Dexter Kozen, Generalized fair termination, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.46-53, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800515]
	14	David Harel, A general result on infinite trees and its applications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.418-427, December 1984 [doi>10.1145/800057.808708]
	15	Sergiu Hart , Micha Sharir(, Probabilistic temporal logics for finite and bounded models, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.1-13, December 1984 [doi>10.1145/800057.808660]
	16	[KO83] Kozen, D., Results on the Propositional Mu-calculus, Theoretical Computer Science, pp. 333-354, December 83.
	17	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]
	18	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
	19	[LP84] Lichtenstein, O. and Pnueli, A., Checking that Finite State Concurrent Programs Satisfy their Linear Specification, unpublished manuscript, July 84, (to appear this POPL85.)
	20	[McN66] McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, Vol. 9, 1966.
	21	[OJ84] Ojala, Leo, Personal Communication at ICALP84, July 1984.
	22	Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
	23	[PN77] Pnueli, A., The Temporal Logic of Programs, 19th annual Symp. on Foundations of Computer Science, 1977.
	24	Amir Pnueli, On the extremely fair treatment of probabilistic algorithms, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.278-290, December 1983 [doi>10.1145/800061.808757]
	25	[PR76] Pratt, V., Semantical Considerations on Floyd-Hoare Logic, 17th FOCS, pp. 109-121, 1976.
	26	[PR81] Pratt, V., A Decidable Mu-Calculus, 22nd FOCS, pp. 421-427, 1981.
	27	[QS83] Queille, J. P., and Sifakis, J., Fairness and Related Properties in Transition Systems, Acta Informatica, vol. 19, pp. 195-220, 1983.
	28	[RA69] Rabin, M., Decidability of Second order Theories and Automata on Infinite Trees, Trans. Amer. Math. Society, Vol. 141, pp. 1-35, 1969.
	29	[RA70] Rabin, M., Automata on Infinite Trees and the Synthesis Problem, Hebrew Univ., Tech. Report no. 37, 1970.
	30	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]
	31	[ST81] Streett, R., Propositional Dynamic Logic of Looping and Converse (PhD Thesis), MIT Lab for Computer Science, TR-263, 1981. (a short version appears in STOC81)
	32	Robert S. Streett , E. Allen Emerson, The Propositional Mu-Calculus is Elementary, Proceedings of the 11th Colloquium on Automata, Languages and Programming, p.465-472, July 16-20, 1984
	33	[VW84] Vardi, M. and Wolper, P., Automata Theoretic Techniques for Modal Logics of Programs, pp. 446-455, STOC84.

CITED BY 35

	E. A. Emerson , T. Sadler , J. Srinivasan, Efficient temporal reasoning (extended abstract), Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-178, January 11-13, 1989, Austin, Texas, 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
	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986
	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
	Alexander Rabinovich , Shahar Maoz, An infinite hierarchy of temporal logics over branching time, Information and Computation, v.171 n.2, p.306-332, December 15, 2001
	Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	A. Aziz , F. Balarin , S.-T. Cheng , R. Hojati , T. Kam , S. C. Krishnan , R. K. Ranjan , T. R. Shiple , V. Singhal , S. Tasiran , H.-Y. Wang , R. K. Brayton , A. L. Sangiovanni-Vincentelli, HSIS: a BDD-based environment for formal verification, Proceedings of the 31st annual conference on Design automation, p.454-459, June 06-10, 1994, San Diego, California, United States
	Paul C. Attie, Liveness-preserving simulation relations, Proceedings of the eighteenth annual ACM symposium on Principles of distributed computing, p.63-72, May 04-06, 1999, Atlanta, Georgia, United States
	E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986
	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
	Anish Arora , Paul C. Attie , E. Allen Emerson, Synthesis of fault-tolerant concurrent programs, Proceedings of the seventeenth annual ACM symposium on Principles of distributed computing, p.173-182, June 28-July 02, 1998, Puerto Vallarta, Mexico
	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
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 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
	Teodor Rus , Eric Van Wyk , Tom Halverson, Generating Model Checkers from Algebraic Specifications, Formal Methods in System Design, v.20 n.3, p.249-284, May 2002
	Shmuel Katz , Doron Peled, Interleaving set temporal logic, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.178-190, August 10-12, 1987, Vancouver, British Columbia, 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
	Paul C. Attie , Anish Arora , E. Allen Emerson, Synthesis of fault-tolerant concurrent programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.1, p.125-185, January 2004
	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
	K. W. Wong , E. A. Unger, Specification and verification of active message systems, Proceedings of the 1990 ACM SIGSMALL/PC symposium on Small systems, p.24-30, March 28-30, 1990, Crystal City, Virginia, United States
	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
	James Ezick, An optimizing compiler for batches of temporal logic formulas, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	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
	A. Prasad Sistla , Patrice Godefroid, Symmetry and reduced symmetry in model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.4, p.702-734, July 2004
	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
	Adnan Aziz , Thomas Shiple , Vigyan Singhal , Robert Brayton , Alberto Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking, Formal Methods in System Design, v.21 n.2, p.193-224, September 2002
	J. S. Ostroff, Deciding Properties of Timed Transition Models, IEEE Transactions on Parallel and Distributed Systems, v.1 n.2, p.170-183, April 1990
	Ansuman Banerjee , Pallab Dasgupta, The open family of temporal logics: Annotating temporal operators with input constraints, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.3, p.492-522, July 2005
	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
	Sascha Klüppelholz , Christel Baier, Symbolic Model Checking for Channel-based Component Connectors, Electronic Notes in Theoretical Computer Science (ENTCS), v.175 n.2, p.19-37, June, 2007
	Bożena Woźna, ACTLS properties and Bounded Model Checking, Fundamenta Informaticae, v.63 n.1, p.65-87, January 2004
	A. N. Chebotarev, The Automata-Theoretic Approach to Verification of Reactive Systems, Cybernetics and Systems Analysis, v.37 n.6, p.810-819, November-December 2001
	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
	Sascha Klüppelholz , Christel Baier, Symbolic model checking for channel-based component connectors, Science of Computer Programming, v.74 n.9, p.688-701, July, 2009