License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.81
URN: urn:nbn:de:0030-drops-41916
URL: http://drops.dagstuhl.de/opus/volltexte/2013/4191/
Go to the corresponding LIPIcs Volume Portal


Bilkowski, Marcin ; Skrzypczak, Michał

Unambiguity and uniformization problems on infinite trees

pdf-format:
11.pdf (0.5 MB)


Abstract

A nondeterministic automaton is called unambiguous if it has at most one accepting run on every input. A regular language is called unambiguous if there exists an unambiguous automaton recognizing this language. Currently, the class of unambiguous languages of infinite trees is not well-understood. In particular, there is no known decision procedure verifying if a given regular tree language is unambiguous. In this work we study the self-dual class of bi-unambiguous languages - languages that are unambiguous and their complement is also unambiguous. It turns out that thin trees (trees with only countably many branches) emerge naturally in this context. We propose a procedure P designed to decide if a given tree automaton recognizes a bi-unambiguous language. The procedure is sound for every input. It is also complete for languages recognisable by deterministic automata. We conjecture that P is complete for all inputs but this depends on a new conjecture stating that there is no MSO-definable choice function on thin trees. This would extend a result by Gurevich and Shelah on the undefinability of choice on the binary tree. We provide a couple of equivalent statements to our conjecture, we also give several related results about uniformizability on thin trees. In particular, we provide a new example of a language that is not unambiguous, namely the language of all thin trees. The main tool in our studies are algebras that can be seen as an adaptation of Wilke algebras to the case of infinite trees.

BibTeX - Entry

@InProceedings{bilkowski_et_al:LIPIcs:2013:4191,
  author =	{Marcin Bilkowski and Michał Skrzypczak},
  title =	{{Unambiguity and uniformization problems on infinite trees}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{81--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4191},
  URN =		{urn:nbn:de:0030-drops-41916},
  doi =		{10.4230/LIPIcs.CSL.2013.81},
  annote =	{Keywords: nondeterministic automata, infinite trees, MSO logic}
}

Keywords: nondeterministic automata, infinite trees, MSO logic
Seminar: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 27.08.2013


DROPS-Home | Fulltext Search | Imprint Published by LZI