arXiv subjects

Christof Löding

Publications and source records attributed to Christof Löding.

28 records · Page 2Linked to original sources

arXiv2019

Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words

We consider decision problems for relations over finite and infinite words defined by finite automata. We prove that the equivalence problem for binary deterministic rational relations over infinite words is undecidable in contrast to the case of finite words, where the problem is decidable. Furthermore, we show that it is decidable in doubly exponential time for an automatic relation over infinite words whether it is a recognizable relation. We also revisit this problem in the context of finite words and improve the complexity of the decision procedure to single exponential time. The procedure is based on a polynomial time regularity test for deterministic visibly pushdown automata, which is a result of independent interest.

cs.FL↗

arXiv2018

On finitely ambiguous Büchi automata

Unambiguous Büchi automata, i.e. Büchi automata allowing only one accepting run per word, are a useful restriction of Büchi automata that is well-suited for probabilistic model-checking. In this paper we propose a more permissive variant, namely finitely ambiguous Büchi automata, a generalisation where each word has at most $k$ accepting runs, for some fixed $k$. We adapt existing notions and results concerning finite and bounded ambiguity of finite automata to the setting of $ω$-languages and present a translation from arbitrary nondeterministic Büchi automata with $n$ states to finitely ambiguous automata with at most $3^n$ states and at most $n$ accepting runs per word.

cs.FL↗

arXiv2018

Pure Strategies in Imperfect Information Stochastic Games

We consider imperfect information stochastic games where we require the players to use pure (i.e. non randomised) strategies. We consider reachability, safety, Büchi and co-Büchi objectives, and investigate the existence of almost-sure/positively winning strategies for the first player when the second player is perfectly informed or more informed than the first player. We obtain decidability results for positive reachability and almost-sure Büchi with optimal algorithms to decide existence of a pure winning strategy and to compute one if exists. We complete the picture by showing that positive safety is undecidable when restricting to pure strategies even if the second player is perfectly informed.

cs.FL↗

arXiv2017

Learning MSO-definable hypotheses on string

We study the classification problems over string data for hypotheses specified by formulas of monadic second-order logic MSO. The goal is to design learning algorithms that run in time polynomial in the size of the training set, independently of or at least sublinear in the size of the whole data set. We prove negative as well as positive results. If the data set is an unprocessed string to which our algorithms have local access, then learning in sublinear time is impossible even for hypotheses definable in a small fragment of first-order logic. If we allow for a linear time pre-processing of the string data to build an index data structure, then learning of MSO-definable hypotheses is possible in time polynomial in the size of the training set, independently of the size of the whole data set.

cs.LG↗

arXiv2016

Abstract Learning Frameworks for Synthesis

We develop abstract learning frameworks (ALFs) for synthesis that embody the principles of CEGIS (counter-example based inductive synthesis) strategies that have become widely applicable in recent years. Our framework defines a general abstract framework of iterative learning, based on a hypothesis space that captures the synthesized objects, a sample space that forms the space on which induction is performed, and a concept space that abstractly defines the semantics of the learning process. We show that a variety of synthesis algorithms in current literature can be embedded in this general framework. While studying these embeddings, we also generalize some of the synthesis problems these instances are of, resulting in new ways of looking at synthesis problems using learning. We also investigate convergence issues for the general framework, and exhibit three recipes for convergence in finite time. The first two recipes generalize current techniques for convergence used by existing synthesis engines. The third technique is a more involved technique of which we know of no existing instantiation, and we instantiate it to concrete synthesis problems.

cs.LO↗

arXiv2016

On Equivalence and Uniformisation Problems for Finite Transducers

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.

cs.FL↗

arXiv2014

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

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.

cs.FL↗

arXiv2014

Decision Problems for Deterministic Pushdown Automata on Infinite Words

The article surveys some decidability results for DPDAs on infinite words (omega-DPDA). We summarize some recent results on the decidability of the regularity and the equivalence problem for the class of weak omega-DPDAs. Furthermore, we present some new results on the parity index problem for omega-DPDAs. For the specification of a parity condition, the states of the omega-DPDA are assigned priorities (natural numbers), and a run is accepting if the highest priority that appears infinitely often during a run is even. The basic simplification question asks whether one can determine the minimal number of priorities that are needed to accept the language of a given omega-DPDA. We provide some decidability results on variations of this question for some classes of omega-DPDAs.

cs.FL↗

arXiv2013

Modeling and Verification of Infinite Systems with Resources

We consider formal verification of recursive programs with resource consumption. We introduce prefix replacement systems with non-negative integer counters which can be incremented and reset to zero as a formal model for such programs. In these systems, we investigate bounds on the resource consumption for reachability questions. Motivated by this question, we introduce relational structures with resources and a quantitative first-order logic over these structures. We define resource automatic structures as a subclass of these structures and provide an effective method to compute the semantics of the logic on this subclass. Subsequently, we use this framework to solve the bounded reachability problem for resource prefix replacement systems. We achieve this result by extending the well-known saturation method to annotated prefix replacement systems. Finally, we provide a connection to the study of the logic cost-WMSO.

cs.LO↗

arXiv2007

Transforming structures by set interpretations

We consider a new kind of interpretation over relational structures: finite sets interpretations. Those interpretations are defined by weak monadic second-order (WMSO) formulas with free set variables. They transform a given structure into a structure with a domain consisting of finite sets of elements of the orignal structure. The definition of these interpretations directly implies that they send structures with a decidable WMSO theory to structures with a decidable first-order theory. In this paper, we investigate the expressive power of such interpretations applied to infinite deterministic trees. The results can be used in the study of automatic and tree-automatic structures.

cs.LO↗