- Arnaud Carayol (Marne-la-Vallée)
- Markus Holzer (Giessen)
- Ondřej Klíma (Brno)
- Christof Löding (Aachen)
- Sebastian Maneth (Edinburgh)
Arnaud Carayol (Marne-la-Vallée) and Matthew Hague (London)
Saturation algorithms for model-checking pushdown systems and their extensions
Pushdown systems have, over the past 15 years, been popular with the software verification community. Their stack can be used to model the call stack of a first-order recursive program. In this setting, a fundamental result due to Büchi in 1964 is that the set of stack contents reachable from the initial configuration form a regular set of words (and hence can be represented by a finite state automaton). All the efficient algorithm to compute this automaton are based on a form a saturation during which transitions are incrementally added.
In this talk, we will present the saturation method and show how it is at the center of most effective model-checking results for pushdown systems. We will also present how it has been adapted to deal with extension of the model of pushdown systems. In particular, we present recent results for higher-order pushdown systems which are a model of higher-order recursive programs.
Hermann Gruber (München) and Markus Holzer (Giessen)
From Finite Automata to Regular Expressions and Back—A Summary on Descriptional Complexity
The equivalence of finite automata and regular expressions dates back to the seminal paper of Kleene on events in nerve nets and finite automata from 1956. In the present paper we tour a fragment of the literature and summarize results on upper and lower bounds on the conversion of finite automata to regular expressions and vice versa. We also briefly recall the known bounds for the removal of spontaneous transitions (epsilon-transitions) on non-epsilon-free nondeterministic devices. Moreover, we report on recent results on the average case descriptional complexity bounds for the conversion of regular expressions to finite automata and brand new developments on the state elimination algorithm that converts finite automata to regular expressions.
Ondřej Klíma (Brno)
On Varieties of Automata Enriched with an Algebraic Structure
Eilenberg correspondence, based on the concept of syntactic monoids, relates varieties of regular languages with pseudovarieties of finite monoids. Various modifications of this correspondence relates more general classes of regular languages with classes of more complex algebraic objects. Such generalized varieties also have natural counterparts formed by classes of finite automata equipped with a certain additional algebraic structure. In this survey, we overview several variants of such varieties of enriched automata.
Christof Löding (Aachen)
Decision Problems for Deterministic Pushdown Automata on Infinite Words
For deterministic pushdown automata (DPDA) on finite words, the equivalence problem and the regularity problem are known to be decidable. The equivalence problem asks whether two given DPDAs are equivalent, and the regularity problem is to determine whether for a given DPDA there exists an equivalent finite automaton. For DPDAs on infinite words (omega-DPDA) these problems are still open. We present some recent partial results that show the decidability for a subclass of omega-DPDAs.
Furthermore, we consider the problem of simplifying the acceptance condition of a given omega-DPDA. A standard class of acceptance conditions are parity conditions. For the specification of such a 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.
Sebastian Maneth (Edinburgh)
Equivalence Problems for Tree Transducers: A Brief Survey
The decidability of equivalence for three important classes of tree transducers is discussed. Each class can be obtained as a natural restriction of deterministic macro tree transducers (MTTs):
(1) no context parameters, i.e., top-down tree transducers,
(2) linear size increase, i.e., MSO definable tree transducers, and
(3) monadic input and output ranked alphabets.
For the full class of MTTs, decidability of equivalence remains a long-standing open problem.