Journal of Logic and Computation

Journal of Logic and Computation Advance Access published online on February 6, 2008
Journal of Logic and Computation, doi:10.1093/logcom/exn002

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Guelev, D. P. Social Bookmarking          What's this?

© The Author, 2008. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original papers

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

Dimitar P. Guelev

Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria.

E-mail: gelevdp{at}math.bas.bg

Received 22 January 2007.

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

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 iff 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.

Keywords: Linear temporal logic; canonical reactivity normal form; separation

References

1. Chang E, Manna Z, Pnueli A. The Safety-Progress Classification. In: Logic and Algebra of Specification (1991) Berlin: Springer. 143–202. NATO Advanced Science Institutes Series.
2. Gabbay DM. Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In: Proceedings of the Colloquium of Temporal Logic in Specification (1989) Vol. 398 of LNCS. Berlin: Springer. 67–89.
3. Gabbay D, Hodkinson I, Reynolds M. Temporal Logic: Mathematical Foundations and Computational Aspects. Volume I (1994) Oxford University Press.
4. Kamp J. A. W, ed. Tense Logic and the Theory of Linear Order. PhD Thesis (1968) Los Angeles: University of California.
5. Krohn K, Rhodes J. The Algebraic Theory of Machines I. In: Transactions of the American Mathematical Society (1965) 116:450–464.[CrossRef][ISI]
6. Manna Z, Pnueli A. The anchored version of the temporal framework. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency—Bakker J. W. De, Roever W-P. de, Rozenberg G, eds. (1989) Vol. 354 of LNCS. Berlin: Springer. 201–284.[CrossRef]
7. Manna Z, Pnueli A. A hierarchy of temporal properties. In: 9th Symposium on Principles of Distributed Computing (1990) ACM Press. 377–408.
8. Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification (1992) Berlin: Springer-Verlag.
9. Manna Z, Pnueli A. Temporal Verification of Reactive Systems: Safety (1995) Berlin: Springer-Verlag.
10. Pnueli A. The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium Foundations of Computer Science (1977) IEEE. 46–57.
11. Reynolds M. More past glories. In: LICS'00: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (2000) Washington, DC, USA: IEEE Computer Society. 229–240.
12. Zuck L. Past Temporal Logic. PhD thesis (1986) Weizmann Institute of Science.

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Guelev, D. P. Social Bookmarking          What's this?