A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic.
Saved in:
| Title: | A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic. |
|---|---|
| Authors: | GUELEV, DIMITAR P.1 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 34034895 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22GUELEV%2C+DIMITAR+P%2E%22">GUELEV, DIMITAR P.</searchLink><relatesTo>1</relatesTo><i> gelevdp@math.bas.bg</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Aug2008, Vol. 18 Issue 4, p615-623. 9p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Machine+theory%22">Machine theory</searchLink><br /><searchLink fieldCode="DE" term="%22Sequential+machine+theory%22">Sequential machine theory</searchLink><br /><searchLink fieldCode="DE" term="%22Cellular+automata%22">Cellular automata</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+design%22">Logic design</searchLink><br /><searchLink fieldCode="DE" term="%22Nonclassical+mathematical+logic%22">Nonclassical mathematical logic</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=34034895 |
| RecordInfo | BibRecord: BibEntity: Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 9 StartPage: 615 Subjects: – SubjectFull: Machine theory Type: general – SubjectFull: Sequential machine theory Type: general – SubjectFull: Cellular automata Type: general – SubjectFull: Mathematical logic Type: general – SubjectFull: Logic design Type: general – SubjectFull: Nonclassical mathematical logic Type: general Titles: – TitleFull: A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: GUELEV, DIMITAR P. IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 08 Text: Aug2008 Type: published Y: 2008 Identifiers: – Type: issn-print Value: 0955792X Numbering: – Type: volume Value: 18 – Type: issue Value: 4 Titles: – TitleFull: Journal of Logic & Computation Type: main |
| ResultId | 1 |
