An Until Hierarchy for Temporal Logic

Kousha Etessami, Thomas Wilke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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-Fraisse (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 proved by Cohen, Perrin, and Pin (1993) 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
Original languageEnglish
Title of host publicationProceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages10
ISBN (Print)0-8186-7463-6
Publication statusPublished - 1996


Dive into the research topics of 'An Until Hierarchy for Temporal Logic'. Together they form a unique fingerprint.

Cite this