The Community for Technology Leaders
Proceedings of 37th Conference on Foundations of Computer Science (1996)
Burlington, VT
Oct. 14, 1996 to Oct. 16, 1996
ISBN: 0-8186-7594-2
pp: 256
D. Therien , Sch. of Comput. Sci., McGill Univ., Montreal, Que., Canada
T. Wilke , Sch. of Comput. Sci., McGill Univ., Montreal, Que., Canada
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 at most 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.
INDEX TERMS
temporal logic; temporal logic; semidirect products; until hierarchy; finite semigroups; algebraic characterization; nesting depth; finite semigroup theory
CITATION

T. Wilke and D. Therien, "Temporal logic and semidirect products: an effective characterization of the until hierarchy," Proceedings of 37th Conference on Foundations of Computer Science(FOCS), Burlington, VT, 1996, pp. 256.
doi:10.1109/SFCS.1996.548484
93 ms
(Ver 3.3 (11022016))