Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Cristau, Julien http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-23132
URL:

Automata and temporal logic over arbitrary linear time

pdf-format:


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.

BibTeX - Entry

@InProceedings{cristau:LIPIcs:2009:2313,
  author =	{Julien Cristau},
  title =	{{Automata and temporal logic over arbitrary linear time}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{133--144},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Ravi Kannan and K. Narayan Kumar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2313},
  URN =		{urn:nbn:de:0030-drops-23132},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2313},
  annote =	{Keywords: LTL, linear orderings, automata}
}

Keywords: LTL, linear orderings, automata
Seminar: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue date: 2009
Date of publication: 2009


DROPS-Home | Fulltext Search | Imprint Published by LZI