Christof Löding

Highlights Conference 2025 Conference Abstract

From finite to infinite words: congruences and learning for finite automata

• Christof Löding

MFCS Conference 2021 Conference Paper

Constructing Deterministic ω-Automata from Examples by an Extension of the RPNI Algorithm

• León Bohn
• Christof Löding

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.

CSL Conference 2020 Conference Paper

State Space Reduction For Parity Automata

• Christof Löding
• Andreas Tollkötter

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.

MFCS Conference 2019 Conference Paper

New Pumping Technique for 2-Dimensional VASS

• Wojciech Czerwinski
• Slawomir Lasota 0001
• Christof Löding
• Radoslaw Piórkowski

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.

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.

MFCS Conference 2016 Conference Paper

Transformation Between Regular Expressions and omega-Automata

• Christof Löding
• Andreas Tollkötter

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.

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

CSL Conference 2015 Conference Paper

A Unified Approach to Boundedness Properties in MSO

• Lukasz Kaiser
• Martin Lang 0001
• Simon Leßenich
• Christof Löding

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.

Highlights Conference 2014 Conference Abstract

Invited talk: Synthesis of Transducers from Automatic Specifications

• Christof Löding

Given a specification as a binary relation that relates inputs to admissible outputs, the synthesis problem asks for a program that produces for each input an output that is admissible according to the specification. We consider this problem over the domain of words and trees. The specifications are given by automatic relations, that is, relations that can be defined by finite automata that read pairs of structures and accept those pairs that are in the relation. For such specifications, we study the synthesis problem of deterministic finite state transducers. In particular, we present some recent results and ongoing work on the synthesis of tree transducers. 10: 00 10: 30 Breakfast & coffee

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.

CSL Conference 2013 Conference Paper

Deciding the weak definability of Büchi definable tree languages

• Thomas Colcombet
• Denis Kuperberg
• Christof Löding
• Michael Vanden Boom

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.

GandALF Workshop 2013 Invited Paper

Games with delay for automaton synthesis

• Christof Löding

Abstract The framework of infinite two-player games is a powerful and flexible tool to verify and synthesize systems from given specifications. The origin of this work is the problem of automatic circuit synthesis from specifications, as posed in [3]. A circuit can be viewed as a device that transforms input sequences of bit vectors into output sequences of bit vectors. If the circuit acts as a kind of control device, then these sequences are assumed to be infinite because the computation should never halt. The task in synthesis is to construct such a circuit based on a formal specification describing the desired input/output behaviour. This problem setting can be viewed as a game of infinite duration between two players: The first player provides the bit vectors for the input, and the second player produces the output bit vectors. The winning condition of the game is given by the specification. The goal is to find a strategy for the second player, such that all pairs of input/output sequences that can be produced according to the strategy, satisfy the specification. Such a strategy can be seen as a realisation of the specification. This approach using games as a model for the synthesis problem has been taken in [1], where it is shown that the synthesis problem can be solved by an algorithm for specifications that are written in monadic second-order logic. Furthermore, for a given specification, one can construct a strategy represented by a finite transducer that reads the input sequence and synchronously produces an output sequence such that the resulting pair of input/output sequence satisfies the specification. An interesting variation of the problem arises when the constructed strategy can use a lookahead: it does not need to produce an output in each step. In the corresponding game this means that the second player, who is in charge of the output, can delay some of his moves. An early decidability result in such a setting has been obtained in [6], where the strategy is allowed to skip a bounded number of moves in order to obtain a bounded look-ahead. The aim of this presentation is to survey some recent results that have been obtained for games with delay, as for example, games with arbitrary (not necessarily bounded) delay [5], delay games with deterministic pushdown specifications [4], and delay games over finite words for the synthesis of sequential transducers [2]. References J. Richard Büchi & Lawrence H. Landweber (1969): Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138, pp. 295–311, doi: 10. 2307/1994916. Arnaud Carayol & Christof Löding: Uniformization in Automata Theory. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science Nancy, July 19-26, 2011. Alonzo Church (1962): Logic, Arithmetic and Automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35. Wladimir Fridman, Christof Löding & Martin Zimmermann (2011): Degrees of Lookahead in Context-free Infinite Games. In: Marc Bezem: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs) 12. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 264–276, doi: 10. 4230/LIPIcs. CSL. 2011. 264. Michael Holtmann, Łukasz Kaiser & Wolfgang Thomas (2010): Degrees of Lookahead in Regular Infinite Games. In: Foundations of Software Science and Computational Structures, Lecture Notes in Computer Science 6014. Springer, pp. 252–266, doi: 10. 1007/978-3-642-12032-9_18. Frederick A. Hosch & Lawrence H. Landweber (1972): Finite Delay Solutions for Sequential Conditions. In: ICALP, pp. 45–60.

Highlights Conference 2013 Conference Abstract

Resource reachability games on pushdown graphs

• Martin Lang
• Christof Löding

We consider two-player games on the configuration graph of pushdown systems with an additional finite set of non-negative integer counters. These counters can be incremented, reset to zero or left unchanged by the transition rules of the pushdown system. We associate the cost of a play with the highest counter value that occurs and look at a combined reachability and cost-limit winning condition. Is there a uniform cost-bound k such that one can win from a set of configurations A with this bound? We provide a solution to this question by an extension of the well-known saturation principle.

MFCS Conference 2012 Conference Paper

Regularity Problems for Weak Pushdown ω-Automata and Games

• Christof Löding
• Stefan Repke

Abstract We show that the regularity and equivalence problems are decidable for deterministic weak pushdown ω -automata, giving a partial answer to a question raised by Cohen and Gold in 1978. We prove the decidability by a reduction to the corresponding problems for deterministic pushdown automata on finite words. Furthermore, we consider the problem of deciding for pushdown games whether a winning strategy exists that can be implemented by a finite automaton. We show that this problem is already undecidable for games defined by one-counter automata or visibly pushdown automata with a safety condition.

CSL Conference 2011 Conference Paper

Degrees of Lookahead in Context-free Infinite Games

• Wladimir Fridman
• Christof Löding
• Martin Zimmermann 0002

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.

CSL Conference 2008 Conference Paper

The Nesting-Depth of Disjunctive µ-Calculus for Tree Languages and the Limitedness Problem

• Thomas Colcombet
• Christof Löding

Abstract In this paper we lift the result of Hashiguchi of decidability of the restricted star-height problem for words to the level of finite trees. Formally, we show that it is decidable, given a regular tree language L and a natural number k whether L can be described by a disjunctive μ -calculus formula with at most k nesting of fixpoints. We show the same result for disjunctive μ -formulas allowing substitution. The latter result is equivalent to deciding if the language is definable by a regular expression with nesting depth at most k of Kleene-stars. The proof, following the approach of Kirsten in the word case, goes by reduction to the decidability of the limitedness problem for non-deterministic nested distance desert automata over trees. We solve this problem in the more general framework of alternating tree automata.

CSL Conference 2007 Conference Paper

MSO on the Infinite Binary Tree: Choice and Order

• Arnaud Carayol
• Christof Löding

Abstract We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.

MFCS Conference 2007 Conference Paper

Transition Graphs of Rewriting Systems over Unranked Trees

• Christof Löding
• Alex Spelten

Abstract We investigate algorithmic properties of infinite transition graphs that are generated by rewriting systems over unranked trees. Two kinds of such rewriting systems are studied. For the first, we construct a reduction to ranked trees via an encoding and to standard ground tree rewriting, thus showing that the generated classes of transition graphs coincide. In the second rewriting formalism, we use subtree rewriting combined with a new operation called flat prefix rewriting and show that strictly more transition graphs are obtained while the first-order theory with reachability relation remains decidable.

MFCS Conference 2003 Conference Paper

Solving the Sabotage Game Is PSPACE-Hard

• Christof Löding
• Philipp Rohde

Abstract We consider the sabotage game as presented by van Benthem. In this game one player moves along the edges of a finite multi-graph and the other player takes out a link after each step. One can consider usual algorithmic tasks like reachability, Hamilton path, or complete search as winning conditions for this game. As the game definitely ends after at most the number of edges steps, it is easy to see that solving the sabotage game for the mentioned tasks takes at most PSPACE in the size of the graph. In this paper we establish the PSPACE-hardness of this problem. Furthermore, we introduce a modal logic over changing models to express tasks corresponding to the sabotage games and we show that model checking this logic is PSPACE-complete.