Alternating-time temporal logic

Journal of the ACM - Tập 49 Số 5 - Trang 672-713 - 2002
Rajeev Alur1, Thomas A. Henzinger2, Orna Kupferman3
1University of Pennsylvania, Philadelphia, Pennsylvania
2University of California, Berkeley, California
3Hebrew University, Jerusalem, Israel

Tóm tắt

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.

Từ khóa


Tài liệu tham khảo

10.1145/203095.201069

Abadi , M. , Lamport , L. , and Wolper , P . 1989. Realizable and unrealizable concurrent program specifications . In Proc. 16th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science , vol. 372 . Springer-Verlag, 1--17.]] Abadi, M., Lamport, L., and Wolper, P. 1989. Realizable and unrealizable concurrent program specifications. In Proc. 16th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 372. Springer-Verlag, 1--17.]]

Alur , R. , de Alfaro , L. , Grosu , R. , Henzinger , T. A. , Kang , M. , Kirsch , C. M. , Majumdar , R. , Mang , F. Y. C. , and Wang , B. Y . 2001. jMocha: A model-checking tool that exploits design structure . In Proc. 23rd International Conference on Software Engineering. IEEE Computer Society Press, 835--836 .]] Alur, R., de Alfaro, L., Grosu, R., Henzinger, T. A., Kang, M., Kirsch, C. M., Majumdar, R., Mang, F. Y. C., and Wang, B. Y. 2001. jMocha: A model-checking tool that exploits design structure. In Proc. 23rd International Conference on Software Engineering. IEEE Computer Society Press, 835--836.]]

10.1023/A:1008739929481

Alur , R. , Henzinger , T. A. , Mang , F. Y. C. , Qadeer , S. K. , Rajamani , S. K. , and Tasiran , S . 1998 . Mocha: Modularity in model checking. In Proc. 10th International Conference, Computer Aided Verification . Lecture Notes in Computer Science , vol. 1427 . Springer-Verlag , 521--525.]] Alur, R., Henzinger, T. A., Mang, F. Y. C., Qadeer, S. K., Rajamani, S. K., and Tasiran, S. 1998. Mocha: Modularity in model checking. In Proc. 10th International Conference, Computer Aided Verification. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, 521--525.]]

Alur R. La Torre S. and Madhusudan P. 2002. Playing games with boxes and diamonds. Tech. Rep. Univ. Pennsylvania.]] Alur R. La Torre S. and Madhusudan P. 2002. Playing games with boxes and diamonds. Tech. Rep. Univ. Pennsylvania.]]

10.1145/320613.320614

10.1145/136035.136043

Büchi , J. R. and Landweber , L. H. 1969 . Solving sequential conditions by finite-state strategies . Trans. AMS 138 , 295 -- 311 .]] Büchi, J. R. and Landweber, L. H. 1969. Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295--311.]]

10.1016/0890-5401(92)90017-A

10.1145/322234.322243

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

10.1145/5397.5399

Cleaveland , R. , and Steffen , B . 1991. A linear-time model-checking algorithm for the alternation-free modal μ-calculus . In Proc. 3rd International Conference on Computer Aided Verification. Lecture Notes in Computer Science , vol. 575 . Springer-Verlag, 48--58.]] Cleaveland, R., and Steffen, B. 1991. A linear-time model-checking algorithm for the alternation-free modal μ-calculus. In Proc. 3rd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 575. Springer-Verlag, 48--58.]]

10.1016/0304-3975(94)90269-0

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 .]] 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.]]

de Alfaro , L. , Henzinger , T. A. , and Mang , F. Y. C. 2000. The control of synchronous systems . In Proc. 11th International Conference on Concurrency Theory. Lecture Notes in Computer Science , vol. 1877 . Springer-Verlag, 458--473.]] de Alfaro, L., Henzinger, T. A., and Mang, F. Y. C. 2000. The control of synchronous systems. In Proc. 11th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1877. Springer-Verlag, 458--473.]]

de Alfaro , L. , Henzinger , T. A. , and Mang , F. Y. C. 2001b. The control of synchronous systems , Part II. In Proc. 12th International Conference on Concurrency Theory. Lecture Notes in Computer Science , vol. 2154 . Springer-Verlag, 566--580.]] de Alfaro, L., Henzinger, T. A., and Mang, F. Y. C. 2001b. The control of synchronous systems, Part II. In Proc. 12th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 2154. Springer-Verlag, 566--580.]]

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

Emerson , E. A. 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science , vol. B. J. van Leeuwen, Ed. Elsevier, 997-- 1072 .]] Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, vol. B. J. van Leeuwen, Ed. Elsevier, 997--1072.]]

10.1145/4904.4999

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 .]] 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.]]

Emerson , E. A. , and Lei , C . -L. 1985. Modalities for model checking: Branching-time logic strikes back . In Proc. 20th Symp. on Principles of Programming Languages. ACM Press, 84--96 .]] 10.1145/3 1859 3.318620 Emerson, E. A., and Lei, C.-L. 1985. Modalities for model checking: Branching-time logic strikes back. In Proc. 20th Symp. on Principles of Programming Languages. ACM Press, 84--96.]] 10.1145/318593.318620

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.]] 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.]]

Emerson , E. A. , and Sistla , A. P . 1984. Deciding branching-time logic . In Proc. 16th Symp. on Theory of Computing. ACM Press, 14--24 .]] 10.1145/800057.808661 Emerson, E. A., and Sistla, A. P. 1984. Deciding branching-time logic. In Proc. 16th Symp. on Theory of Computing. ACM Press, 14--24.]] 10.1145/800057.808661

Etessami , K. , Wilke , T. , and Schuller , R. A . 2001. Fair simulation relations, parity games, and state space reduction for Büchi automata . In Proc. 28th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science , vol. 2076 . Springer-Verlag, 694--707.]] Etessami, K., Wilke, T., and Schuller, R. A. 2001. Fair simulation relations, parity games, and state space reduction for Büchi automata. In Proc. 28th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076. Springer-Verlag, 694--707.]]

Fischer , M. J. , and Ladner , R. E. 1979 . Propositional dynamic logic of regular programs . J. Comput. Syst. Sci. 18 , 194 -- 211 .]] Fischer, M. J., and Ladner, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194--211.]]

Gawlick , R. , Segala , R. , Sogaard-Andersen , J. , and Lynch , N. A . 1994. Liveness in timed and untimed systems . In Proc. 21st International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science , vol. 820 . Springer-Verlag, 166--177.]] Gawlick, R., Segala, R., Sogaard-Andersen, J., and Lynch, N. A. 1994. Liveness in timed and untimed systems. In Proc. 21st International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 820. Springer-Verlag, 166--177.]]

Gurevich , Y. , and Harrington , L . 1982. Trees, automata, and games . In Proc. 14th Symp. on Theory of Computing. ACM Press, 60--65 .]] 10.1145/800070.802177 Gurevich, Y., and Harrington, L. 1982. Trees, automata, and games. In Proc. 14th Symp. on Theory of Computing. ACM Press, 60--65.]] 10.1145/800070.802177

Halpern , J. Y. and Fagin , R. 1989 . Modeling knowledge and action in distributed systems . Distrib. Comput. 3 , 4, 159 -- 179 .]] Halpern, J. Y. and Fagin, R. 1989. Modeling knowledge and action in distributed systems. Distrib. Comput. 3, 4, 159--179.]]

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

10.1109/32.588521

Immerman , N. 1981 . Number of quantifiers is better than number of tape cells . J. Comput. Syst. Sci. 22 , 3, 384 -- 406 .]] Immerman, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 3, 384--406.]]

Jurdzinski , M. 2000. Small progress measures for solving parity games . In Proc. 17th Symp. on Theoretical Aspects of Computer Science . Lecture Notes in Computer Science , vol. 1770 . Springer-Verlag , 290--301.]] Jurdzinski, M. 2000. Small progress measures for solving parity games. In Proc. 17th Symp. on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1770. Springer-Verlag, 290--301.]]

Kozen , D. 1983 . Results on the propositional μ-calculus . Theoret. Comput. Sci. 27 , 333 -- 354 .]] Kozen, D. 1983. Results on the propositional μ-calculus. Theoret. Comput. Sci. 27, 333--354.]]

Kupferman , O. , and Vardi , M. Y . 1995. On the complexity of branching modular model checking . In Proc. 6th International Conference on Concurrency Theory. Lecture Notes in Computer Science , vol. 962 . Springer-Verlag, 408--422.]] Kupferman, O., and Vardi, M. Y. 1995. On the complexity of branching modular model checking. In Proc. 6th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 962. Springer-Verlag, 408--422.]]

Kupferman , O. and Vardi , M. Y. 1998 . Verification of fair transition systems . Chicago J. Theoret. Comput. Sci. 1998 , 2 .]] Kupferman, O. and Vardi, M. Y. 1998. Verification of fair transition systems. Chicago J. Theoret. Comput. Sci. 1998, 2.]]

10.1145/333979.333987

10.1006/inco.2000.2893

Lichtenstein , O. , and Pnueli , A . 1985. Checking that finite state concurrent programs satisfy their linear specification . In Proc. 12th Symp. on Principles of Programming Languages. ACM Press, 97--107 .]] 10.1145/3 1859 3.318622 Lichtenstein, O., and Pnueli, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th Symp. on Principles of Programming Languages. ACM Press, 97--107.]] 10.1145/318593.318622

Lynch N. A. 1996. Distributed Algorithms. Morgan-Kaufmann.]] Lynch N. A. 1996. Distributed Algorithms. Morgan-Kaufmann.]]

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

Parikh , R. 1983 . Propositional game logic . In Proc. 24th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 195--200 .]] Parikh, R. 1983. Propositional game logic. In Proc. 24th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 195--200.]]

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 .]] 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.]]

Pnueli , A. 1977 . The temporal logic of programs . In Proc. 18th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 46--57 .]] Pnueli, A. 1977. The temporal logic of programs. In Proc. 18th Symp. on Foundations of Computer Science. IEEE Computer Society Press, 46--57.]]

Pnueli , A. , and Rosner , R . 1989a. On the synthesis of a reactive module . In Proc. 16th Symp. on Principles of Programming Languages. ACM Press, 179--190 .]] 10.1145/75277.75293 Pnueli, A., and Rosner, R. 1989a. On the synthesis of a reactive module. In Proc. 16th Symp. on Principles of Programming Languages. ACM Press, 179--190.]] 10.1145/75277.75293

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

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 .]] 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.]]

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

Rabin , M. O. 1972 . Automata on Infinite Objects and Church's Problem . Regional Conference Series in Mathematics , vol. 13 ., AMS.]] Rabin, M. O. 1972. Automata on Infinite Objects and Church's Problem. Regional Conference Series in Mathematics, vol. 13., AMS.]]

Ramadge , P. , and Wonham , W. 1989 . The control of discrete event systems . IEEE Transactions on Control Theory 77 , 81 -- 98 .]] Ramadge, P., and Wonham, W. 1989. The control of discrete event systems. IEEE Transactions on Control Theory 77, 81--98.]]

Reif , J. H. 1984 . The complexity of two-player games of incomplete information . J. Comput. Syst. Sci. 29 , 274 -- 301 .]] Reif, J. H. 1984. The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29, 274--301.]]

Shapley , L. S. 1953 . Stochastic games . In Proc. Nat. Acad. Sci. , 39 , 1095 -- 1100 .]] Shapley, L. S. 1953. Stochastic games. In Proc. Nat. Acad. Sci., 39, 1095--1100.]]

Thomas , W. 1990. Automata on infinite objects. Handbook of Theoretical Computer Science , vol. B, J. van Leeuwen, Ed. Elsevier, 165-- 191 .]] Thomas, W. 1990. Automata on infinite objects. Handbook of Theoretical Computer Science, vol. B, J. van Leeuwen, Ed. Elsevier, 165--191.]]

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.]] 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.]]

Thông tin
Thông tin xuất bản

Journal of the ACM

Tập 49 Số 5

672-713

Thông tin tác giả