Author name cluster

Sarah Winter

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

GandALF Workshop 2023 Workshop Paper

Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games

Martin Fränzle
Sarah Winter
Martin Zimmermann

We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyze existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down.

PDF Details DOI

MFCS Conference 2021 Conference Paper

Decision Problems for Origin-Close Top-Down Tree Transducers

Sarah Winter

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.

Details

I&C Journal 2020 Journal Article

Finite-state strategies in delay games

Sarah Winter
Martin Zimmermann

What is a finite-state strategy in a delay game? We answer this surprisingly non-trivial question by presenting a very general framework that allows to remove delay: finite-state strategies exist for all winning conditions where the resulting delay-free game admits a finite-state strategy. The framework is applicable to games whose winning condition is recognized by an automaton with an acceptance condition that satisfies a certain aggregation property. Our framework also yields upper bounds on the complexity of determining the winner of such delay games and upper bounds on the necessary lookahead to win the game. In particular, we cover all previous results of that kind as special cases of our uniform approach.

Details DOI

Highlights Conference 2020 Conference Abstract

Synthesis from Weighted Specifications over Finite Words

Sarah Winter

A (Boolean) finite word specification S is a binary relation of finite words. The domain of S, which is all words u such that (u, v) belongs to S for some v, may be a strict subset of the set of all words. The (Boolean) synthesis problem on finite words, asks, given such a specification S, whether there exists a function f from the domain of S into words such that (i) for all words u in the domain of S, (u, f(u)) belongs to S, and (ii) f is computable by some finite-state machine (a transducer). In this paper, we consider three quantitative extensions of this synthesis problem, through weighted specifications S which maps pairs of words to a rational value or -infinity, in which requirement (i) of the Boolean synthesis problem is respectively replaced by the following conditions: — threshold synthesis — S(u, f(u))>=t for some rational threshold t, — best-value synthesis — S(u, f(u)) is the best-value which can be achieved knowing u, i. e. f picks the output that maximizes the value, and — approximate synthesis — S(u, f(u)) is r-close from the best-value, for a given rational threshold r. We establish a landscape of decidability results for these three extensions and (synchronous) weighted specifications given by deterministic weighted automata equipped with sum, discounted sum and average measures. Such specifications 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, which are tailored to handle specifications with partial domain. Our decidability results entail decidability of quantitative extensions of the Church synthesis problem over infinite words, for some classes of weighted safety specifications. Finally, we also address several decidable and undecidable extensions of our setting, when the specification is given by an unambiguous weighted automaton and when the relation between input and output words is automatic.

Details

I&C Journal 2017 Journal Article

Synthesis of deterministic top-down tree transducers from automatic tree relations

Christof Löding
Sarah Winter

We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of tree-automatic specifications, meaning the specification is recognizable by a top-down tree automaton that reads the two given trees synchronously in parallel. In this setting we study tree transducers that are allowed to have either delay that remains in a given bound or arbitrary delay. Delay is caused whenever the transducer reads a symbol from the input tree without producing output. For specifications that are deterministic top-down tree-automatic, we provide decision procedures for both bounded and arbitrary delay that yield deterministic top-down tree transducers which realize the specification for input trees that are part of the specification domain, and can behave arbitrarily on trees outside the domain. Similarly to the case of relations over words, we use two-player games as the main technique to obtain our results.

Details DOI

Highlights Conference 2016 Conference Abstract

On Equivalence and Uniformisation Problems for Finite Transducers

With Emmanuel Filiot
Christof Löding
Sarah Winter

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 talk, I investigate stronger variants of inclusion, equivalence and sequential uniformisation, based on a general notion of transducer resynchronisation, and show their decidability. I also investigate the classes of finite-valued rational transductions and deterministic rational transductions, which are known to have a decidable equivalence problem, and show that sequential uniformisation is also decidable for them.

Details

MFCS Conference 2016 Conference Paper

Uniformization Problems for Tree-Automatic Relations and Top-Down Tree Transducers

Christof Löding
Sarah Winter

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).

Details

GandALF Workshop 2014 Workshop Paper

Synthesis of Deterministic Top-down Tree Transducers from Automatic Tree Relations

Christof Löding
Sarah Winter

We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of specifications that are deterministic top-down tree automatic, meaning the specification is recognizable by a deterministic top-down tree automaton that reads the two given trees synchronously in parallel. In this setting we study tree transducers that are allowed to have either bounded delay or arbitrary delay. Delay is caused whenever the transducer reads a symbol from the input tree but does not produce output. We provide decision procedures for both bounded and arbitrary delay that yield deterministic top-down tree transducers which realize the specification for valid input trees. Similar to the case of relations over words, we use two-player games to obtain our results.

PDF Details DOI