@article{Therien:Wilke:ToCS:2004,
    Abstract = {We provide an effective characterization of the ``until-since hierarchy''oflinear temporal logic over finite models (strings), that is, we show how tocompute for a given temporal property of strings the minimal nesting depthin ``until''and ``since''required to express it. This settles the mostprominent classification problem for linear temporal logic. Ourcharacterization of the individual levels of the ``until-since hierarchy''is algebraic: for each n, we present a decidable class of finitesemigroups and show that a temporal property is expressible with nestingdepth at most n if and only if the syntactic semigroup of the formallanguage associated with the property belongs to the class provided. Thecore of our algebraic characterization is a new description of substitutionin linear temporal logic in terms of block products of finite semigroups.},
    Author = {Th{\'e}rien, Denis and Wilke, Thomas},
    File = {Nesting Until and Since in Linear Temporal Logic -10.1007@s00224-003-1109-3 - a - a - a - r.pdf},
    ISBN = {1433-0490},
    Journal = {Theory of Computing Systems},
    Number = {1},
    Pages = {111--131},
    Title = {Nesting Until and Since in Linear Temporal Logic},
    URL = {https://doi.org/10.1007/s00224-003-1109-3},
    Volume = {37},
    Year = {2004},
    bdsk-url-1 = {https://doi.org/10.1007/s00224-003-1109-3},
    da = {2004/01/01},
    date-added = {2020-02-06 16:28:31 +0100},
    date-modified = {2020-08-05 18:10:43 +0200},
    id = {Th{\'e}rien2004},
    ty = {JOUR},
    doi = {10.1007/s00224-003-1109-3}
}

@article{Therien:Wilke:ToCS:2004, Abstract = {We provide an effective characterization of the until-since hierarchy''oflinear temporal logic over finite models (strings), that is, we show how tocompute for a given temporal property of strings the minimal nesting depthinuntil''and since''required to express it. This settles the mostprominent classification problem for linear temporal logic. Ourcharacterization of the individual levels of theuntil-since hierarchy''is algebraic: for each n, we present a decidable class of finitesemigroups and show that a temporal property is expressible with nestingdepth at most n if and only if the syntactic semigroup of the formallanguage associated with the property belongs to the class provided. Thecore of our algebraic characterization is a new description of substitutionin linear temporal logic in terms of block products of finite semigroups.}, Author = {Th{\'e}rien, Denis and Wilke, Thomas}, File = {Nesting Until and Since in Linear Temporal Logic -10.1007@s00224-003-1109-3 - a - a - a - r.pdf}, ISBN = {1433-0490}, Journal = {Theory of Computing Systems}, Number = {1}, Pages = {111--131}, Title = {Nesting Until and Since in Linear Temporal Logic}, URL = {https://doi.org/10.1007/s00224-003-1109-3}, Volume = {37}, Year = {2004}, bdsk-url-1 = {https://doi.org/10.1007/s00224-003-1109-3}, da = {2004/01/01}, date-added = {2020-02-06 16:28:31 +0100}, date-modified = {2020-08-05 18:10:43 +0200}, id = {Th{\'e}rien2004}, ty = {JOUR}, doi = {10.1007/s00224-003-1109-3} }