Search Results

Documents authored by Vanden Boom, Michael

Document
DOI: 10.4230/LIPIcs.ICALP.2017.107
Characterizing Definability in Decidable Fixpoint Logics

Authors: Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back-and-forth between relational logics and logics over trees.
Cite as

Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. Characterizing Definability in Decidable Fixpoint Logics. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 107:1-107:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2017.107,
  author =	{Benedikt, Michael and Bourhis, Pierre and Vanden Boom, Michael},
  title =	{{Characterizing Definability in Decidable Fixpoint Logics}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{107:1--107:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.107},
  URN =		{urn:nbn:de:0030-drops-74062},
  doi =		{10.4230/LIPIcs.ICALP.2017.107},
  annote =	{Keywords: Guarded logics, bisimulation, definability, automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.215
Deciding the weak definability of Büchi definable tree languages

Authors: Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
Weakly definable languages of infinite trees are an expressive subclass of regular tree languages definable in terms of weak monadic second-order logic, or equivalently weak alternating automata. Our main result is that given a Büchi automaton, it is decidable whether the language is weakly definable. We also show that given a parity automaton, it is decidable whether the language is recognizable by a nondeterministic co-Büchi automaton. The decidability proofs build on recent results about cost automata over infinite trees. These automata use counters to define functions from infinite trees to the natural numbers extended with infinity. We reduce to testing whether the functions defined by certain "quasi-weak" cost automata are bounded by a finite value.
Cite as

Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 215-230, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CSL.2013.215,
  author =	{Colcombet, Thomas and Kuperberg, Denis and L\"{o}ding, Christof and Vanden Boom, Michael},
  title =	{{Deciding the weak definability of B\"{u}chi definable tree languages}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{215--230},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.215},
  URN =		{urn:nbn:de:0030-drops-41998},
  doi =		{10.4230/LIPIcs.CSL.2013.215},
  annote =	{Keywords: Tree automata, weak definability, decidability, cost automata, boundedness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.66
Quasi-Weak Cost Automata: A New Variant of Weakness

Authors: Denis Kuperberg and Michael Vanden Boom

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

Abstract
Cost automata have a finite set of counters which can be manipulated on each transition but do not affect control flow. Based on the evolution of the counter values, these automata define functions from a domain like words or trees to \N \cup \set{\infty}, modulo an equivalence relation which ignores exact values but preserves boundedness properties. These automata have been studied by Colcombet et al. as part of a "theory of regular cost functions", an extension of the theory of regular languages which retains robust equivalences, closure properties, and decidability like the classical theory. We extend this theory by introducing quasi-weak cost automata. Unlike traditional weak automata which have a hard-coded bound on the number of alternations between accepting and rejecting states, quasi-weak automata bound the alternations using the counter values (which can vary across runs). We show that these automata are strictly more expressive than weak cost automata over infinite trees. The main result is a Rabin-style characterization theorem: a function is quasi-weak definable if and only if it is definable using two dual forms of non-deterministic Büchi cost automata. This yields a new decidability result for cost functions over infinite trees.
Cite as

Denis Kuperberg and Michael Vanden Boom. Quasi-Weak Cost Automata: A New Variant of Weakness. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 66-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.FSTTCS.2011.66,
  author =	{Kuperberg, Denis and Vanden Boom, Michael},
  title =	{{Quasi-Weak Cost Automata: A New Variant of Weakness}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{66--77},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.66},
  URN =		{urn:nbn:de:0030-drops-33517},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.66},
  annote =	{Keywords: Automata, infinite trees, cost functions, weak}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact