Rajeev Alur
Abstract
Deciding infinite two-player games on finite graphs with the winning condition specified by a linear temporal logic (Ltl) formula, is known to be 2Exptime-complete. In this paper, we identify Ltl fragments of lower complexity. Solving Ltl games typically involves a doubly exponential translation from Ltl formulas to deterministic ω-automata. First, we show that the longest distance (length of the longest simple path) of the generator is also an important parameter, by giving an O(d log n)-space procedure to solve a Büchi game on a graph with n vertices and longest distance d. Then, for the Ltl fragment of the Boolean combinations of formulas obtained only by eventualities and conjunctions, we provide a translation to deterministic generators of exponential size and linear longest distance, show both of these bounds to be optimal, and prove the corresponding games to be Pspace-complete. Introducing next modalities in this fragment, we give a translation to deterministic generators still of exponential size but also with exponential longest distance, show both of these bounds to be optimal, and prove the corresponding games to be Exptime-complete. For the fragment resulting by further adding disjunctions, we provide a translation to deterministic generators of doubly exponential size and exponential longest distance, show both of these bounds to be optimal, and prove the corresponding games to be Expspace. We also show tightness of the double exponential bound on the size as well as the longest distance for deterministic generators of Ltl formulas without next and until modalities. Finally, we identify a class of deterministic Büchi automata corresponding to a fragment of Ltl with restricted use of always and until modalities, for which deciding games is Pspace-complete.
- Alur, R., Alfaro, L. de, Henzinger, T., and Mang., F. 1999. Automating modular verification. In CONCUR'99: Concurrency Theory, Tenth International Conference, LNCS 1664, pages 82--97.]] Google Scholar
- Alur, R., Henzinger, T. A., and Kupferman, O. 1997. Alternating-time temporal logic. In Proceedings of the 38th IEEE Symposium on Foundations of Computer Science, pages 100--109.]] Google Scholar
- Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., and Tasiran, S. 1998. MOCHA: Modularity in model checking. In Proceedings of the 10th International Conference on Computer Aided Verification, LNCS 1427, pages 521--525. Springer-Verlag.]] Google Scholar
- Abadi, M., Lamport, L. and Wolper, P. 1989. Realizable and unrealizable specifications of reactive systems. In Proceedings of the 16th International Colloquium on Automata, Languages and Programming, ICALP'89, LNCS 372, pages 1--17.]] Google Scholar
- Dill, D. L. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. ACM Distinguished Dissertation Series. MIT Press.]] Google Scholar
- Demri, S. and Schnoebelen, Ph. 1998. The complexity of propositional linear temporal logics in simple cases. In Proceedings of the 15th Annual Symposium on Theoretical Aspects of Computer Science, STACS'98, LNCS 1373, pages 61--72. Springer-Verlag.]] Google Scholar
- Emerson, E. A. and Jutla, C. S. 1988. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE-CS Symposium on Foundations of Computer Science, pages 328--337.]]Google Scholar
- Emerson, E. A. 1990. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995--1072. Elsevier Science Publishers.]] Google Scholar
- Kupferman, O. and Vardi, M. Y. 1996. Module checking. In Computer Aided Verification, Proceedings of the Eighth International Workshop, LNCS 1102, pages 75--86. Springer-Verlag.]] Google Scholar
- Kupferman, O. and Vardi, M. Y. 1997. Module checking revisited. In Proceedings of the 9th International Conference on Computer Aided Verification, CAV'97, LNCS 1254, pages 36 --47.]] Google Scholar
- Kupferman, O. and Vardi, M. Y. 1998. Freedom, weakness, and determinism: From linear-time to branching-time. In Proceedings of the 13th IEEE Symposium on Logic in Computer Science, pages 81--92.]] Google Scholar
- Lichtenstein, O. and Pnueli, A. 1985. Checking that finite-state concurrent programs satisfy their linear specification. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 97--107.]] Google Scholar
- Manna, Z. and Pnueli, A. 1991. The temporal logic of reactive and concurrent systems: Specification. Springer-verlag.]] Google Scholar
- Marcinkowski, J. and Truderung, T. 2002. Optimal complexity bounds for positive LTL games. In Proceedings of the 16th Annual Conference of the European Association for Computer Science Logic, CSL'02. Springer-verlag.]] Google Scholar
- Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46--77.]]Google Scholar
- Pnueli, A. and Rosner, R. 1989. On the synthesis of a reactive module. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pages 179--190.]] Google Scholar
- Rabin, M. O. 1972. Automata on infinite objects and Church's problem. Trans. Amer. Math. Soc.]] Google Scholar
- Rosner, R. 1992. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science.]]Google Scholar
- Safra, S. 1998. On the complexity of ω-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319--327.]]Google Scholar
- Sistla, A. P. and Clarke, E. M. 1985. The complexity of propositional linear temporal logics. J. ACM, 32, 733--749.]] Google Scholar
- Thomas, W. 1995. On the synthesis of strategies in infinite games. In Ernst W. Mayr and Claude Puech, editors, 12th Annual Symposium on Theoretical Aspects of Computer Science, STACS'95, LNCS 900, pages 1--13. Springer-Verlag.]]Google Scholar
- Vardi, M. Y. and Wolper, P. 1994. Reasoning about infinite computations. Information and Computation, 115, 1--37.]] Google Scholar
Index Terms
- Deterministic generators and games for Ltl fragments
Recommendations
Deterministic Generators and Games for Ltl Fragments
LICS '01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer ScienceAbstract: Deciding infinite two-player games on finite graphs with the winning condition specified by a linear temporal logic (Ltl) formula, is known to be 2Exptime-complete. In this paper, we identify Ltl fragments of lower complexity. Solving Ltl ...
From LTL to deterministic automata
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula $$\varphi $$ź. The automaton is the product of a co-Büchi automaton for $$\varphi $$ź and an array of Rabin automata, one for each $${\mathbf {G}}$$...
Token Games and History-Deterministic Quantitative Automata
Foundations of Software Science and Computation StructuresAbstractA nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving ...
Comments