Nesting until and since in linear temporal logic

Abstract

We provide an effective characterization of the “until-since hierarchy” of linear temporal logic, that is, we show how to compute for a given temporal property the minimal nesting depth in “until” and “since” required to express it. This settles the most prominent classification problem for linear temporal logic. Our characterization of the individual levels of the “until-since hierarchy” is algebraic: for each n, we present a decidable class of finite semigroups and show that a temporal property is expressible with nesting depth at most n if and only if the syntactic semigroup of the formal language associated with the property belongs to the class provided. The core of our algebraic characterization is a new description of substitution in linear temporal logic in terms of block products of finite semigroups.