Logic in Computer Science (LICS 1996)

Paper: An Until Hierarchy for Temporal Logic (at LICS 1996)

Authors: Kousha Etessami Thomas Wilke

Abstract

We prove there is a strict hierarchy of expressive power according to the Until depth of linear temporal logic (TL) formulas: for each k, there is a very natural property that is not expressible with k nestings of Until operators, regardless of the number of applications of other operators, but is expressible by a formula with Until depth k+1. Our proof uses a new Ehrenfeucht-Frai}sse (EF) game designed specifically for TL. These properties can all be expressed in first-order logic with quantifier depth and size O(log k), and we use them to observe some interesting relationships between TL and first-order expressibility. We then use the EF game in a novel way to effectively characterize (1) the TL properties expressible without Until, as well as (2) those expressible without both Until and Next. By playing the game ``on finite automata'', we prove that the automata recognizing languages expressible in each of the two fragments have distinctive structural properties. The characterization for the first fragment was originally proven by Cohen, Perrin, and Pin using sophisticated semigroup-theoretic techniques. They asked whether such a characterization exists for the second fragment. The technique we develop is general and can potentially be applied in other contexts.

BibTeX

  @InProceedings{EtessamiWilke-AnUntilHierarchyfor,
    author = 	 {Kousha Etessami and Thomas Wilke},
    title = 	 {An Until Hierarchy for Temporal Logic},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {108-127},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }