On the expressive power of temporal logic
作者:
Highlights:
•
摘要
We study the expressive power of linear propositional temporal logic interpreted on finite sequences or words. We first give a transparent proof of the fact that a formal language is expressible in this logic if and only if its syntactic semigroup is finite and aperiodic. This gives an effective algorithm to decide whether a given rational language is expressible. Our main result states a similar condition for the “restricted” temporal logic (RTL), obtained by discarding the “until” operator. A formal language is RTL-expressible if and only if its syntactic semigroup is finite and satisfies a certain simple algebraic condition. This leads to a polynomial time algorithm to check whether the formal language accepted by an n-state deterministic automaton is RTL-expressible.
论文关键词:
论文评审过程:Available online 2 December 2003.
论文官网地址:https://doi.org/10.1016/0022-0000(93)90005-H