A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic.

Saved in:

Bibliographic Details
Title:	A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic.
Authors:	GUELEV, DIMITAR P.¹ gelevdp@math.bas.bg
Source:	Journal of Logic & Computation. Aug2008, Vol. 18 Issue 4, p615-623. 9p.
Subjects:	Machine theory, Sequential machine theory, Cellular automata, Mathematical logic, Logic design, Nonclassical mathematical logic
Abstract:	We present a new proof of the fact that every formula in linear temporal logic with past is equivalent to a formula of the form "Multiple line equation(s) cannot be represented in ASCII text" where αi and βi are past formulas, which is known as general canonical reactivity form. The original proof is based on the fact that a finite automaton recognizes an LTL-definable ω-language if it is counter-free, which was proved in Lenore Zuck's thesis and relies on the theorem of Krohn-Rhodes about cascade decomposition of finite automata. Unlike that, the proof presented in this paper involves only equivalence transformations of LTL formula and makes use of Gabbay's separation theorem, whose proof is based on equivalence transformations too. This makes it possible to obtain the canonical form without resorting to constructions outside LTL with past operators such as automata. [ABSTRACT FROM AUTHOR]
	Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	We present a new proof of the fact that every formula in linear temporal logic with past is equivalent to a formula of the form "Multiple line equation(s) cannot be represented in ASCII text" where αi and βi are past formulas, which is known as general canonical reactivity form. The original proof is based on the fact that a finite automaton recognizes an LTL-definable ω-language if it is counter-free, which was proved in Lenore Zuck's thesis and relies on the theorem of Krohn-Rhodes about cascade decomposition of finite automata. Unlike that, the proof presented in this paper involves only equivalence transformations of LTL formula and makes use of Gabbay's separation theorem, whose proof is based on equivalence transformations too. This makes it possible to obtain the canonical form without resorting to constructions outside LTL with past operators such as automata. [ABSTRACT FROM AUTHOR]
ISSN:	0955792X