Alternating-time temporal logic

ABSTRACT

Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; 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. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. 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.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.507-535, May 1995 [doi>10.1145/203095.201069]
• 2: Martín Abadi , Leslie Lamport , Pierre Wolper, Realizable and Unrealizable Specifications of Reactive Systems, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.1-17, July 11-15, 1989
• 3: R. Alur , L. de Alfaro , R. Grosu , T. A. Henzinger , M. Kang , C. M. Kirsch , R. Majumdar , F. Mang , B. Y. Wang, JMOCHA: a model checking tool that exploits design structure, Proceedings of the 23rd International Conference on Software Engineering, p.835-836, May 12-19, 2001, Toronto, Ontario, Canada
• 4: Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999 [doi>10.1023/A:1008739929481]
• 5: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 6: Alur, R., La Torre, S., and Madhusudan, P. 2002. Playing games with boxes and diamonds. Tech. Rep., Univ. Pennsylvania.
• 7: Catriel Beeri, On the menbership problem for functional and multivalued dependencies in relational databases, ACM Transactions on Database Systems (TODS), v.5 n.3, p.241-259, Sept. 1980 [doi>10.1145/320613.320614]
• 8: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 9: Büchi, J. R. and Landweber, L. H. 1969. Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295--311.
• 10: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 11: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 12: 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
• 13: 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 [doi>10.1145/5397.5399]
• 14: Rance Cleaveland , Bernhard Steffen, A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.48-58, July 01-04, 1991
• 15: Mads Dam, CTL and ECTL as fragments of the modal &mgr;-calculus, Theoretical Computer Science, v.126 n.1, p.77-96, April 11, 1994 [doi>10.1016/0304-3975(94)90269-0]
• 16: de Alfaro, L., Henzinger, T. A., and Majumdar, R. 2001a. From verification to control: Dynamic programs for omega-regular objectives. In Proc. 16th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 279--299.
• 17: Luca de Alfaro , Thomas A. Henzinger , Freddy Y. C. Mang, The Control of Synchronous Systems, Proceedings of the 11th International Conference on Concurrency Theory, p.458-473, August 22-25, 2000
• 18: Luca de Alfaro , Thomas A. Henzinger , Freddy Y. C. Mang, The Control of Synchronous Systems, Part II, Proceedings of the 12th International Conference on Concurrency Theory, p.566-582, August 20-25, 2001
• 19: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
• 20: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 21: 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 [doi>10.1145/4904.4999]
• 22: Emerson, E. A., and Jutla, C. 1988. The complexity of tree automata and logics of programs. In Proc. 29th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 328--337.
• 23: 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]
• 24: Emerson, E. A., and Lei, C.-L. 1986. Efficient model checking in fragments of the propositional μ-calculus. In Proc. 1st Symp. on Logic in Computer Science. IEEE Computer Society Press, 267--278.
• 25: 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]
• 26: Kousha Etessami , Thomas Wilke , Rebecca A. Schuller, Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.694-707, July 08-12, 2001
• 27: Fischer, M. J., and Ladner, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194--211.
• 28: Rainer Gawlick , Roberto Segala , Jørgen F. Søgaard-Andersen , Nancy A. Lynch, Liveness in Timed and Untimed Systems, Proceedings of the 21st International Colloquium on Automata, Languages and Programming, p.166-177, July 11-14, 1994
• 29: Yuri Gurevich , Leo Harrington, Trees, automata, and games, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.60-65, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802177]
• 30: Halpern, J. Y. and Fagin, R. 1989. Modeling knowledge and action in distributed systems. Distrib. Comput. 3, 4, 159--179.
• 31: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 32: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 33: Immerman, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 3, 384--406.
• 34: Marcin Jurdzinski, Small Progress Measures for Solving Parity Games, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, p.290-301, February 01, 2000
• 35: Kozen, D. 1983. Results on the propositional μ-calculus. Theoret. Comput. Sci. 27, 333--354.
• 36: Orna Kupferman , Moshe Y. Vardi, On the Complexity of Branching Modular Model Checking (Extended Abstract), Proceedings of the 6th International Conference on Concurrency Theory, p.408-422, August 21-24, 1995
• 37: Kupferman, O. and Vardi, M. Y. 1998. Verification of fair transition systems. Chicago J. Theoret. Comput. Sci. 1998, 2.
• 38: 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 [doi>10.1145/333979.333987]
• 39: Module checking, Information and Computation, v.164 n.2, p.322-344, Jan. 29, 2001 [doi>10.1006/inco.2000.2893]
• 40: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 41: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 42: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 43: Parikh, R. 1983. Propositional game logic. In Proc. 24th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 195--200.
• 44: Peterson, G. L., and Reif, J. H. 1979. Multiple-person alternation. In Proc. 20st Symp. on Foundations of Computer Science. IEEE Computer Society Press, 348--363.
• 45: Pnueli, A. 1977. The temporal logic of programs. In Proc. 18th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 46--57.
• 46: 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 [doi>10.1145/75277.75293]
• 47: Amir Pnueli , Roni Rosner, On the Synthesis of an Asynchronous Reactive Module, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.652-671, July 11-15, 1989
• 48: Pnueli, A., and Rosner, R. 1990. Distributed reactive systems are hard to synthesize. In Proc. 31st Symp. on Foundations of Computer Science. IEEE Computer Society Press, 746--757.
• 49: 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
• 50: Michael Oser Rabin, Automata on Infinite Objects and Church's Problem, American Mathematical Society, Boston, MA, 1972
• 51: Ramadge, P., and Wonham, W. 1989. The control of discrete event systems. IEEE Transactions on Control Theory 77, 81--98.
• 52: Reif, J. H. 1984. The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29, 274--301.
• 53: Rosner, R. 1992. Modular synthesis of reactive systems. Ph.D. dissertation, Weizmann Institute of Science, Rehovot, Israel.
• 54: Shapley, L. S. 1953. Stochastic games. In Proc. Nat. Acad. Sci., 39, 1095--1100.
• 55: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 56: Thomas, W. 1995. On the synthesis of strategies in infinite games. In Proc. 12th Symp. on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 900. Springer-Verlag, 1--13.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Theory, Verification

Keywords:
Alternation, games, model checking, temporaxl logic