Search Results

Documents authored by Löding, Christof

Document
DOI: 10.4230/LIPIcs.STACS.2023.32
A Regular and Complete Notion of Delay for Streaming String Transducers

Authors: Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.
Cite as

Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter. A Regular and Complete Notion of Delay for Streaming String Transducers. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.STACS.2023.32,
  author =	{Filiot, Emmanuel and Jecker, Isma\"{e}l and L\"{o}ding, Christof and Winter, Sarah},
  title =	{{A Regular and Complete Notion of Delay for Streaming String Transducers}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{32:1--32:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.32},
  URN =		{urn:nbn:de:0030-drops-176843},
  doi =		{10.4230/LIPIcs.STACS.2023.32},
  annote =	{Keywords: Streaming string transducers, Delay, Origin}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.114
Passive Learning of Deterministic Büchi Automata by Combinations of DFAs

Authors: León Bohn and Christof Löding

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We present an algorithm that constructs a deterministic Büchi automaton in polynomial time from given sets of positive and negative example words. This learner constructs multiple DFAs using a polynomial-time active learning algorithm on finite words as black box using an oracle that we implement based on the given sample of ω-words, and combines these DFAs into a single DBA. We prove that the resulting algorithm can learn a DBA for each DBA-recognizable language in the limit by providing a characteristic sample for each DBA-recognizable language. We can only guarantee completeness of our algorithm for the full class of DBAs through characteristic samples that are, in general, exponential in the size of a minimal DBA for the target language. But we show that for each fixed k these characteristic samples are of polynomial size for the class of DBAs in which each subset of pairwise language-equivalent states has size at most k.
Cite as

León Bohn and Christof Löding. Passive Learning of Deterministic Büchi Automata by Combinations of DFAs. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 114:1-114:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bohn_et_al:LIPIcs.ICALP.2022.114,
  author =	{Bohn, Le\'{o}n and L\"{o}ding, Christof},
  title =	{{Passive Learning of Deterministic B\"{u}chi Automata by Combinations of DFAs}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{114:1--114:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.114},
  URN =		{urn:nbn:de:0030-drops-164553},
  doi =		{10.4230/LIPIcs.ICALP.2022.114},
  annote =	{Keywords: deterministic B\"{u}chi automata, learning from examples, learning in the limit, active learning}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.20
Constructing Deterministic ω-Automata from Examples by an Extension of the RPNI Algorithm

Authors: León Bohn and Christof Löding

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The RPNI algorithm (Oncina, Garcia 1992) constructs deterministic finite automata from finite sets of negative and positive example words. We propose and analyze an extension of this algorithm to deterministic ω-automata with different types of acceptance conditions. In order to obtain this generalization of RPNI, we develop algorithms for the standard acceptance conditions of ω-automata that check for a given set of example words and a deterministic transition system, whether these example words can be accepted in the transition system with a corresponding acceptance condition. Based on these algorithms, we can define the extension of RPNI to infinite words. We prove that it can learn all deterministic ω-automata with an informative right congruence in the limit with polynomial time and data. We also show that the algorithm, while it can learn some automata that do not have an informative right congruence, cannot learn deterministic ω-automata for all regular ω-languages in the limit. Finally, we also prove that active learning with membership and equivalence queries is not easier for automata with an informative right congruence than for general deterministic ω-automata.
Cite as

León Bohn and Christof Löding. Constructing Deterministic ω-Automata from Examples by an Extension of the RPNI Algorithm. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bohn_et_al:LIPIcs.MFCS.2021.20,
  author =	{Bohn, Le\'{o}n and L\"{o}ding, Christof},
  title =	{{Constructing Deterministic \omega-Automata from Examples by an Extension of the RPNI Algorithm}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.20},
  URN =		{urn:nbn:de:0030-drops-144607},
  doi =		{10.4230/LIPIcs.MFCS.2021.20},
  annote =	{Keywords: deterministic omega-automata, learning from examples, learning in the limit, constructing acceptance conditions, active learning}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.46
Synthesis from Weighted Specifications with Partial Domains over Finite Words

Authors: Emmanuel Filiot, Christof Löding, and Sarah Winter

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
In this paper, we investigate the synthesis problem of terminating reactive systems from quantitative specifications. Such systems are modeled as finite transducers whose executions are represented as finite words in (I × O)^*, where I, O are finite sets of input and output symbols, respectively. A weighted specification S assigns a rational value (or -∞) to words in (I × O)^*, and we consider three kinds of objectives for synthesis, namely threshold objectives where the system’s executions are required to be above some given threshold, best-value and approximate objectives where the system is required to perform as best as it can by providing output symbols that yield the best value and ε-best value respectively w.r.t. S. We establish a landscape of decidability results for these three objectives and weighted specifications with partial domain over finite words given by deterministic weighted automata equipped with sum, discounted-sum and average measures. The resulting objectives are not regular in general and we develop an infinite game framework to solve the corresponding synthesis problems, namely the class of (weighted) critical prefix games.
Cite as

Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from Weighted Specifications with Partial Domains over Finite Words. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2020.46,
  author =	{Filiot, Emmanuel and L\"{o}ding, Christof and Winter, Sarah},
  title =	{{Synthesis from Weighted Specifications with Partial Domains over Finite Words}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{46:1--46:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.46},
  URN =		{urn:nbn:de:0030-drops-132874},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.46},
  annote =	{Keywords: synthesis, weighted games, weighted automata on finite words}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.27
State Space Reduction For Parity Automata

Authors: Christof Löding and Andreas Tollkötter

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Exact minimization of ω-automata is a difficult problem and heuristic algorithms are a subject of current research. We propose several new approaches to reduce the state space of deterministic parity automata. These are based on extracting information from structures within the automaton, such as strongly connected components, coloring of the states, and equivalence classes of given relations, to determine states that can safely be merged. We also establish a framework to generalize the notion of quotient automata and uniformly describe such algorithms. The description of these procedures consists of a theoretical analysis as well as data collected from experiments.
Cite as

Christof Löding and Andreas Tollkötter. State Space Reduction For Parity Automata. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.CSL.2020.27,
  author =	{L\"{o}ding, Christof and Tollk\"{o}tter, Andreas},
  title =	{{State Space Reduction For Parity Automata}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{27:1--27:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel 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.CSL.2020.27},
  URN =		{urn:nbn:de:0030-drops-116701},
  doi =		{10.4230/LIPIcs.CSL.2020.27},
  annote =	{Keywords: automata, \omega-automata, parity, minimization, state space reduction, deterministic, simulation relations}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.62
New Pumping Technique for 2-Dimensional VASS

Authors: Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski. New Pumping Technique for 2-Dimensional VASS. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 62:1-62:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.MFCS.2019.62,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and L\"{o}ding, Christof and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{New Pumping Technique for 2-Dimensional VASS}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{62:1--62:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.62},
  URN =		{urn:nbn:de:0030-drops-110066},
  doi =		{10.4230/LIPIcs.MFCS.2019.62},
  annote =	{Keywords: vector addition systems with states, pumping, decidability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.120
Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Christof Löding and Anton Pirogov

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Determinization of Büchi automata is a long-known difficult problem, and after the seminal result of Safra, who developed the first asymptotically optimal construction from Büchi into Rabin automata, much work went into improving, simplifying, or avoiding Safra’s construction. A different, less known determinization construction was proposed by Muller and Schupp. The two types of constructions share some similarities but their precise relationship was still unclear. In this paper, we shed some light on this relationship by proposing a construction from nondeterministic Büchi to deterministic parity automata that subsumes both constructions: Our construction leaves some freedom in the choice of the successor states of the deterministic automaton, and by instantiating these choices in different ways, one obtains as particular cases the construction of Safra and the construction of Muller and Schupp. The basis is a correspondence between structures that are encoded in the macrostates of the determinization procedures - Safra trees on one hand, and levels of the split-tree, which underlies the Muller and Schupp construction, on the other hand. Our construction also allows for mixing the mentioned constructions, and opens up new directions for the development of heuristics.
Cite as

Christof Löding and Anton Pirogov. Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 120:1-120:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.ICALP.2019.120,
  author =	{L\"{o}ding, Christof and Pirogov, Anton},
  title =	{{Determinization of B\"{u}chi Automata: Unifying the Approaches of Safra and Muller-Schupp}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{120:1--120:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.120},
  URN =		{urn:nbn:de:0030-drops-106963},
  doi =		{10.4230/LIPIcs.ICALP.2019.120},
  annote =	{Keywords: B\"{u}chi automata, determinization, parity automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2019.47
Tree Automata with Global Constraints for Infinite Trees

Authors: Patrick Landwehr and Christof Löding

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
We study an extension of tree automata on infinite trees with global equality and disequality constraints. These constraints can enforce that all subtrees for which in the accepting run a state q is reached (at the root of that subtree) are identical, or that these trees differ from the subtrees at which a state q' is reached. We consider the closure properties of this model and its decision problems. While the emptiness problem for the general model remains open, we show the decidability of the emptiness problem for the case that the given automaton only uses equality constraints.
Cite as

Patrick Landwehr and Christof Löding. Tree Automata with Global Constraints for Infinite Trees. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 47:1-47:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{landwehr_et_al:LIPIcs.STACS.2019.47,
  author =	{Landwehr, Patrick and L\"{o}ding, Christof},
  title =	{{Tree Automata with Global Constraints for Infinite Trees}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{47:1--47:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.47},
  URN =		{urn:nbn:de:0030-drops-102863},
  doi =		{10.4230/LIPIcs.STACS.2019.47},
  annote =	{Keywords: Tree automata, infinite trees, global constraints}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.125
On Equivalence and Uniformisation Problems for Finite Transducers

Authors: Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Transductions are binary relations of finite words. For rational transductions, i.e., transductions defined by finite transducers, the inclusion, equivalence and sequential uniformisation problems are known to be undecidable. In this paper, we investigate stronger variants of inclusion, equivalence and sequential uniformisation, based on a general notion of transducer resynchronisation, and show their decidability. We also investigate the classes of finite-valued rational transductions and deterministic rational transductions, which are known to have a decidable equivalence problem. We show that sequential uniformisation is also decidable for them.
Cite as

Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter. On Equivalence and Uniformisation Problems for Finite Transducers. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 125:1-125:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2016.125,
  author =	{Filiot, Emmanuel and Jecker, Isma\"{e}l and L\"{o}ding, Christof and Winter, Sarah},
  title =	{{On Equivalence and Uniformisation Problems for Finite Transducers}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{125:1--125:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.125},
  URN =		{urn:nbn:de:0030-drops-62605},
  doi =		{10.4230/LIPIcs.ICALP.2016.125},
  annote =	{Keywords: Transducers, Equivalence, Uniformisation}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.65
Uniformization Problems for Tree-Automatic Relations and Top-Down Tree Transducers

Authors: Christof Löding and Sarah Winter

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
For a given binary relation of finite trees, we consider the synthesis problem of deciding whether there is a deterministic top-down tree transducer that uniformizes the relation, and constructing such a transducer if it exists. A uniformization of a relation is a function that is contained in the relation and has the same domain as the relation. It is known that this problem is decidable if the relation is a deterministic top-down tree-automatic relation. We show that it becomes undecidable for general tree-automatic relations (specified by non-deterministic top-down tree automata). We also exhibit two cases for which the problem remains decidable. If we restrict the transducers to be path-preserving, which is a subclass of linear transducers, then the synthesis problem is decidable for general tree-automatic relations. If we consider relations that are finite unions of deterministic top-down tree-automatic relations, then the problem is decidable for synchronous transducers, which produce exactly one output symbol in each step (but can be non-linear).
Cite as

Christof Löding and Sarah Winter. Uniformization Problems for Tree-Automatic Relations and Top-Down Tree Transducers. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 65:1-65:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.MFCS.2016.65,
  author =	{L\"{o}ding, Christof and Winter, Sarah},
  title =	{{Uniformization Problems for Tree-Automatic Relations and Top-Down Tree Transducers}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{65:1--65:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.65},
  URN =		{urn:nbn:de:0030-drops-64771},
  doi =		{10.4230/LIPIcs.MFCS.2016.65},
  annote =	{Keywords: tree transducers, tree automatic relation, uniformization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.88
Transformation Between Regular Expressions and omega-Automata

Authors: Christof Löding and Andreas Tollkötter

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
We propose a new definition of regular expressions for describing languages of omega-words, called infinity-regular expressions. These expressions are obtained by adding to the standard regular expression on finite words an operator infinity that acts similar to the Kleene-star but can be iterated finitely or infinitely often (as opposed to the omega-operator from standard omega-regular expressions, which has to be iterated infinitely often). We show that standard constructions between automata and regular expressions for finite words can smoothly be adapted to infinite words in this setting: We extend the Glushkov construction yielding a simple translation of infinity-regular expressions into parity automata, and we show how to translate parity automata into infinity-regular expressions by the classical state elimination technique, where in both cases the nesting of the * and the infinity operators corresponds to the priority range used in the parity automaton. We also briefly discuss the concept of deterministic expressions that directly transfers from standard regular expressions to infinity-regular expressions.
Cite as

Christof Löding and Andreas Tollkötter. Transformation Between Regular Expressions and omega-Automata. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 88:1-88:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.MFCS.2016.88,
  author =	{L\"{o}ding, Christof and Tollk\"{o}tter, Andreas},
  title =	{{Transformation Between Regular Expressions and omega-Automata}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{88:1--88:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.88},
  URN =		{urn:nbn:de:0030-drops-64962},
  doi =		{10.4230/LIPIcs.MFCS.2016.88},
  annote =	{Keywords: infinity regular expressions, parity automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.441
A Unified Approach to Boundedness Properties in MSO

Authors: Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
In the past years, extensions of monadic second-order logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.
Cite as

Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 441-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.CSL.2015.441,
  author =	{Kaiser, Lukasz and Lang, Martin and Le{\ss}enich, Simon and L\"{o}ding, Christof},
  title =	{{A Unified Approach to Boundedness Properties in MSO}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{441--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.441},
  URN =		{urn:nbn:de:0030-drops-54309},
  doi =		{10.4230/LIPIcs.CSL.2015.441},
  annote =	{Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.327
Decidability Results on the Existence of Lookahead Delegators for NFA

Authors: Christof Löding and Stefan Repke

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

Abstract
In this paper, we study lookahead delegators for nondeterministic finite automata (NFA), which are functions that deterministically choose transitions by additionally using a bounded lookahead on the input word. Of course, the delegator has to lead to an accepting state for each word that is accepted by the NFA. In the special case where no lookahead is allowed, a delegator coincides with a deterministic transition function that preserves the language. Typical decision problems are to decide whether a delegator with a given fixed lookahead exists, or whether a delegator with some bounded lookahead exists for a given NFA. In a paper of Ravikumar and Santean from 2007, the complexity and decidability of these questions have been tackled, mainly for the case of unambiguous NFA. In this paper, we revisit the subject and provide results for the case of general NFA. First, we correct a complexity result from the above paper by showing that the existence of delegators with fixed lookahead can be decided in time polynomial in the number of states. We use two player games on graphs as a tool to obtain the result. As second contribution, we show that the problem becomes PSPACE-complete if the bound on the lookahead is a part of the input. The third result provides a bound on the maximal required amount of lookahead. We use this to show that the (previously open) problem of deciding the existence of a bounded lookahead delegator is also PSPACE-complete.
Cite as

Christof Löding and Stefan Repke. Decidability Results on the Existence of Lookahead Delegators for NFA. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 327-338, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.FSTTCS.2013.327,
  author =	{L\"{o}ding, Christof and Repke, Stefan},
  title =	{{Decidability Results on the Existence of Lookahead Delegators for NFA}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{327--338},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.327},
  URN =		{urn:nbn:de:0030-drops-43838},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.327},
  annote =	{Keywords: Automata, Lookahead Delegators, Safety Games}
}
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.CSL.2011.264
Degrees of Lookahead in Context-free Infinite Games

Authors: Wladimir Fridman, Christof Löding, and Martin Zimmermann

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponent's moves. We show that the problem of determining the winner of such a game is undecidable for deterministic context-free winning conditions. Furthermore, we show that the necessary lookahead to win a deterministic context-free delay game cannot be bounded by any elementary function. Both results hold already for restricted classes of deterministic context-free winning conditions.
Cite as

Wladimir Fridman, Christof Löding, and Martin Zimmermann. Degrees of Lookahead in Context-free Infinite Games. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 264-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fridman_et_al:LIPIcs.CSL.2011.264,
  author =	{Fridman, Wladimir and L\"{o}ding, Christof and Zimmermann, Martin},
  title =	{{Degrees of Lookahead in Context-free Infinite Games}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{264--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.264},
  URN =		{urn:nbn:de:0030-drops-32365},
  doi =		{10.4230/LIPIcs.CSL.2011.264},
  annote =	{Keywords: infinite games, delay, context-free languages}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2328
On Nondeterministic Unranked Tree Automata with Sibling Constraints

Authors: Christof Löding and Karianto Wong

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

Abstract
We continue the study of bottom-up unranked tree automata with equality and disequality constraints between direct subtrees. In particular, we show that the emptiness problem for the nondeterministic automata is decidable. In addition, we show that the universality problem, in contrast, is undecidable.
Cite as

Christof Löding and Karianto Wong. On Nondeterministic Unranked Tree Automata with Sibling Constraints. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 311-322, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{loding_et_al:LIPIcs.FSTTCS.2009.2328,
  author =	{L\"{o}ding, Christof and Wong, Karianto},
  title =	{{On Nondeterministic Unranked Tree Automata with Sibling Constraints}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{311--322},
  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.2328},
  URN =		{urn:nbn:de:0030-drops-23281},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2328},
  annote =	{Keywords: Unranked tree automata, equality and disequality constraints, monadic second-order logic}
}
Document
DOI: 10.4230/DagSemProc.05061.3
Deterministic Automata on Unranked Trees

Authors: Wolfgang Thomas, Julien Christau, and Christof Löding

Published in: Dagstuhl Seminar Proceedings, Volume 5061, Foundations of Semistructured Data (2005)

Abstract
We investigate bottom-up and top-down deterministic automata on unranked trees. We show that for an appropriate definition of bottom-up deterministic automata it is possible to minimize the number of states efficiently and to obtain a unique canonical representative of the accepted tree language. For top-down deterministic automata it is well known that they are less expressive than the non-deterministic ones. By generalizing a corresponding proof from the theory of ranked tree automata we show that it is decidable whether a given regular language of unranked trees can be recognized by a top-down deterministic automaton. The standard deterministic top-down model is slightly weaker than the model we use, where at each node the automaton can scan the sequence of the labels of its successors before deciding its next move.
Cite as

Wolfgang Thomas, Julien Christau, and Christof Löding. Deterministic Automata on Unranked Trees. In Foundations of Semistructured Data. Dagstuhl Seminar Proceedings, Volume 5061, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{thomas_et_al:DagSemProc.05061.3,
  author =	{Thomas, Wolfgang and Christau, Julien and L\"{o}ding, Christof},
  title =	{{Deterministic Automata on Unranked Trees}},
  booktitle =	{Foundations of Semistructured Data},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5061},
  editor =	{Frank Neven and Thomas Schwentick and Dan Suciu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05061.3},
  URN =		{urn:nbn:de:0030-drops-2281},
  doi =		{10.4230/DagSemProc.05061.3},
  annote =	{Keywords: Automata, unranked trees, parikh automata}
}
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 Imprint Privacy Contact