Logic in Computer Science (LICS 2001)

Paper: Deterministic Generators and Games for LTL Fragments (at LICS 2001)

Authors: Rajeev Alur Salvatore La Torre

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 omega-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 with only 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 provide 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. Finally, we show tightness of the double-exponential bound on the size as well as the longest distance for deterministic generators for Ltl even in the absence of next and until modalities.

BibTeX

  @InProceedings{AlurLaTorre-DeterministicGenera,
    author = 	 {Rajeev Alur and Salvatore La Torre},
    title = 	 {Deterministic Generators and Games for LTL Fragments},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001},
    year =	 2001,
    editor =	 {Joseph Halpern},
    month =	 {June}, 
    pages =      {291--302},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }