“Sometimes” and “not never” revisited

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

“Sometimes” and “not never” revisited: on branching versus linear time temporal logic

Full text

Pdf (2.07 MB)

Source

Journal of the ACM (JACM) archive
Volume 33 , Issue 1 (January 1986) table of contents
The MIT Press scientific computation series

Pages: 151 - 178

Year of Publication: 1986

ISSN:0004-5411

Authors

E. Allen Emerson	Univ. of Texas, Austin
Joseph Y. Halpern	IBM Research Laboratory, San Jose, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 18, Downloads (12 Months): 156, Citation Count: 89

Additional Information:

abstract references cited by index terms review 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/4904.4999 What is a DOI?

ABSTRACT

The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.

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	Karl Raymond Abrahamson, Decidability and expressiveness of logics of processes, 1980
	2	Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
	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	EMERSON, E. A. Alternative semantics for temporal logics. Theor. Comput. Sci. 26 (1983), 121-130.
	6	E. Allen Emerson, Automata, Tableaux and Temporal Logics (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.79-88, June 17-19, 1985
	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	EMERSON, E. A., AND CLARKE, E.M. Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Prog. 2 (1982), 241-266.
	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. A Emerson , Joseph Y. Halpern, "Sometimes" and "Not Never" Revisited: on Branching Versus Linear Time, University of Texas at Austin, Austin, TX, 1984
	11	E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318620]
	12	EMERSON, E. A., AND SIS'rLA, A.P. Deciding full branching time logic. Inf. Control 61, 3 (1984), 175-201.
	13	FISCHER, M. J., AND LADNER, R.E. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18 (1979), 194-211.
	14	Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
	15	HAILPERN, B., AND OWICKI, S. Modular verification of concurrent programs using temporal logic. Tech. Rep., Stanford Univ. Stanford, Calif., 1981.
	16	HAREL, D., KOZEN, D., AND PARXK,, R. Process logic: Expressiveness, decidability, and completeness. J. Comput. Syst. Sci. 25 (1982), 144-170.
	17	HAREL, D., AND SHERMAN, R. Looping vs. repeating in dynamic logic. Inf. Control 55 (1982), 175-192.
	18	KAMP, H. Tense logic and the theory of linear order. Ph.D. dissertation, UCLA, Los Angeles, 1968.
	19	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]
	20	LEHMANN, D., AND SHELAH, S. Reasoning with time and chance. Inf. Control 53 (1982), 165-198.
	21	Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
	22	Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
	23	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]
	24	PNUELI, A. The temporal logic of programs. In Proceedings of the 19th Annual Symposium on Foundations of Computer Science. IEEE, New York, 1977, pp. 46-57.
	25	PNUELI, A. The temporal semantics of concurrent programs. Theor. Comput. Sci. 13 ( 198 l), 45- 60.
	26	V. R. Pratt, Process logic: preliminary report, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.93-100, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567761]
	27	PRIOR, A. Time and Modality. Oxford Univ. Press, London, 1957.
	28	PRIOR, A. Past, Present, and Future. Oxford Univ. Press, London, 1967.
	29	RESCHER, N., AND URQUHART, A. Temporal logic. Springer-Verlag, Berlin, 197 I.
	30	A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
	31	M Y Vardi , L Stockmeyer, Improved upper and lower bounds for modal logics of programs, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.240-251, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22173]
	32	Moshe Y. Vardi , Pierre Wolper, Yet Another Process Logic (Preliminary Version), Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.501-512, June 06-08, 1983
	33	Pierre Wolper, Specification and synthesis of communicating processes using an extended temporal logic: (preliminary version), Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.20-33, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582156]
	34	WOLPER, P. Temporal logic can be more expressive. Inf. Control 56, 1/2 (1983), 72-99.

CITED BY 89

	Irène Guessarian , Eugénie Foustoucos , Theodore Andronikos , Foto Afrati, On temporal logic versus datalog, Theoretical Computer Science, v.303 n.1, p.103-133, 28 June 2003
	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
	Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995
	Rance Cleaveland , Scott A. Smolka, Strategic directions in concurrency research, ACM Computing Surveys (CSUR), v.28 n.4, p.607-625, Dec. 1996
	C. S. Jutla , E. Knapp , J. R. Rao, A predicate transformer approach to semantics of parallel programs, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.249-263, June 1989, Edmonton, Alberta, Canada
	Rob J. van Glabbeek , W. Peter Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM (JACM), v.43 n.3, p.555-600, May 1996
	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
	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
	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
	Joanne Atlee , John Gannon, State-based model checking of event-driven system requirements, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.16-28, Dec. 1991
	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
	P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000
	Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists, Formal Methods in System Design, v.23 n.1, p.39-65, July 2003
	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
	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
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	M. P. Singh , M. N. Huhns , L. M. Stephens, Declarative Representations of Multiagent Systems, IEEE Transactions on Knowledge and Data Engineering, v.5 n.5, p.721-739, October 1993
	Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design, v.18 n.2, p.141-163, March 1, 2001
	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
	Thomas T. Hildebrandt, Towards categorical models for fairness: fully abstract presheaf semantics of SCCS with finite delay, Theoretical Computer Science, v.294 n.1-2, p.151-181, 15 February 2003
	Mario Verdicchio , Marco Colombetti, A logical model of social commitment for agent communication, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
	Panagiotis Manolios , Richard Trefler, A lattice-theoretic characterization of safety and liveness, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.325-333, July 13-16, 2003, Boston, Massachusetts
	Mathias Broxvall , Peter Jonsson, Point algebras for temporal reasoning: algorithms and complexity, Artificial Intelligence, v.149 n.2, p.179-220, October 2003
	James Ezick, An optimizing compiler for batches of temporal logic formulas, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Gérard Cécé , Alain Finkel , S. Purushothaman Iyer, Duplication, insertion and lossiness errors in unreliable communication channels, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.35-43, Dec. 1994
	J Y Halpern , M Y Vardi, The complexity of reasoning about knowledge and time, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.304-315, May 28-30, 1986, Berkeley, California, United States
	Tevfik Bultan , Jeffrey Fischer , Richard Gerber, Compositional verification by model checking for counter-examples, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.224-238, May 1996
	Gian-Luigi Ferrari , Stefania Gnesi , Ugo Montanari , Marco Pistore, A model-checking verification environment for mobile processes, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.4, p.440-473, October 2003
	Patrick Cousot , Radhia Cousot, Temporal abstract interpretation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-25, January 19-21, 2000, Boston, MA, USA
	Faron Moller , Alexander Rabinovich, Counting on CTL: on the expressive power of monadic path logic, Information and Computation, v.184 n.1, p.147-159, July 10, 2003
	Brandon Bennett , Antony P. Galton, A unifying semantics for time and events, Artificial Intelligence, v.153 n.1-2, p.13-48, March 2004
	Amy P. Felty , Kedar S. Namjoshi, Feature specification and automated conflict detection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.1, p.3-27, January 2003
	Joseph Y. Halpern, A note on knowledge-based programs and specifications, Distributed Computing, v.13 n.3, p.145-153, July 2000
	Riccardo Mattolini , Paolo Nesi, An Interval Logic for Real-Time System Specification, IEEE Transactions on Software Engineering, v.27 n.3, p.208-227, March 2001
	Michael Wooldridge , Michael Fisher , Marc-Philippe Huget , Simon Parsons, Model checking multi-agent systems with MABLE, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy
	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
	Robert Goldblatt, Mathematical modal logic: a view of its evolution, Journal of Applied Logic, v.1 n.5-6, p.309-392, October 2003
	Riccardo Pucella, The finite and the infinite in temporal logic, ACM SIGACT News, v.36 n.1, March 2005
	Yoram Hirshfeld , Alexander Rabinovich, Future temporal logic needs infinitely many modalities, Information and Computation, v.187 n.2, p.196-208, 15 December 2003
	Shmuel Katz , Doron Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing, v.6 n.2, p.107-120, September 1992
	Susanne Graf, Characterization of a sequentially consistent memory and verification of a cache memory by abstraction, Distributed Computing, v.12 n.2/3, p.75-90, June 1999
	Christie Bolton , Gavin Lowe, A hierarchy of failures-based models: theory and application, Theoretical Computer Science, v.330 n.3, p.407-438, 9 February 2005
	Hidetomo Machi , Kohji Tomita , Chiharu Hosono, The relative completeness of a version of CTL, Proceedings of the 2005 Australasian symposium on Theory of computing, p.81-85, January 01, 2005, Newcastle, Australia
	Frank Wolter , Michael Zakharyaschev, Qualitative spatiotemporal representation and reasoning: a computational perspective, Exploring artificial intelligence in the new millennium, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
	Mark Reynolds, An axiomatization of PCTL, Information and Computation, v.201 n.1, p.72-119, 25 August 2005
	Dongfeng Wang , Farokh B. Bastani , I. -Ling Yen, Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance, IEEE Transactions on Software Engineering, v.31 n.9, p.713-732, September 2005
	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
	Sophie Pinchinat , Stéphane Riedweg, A decidable class of problems for control under partial observation, Information Processing Letters, v.95 n.4, p.454-460, 31 August 2005
	Foto Afrati , Theodore Andronikos , Vassia Pavlaki , Eugenie Foustoucos , Irène Guessarian, From CTL to datalog, Proceedings of the Paris C. Kanellakis memorial workshop on Principles of computing & knowledge: Paris C. Kanellakis memorial workshop on the occasion of his 50th birthday, p.72-85, June 08-08, 2003, San Diego, California, USA
	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
	Flavio Corradini , Paola Inverardi , Alexander L. Wolf, On relating functional specifications to architectural specifications: a case study, Science of Computer Programming, v.59 n.3, p.171-208, February 2006
	Thomas A. Henzinger , Orna Kupferman , Rupak Majumdar, On the universal and existential fragments of the μ-calculus, Theoretical Computer Science, v.354 n.2, p.173-186, 28 March 2006
	Roberto Giacobazzi , Francesco Ranzato, Imcompleteness of States w.r.t traces in model Checking, Information and Computation, v.204 n.3, p.376-407, March 2006
	Klaus Schild, On the Relationship Between BDI Logics and Standard Logics of Concurrency, Autonomous Agents and Multi-Agent Systems, v.3 n.3, p.259-283, September 2000
	Rance Cleaveland , S. Purushothaman Iyer , Murali Narasimha, Probabilistic temporal logics via the modal mu-calculus, Theoretical Computer Science, v.342 n.2-3, p.316-350, 7 September 2005
	Alexander Rabinovich , Philippe Schnoebelen, BTL2 and the expressive power of ECTL⁺, Information and Computation, v.204 n.7, p.1023-1044, July 2006
	A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States
	Yonit Kesten , Amir Pnueli, A compositional approach to CTL^* verification, Theoretical Computer Science, v.331 n.2-3, p.397-428, 25 February 2005
	Mikolaj Bojańczyk , Igor Walukiewicz, Characterizing EF and EX tree logics, Theoretical Computer Science, v.358 n.2, p.255-272, 7 August 2006
	Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
	Salvatore La Torre , Aniello Murano , Margherita Napoli, Weak Muller acceptance conditions for tree automata, Theoretical Computer Science, v.332 n.1-3, p.233-250, 28 February 2005
	Muffy Calder , Alice Miller, Feature interaction detection by pairwise analysis of LTL properties: a case study, Formal Methods in System Design, v.28 n.3, p.213-261, May 2006
	Franz Baader , Silvio Ghilardi , Cesare Tinelli, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Information and Computation, v.204 n.10, p.1413-1452, October 2006
	Mauricio Varea , Bashir M. Al-Hashimi , Luis A. CortéS , Petru Eles , Zebo Peng, Dual Flow Nets: Modeling the control/data-flow relation in embedded systems, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.1, p.54-81, February 2006
	Stéphane Demri , Ranko Lazić , David Nowak, On the freeze quantifier in Constraint LTL: Decidability and complexity, Information and Computation, v.205 n.1, p.2-24, January, 2007
	Mehdi Dastani , M. Birna van Riemsdijk , John-Jules Ch. Meyer, A grounded specification language for agent programs, Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, May 14-18, 2007, Honolulu, Hawaii
	Laura Bozzelli, Complexity results on branching-time pushdown model checking, Theoretical Computer Science, v.379 n.1-2, p.286-297, June, 2007
	Marek A. Bednarczyk , Wojciech Jamroga , Wiesław Pawłowski, Expressing and Verifying Temporal and Structural Properties of Mobile Agents, Fundamenta Informaticae, v.72 n.1-3, p.51-63, January 2006
	Alexander Bolotov , Artie Basukoski, A clausal resolution method for branching-time logic ECTL+, Annals of Mathematics and Artificial Intelligence, v.46 n.3, p.235-263, March 2006
	Glenn Shafer , Peter R. Gillett , Richard Scherl, The logic of events, Annals of Mathematics and Artificial Intelligence, v.28 n.1-4, p.315-389, 2000
	Wojciech Jamroga , Wiebe van der Hoek, Agents that Know How to Play, Fundamenta Informaticae, v.63 n.2-3, p.185-219, April 2004
	Cinzia Bernardeschi , Alessandro Fantechi , Stefania Gnesi , Salvatore Larosa , Giorgio Mongardi , Dario Romano, A Formal Verification Environment for Railway Signaling System Design, Formal Methods in System Design, v.12 n.2, p.139-161, March 1, 1998
	Francesco Viganò , Marco Colombetti, Symbolic model checking of institutions, Proceedings of the ninth international conference on Electronic commerce, August 19-22, 2007, Minneapolis, MN, USA
	Brandon Bennett , Anthony G. Cohn , Frank Wolter , Michael Zakharyaschev, Multi-Dimensional Modal Logic as a Framework for Spatio-Temporal Reasoning, Applied Intelligence, v.17 n.3, p.239-251, November-December 2002
	Joeri Engelfriet , Jan Treur, Linear, Branching Time and Joint ClosureSemantics for Temporal Logic, Journal of Logic, Language and Information, v.11 n.4, p.389-425, Fall 2002
	Mark D'Inverno , Michael Luck , Michael Georgeff , David Kinny , Michael Wooldridge, The dMARS Architecture: A Specification of the Distributed Multi-Agent Reasoning System, Autonomous Agents and Multi-Agent Systems, v.9 n.1-2, p.5-53, July-September 2004
	Toufik Taibi, Formal specification and validation of multi-agent behaviour using TLA+ and TLC model checker, International Journal of Artificial Intelligence and Soft Computing, v.1 n.1, p.99-113, November 2008
	Thomas Ågotnes , Wiebe van der Hoek , Michael Wooldridge, Normative system games, Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, May 14-18, 2007, Honolulu, Hawaii
	Nils Bulling , Wojciech Jamroga, Agents, beliefs, and plausible behavior in a temporal setting, Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, May 14-18, 2007, Honolulu, Hawaii
	Susanne Graf , Andreas Prinz, Time in State Machines, Fundamenta Informaticae, v.77 n.1-2, p.143-174, January 2007
	Zoltán Ésik , Szabolcs Iván, Some Varieties of Finite Tree Automata Related to Restricted Temporal Logics, Fundamenta Informaticae, v.82 n.1-2, p.79-103, January 2008
	Alexander Rabinovich, Arity hierarchy for temporal logics, Theoretical Computer Science, v.403 n.2-3, p.373-381, August, 2008
	Jin-Cheon Na , Richard Furuta, Open paper: caT: adapting and updating the trellis hypertext model, The New Review of Hypermedia and Multimedia, v.12 n.2, p.217-246, December 2006
	Harry Foster, Applied Assertion-Based Verification: An Industry Perspective, Foundations and Trends in Electronic Design Automation, v.3 n.1, p.1-95, January 2009
	Volker Weber, Branching-Time Logics Repeatedly Referring to States, Journal of Logic, Language and Information, v.18 n.4, p.593-624, October 2009

INDEX TERMS

Primary Classification:
D. Software
D.2 SOFTWARE ENGINEERING

Additional Classification:
F. Theory of Computation
F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
F.4.1 Mathematical Logic
Subjects: Temporal logic

General Terms:
Design, Languages, Performance, Theory, Verification

REVIEW

"Ali Mili : Reviewer"

This paper extends earlier work by Lamport [1] on comparing two logics of concurrent programming: Branching Temporal Logic and Linear Time Temporal Logic. In order to carry out the comparisons, the paper introduces a special-purpose temporal not more...

Collaborative Colleagues:

E. Allen Emerson: colleagues

Joseph Y. Halpern: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player