Alternating-time Temporal Logic | Springer Nature Link

Alternating-time Temporal Logic | Springer Nature Link
Advertisement
Alternating-time Temporal Logic
Conference paper
First Online:
01 January 1999
pp 23–60
Cite this conference paper
Compositionality: The Significant Difference
(COMPOS 1997)
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
Institutional subscriptions
Preview
Unable to display preview.
Download preview
PDF.
Unable to display preview.
Download preview
PDF.
Similar content being viewed by others
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Chapter
Coalition Alternating-Time Temporal Logic: A Logic to Find Good Coalitions to Achieve Strategic Objectives
Chapter
Temporal Logic and Fair Discrete Systems
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Algebraic Logic
Logic in AI
Formal Languages and Automata Theory
General Logic
Linear Logic
Substructural Logics
Temporal Logic in Multi-Agent Systems
References
R. Alur and T.A. Henzinger. Reactive modules. In
Proc. 11th IEEE Symposium on Logic in Computer Science
, pages 207–218, 1996.
Google Scholar
M. Abadi and L. Lamport. Composing specifications.
ACM Transactions on Programming Languages and Systems
, 15(1):73–132, 1993.
Article
Google Scholar
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
[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
[BCM
90]_J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 10
20
states and beyond. In
Proc. 5th Symposium on Logic in Computer Science
, pages 428–439, 1990.
Google Scholar
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
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
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
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
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
D.L. Dill.
Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits
. MIT Press, 1989.
Google Scholar
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
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
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
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
E.A. Emerson and A.P. Sistla. Deciding branching-time logic. In
Proc. 16th ACM Symposium on Theory of Computing
, 1984.
Google Scholar
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
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
C.A.R. Hoare.
Communicating Sequential Processes
. Prentice-Hall, 1985.
Google Scholar
G.J. Holzmann. The model checker SPIN.
LEEE Transactions on Software Engineering
, 23(5):279–295, 1997.
Article
MathSciNet
Google Scholar
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
D. Kozen. Results on the propositional μ-calculus.
Theoretical Computer Science
, 27:333–354, 1983.
Article
MATH
MathSciNet
Google Scholar
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
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
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
N.A. Lynch.
Distributed Algorithms
. Morgan-Kaufmann, 1996.
Google Scholar
K.L. McMillan.
Symbolic Model Checking
. Kluwer Academic Publishers, 1993.
Google Scholar
R. Parikh. Propositional game logic. In
Proc. 24th LEEE Symposium on Foundation of Computer Science
, pages 195–200, 1983.
Google Scholar
A. Pnueli. The temporal logic of programs. In
Proc. 18th LEEE Symposium on Foundation of Computer Science
, pages 46–57, 1977.
Google Scholar
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
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
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
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
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
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
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
R. Rosner.
Modular Synthesis of Reactive Systems
. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1992.
Google Scholar
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
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
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
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
M. Yannakakis. Synchronous multi-player gaines with incomplete information are undecidable. Personal communication, 1997.
Google Scholar
Download references
Author information
Authors and Affiliations
Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, 19104
Rajeev Alur
Bell Laboratories, Computing Science Research Center, Murray Hill, NJ, 07974
Rajeev Alur
Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA, 94720
Thomas A. Henzinger & Orna Kupferman
Authors
Rajeev Alur
View author publications
Search author on:
PubMed
Google Scholar
Thomas A. Henzinger
View author publications
Search author on:
PubMed
Google Scholar
Orna Kupferman
View author publications
Search author on:
PubMed
Google Scholar
Editor information
Editors and Affiliations
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  &
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
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
.RIS
.ENW
.BIB
DOI
Published
21 May 1999
Publisher Name
Springer, Berlin, Heidelberg
Print ISBN
978-3-540-65493-3
Online ISBN
978-3-540-49213-9
eBook Packages
Springer Book Archive
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Model Check
Temporal Logic
Tree Automaton
Fairness Constraint
Path Formula
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Publish with us
Policies and ethics
Access this chapter
Log in via an institution
Institutional subscriptions