Skip to main content
SpringerLink
Log in

Alternating-time Temporal Logic

  • Conference paper
  • First Online:
Compositionality: The Significant Difference (COMPOS 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1536))

Included in the following conference series:

Abstract

Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas.

Depending on whether we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL. We interpret the formulas of ATL and ATL over alternating transition systems. While in ordinary transition systems, each transition corresponds to a possible step of the system, in alternating transition systems, each transition corresponds to a possible move in the game between the system and the environment. Fair alternating transition systems can capture both synchronous and asynchronous compositions of open systems. For synchronous systems, the expressive power of ATL beyond CTL comes at no cost: the model-checking complexity of synchronous ATL is linear in the size of the system and the length of the formula. The symbolic model-checking algorithm for CTL extends with few modifications to synchronous ATL, and with some work, also to asynchronous ATL, whose model-checking complexity is quadratic. This makes ATL an obvious candidate for the automatic verification of open systems. In the case of ATL, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time for both synchronous and asynchronous systems.

A preliminary version of this paper appeared in the Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (FOCS 1997), pp. 100–109.

This work was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 97-DC-324.041.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur and T.A. Henzinger. Reactive modules. In Proc. 11th IEEE Symposium on Logic in Computer Science, pages 207–218, 1996.

    Google Scholar 

  2. M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, 1993.

    Article  Google Scholar 

  3. M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Lnt. Colloquium on Automata, Languages, and Programming, volume 372 of Lecture Notes in Computer Science, Springer-Verlag, pages 1–17, 1989.

    Chapter  Google Scholar 

  4. [BBG+94]_I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Conference on Computer-aided Verification, volume 818 of Lecture Notes in Computer Science, Springer-Verlag, pages 182–193, 1994.

    Google Scholar 

  5. [BCM+90]_J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Symposium on Logic in Computer Science, pages 428–439, 1990.

    Google Scholar 

  6. O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Proc. 6th Conference on Computer-aided Verification, volume 818 of Lecture Notes in Computer Science, Springer-Verlag, pages 142–155, 1994.

    Google Scholar 

  7. E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, Springer-Verlag, pages 52–71, 1981.

    Chapter  Google Scholar 

  8. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.

    Article  MATH  Google Scholar 

  9. A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  10. R. Cleaveland. A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in System Design, 2:121–147, 1993.

    Article  MATH  Google Scholar 

  11. D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, 1989.

    Google Scholar 

  12. E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151–178, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  13. E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th LEEE Symposium on Foundations of Computer Science, pages 368–377, 1988.

    Google Scholar 

  14. E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 84–96, 1985.

    Google Scholar 

  15. E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proc. 1st Symposium on Logic in Computer Science, pages 267–278, 1986.

    Google Scholar 

  16. E.A. Emerson and A.P. Sistla. Deciding branching-time logic. In Proc. 16th ACM Symposium on Theory of Computing, 1984.

    Google Scholar 

  17. M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194–211, 1979.

    Article  MATH  MathSciNet  Google Scholar 

  18. R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. In Proc. 23rd Int. Colloquium on Automata, Languages, and Programming, volume 820 of Lecture Notes in Computer Science, Springer-Verlag, pages 166–177, 1994.

    Google Scholar 

  19. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    Google Scholar 

  20. G.J. Holzmann. The model checker SPIN. LEEE Transactions on Software Engineering, 23(5):279–295, 1997.

    Article  MathSciNet  Google Scholar 

  21. N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384–406, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  22. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  23. O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conferance on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, Springer-Verlag, pages 408–422, 1995.

    Google Scholar 

  24. O. Kupferman and M.Y. Vardi. Module checking. In Proc. 8th Conference on Computer-aided Verification, volume 1102 of Lecture Notes in Computer Science, Springer-Verlag, pages 75–86, 1996.

    Google Scholar 

  25. O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symposium on Principles of Programming Languages, pages 97–107, 1985.

    Google Scholar 

  26. N.A. Lynch. Distributed Algorithms. Morgan-Kaufmann, 1996.

    Google Scholar 

  27. K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  28. R. Parikh. Propositional game logic. In Proc. 24th LEEE Symposium on Foundation of Computer Science, pages 195–200, 1983.

    Google Scholar 

  29. A. Pnueli. The temporal logic of programs. In Proc. 18th LEEE Symposium on Foundation of Computer Science, pages 46–57, 1977.

    Google Scholar 

  30. G.L. Peterson and J.H. Reif. Multiple-person alternation. In Proc. 20th LEEE Symposium on Foundation of Computer Science, pages 348–363, 1979.

    Google Scholar 

  31. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symposium on Principles of Programming Languages, 1989.

    Google Scholar 

  32. A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In Proc. 16th Lnt. Colloquium on Automata, Languages, and Programming, volume 372 of Lecture Notes in Computer Science, Springer-Verlag, pages 652–671, 1989.

    Chapter  Google Scholar 

  33. A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proc. 31st LEEE Symposium on Foundation of Computer Science, pages 746–757, 1990.

    Google Scholar 

  34. J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symposium on Programming, volume 137 of Lecture Notes in Computer Science, Springer-Verlag, pages 337–351, 1981.

    Google Scholar 

  35. M.O. Rabin. Weakly definable relations and special automata. In Proc. Symposium on Mathematical Logic and Foundations of Set Theory, pages 1–23. North Holland, 1970.

    Google Scholar 

  36. J.H. Reif. The complexity of two-player games of incomplete information. Lournal on Computer and System Sciences, 29:274–301, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  37. R. Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1992.

    Google Scholar 

  38. P.J.G. Ramadge and W.M. Wonham. The control of descrete event systems. LEEE Transactions on Control Theory, 77:81–98, 1989.

    Google Scholar 

  39. W. Thomas. On the synthesis of strategies in infinite games. In Proc. 12th Symposium on Theoretical Aspects of Computer Science, volume 900 of Lecture Notes in Computer Science, Springer-Verlag, pages 1–13, 1995.

    Google Scholar 

  40. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st LEEE Symposium on Logic in Computer Science, pages 322–331, 1986.

    Google Scholar 

  41. M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182–221, 1986.

    Article  MathSciNet  Google Scholar 

  42. M. Yannakakis. Synchronous multi-player gaines with incomplete information are undecidable. Personal communication, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, 19104

    Rajeev Alur

  2. Bell Laboratories, Computing Science Research Center, Murray Hill, NJ, 07974

    Rajeev Alur

  3. Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA, 94720

    Thomas A. Henzinger & Orna Kupferman

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas A. Henzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Orna Kupferman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics and Applied Mathematics, Christian Albrechts University at Kiel, Preußerstr. 1-9, D-24105, Kiel, Germany

    Willem-Paul de Roever  & Hans Langmaack  & 

  2. Department of Applied Mathematics and Computer Science, Weizmann Institute of Science, P.O. Box 26, Rehovot, 76100, Israel

    Amir Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Henzinger, T.A., Kupferman, O. (1998). Alternating-time Temporal Logic. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-49213-5_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65493-3

  • Online ISBN: 978-3-540-49213-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation