LIPIcs.FSTTCS.2009.2313.pdf
- Filesize: 123 kB
- 12 pages
Document
Automata and temporal logic over arbitrary linear time
Author
-
Part of:
Volume:
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2009-12-14
Cite AsGet BibTex
Julien Cristau. Automata and temporal logic over arbitrary linear time. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 133-144, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2313
https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2313
Abstract
Linear temporal logic was introduced in order to reason about reactive
systems. It is often considered with respect to infinite words, to specify
the behaviour of long-running systems. One can consider more general models
for linear time, using words indexed by arbitrary linear orderings. We
investigate the connections between temporal logic and automata on linear
orderings, as introduced by Bruyere and Carton. We provide a doubly
exponential procedure to compute from any LTL formula with \until, \since, and
the Stavi connectives an automaton that decides whether that formula holds on
the input word. In particular, since the emptiness problem for these automata
is decidable, this transformation gives a decision procedure for the
satisfiability of the logic.
Keywords
- LTL
- linear orderings
- automata
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads