Search Results

Documents authored by Winter, Sarah

Document
DOI: 10.4230/DagRep.13.5.96
Regular Transformations (Dagstuhl Seminar 23202)

Authors: Rajeev Alur, Mikołaj Bojańczyk, Emmanuel Filiot, Anca Muscholl, and Sarah Winter

Published in: Dagstuhl Reports, Volume 13, Issue 5 (2023)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 23202 "Regular Transformations". The goal of this seminar was to advance on a list of topics about transducers that have gathered much interest recently, and to explore new connections between the theory of regular transformations and its applications in linguistics.
Cite as

Rajeev Alur, Mikołaj Bojańczyk, Emmanuel Filiot, Anca Muscholl, and Sarah Winter. Regular Transformations (Dagstuhl Seminar 23202). In Dagstuhl Reports, Volume 13, Issue 5, pp. 96-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{alur_et_al:DagRep.13.5.96,
  author =	{Alur, Rajeev and Boja\'{n}czyk, Miko{\l}aj and Filiot, Emmanuel and Muscholl, Anca and Winter, Sarah},
  title =	{{Regular Transformations (Dagstuhl Seminar 23202)}},
  pages =	{96--113},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{13},
  number =	{5},
  editor =	{Alur, Rajeev and Boja\'{n}czyk, Miko{\l}aj and Filiot, Emmanuel and Muscholl, Anca and Winter, Sarah},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.5.96},
  URN =		{urn:nbn:de:0030-drops-193663},
  doi =		{10.4230/DagRep.13.5.96},
  annote =	{Keywords: transducers; (poly-)regular functions; linguistic transformations}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.121
Deterministic Regular Functions of Infinite Words

Authors: Olivier Carton, Gaëtan Douéneau-Tabot, Emmanuel Filiot, and Sarah Winter

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
Regular functions of infinite words are (partial) functions realized by deterministic two-way transducers with infinite look-ahead. Equivalently, Alur et. al. have shown that they correspond to functions realized by deterministic Muller streaming string transducers, and to functions defined by MSO-transductions. Regular functions are however not computable in general (for a classical extension of Turing computability to infinite inputs), and we consider in this paper the class of deterministic regular functions of infinite words, realized by deterministic two-way transducers without look-ahead. We prove that it is a well-behaved class of functions: they are computable, closed under composition, characterized by the guarded fragment of MSO-transductions, by deterministic Büchi streaming string transducers, by deterministic two-way transducers with finite look-ahead, and by finite compositions of sequential functions and one fixed basic function called map-copy-reverse.
Cite as

Olivier Carton, Gaëtan Douéneau-Tabot, Emmanuel Filiot, and Sarah Winter. Deterministic Regular Functions of Infinite Words. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 121:1-121:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{carton_et_al:LIPIcs.ICALP.2023.121,
  author =	{Carton, Olivier and Dou\'{e}neau-Tabot, Ga\"{e}tan and Filiot, Emmanuel and Winter, Sarah},
  title =	{{Deterministic Regular Functions of Infinite Words}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{121:1--121:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.121},
  URN =		{urn:nbn:de:0030-drops-181733},
  doi =		{10.4230/LIPIcs.ICALP.2023.121},
  annote =	{Keywords: infinite words, streaming string transducers, two-way transducers, monadic second-order logic, look-aheads, factorization forests}
}
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
DOI: 10.4230/LIPIcs.FSTTCS.2021.43
Synthesizing Computable Functions from Rational Specifications over Infinite Words

Authors: Emmanuel Filiot and Sarah Winter

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined by non-deterministic parity transducers. We prove that the synthesis problem of computable functions from rational specifications is undecidable. We provide an incomplete but sound reduction to some parity game, such that if Eve wins the game, then the rational specification is realizable by a computable function. We prove that this function is even computable by a deterministic two-way transducer. We provide a sufficient condition under which the latter game reduction is complete. This entails the decidability of the synthesis problem of computable functions, which we proved to be ExpTime-complete, for a large subclass of rational specifications, namely deterministic rational specifications. This subclass contains the class of automatic relations over infinite words, a yardstick in reactive synthesis.
Cite as

Emmanuel Filiot and Sarah Winter. Synthesizing Computable Functions from Rational Specifications over Infinite Words. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 43:1-43:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2021.43,
  author =	{Filiot, Emmanuel and Winter, Sarah},
  title =	{{Synthesizing Computable Functions from Rational Specifications over Infinite Words}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{43:1--43:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.43},
  URN =		{urn:nbn:de:0030-drops-155541},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.43},
  annote =	{Keywords: uniformization, synthesis, transducers, continuity, computability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.90
Decision Problems for Origin-Close Top-Down Tree Transducers

Authors: Sarah Winter

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

Abstract
Tree transductions are binary relations of finite trees. For tree transductions defined by non-deterministic top-down tree transducers, inclusion, equivalence and synthesis problems are known to be undecidable. Adding origin semantics to tree transductions, i.e., tagging each output node with the input node it originates from, is a known way to recover decidability for inclusion and equivalence. The origin semantics is rather rigid, in this work, we introduce a similarity measure for transducers with origin semantics and show that we can decide inclusion, equivalence and synthesis problems for origin-close non-deterministic top-down tree transducers.
Cite as

Sarah Winter. Decision Problems for Origin-Close Top-Down Tree Transducers. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 90:1-90:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{winter:LIPIcs.MFCS.2021.90,
  author =	{Winter, Sarah},
  title =	{{Decision Problems for Origin-Close Top-Down Tree Transducers}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{90:1--90:16},
  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.90},
  URN =		{urn:nbn:de:0030-drops-145308},
  doi =		{10.4230/LIPIcs.MFCS.2021.90},
  annote =	{Keywords: tree tranducers, equivalence, uniformization, synthesis, origin semantics}
}
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.ICALP.2018.142
Uniformization Problems for Synchronizations of Automatic Relations on Words

Authors: Sarah Winter

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
A uniformization of a binary relation is a function that is contained in the relation and has the same domain as the relation. The synthesis problem asks for effective uniformization for classes of relations and functions that can be implemented in a specific way. We consider the synthesis problem for automatic relations over finite words (also called regular or synchronized rational relations) by functions implemented by specific classes of sequential transducers. It is known that the problem "Given an automatic relation, does it have a uniformization by a subsequential transducer?" is decidable in the two variants where the uniformization can either be implemented by an arbitrary subsequential transducer or it has to be implemented by a synchronous transducer. We introduce a new variant of this problem in which the allowed input/output behavior of the subsequential transducer is specified by a set of synchronizations and prove decidability for a specific class of synchronizations.
Cite as

Sarah Winter. Uniformization Problems for Synchronizations of Automatic Relations on Words. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 142:1-142:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{winter:LIPIcs.ICALP.2018.142,
  author =	{Winter, Sarah},
  title =	{{Uniformization Problems for Synchronizations of Automatic Relations on Words}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{142:1--142:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.142},
  URN =		{urn:nbn:de:0030-drops-91463},
  doi =		{10.4230/LIPIcs.ICALP.2018.142},
  annote =	{Keywords: automatic relation, uniformization, synchronization, transducer}
}
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}
}
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