Author

Christof Loding

63 papers · 1999–2026

1999peak 8 in 20132026

Frequent co-authors

Papers

showing 1–25 of 63 RSS

Transforming structures by set interpretations

Thomas Colcombet, Christof Löding

cs.LO · March 2007 · cited 90× · arXiv ↗ · more like this ·

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.

Learning Universally Quantified Invariants of Linear Data Structures

Pranav Garg, Christof Loding, P. Madhusudan +1 more

cs.PL · 9 Feb 2013 · cited 42× · arXiv ↗ · more like this ·

We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and prove that every QDA has a unique minimally-over-approximating elastic QDA. We then give an application of these theoretically sound and efficient active learning algorithms in a passive learning framework and show that we can efficiently learn quantified linear data structure invariants from samples obtained from dynamic runs for a large class of programs.

Regular Cost Functions over Finite Trees

Thomas Colcombet, Christof Löding

Computational Theory and Mathematics · RWTH Publications (RWTH Aachen) · July 2010 · cited 37× · DOI ↗ · more like this ·

We develop the theory of regular cost functions over finite trees: aquantitative extension to the notion of regular languages of trees: Cost functions map each input (tree) to a value in~$\omega+1$, and are considered modulo an equivalence relation which forgets about specific values, but preserves boundedness of functions on all subsets of the domain. We introduce nondeterministic and alternating finite tree cost automata for describing cost functions. We show that all these forms of automata are effectively equivalent. We also provide decision procedures for them. Finally, following B\"uchi's seminal idea, we use cost automata for providing decision procedures for cost monadic logic, a quantitative extension of monadic second order logic.

Synthesis of Open Reactive Systems from Scenario-Based Specifications

Yves Bontemps, Pierre‐Yves Schobbens, Christof Löding

Computational Theory and Mathematics · Repository of the University of Namur · February 2004 · cited 29× · OpenAlex ↗ · more like this ·

We propose here Live Sequence Charts with a new, game-based semantics to model inter-actions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected,or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We givea polynomial time algorithm for synthesizing merciful winning strategies.

INFINITE GRAPHS GENERATED BY TREE REWRITING

Christof Löding, Wolfgang Thomas, Erich Grädel

Computational Theory and Mathematics · RWTH Publications (RWTH Aachen) · 2002 · cited 29× · OpenAlex ↗ · more like this ·

Finite graphs and algorithms on finite graphs are an important tool for the verification of finite-state systems. To transfer the methods for finite systems, at least partially, to infinite systems a theory of infinite graphs with finite representations is needed. In this thesis the class of the transition graphs of ground tree rewriting systems is studied. To investigate the structure of ground tree rewriting graphs they are analyzed under the aspect of tree-width of graphs and are compared to already well-studied classes of graphs, as the class of pushdown graphs and the class of automatic graphs. Furthermore, the trace languages that are definable by ground tree rewriting graphs are investigated. The algorithmic properties of ground tree rewriting graphs are studied by means of reachability problems that correspond to the semantics of basic temporal operators. The decidability…

Logical theories and compatible operations

Achim Blumensath, Thomas Colcombet, Christof Löding

Artificial Intelligence · RWTH Publications (RWTH Aachen) · 2007 · cited 26× · OpenAlex ↗ · more like this ·

We survey operations on (possibly infinite) relational structures that are compatible with logical theories in the sense that, if we apply the operation to given structures then we can compute the theory of the resulting structure from the theories of the arguments (the logics under consideration for the result and the arguments might differ). Besides general compatibility results for these operations we also present several results on restricted classes of structures, and their use for obtaining classes of infinite structures with decidable theories.

Foundations for natural proofs and quantifier instantiation

Christof Löding, P. Madhusudan, Lucas Peña

Artificial Intelligence · Proceedings of the ACM on Programming Languages · 27 Dec 2017 · cited 23× · DOI ↗ · more like this ·

We give foundational results that explain the efficacy of heuristics used for dealing with quantified formulas and recursive definitions. We develop a framework for first order logic (FOL) over an uninterpreted combination of background theories. Our central technical result is that systematic term instantiation is complete for a fragment of FOL that we call safe . Coupled with the fact that unfolding recursive definitions is essentially term instantiation and with the observation that heap verification engines generate verification conditions in the safe fragment explains the efficacy of verification engines like natural proofs that resort to such heuristics. Furthermore, we study recursive definitions with least fixpoint semantics and show that though they are not amenable to complete procedures, we can systematically introduce induction principles that in practice bridge the divide…

Choice functions and well-orderings over the infinite binary tree

Arnaud Carayol, Christof Löding, Damian Niwiński +1 more

Computational Theory and Mathematics · Open Mathematics · 2010 · cited 21× · DOI ↗ · more like this ·

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 show how the result can be used to prove the inherent ambiguity of languages of infinite trees. 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.

Degrees of Lookahead in Context-free Infinite Games

Wladimir Fridman, Christof Löding, Martín Zimmermann

Computational Theory and Mathematics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2011 · cited 16× · DOI ↗ · more like this ·

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.

Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints

Adithya Murali, Lucas Peña, Eion Blanchard +2 more

cs.LO · September 2020 · cited 15× · arXiv ↗ · more like this ·

Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.

Applications of automata learning in verification and synthesis

Daniel Neider, Wolfgang Thomas, Christof Löding +1 more

Artificial Intelligence · RWTH Publications (RWTH Aachen) · 2014 · cited 13× · OpenAlex ↗ · more like this ·

The objective of this thesis is to explore automata learning, which is an umbrella term for techniques that derive finite automata from external information sources, in the areas of verification and synthesis. We consider four application scenarios that turn out to be particularly well-suited: Regular Model Checking, quantified invariants of linear data structures, automatic reachability games, and labeled safety games. The former two scenarios stem from the area of verification whereas the latter two stem from the area of synthesis (more precisely, from the area of infinite-duration two-player games over graphs, as popularized by McNaughton). Regular Model Checking is a special kind of Model Checking in which the program to verify is modeled in terms of finite automata. We develop various (semi-)algorithms for computing invariants in Regular Model Checking: a white-box algorithm, which…

A characterization of first-order topological properties of planar spatial data

Michael Benedikt, Bart Kuijpers, Christof Löding +2 more

Signal Processing · Journal of the ACM · March 2006 · cited 9× · DOI ↗ · more like this ·

Planar spatial datasets can be modeled by closed semi-algebraic sets in the plane. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only point that can only talk about points in the set and the “cones” around these points.

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

Christof Löding, Sarah Winter

cs.FL · 26 Aug 2014 · cited 8× · arXiv ↗ · more like this ·

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.

On Nondeterministic Unranked Tree Automata with Sibling Constraints

Christof Löding, Wong Karianto

Computational Theory and Mathematics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2009 · cited 8× · DOI ↗ · more like this ·

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.

ICE: A Robust Learning Framework for Synthesizing Invariants

Pranav Garg, Christof Löding, P. Madhusudan +1 more

Information Systems · October 2013 · cited 7× · OpenAlex ↗ · more like this ·

Invariant generation lies at the heart of automated program verification, and the learning paradigm for synthesizing invariants is a new promising approach to solve this important problem. Unlike white-box techniques that try to generate an invariant by analyzing the program, learning approaches try to synthesize the invariant given concrete configurations that the invariant must include and exclude, and are algorithmically based on learning theory and scalable machine learning algorithms. In this paper we argue that traditional learning paradigms that use concrete examples and counterexamples are inherently non-robust for synthesizing invariants. We introduce a more general learning paradigm, called ICE-learning, that learns using examples, counter-examples, and implications, and show that this paradigm allows building honest teachers and convergent mechanisms for invariant synthesis.…

Decidability Results on the Existence of Lookahead Delegators for NFA

Christof Löding, Stefan Repke

Computational Theory and Mathematics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2013 · cited 7× · DOI ↗ · more like this ·

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…

A First-Order Logic with Frames

Adithya Murali, Lucas Peña, Christof Löding +1 more

cs.LO · January 2019 · cited 6× · arXiv ↗ · more like this ·

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.

Modeling and Verification of Infinite Systems with Resources

Martin Lang, Christof Löding

cs.LO · November 2013 · cited 6× · arXiv ↗ · more like this ·

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…

Deciding the weak definability of Büchi definable tree languages

Thomas Colcombet, Denis Kuperberg, Christof Löding +1 more

Computational Theory and Mathematics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2013 · cited 6× · DOI ↗ · more like this ·

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.

Infinite Games and Automata Theory

Christof Löding

Artificial Intelligence · Cambridge University Press eBooks · 6 Jan 2011 · cited 6× · DOI ↗ · more like this ·

This chapter gives an introduction to the connection between automata theory and the theory of two player games of infinite duration. We illustrate how the theory of automata on infinite words can be used to solve games with complex winning conditions, for example specified by logical formulae. Conversely, infinite games are a useful tool to solve problems for automata on infinite trees such as complementation and the emptiness test.

A Unified Approach to Boundedness Properties in MSO

Łukasz Kaiser, Martin Lang, Simon Robert Leßenich +1 more

Computational Theory and Mathematics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015 · cited 5× · DOI ↗ · more like this ·

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…

Obliging games

Krishnendu Chatterjee, Florian Horn, Christof Löding

Computational Theory and Mathematics · 31 Aug 2010 · cited 5× · OpenAlex ↗ · more like this ·

Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. The specification for the system is usually given as an ω-regular language L over paths and Eve's goal is to ensure that the play belongs to L irrespective of Adam's behaviour. The classical notion of winning strategies fails to capture several interesting scenarios. For example, strong fairness (Streett) conditions are specified by a number of request-grant pairs and require every pair that is requested infinitely often to be granted infinitely often: Eve might win just by preventing Adam from making any new request, but a better strategy would allow Adam to make as many requests as possible and still ensure fairness. To address such…

Constructing Deterministic Parity Automata from Positive and Negative Examples

León Bohn, Christof Löding

cs.FL · February 2023 · cited 4× · arXiv ↗ · more like this ·

We present a polynomial time algorithm that constructs a deterministic parity automaton (DPA) from a given set of positive and negative ultimately periodic example words. We show that this algorithm is complete for the class of $ω$-regular languages, that is, it can learn a DPA for each regular $ω$-language. For use in the algorithm, we give a definition of a DPA, that we call the precise DPA of a language, and show that it can be constructed from the syntactic family of right congruences for that language (introduced by Maler and Staiger in 1997). Depending on the structure of the language, the precise DPA can be of exponential size compared to a minimal DPA, but it can also be a minimal DPA. The upper bound that we obtain on the number of examples required for our algorithm to find a DPA for $L$ is therefore exponential in the size of a minimal DPA, in general. However we identify two…

New Pumping Technique for 2-dimensional VASS

Wojciech Czerwiński, Sławomir Lasota, Christof Löding +1 more

cs.FL · 25 Jun 2019 · cited 3× · arXiv ↗ · more like this ·

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.

Transformation Between Regular Expressions and omega-Automata

Christof Löding, Andreas Tollkötter

Computational Theory and Mathematics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2016 · cited 3× · DOI ↗ · more like this ·

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…