License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2014.267
URN: urn:nbn:de:0030-drops-48483
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4848/
Go to the corresponding LIPIcs Volume Portal

Colcombet, Thomas ; Manuel, Amaldev

Generalized Data Automata and Fixpoint Logic

pdf-format:
24.pdf (0.5 MB)

Abstract

Data omega-words are omega-words where each position is additionally labelled by a data value from an infinite alphabet. They can be seen as graphs equipped with two sorts of edges: "next position" and "next position with the same data value". Based on this view, an extension of Data Automata called Generalized Data Automata (GDA) is introduced. While the decidability of emptiness of GDA is open, the decidability for a subclass class called Büchi GDA is shown using Multicounter Automata. Next a natural fixpoint logic is defined on the graphs of data omega-words and it is shown that the mu-fragment as well as the alternation-free fragment is undecidable. But the fragment which is defined by limiting the number of alternations between future and past formulas is shown to be decidable, by first converting the formulas to equivalent alternating Büchi automata and then to Büchi GDA.

BibTeX - Entry

@InProceedings{colcombet_et_al:LIPIcs:2014:4848,
  author =	{Thomas Colcombet and Amaldev Manuel},
  title =	{{Generalized Data Automata and Fixpoint Logic}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{267--278},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Venkatesh Raman and S. P. Suresh},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4848},
  URN =		{urn:nbn:de:0030-drops-48483},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.267},
  annote =	{Keywords: Data words, Data Automata, Decidability, Fixpoint Logic}
}

Keywords: Data words, Data Automata, Decidability, Fixpoint Logic
Collection: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)
Issue Date: 2014
Date of publication: 12.12.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI