|
Abstract : |
Abstract. We provide an eective 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 classi-cation 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 nite 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 nite semigroups. 1, |
