DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2009.2313

Automata and temporal logic over arbitrary linear time

Authors: Julien Cristau

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{cristau:LIPIcs.FSTTCS.2009.2313,
  author =	{Cristau, Julien},
  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 =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2313},
  URN =		{urn:nbn:de:0030-drops-23132},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2313},
  annote =	{Keywords: LTL, linear orderings, automata}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2008.1748

Graph Games on Ordinals

Authors: Julien Cristau and Florian Horn

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract

We consider an extension of Church\'s synthesis problem to ordinals by adding limit transitions to graph games. We consider game arenas where these limit transitions are defined using the sets of cofinal states. In a previous paper, we have shown that such games of ordinal length are determined and that the winner problem is \pspace-complete, for a subclass of arenas where the length of plays is always smaller than $\omega^\omega$. However, the proof uses a rather involved reduction to classical Muller games, and the resulting strategies need infinite memory. We adapt the LAR reduction to prove the determinacy in the general case, and to generate strategies with finite memory, using a reduction to games where the limit transitions are defined by priorities. We provide an algorithm for computing the winning regions of both players in these games, with a complexity similar to parity games. Its analysis yields three results: determinacy without hypothesis on the length of the plays, existence of memoryless strategies, and membership of the winner problem in \npconp.

Cite as

Julien Cristau and Florian Horn. Graph Games on Ordinals. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 143-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{cristau_et_al:LIPIcs.FSTTCS.2008.1748,
  author =	{Cristau, Julien and Horn, Florian},
  title =	{{Graph Games on Ordinals}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{143--154},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1748},
  URN =		{urn:nbn:de:0030-drops-17485},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1748},
  annote =	{Keywords: Games, ordinals, zeno}
}

Search Results

Documents authored by Cristau, Julien

Automata and temporal logic over arbitrary linear time

Abstract

Cite as

Graph Games on Ordinals

Abstract

Cite as

Thanks for your feedback!

Could not send message