2026-07-22T22:30:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2313 2024-03-06T10:33:16Z ddc:004 open_access

Automata and temporal logic over arbitrary linear time Cristau, Julien LTL linear orderings automata 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Julien Cristau 2009 Is Part Of LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2009.2313 urn:nbn:de:0030-drops-23132 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2313 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode