96-28: Temporal Logic and Semidirect Products: An Effective Characterization of the Until Hierarchy

DIMACS TR: 96-28

Temporal Logic and Semidirect Products: An Effective Characterization of the Until Hierarchy

Authors: Denis Therien, Thomas Wilke

ABSTRACT
We reveal an intimate connection between semidirect products of finite semigroups and substitution of formulas in linear temporal logic. We use this connection to obtain an algebraic characterization of the `until' hierarchy of linear temporal logic; the k-th level of that hierarchy is comprised of all temporal properties that are expressible by a formula of nesting depth k in the `until' operator. Applying deep results from finite semigroup theory we are able to prove that each level of the `until' hierarchy is decidable.

Paper Available at: ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1996/96-28.ps.gz

DIMACS Home Page