Georg Zetzsche
 Mail address IRIF - Case 7014 Université Paris-Diderot 75205 Paris Cedex 13 France Email zetzsche(at)irif(dot)fr Office address Office 4032, 4th floor Bâtiment Sophie Germain 8 place Aurélie Nemours 75013 Paris

Since November 2017, I am a Postdoc at IRIF, Université Paris-Diderot, funded by a fellowship of the Fondation Sciences Mathématiques de Paris and hosted by Olivier Serre.

From November 2015 till October 2017, I was a Postdoc at the LSV Cachan, funded by a fellowship of the DAAD (German Academic Exchange Service), hosted by Philippe Schnoebelen, and the project VERICONISS by Stefan Göller.

Before that, I obtained a PhD with Prof. Dr. Roland Meyer in the Concurrency Theory Group in Kaiserslautern. I defended my dissertation on June 19th, 2015. Until December 2010, I studied Computer Science (with a minor in Mathematics) at Universität Hamburg.

My research is concerned with theoretical foundations of verification and synthesis of software systems. More specifically, I am interested in decidability and complexity issues of infinite-state systems. One current focus is synthesis of finite-state abstractions of infinite-state systems (separability problems, downward closures, Parikh images), which can be used as correctness certificates or as building blocks for decision procedures.

In addition, I am working on decision problems for infinite groups, where I seek to apply methods from verification and gain insights on how to devise infinite-state models with pleasant analysis properties.

News:

• I will be on the program committee of CiE 2019.
Awards: Events I attended/will attend:
Publications
Accepted

Bounded Context Switching for Valence Systems
with Roland Meyer and Sebastian Muskalla
Accepted for CONCUR 2018
Abstract
We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of context switches is in $\NPTIME$, independent of the memory (the graph monoid). Our proof is genuinely algebraic, and therefore contributes a new way to think about BCS.

Unboundedness problems for languages of vector addition systems
with Wojciech Czerwiński and Piotr Hofman
Accepted for ICALP 2018
Abstract
A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these \emph{unboundedness properties}. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i)~separability by bounded regular languages, (ii)~unboundedness of occurring factors from a language $K$ with mild conditions on $K$, and (iii)~universality of the set of factors.

PTL-separability and closures for WQOs on words
Accepted for LICS 2018
Abstract
We introduce a flexible class of well-quasi-orderings (WQOs) on words that generalizes the ordering of (not necessarily contiguous) subwords. Each such WQO induces a class of piecewise testable languages (PTLs) as Boolean combinations of upward closed sets. In this way, a range of regular language classes arises as PTLs. Moreover, each of the WQOs guarantees regularity of all downward closed sets.
We consider two problems. First, we study which (perhaps non-regular) language classes permit a decision procedure to decide whether two given languages are separable by a PTL with respect to a given WQO. Second, we want to effectively compute downward closures with respect to these WQOs.
Our first main result that for each of the WQOs, under mild assumptions, both problems reduce to the simultaneous unboundedness problem (SUP) and are thus solvable for many powerful system classes. In the second main result, we apply the framework to show decidability of separability of regular languages by $\mathcal{B}\Sigma_1[<, \mathsf{mod}]$, a fragment of first-order logic with modular predicates.

The Emptiness Problem for Valence Automata over Graph Monoids
Accepted for Information and Computation
Special Issue on RP 2015
Abstract
This work studies which storage mechanisms in automata permit decidability of the emptiness problem. The question is formalized using valence automata, an abstract model of automata in which the storage mechanism is given by a monoid. For each of a variety of storage mechanisms, one can choose a (typically infinite) monoid $M$ such that valence automata over $M$ are equivalent to (one-way) automata with this type of storage. In fact, many important storage mechanisms can be realized by monoids defined by finite graphs, called graph monoids. Examples include pushdown stacks, partially blind counters (which behave like Petri net places), blind counters (which may attain negative values), and combinations thereof.
Hence, we study for which graph monoids the emptiness problem for valence automata is decidable. A particular model realized by graph monoids is that of Petri nets with a pushdown stack. For these, decidability is a long-standing open question and we do not answer it here.
However, if one excludes subgraphs corresponding to this model, a characterization can be achieved. Moreover, we provide a description of those storage mechanisms for which decidability remains open. This leads to a model that naturally generalizes both pushdown Petri nets and the priority multicounter machines introduced by Reinhardt.
The cases that are proven decidable constitute a natural and apparently new extension of Petri nets with decidable reachability. It is finally shown that this model can be combined with another such extension by Atig and Ganty: We present a further decidability result that subsumes both of these Petri net extensions.

Conference contributions

Knapsack problems for wreath products
with Moses Ganardi, Daniel König, and Markus Lohrey
Proceedings of STACS 2018
Abstract
In recent years, knapsack problems for (in general non-commutative) groups have attracted attention. In this paper, the knapsack problem for wreath products is studied. It turns out that decidability of knapsack is not preserved under wreath product. On the other hand, the class of knapsack-semilinear groups, where solutions sets of knapsack equations are effectively semilinear, is closed under wreath product. As a consequence, we obtain the decidability of knapsack for free solvable groups. Finally, it is shown that for every non-trivial abelian group $G$, knapsack (as well as the related subset sum problem) for the wreath product $G \wr \Z$ is $\NP$-complete.

Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
with Simon Halfon and Philippe Schnoebelen
Proceedings of LICS 2017
Abstract
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $\Sigma_1$ theory is undecidable (already over two letters).
We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $\Sigma_1$ fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the $\Sigma_2$ fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable.

The Complexity of Knapsack in Graph Groups
with Markus Lohrey
Proceedings of STACS 2017
Abstract
Myasnikov et al. have introduced the knapsack problem for arbitrary finitely generated groups. In previous work, the authors proved that for each graph group, the knapsack problem can be solved in NP. Here, we determine the exact complexity of the problem for every graph group. While the problem is TC0-complete for complete graphs, it is LogCFL-complete for each (non-complete) transitive forest. For every remaining graph, the problem is NP-complete.

The Complexity of Downward Closure Comparisons
Proceedings of ICALP 2016
Abstract
The downward closure of a language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of every language is regular. Moreover, recent results show that downward closures are computable for quite powerful system models.
One advantage of abstracting a language by its downward closure is that then, equivalence and inclusion become decidable. In this work, we study the complexity of these two problems. More precisely, we consider the following decision problems: Given languages $K$ and $L$ from classes $\C$ and $\D$, respectively, does the downward closure of $K$ include (equal) that of $L$?
These problems are investigated for finite automata, one-counter automata, context-free grammars, and reversal-bounded counter automata. For each combination, we prove a completeness result either for fixed or for arbitrary alphabets. Moreover, for Petri net languages, we show that both problems are Ackermann-hard and for higher-order pushdown automata of order $k$, we prove hardness for complements of nondeterministic $k$-fold exponential time.

The complexity of regular abstractions of one-counter languages
with Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K Narayan Kumar, and Prakash Saivasan
Proceedings of LICS 2016
Abstract
We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language of A: its (1) downward closure, (2) upward closure, or (3) Parikh image. For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial time algorithm and prove a completeness result: we construct a sequence of OCA that admits a polynomial-time algorithm iff there is one for all OCA. For all three abstractions, it was previously unknown if appropriate NFA of sub-exponential size exist.

First-order logic with reachability for infinite-state systems
with Emanuele D'Osualdo and Roland Meyer
Proceedings of LICS 2016
Abstract
First-order logic with the reachability predicate (FOR) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable). This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a complete characterization of those graph monoids where FOR is decidable for the resulting transition systems.

Knapsack in Graph Groups, HNN-Extensions and Amalgamated Products
with Markus Lohrey
Proceedings of STACS 2016
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al. for arbitrary finitely generated groups, can be solved in NP for graph groups. This result even holds if the group elements are represented in a compressed form by SLPs, which generalizes the classical NP-completeness result of the integer knapsack problem. We also prove general transfer results: NP-membership of the knapsack problem is passed on to finite extensions, HNN-extensions over finite associated subgroups, and amalgamated products with finite identified subgroups.

The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets
Proceedings of RP 2015
Abstract
This work studies which storage mechanisms in automata permit decidability of the reachability problem. The question is formalized using valence automata, an abstract model that generalizes automata with storage. For each of a variety of storage mechanisms, one can choose a (typically infinite) monoid $M$ such that valence automata over $M$ are equivalent to (one-way) automata with this type of storage.
In fact, many interesting storage mechanisms can be realized by monoids defined by finite graphs, called graph monoids. Hence, we study for which graph monoids the emptiness problem for valence automata is decidable. A particular model realized by graph monoids is that of Petri nets with a pushdown stack. For these, decidability is a long-standing open question and we do not answer it here.
However, if one excludes subgraphs corresponding to this model, a characterization can be achieved. This characterization yields a new extension of Petri nets with a decidable reachability problem. Moreover, we provide a description of those storage mechanisms for which decidability remains open. This leads to a natural model that generalizes both pushdown Petri nets and priority multicounter machines.

An Approach to Computing Downward Closures
Proceedings of ICALP 2015
Best Student Paper Award in Track B
Abstract
The downward closure of a word language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of any language is regular. While the downward closure appears to be a powerful abstraction, algorithms for computing a finite automaton for the downward closure of a given language have been established only for few language classes.
This work presents a simple general method for computing downward closures. For language classes that are closed under rational transductions, it is shown that the computation of downward closures can be reduced to checking a certain unboundedness property.
This result is used to prove that downward closures are computable for (i) every language class with effectively semilinear Parikh images that are closed under rational transductions, (ii) matrix languages, and (iii) indexed languages (equivalently, languages accepted by higher-order pushdown automata of order~2).

Computing downward closures for stacked counter automata
Proceedings of STACS 2015
Abstract
The downward closure of a language $L$ of words is the set of all (not necessarily contiguous) subwords of members of $L$. It is well known that the downward closure of any language is regular. Although the downward closure seems to be a promising abstraction, there are only few language classes for which an automaton for the downward closure is known to be computable.
It is shown here that for stacked counter automata, the downward closure is computable. Stacked counter automata are finite automata with a storage mechanism obtained by \emph{adding blind counters} and \emph{building stacks}. Hence, they generalize pushdown and blind counter automata.
The class of languages accepted by these automata are precisely those in the hierarchy obtained from the context-free languages by alternating two closure operators: imposing semilinear constraints and taking the algebraic extension. The main tool for computing downward closures is the new concept of Parikh annotations. As a second application of Parikh annotations, it is shown that the hierarchy above is strict at every level.

The Monoid of Queue Actions
with Martin Huschenbett and Dietrich Kuske
Proceedings of MFCS 2014
Abstract
We investigate the monoid of transformations that are induced by sequences of writing to and reading from a queue storage. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem is NL-complete. Furthermore, we present an algebraic characterization of this monoid's recognizable subsets. Finally, we prove that it is not Thurston-automatic.

On Boolean closed full trios and rational Kripke frames
with Markus Lohrey
Proceedings of STACS 2014
Abstract
A Boolean closed full trio is a class of languages that is closed under the Boolean operations (union, intersection, and complementation) and rational transductions. It is well-known that the regular languages constitute such a Boolean closed full trio. It is shown here that every such language class that contains any non-regular language already includes the whole arithmetical hierarchy (and even the one relative to this language).
A consequence of this result is that aside from the regular languages, no full trio generated by one language is closed under complementation.
Our construction also shows that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the definition of any language from the arithmetical hierarchy in the corresponding Kripke structure using multimodal logic.

Semilinearity and Context-Freeness of Languages Accepted by Valence Automata
with Phoebe Buckheister
Proceedings of MFCS 2013
Abstract
Valence automata are a generalization of various models of automata with storage. Here, each edge carries, in addition to an input word, an element of a monoid. A computation is considered valid if multiplying the monoid elements on the visited edges yields the identity element. By choosing suitable monoids, a variety of automata models can be obtained as special valence automata. This work is concerned with the accepting power of valence automata. Specifically, we ask for which monoids valence automata can accept only context-free languages or only languages with semilinear Parikh image, respectively. First, we present a characterization of those graph products (of monoids) for which valence automata accept only context-free languages. Second, we provide a necessary and sufficient condition for a graph product of copies of the bicyclic monoid and the integers to yield only languages with semilinear Parikh image when used as a storage mechanism in valence automata. Third, we show that all languages accepted by valence automata over torsion groups have a semilinear Parikh image.

Rational Subsets and Submonoids of Wreath Products
with Markus Lohrey and Benjamin Steinberg
Proceedings of ICALP 2013
Abstract
It is shown that membership in rational subsets of wreath products $H \wr V$ with $H$ a finite group and $V$ a virtually free group is decidable. On the other hand, it is shown that there exists a fixed finitely generated submonoid in the wreath product $\mathbb{Z}\wr\mathbb{Z}$ with an undecidable membership problem.

Silent Transitions in Automata with Storage
Proceedings of ICALP 2013
Abstract
We consider the computational power of silent transitions in one-way automata with storage. Specifically, we ask which storage mechanisms admit a transformation of a given automaton into one that accepts the same language and reads at least one input symbol in each step.
We study this question using the model of valence automata. Here, a finite automaton is equipped with a storage mechanism that is given by a monoid.
This work presents generalizations of known results on silent transitions. For two classes of monoids, it provides characterizations of those monoids that allow the removal of silent transitions. Both classes are defined by graph products of copies of the bicyclic monoid and the group of integers. The first class contains pushdown storages as well as the blind counters while the second class contains the blind and the partially blind counters.

A Sufficient Condition for Erasing Productions to Be Avoidable
Proceedings of DLT 2011
Abstract
In each grammar model, it is an important question whether erasing productions are necessary to generate all languages. Using the concept of grammars with control languages by Salomaa, which offers a uniform treatment of a variety of grammar models, we present a condition on the class of control languages that guarantees that erasing productions are avoidable in the resulting grammar model. On the one hand, this generalizes the previous result that in Petri net controlled grammars, erasing productions can be eliminated. On the other hand, it allows us to infer that the same is true for vector grammars.

On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids
Proceedings of ICALP 2011
Abstract
During recent decades, classical models in language theory have been extended by control mechanisms defined by monoids. We study which monoids cause the extensions of context-free grammars, finite automata, or finite state transducers to exceed the capacity of the original model. Furthermore, we investigate when, in the extended automata model, the nondeterministic variant differs from the deterministic one in capacity. We show that all these conditions are in fact equivalent and present an algebraic characterization. In particular, the open question of whether every language generated by a valence grammar over a finite monoid is context-free is provided with a positive answer.

On Erasing Productions in Random Context Grammars
Proceedings of ICALP 2010
Abstract
Three open questions in the theory of regulated rewriting are addressed. The first is whether every permitting random context grammar has a non-erasing equivalent. The second asks whether the same is true for matrix grammars without appearance checking. The third concerns whether permitting random context grammars have the same generative capacity as matrix grammars without appearance checking. The main result is a positive answer to the first question. For the other two, conjectures are presented. It is then deduced from the main result that at least one of the two holds.

Erasing in Petri Net Languages and Matrix Grammars
Proceedings of DLT 2009
Abstract
It is shown that applying linear erasing to a Petri net language yields a language generated by a non-erasing matrix grammar. The proof uses Petri net controlled grammars. These are context-free grammars, where the application of productions has to comply with a firing sequence in a Petri net. Petri net controlled grammars are equivalent to arbitrary matrix grammars (without appearance checking), but a certain restriction on them (linear Petri net controlled grammars) leads to the class of languages generated by non-erasing matrix grammars. It is also shown that in Petri net controlled grammars (with final markings and arbitrary labeling), erasing rules can be eliminated, which yields a reformulation of the problem of whether erasing rules in matrix grammars can be eliminated.

Labeled Step Sequences in Petri Nets
with Matthias Jantzen
Proceedings of PETRI NETS 2008
Abstract
We compare various modes of firing transitions in Petri nets and define classes of languages defined this way. We define languages through steps, i. e. sets of transitions, maximal steps, multi-steps, and maximal multi-steps of transitions in Petri nets, but in a different manner than those defined in [Burk 81a,Burk 83], by considering labeled transitions. We will show that we obtain a hierarchy of families of languages defined by multiple use of transition in firing transitions in a single multistep. Except for the maximal multi-steps all classes can be simulated by sequential firing of transitions.

Journal articles

Knapsack in Graph Groups
with Markus Lohrey
Theory of Computing Systems 62, 2018
Special Issue on STACS 2016
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al. for arbitrary finitely generated groups, can be solved in {\sf NP} for every graph group. This result even holds if the group elements are represented in a compressed form by so called straight-line programs, which generalizes the classical {\sf NP}-completeness result of the integer knapsack problem. If group elements are represented explicitly by words over the generators, then knapsack for a graph group belongs the class {\sf LogCFL} (a subclass of {\sf P}) if the graph group can be built up from the trivial group using the operations of free product and direct product with $\Z$. In all other cases, the knapsack problem is {\sf NP}-complete.

A Characterization for Decidable Separability by Piecewise Testable Languages
with Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, and Marc Zeitoun
Discrete Mathematics & Theoretical Computer Science 19(4), 2017
Special Issue on FCT 2015
Abstract
The separability problem for word languages of a class $\C$ by languages of a class $\S$ asks, for two given languages $I$ and $E$ from $\C$, whether there exists a language $S$ from $\S$ that includes $I$ and excludes $E$, that is, $I \subseteq S$ and $S\cap E = \emptyset$. In this work, we assume some mild closure properties for $\C$ and study for which such classes $\C$, separability by piecewise testable languages (PTL) is decidable. We characterize these classes in terms of decidability of (two variants of) an unboundedness problem. From this we deduce that separability by PTL is decidable for a number of language classes, such as the context-free languages and languages of labeled vector addition systems. Furthermore, it follows that separability by PTL is decidable if and only if one can compute for any language of the class its downward closure wrt.\ the \subword ordering (i.e., if the set of \subwords of any language of the class is effectively regular).
The obtained decidability results contrast some undecidability results. In fact, for all the (non-regular) language classes we present as examples with decidable separability, it is undecidable whether a given language is a PTL itself.
Our characterization involves a result of independent interest, which states that for \emph{any} kind of languages $I$ and $E$, non-separability is equivalent to the existence of common patterns in $I$ and $E$.

Monoids as Storage Mechanisms
Bulletin of the EATCS 120, 2016

The Monoid of Queue Actions
with Martin Huschenbett and Dietrich Kuske
Semigroup Forum 95, 2017
Abstract
We investigate the monoid of transformations that are induced by sequences of writing to and reading from a queue storage. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem is NL-complete. Furthermore, we present an algebraic characterization of this monoid's recognizable subsets. Finally, we prove that it is not Thurston-automatic.

Permutations of context-free, ET0L and indexed languages
with Tara Brough, Laura Ciobanu, and Murray Elder
Discrete Mathematics & Theoretical Computer Science 17(3), 2016
Abstract
For a language $L$, we consider its cyclic closure, and more generally the language $C^k(L)$, which consists of all words obtained by partitioning words from $L$ into $k$ factors and permuting them. We prove that the classes of ET0L and EDT0L languages are closed under the operators $C^k$. This both sharpens and generalises Brandstädt's result that if $L$ is context-free then $C^k(L)$ is context-sensitive and not context-free in general for $k\geq 3$. We also show that the cyclic closure of an indexed language is indexed.

On Boolean closed full trios and rational Kripke frames
with Dietrich Kuske and Markus Lohrey
Theory of Computing Systems 60, 2017
Special Issue on STACS 2014
Abstract
We study what languages can be constructed from a non-regular language $L$ using Boolean operations and (synchronized) rational transductions. If all rational transductions are allowed, one can construct the whole arithemtical hierarchy relative to $L$. If only synchronized rational transductions are allowed, we present non-regular languages that allow to construct at least languages arbitrarily high in the arithmetical hierarchy and we present non-regular languages that allow to construct only decidable languages.
A consequence of the results is that aside from the regular languages, no full trio generated by a single language is closed under complementation.
Our construction also shows that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the definition of any language from the arithmetical hierarchy in the corresponding Kripke structure using multimodal logic.

Knapsack and subset sum problems in nilpotent, polycyclic, and co-context-free groups
with Daniel König and Markus Lohrey
Contemporary Mathematics 677, 2016

Rational subsets and submonoids of wreath products
with Markus Lohrey and Benjamin Steinberg
Information and Computation 243, 2015
Special Issue on ICALP 2013
Abstract
It is shown that membership in rational subsets of wreath products $H \wr V$ with $H$ a finite group and $V$ a virtually free group is decidable. On the other hand, it is shown that there exists a fixed finitely generated submonoid in the wreath product $\mathbb{Z}\wr\mathbb{Z}$ with an undecidable membership problem.

Toward Understanding the Generative Capacity of Erasing Rules in Matrix Grammars
International Journal of Foundations of Computer Science 22(2), 2011
Special Issue on DLT 2009
Abstract
This article presents approaches to the open problem of whether erasing rules can be eliminated in matrix grammars. The class of languages generated by non-erasing matrix grammars is characterized by the newly introduced linear Petri net grammars. Petri net grammars are known to be equivalent to arbitrary matrix grammars (without appearance checking). In linear Petri net grammars, the marking has to be linear in size with respect to the length of the sentential form. The characterization by linear Petri net grammars is then used to show that applying linear erasing to a Petri net language yields a language generated by a non-erasing matrix grammar. It is also shown that in Petri net grammars (with final markings and arbitrary labeling), erasing rules can be eliminated, which yields two reformulations of the problem of whether erasing rules in matrix grammars can be eliminated.

Properties of Multiset Language Classes Defined by Multiset Pushdown Automata
with Manfred Kudlek and Patrick Totzke
Fundamenta Informaticae 93(1-3), 2009
Special Issue on CS&P 2008
Abstract
The previously introduced multiset language classes defined by multiset pushdown automata are being explored with respect to their closure properties and alternative characterizations.

Multiset Pushdown Automata
with Manfred Kudlek and Patrick Totzke
Fundamenta Informaticae 93(1-3), 2009
Special Issue on CS&P 2008
Abstract
Multiset finite Automata, a model equivalent to regular commutative grammars, are extended with a multiset store and the accepting power of this extended model of computation is investigated. This type of multiset automata come in two flavours, varying only in the ability of testing the storage for emptiness. This paper establishes normal forms and relates the derived language classes to each other as well as to known multiset language classes.

Petri Net Controlled Finite Automata
with Berndt Farwer, Matthias Jantzen, Manfred Kudlek, and Heiko Rölke
Fundamenta Informaticae 85(1-4), 2008
Special Issue on CS&P 2007
Abstract
We present a generalization of finite automata using Petri nets as control, called Concurrent Finite Automata for short. Several modes of acceptance, defined by final markings of the Petri net, are introduced, and their equivalence is shown. The class of languages obtained by l-free concurrent finite automata contains both the class of regular sets and the class of Petri net languages defined by final marking, and is contained in the class of context-sensitive languages.

Language Classes Defined by Concurrent Finite Automata
with Matthias Jantzen and Manfred Kudlek
Fundamenta Informaticae 85(1-4), 2008
Special Issue on CS&P 2007
Abstract
This paper presents results regarding the various relations among the language classes defined by Concurrent Finite Automata, relations to other language classes, as well as decidability and closure properties.

Workshop contributions

Multiset Storage Automata
with Manfred Kudlek and Patrick Totzke
Proceedings of CS&P 2008
Abstract
Two kinds of multiset automata with a storage attached, varying only in their ability of testing the storage for emptiness, are introduced, as well as normal forms. Their accepting power and relation to other multiset languages classes is investigated.

Properties of Multiset Language Classes Defined by Multiset Storage Automata
with Manfred Kudlek and Patrick Totzke
Proceedings of CS&P 2008
Abstract
The previously introduced multiset language classes defined by multiset storage automata are being explored with respect to their closure properties and alternative characterizations.

Concurrent finite automata and related language classes (an overview)
with Manfred Kudlek
Proceedings of AFLAS 2008

On Concurrent Finite Automata
with Berndt Farwer, Matthias Jantzen, Manfred Kudlek, and Heiko Rölke
Proceedings of CS&P 2007

On Languages Accepted by Concurrent Finite Automata
with Matthias Jantzen and Manfred Kudlek
Proceedings of CS&P 2007

Finite Automata Controlled by Petri Nets
with Matthias Jantzen and Manfred Kudlek
Proceedings of AWPN 2007

Theses

On Erasing Productions in Grammars with Regulated Rewriting
Diplomarbeit (Master's thesis), Universität Hamburg, 2010

Monoids as Storage Mechanisms
PhD thesis, Technische Universität Kaiserslautern, 2016
EATCS Distinguished Dissertation Award
Abstract
Automata theory has given rise to a variety of automata models that consist of a finite-state control and an infinite-state storage mechanism. The aim of this work is to provide insights into how the structure of the storage mechanism influences the expressiveness and the analyzability of the resulting model. To this end, it presents generalizations of results about individual storage mechanisms to larger classes. These generalizations characterize those storage mechanisms for which the given result remains true and for which it fails.
In order to speak of classes of storage mechanisms, we need an overarching framework that accommodates each of the concrete storage mechanisms we wish to address. Such a framework is provided by the model of valence automata, in which the storage mechanism is represented by a monoid. Since the monoid serves as a parameter to specifying the storage mechanism, our aim translates into the question: For which monoids does the given (automata-theoretic) result hold?
As a first result, we present an algebraic characterization of those monoids over which valence automata accept only regular languages. In addition, it turns out that for each monoid, this is the case if and only if valence grammars, an analogous grammar model, can generate only context-free languages.
Furthermore, we are concerned with closure properties: We study which monoids result in a Boolean closed language class. For every language class that is closed under rational transductions (in particular, those induced by valence automata), we show: If the class is Boolean closed and contains any non-regular language, then it already includes the whole arithmetical hierarchy.
This work also introduces the class of graph monoids, which are defined by finite graphs. By choosing appropriate graphs, one can realize a number of prominent storage mechanisms, but also combinations and variants thereof. Examples are pushdowns, counters, and Turing tapes. We can therefore relate the structure of the graphs to computational properties of the resulting storage mechanisms.
In the case of graph monoids, we study (i) the decidability of the emptiness problem, (ii) which storage mechanisms guarantee semilinear Parikh images, (iii) when silent transitions (i.e. those that read no input) can be avoided, and (iv) which storage mechanisms permit the computation of downward closures.

Service
I will be on the program committee of CiE 2019.
Teaching
Supervised theses
1. Phoebe Buckheister (Bachelor thesis, 2013)
2. Martin Köhler (Bachelor thesis, 2014)
Lectures
• Concurrency Theory, Summer term 2015, at Technische Universität Kaiserslautern
Organization of exercise courses
• Logik, Summer term 2014, at Technische Universität Kaiserslautern
• Logik, Summer term 2013, at Technische Universität Kaiserslautern
• Logik, Summer term 2012, at Technische Universität Kaiserslautern
• Applied Automata Theory, Summer term 2011, at Technische Universität Kaiserslautern
Tutoring
• Formale Grundlagen der Informatik I, Summer term 2009, at Universität Hamburg
• Algorithmen und Datenstrukturen, Winter term 2008/2009, at Universität Hamburg
• Formale Grundlagen der Informatik I, Summer term 2008, at Universität Hamburg
• Formale Grundlagen der Informatik II, Winter term 2007/2008, at Universität Hamburg
• Formale Grundlagen der Informatik I, Summer term 2007, at Universität Hamburg
Talks
Invited talks

Subword Based Abstractions of Formal Languages
Given at Theorietag "Automaten und formale Sprachen" 2016 in Tannenfelde, Germany
Abstract
A successful idea in the area of verification is to consider finite-state abstractions of infinite-state systems. A prominent example is the fact that many language classes satisfy a Parikh's theorem, i.e. for each language, there exists a finite automaton that accepts the same language up to the order of letters. Hence, provided that the abstraction preserves pertinent properties, this allows us to work with finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very intensely over the last decades, recent years have seen an increasing interest in abstractions based on the subword ordering. Examples include the set of (non necessarily contiguous) subwords of members of a language (the downward closure), or their superwords (the upward closure). Whereas it is well-known that these closures are regular for any language, it is often not obvious how to compute them. Another type of subword based abstractions are piecewise testable separators. Here, a separators acts as an abstraction of a pair of languages.
This talk will present approaches to computing closures, deciding separability by piecewise testable languages, and a (perhaps surprising) connection between these problems. If time permits, complexity issues will be discussed as well.

Knapsack in Graph Groups, HNN-Extensions and Amalgamated Products
(joint work with Markus Lohrey)
Given at Equations and formal languages in algebra in Les Diablerets, Switzerland
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al. for arbitrary finitely generated groups, can be solved in NP for graph groups. This result even holds if the group elements are represented in a compressed form by SLPs, which generalizes the classical NP-completeness result of the integer knapsack problem. We also prove general transfer results: NP-membership of the knapsack problem is passed on to finite extensions, HNN-extensions over finite associated subgroups, and amalgamated products with finite identified subgroups.

Recent Results on Erasing in Regulated Rewriting
Given at Theorietag "Automaten und formale Sprachen" 2011 in Allrode, Germany
Abstract
For each grammar model with regulated rewriting, it is an important question whether erasing productions add to its expressivity. In some cases, however, this has been a longstanding open problem. In recent years, several results have been obtained that clarified the generative capacity of erasing productions in some grammar models with classical types of regulated rewriting. The aim of this talk is to give an overview of these results.

Other talks

Parameterized WQOs, downward closures, and separability problems
Given at Workshop on Separability Problems in Warsaw, Poland
Abstract
We discuss a flexible class of well-quasi-orderings on words that generalizes the ordering of (not necessarily contiguous) subwords. Each of these orderings is specified by a finite automaton or a counter automaton and, like the subword ordering, guarantees regularity of all downward (or upward) closures. We then consider two problems. First, we study for which language classes one can effectively compute downward closures with respect to these orderings. Second, we are interested in which language classes permit a decision procedure to decide whether two given languages are separable by a PTL with respect to such an ordering. Here, a PTL is a finite Boolean combination of upward closed sets. The main result is that, under mild assumptions on closure properties, these two problems are solvable for the same language classes. Moreover, solvability is equivalent to that of a particular unboundedness problem that has recently been shown to be decidable for many powerful language classes.

First-order logic over the subword ordering
(joint work with Simon Halfon and Philippe Schnoebelen)
Given at Verification Seminar at Oxford University, United Kingdom
Abstract
This talk reports on results concerning first-order logic over the subword ordering on finite words. It has been known since 2006 that the whole first-order logic over this structure is undecidable, whereas the Sigma_1 fragment is NP-complete. One might therefore expect that introducing each word as a constant would leave the Sigma_1 fragment decidable. However, it was shown recently that in the presence of these constants, the \Sigma_1 theory becomes undecidable (already over two letters). Regarding the decidability border, we will consider fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. Here, the second result is that when at most two variables are not alternation bounded, the \Sigma_1 fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Concerning higher quantifier alternation depths, the \Sigma_2 fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable. If time permits, complexity aspects will be treated as well. This is joint work with Simon Halfon and Philippe Schnoebelen (to be presented at LICS 2017).

Monoids as Storage Mechanisms
Given at Kasseler Informatik-Kolloquium, Universität Kassel in Germany
Abstract
The investigation of models extending finite automata by some storage mechanism is a central theme in theoretical computer science. Choosing an appropriate storage mechanism can yield a model that is expressive enough to capture a given behavioral aspect while admitting desired means of analysis. It is therefore a central concern to understand which storage mechanisms have which properties regarding expressiveness and (algorithmic) analysis. This talk presents a line of research that aims for general insights in this direction. In other words: How does the structure of the storage mechanism influence expressiveness and analysis of the resulting model? In order to study this question, one needs a model in which the storage mechanism appears as a parameter. Such a model is available in valence automata, where the storage mechanism is given by a (typically infinite) monoid. Choosing a suitable monoid then yields models such as Turing machines, pushdown automata, vector addition systems, or combinations thereof. This talk surveys a selection of results that characterize storage mechanisms with certain desirable properties, such as decidability of reachability, semilinearity of Parikh images, and decidability of logics.

The Complexity of Knapsack in Graph Groups
(joint work with Markus Lohrey)
Given at STACS 2017 in Hannover, Germany
Abstract
Myasnikov et al. have introduced the knapsack problem for arbitrary finitely generated groups. In previous work, the authors proved that for each graph group, the knapsack problem can be solved in NP. Here, we determine the exact complexity of the problem for every graph group. While the problem is TC0-complete for complete graphs, it is LogCFL-complete for each (non-complete) transitive forest. For every remaining graph, the problem is NP-complete.

First-order logic with reachability for infinite-state systems
(joint work with Emanuele D'Osualdo and Roland Meyer)
Given at Seminar "Modélisation et vérification" at IRIF in Paris, France
Abstract
First-order logic with the reachability predicate (FOR) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).
This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FOR is decidable for the resulting transition systems.

Subword Based Abstractions of Formal Languages
Given at Seminar "Méthodes Formelles" at LaBRI in Bordeaux, France
Abstract
A successful idea in the area of verification is to consider finite-state abstractions of infinite-state systems. A prominent example is the fact that many language classes satisfy a Parikh's theorem, i.e. for each language, there exists a finite automaton that accepts the same language up to the order of letters. Hence, provided that the abstraction preserves pertinent properties, this allows us to work with finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very intensely over the last decades, recent years have seen an increasing interest in abstractions based on the subword ordering. Examples include the set of (non necessarily contiguous) subwords of members of a language (the downward closure), or their superwords (the upward closure). Whereas it is well-known that these closures are regular for any language, it is often not obvious how to compute them. Another type of subword based abstractions are piecewise testable separators. Here, a separators acts as an abstraction of a pair of languages.
This talk will present approaches to computing closures, deciding separability by piecewise testable languages, and a (perhaps surprising) connection between these problems. If time permits, complexity issues will be discussed as well.

Subword Based Abstractions of Formal Languages
Given at Seminar "Automates et applications" at IRIF in Paris, France
Abstract
A successful idea in the area of verification is to consider finite-state abstractions of infinite-state systems. A prominent example is the fact that many language classes satisfy a Parikh's theorem, i.e. for each language, there exists a finite automaton that accepts the same language up to the order of letters. Hence, provided that the abstraction preserves pertinent properties, this allows us to work with finite-state systems, which are much easier to handle.
While Parikh-style abstractions have been studied very intensely over the last decades, recent years have seen an increasing interest in abstractions based on the subword ordering. Examples include the set of (non necessarily contiguous) subwords of members of a language (the downward closure), or their superwords (the upward closure). Whereas it is well-known that these closures are regular for any language, it is often not obvious how to compute them. Another type of subword based abstractions are piecewise testable separators. Here, a separators acts as an abstraction of a pair of languages.
This talk will present approaches to computing closures, deciding separability by piecewise testable languages, and a (perhaps surprising) connection between these problems. If time permits, complexity issues will be discussed as well.

First-order logic with reachability for valence automata over graph monoids
(joint work with Emanuele D'Osualdo and Roland Meyer)
Given at Jahrestagung "Logik in der Informatik" 2016 in Tannenfelde, Germany
Abstract
First-order logic with the reachability predicate (FOR) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).
This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FOR is decidable for the resulting transition systems.

Monoids as Storage Mechanisms
Given at Theory Seminar at the National University of Singapore
Abstract
The investigation of models extending finite automata by some storage mechanism is a central theme in theoretical computer science. Choosing an appropriate storage mechanism can yield a model that is expressive enough to capture a given behavioral aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage mechanisms have which properties regarding expressiveness and (algorithmic) analysis. This talk presents a line of research that aims for general insights in this direction. In other words: How does the structure of the storage mechanism influence expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the storage mechanism appears as a parameter. Such a model is available in valence automata, where the storage mechanism is given by a (typically infinite) monoid. Choosing a suitable monoid then yields models such as Turing machines, pushdown automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize storage mechanisms with certain desirable properties, such as decidability of reachability, semilinearity of Parikh images, and decidability of logics.

Monoids as Storage Mechanisms
Given at Communicating, Distributed and Parameterized Systems in Singapore
Abstract
The investigation of models extending finite automata by some storage mechanism is a central theme in theoretical computer science. Choosing an appropriate storage mechanism can yield a model that is expressive enough to capture a given behavioral aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage mechanisms have which properties regarding expressiveness and (algorithmic) analysis. This talk presents a line of research that aims for general insights in this direction. In other words: How does the structure of the storage mechanism influence expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the storage mechanism appears as a parameter. Such a model is available in valence automata, where the storage mechanism is given by a (typically infinite) monoid. Choosing a suitable monoid then yields models such as Turing machines, pushdown automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize storage mechanisms with certain desirable properties, such as decidability of reachability, semilinearity of Parikh images, and decidability of logics.

The Complexity of Downward Closure Comparisons
Given at ICALP 2016 in Rome, Italy
Abstract
The downward closure of a language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of every language is regular. Moreover, recent results show that downward closures are computable for quite powerful system models.
One advantage of abstracting a language by its downward closure is that then, equivalence and inclusion become decidable. In this work, we study the complexity of these two problems. More precisely, we consider the following decision problems: Given languages $K$ and $L$ from classes $\C$ and $\D$, respectively, does the downward closure of $K$ include (equal) that of $L$?
These problems are investigated for finite automata, one-counter automata, context-free grammars, and reversal-bounded counter automata. For each combination, we prove a completeness result either for fixed or for arbitrary alphabets. Moreover, for Petri net languages, we show that both problems are Ackermann-hard and for higher-order pushdown automata of order $k$, we prove hardness for complements of nondeterministic $k$-fold exponential time.

Boolean closed full trios and rational Kripke frames
(joint work with Dietrich Kuske and Markus Lohrey)
Given at Seminar of the INFINI group at LSV in May 2016 in Cachan, France
Abstract
It is a well-known phenomenon that languages classes induced by infinite-state systems usually lack decidability and closure properties that make regular languages pleasant to analyze. Most notably, nondeterministic infinite-state systems typically fail to be closed under Boolean operations. In visibly pushdown automata, one has closure under Boolean operations, but at the expense of restricting the employed input alphabets, meaning they are not closed under rational transductions.
This raises the question of whether there is some type of infinite-state system that enjoys closure under Boolean operations and rational transductions (and permits decidability of, say, the emptiness problem). This talk demonstrates that this is not the case. It is shown that every language class that contains any non-regular language and is closed under Boolean operations and rational transductions already contains the whole arithmetic hierarchy (which significantly extends the recursively enumerable languages).

The complexity of downward closure comparisons
Given at NII Shonan Meeting on Higher-Order Model Checking in Shonan, Japan
Abstract
The downward closure of a language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of every language is regular. One advantage of abstracting a language by its downward closure is that then, equivalence and inclusion become decidable.
It has recently been shown by Hague, Kochems, and Ong that downward closures are computable for higher-order pushdown automata. However, the current method yields no upper bound on the complexity of such a computation. This talk will present recent results on complexity issues surrounding downward closures. Aside from general algorithms and possible approaches to obtain upper bounds in the case of HOPA, we will discuss a lower bound result for the abovementioned equivalence and inclusion problem for HOPA.

Knapsack in Graph Groups, HNN-Extensions and Amalgamated Products
(joint work with Markus Lohrey)
Given at STACS 2016 in Orléans, France
Abstract
It is shown that the knapsack problem, which was introduced by Myasnikov et al. for arbitrary finitely generated groups, can be solved in NP for graph groups. This result even holds if the group elements are represented in a compressed form by SLPs, which generalizes the classical NP-completeness result of the integer knapsack problem. We also prove general transfer results: NP-membership of the knapsack problem is passed on to finite extensions, HNN-extensions over finite associated subgroups, and amalgamated products with finite identified subgroups.

Monoids as Storage Mechanisms
Given at Seminar of the INFINI group at LSV in December 2015 in Cachan, France
Abstract
The investigation of models extending finite automata by some storage mechanism is a central theme in theoretical computer science. Choosing an appropriate storage mechanism can yield a model that is expressive enough to capture a given behavioral aspect while admitting desired means of analysis.
It is therefore a central concern to understand which storage mechanisms have which properties regarding expressiveness and (algorithmic) analysis. This talk presents a line of research that aims for general insights in this direction. In other words: How does the structure of the storage mechanism influences expressiveness and analysis of the resulting model?
In order to study this question, one needs a model in which the storage mechanism appears as a parameter. Such a model is available in valence automata, where the storage mechanism is given by a (typically infinite) monoid. Choosing a suitable monoid then yields models such as Turing machines, pushdown automata, vector addition systems, or combinations thereof.
This talk surveys a selection of results that characterize storage mechanisms with certain desirable properties, such as deciability of reachability, semilinearity of Parikh images, and avoidability of epsilon-transitions.

An Approach to Computing Downward Cosures
Given at Theorietag "Automaten und formale Sprachen" 2015 in Speyer, Germany
Abstract
The downward closure of a word language is the set of all (not necessarily contiguous) subwords of its members. It is known that the downward closure of every language is regular. However, algorithms for computing a finite automaton for the downward closure of a given language are known only for few language classes. This work presents a simple general approach to this problem. It is used to prove that downward closures are computable for (i)~every language class with effectively semilinear Parikh images that is closed under rational transductions, (ii)~matrix languages, and (iii)~indexed languages (equivalently, languages accepted by higher-order pushdown automata of order~2).

The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets
Given at RP 2015 in Warsaw, Poland
Abstract
This work studies which storage mechanisms in automata permit decidability of the reachability problem. The question is formalized using valence automata, an abstract model that generalizes automata with storage. For each of a variety of storage mechanisms, one can choose a (typically infinite) monoid $M$ such that valence automata over $M$ are equivalent to (one-way) automata with this type of storage.
In fact, many interesting storage mechanisms can be realized by monoids defined by finite graphs, called graph monoids. Hence, we study for which graph monoids the emptiness problem for valence automata is decidable. A particular model realized by graph monoids is that of Petri nets with a pushdown stack. For these, decidability is a long-standing open question and we do not answer it here.
However, if one excludes subgraphs corresponding to this model, a characterization can be achieved. This characterization yields a new extension of Petri nets with a decidable reachability problem. Moreover, we provide a description of those storage mechanisms for which decidability remains open. This leads to a natural model that generalizes both pushdown Petri nets and priority multicounter machines.

An Approach to Computing Downward Closures
Given at ICALP 2015 in Kyoto, Japan
Abstract
The downward closure of a word language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of any language is regular. While the downward closure appears to be a powerful abstraction, algorithms for computing a finite automaton for the downward closure of a given language have been established only for few language classes.
This work presents a simple general method for computing downward closures. For language classes that are closed under rational transductions, it is shown that the computation of downward closures can be reduced to checking a certain unboundedness property.
This result is used to prove that downward closures are computable for (i) every language class with effectively semilinear Parikh images that are closed under rational transductions, (ii) matrix languages, and (iii) indexed languages (equivalently, languages accepted by higher-order pushdown automata of order~2).

Downward Closures of Indexed Languages
Given at HOPA 2015 in Kyoto, Japan

Computing downward closures for stacked counter automata
Given at STACS 2015 in Munich, Germany
Abstract
The downward closure of a language $L$ of words is the set of all (not necessarily contiguous) subwords of members of $L$. It is well known that the downward closure of any language is regular. Although the downward closure seems to be a promising abstraction, there are only few language classes for which an automaton for the downward closure is known to be computable.
It is shown here that for stacked counter automata, the downward closure is computable. Stacked counter automata are finite automata with a storage mechanism obtained by \emph{adding blind counters} and \emph{building stacks}. Hence, they generalize pushdown and blind counter automata.
The class of languages accepted by these automata are precisely those in the hierarchy obtained from the context-free languages by alternating two closure operators: imposing semilinear constraints and taking the algebraic extension. The main tool for computing downward closures is the new concept of Parikh annotations. As a second application of Parikh annotations, it is shown that the hierarchy above is strict at every level.

Effectively regular downward closures
Given at LSV Seminar at ENS Cachan in Cachan, France
Abstract
The downward closure of a language is the set of all (not necessarily contiguous) subwords of its members. It is a well-known consequence of Higman's Lemma that the downward closure of every language is regular.
Aside from encoding interesting counting properties, the downward closure constitutes a promising abstraction: If L is the set of action sequences of a system, then the downward closure of L is precisely what is observed through a lossy channel, i.e. when actions can go unnoticed arbitrarily. Hence, if the downward closure is available as a regular language, the equivalence and even inclusion of system behaviors can be decided with respect to such observations.
However, there are only few classes of languages for which it is known how to compute the downward closure of a given language as a finite automaton. This talk presents new approaches to this problem.

Expressiveness and analysis of valence automata over graph monoids
Given at FORMAT Workshop 07/2014 in Kaiserslautern, Germany

Of stacks (of stacks (...) with blind counters) with blind counters
Given at AISS 2014 in Vienna, Austria
Abstract
Recent work on automata with abstract storage revealed a class of storage mechanisms that proves quite expressive and amenable to various kinds of algorithmic analysis. The storage mechanisms in this class are obtained by \emph{building stacks} and \emph{adding blind counters}.
The former is to construct a new mechanism that stores a stack whose entries are configurations of an old mechanism. One can then manipulate the topmost entry, pop it if empty, or start a new one on top. Adding a blind counter to an old mechanism yields a new mechanism in which the old one and a blind counter can be used simultaneously. We call the resulting model \emph{stacked counter automaton}.
This talk presents results on expressivity, Parikh images, membership problems, and the computability of downward closures.

On Boolean closed full trios and rational Kripke frames
(joint work with Markus Lohrey)
Given at STACS 2014 in Lyon, France
Abstract
A Boolean closed full trio is a class of languages that is closed under the Boolean operations (union, intersection, and complementation) and rational transductions. It is well-known that the regular languages constitute such a Boolean closed full trio. It is shown here that every such language class that contains any non-regular language already includes the whole arithmetical hierarchy (and even the one relative to this language).
A consequence of this result is that aside from the regular languages, no full trio generated by one language is closed under complementation.
Our construction also shows that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the definition of any language from the arithmetical hierarchy in the corresponding Kripke structure using multimodal logic.

On Boolean closed full trios and rational Kripke frames
(joint work with Markus Lohrey)
Given at Seminar "Automata and Logic" at Technische Universität Ilmenau in Ilmenau, Germany
Abstract
A Boolean closed full trio is a class of languages that is closed under Boolean operations (union, intersection, and complement) and rational transductions. It is well-known that the regular languages constitute such a Boolean closed full trio. It is shown here that every such language class that contains any non-regular language already includes the whole arithmetical hierarchy (and even the one relative to this language).
Our construction also shows that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the interpretation of any language from the arithmetical hierarchy in the corresponding Kripke structure.
Another consequence of our result is that no full trio generated by one language is closed under complementation, unless it coincides with the regular languages.

On Boolean closed full trios and rational Kripke frames
(joint work with Markus Lohrey)
Given at Theorietag "Automaten und formale Sprachen" 2013 in Ilmenau, Germany
Abstract
A Boolean closed full trio is a class of languages that is closed under Boolean operations (union, intersection, and complement) and rational transductions. It is well-known that the regular languages constitute such a Boolean closed full trio. We present a result stating that every such language class that contains any non-regular language already contains the whole arithmetical hierarchy.
Our construction also shows that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the interpretation of any language from the arithmetical hierarchy in the corresponding Kripke structure.

Recent advances on valence automata as a generalization of automata with storage
(joint work with Phoebe Buckheister)
Given at Theorietag "Automaten und formale Sprachen" 2013 in Ilmenau, Germany
Abstract
A valence automaton over a monoid $M$ is a finite automaton in which each edge carries an input word and an element of $M$. A word is then accepted if there is a run that spells the word such that the product of the monoid elements is the identity.
By choosing suitable monoids $M$, one can obtain various kinds of automata with storage as special valence automata. Examples include pushdown automata, blind multicounter automata, and partially blind multicounter automata. Therefore, valence automata offer a framework to generalize results on such automata with storage.
This talk will present recent advances in this direction. The addressed questions include: For which monoids do we have a Parikh's Theorem (as for pushdown automata)? For which monoids can we avoid silent transitions?

Semilinearity and Context-Freeness of Languages Accepted by Valence Automata
(joint work with Phoebe Buckheister)
Given at MFCS 2013 in Klosterneuburg, Austria
Abstract
Valence automata are a generalization of various models of automata with storage. Here, each edge carries, in addition to an input word, an element of a monoid. A computation is considered valid if multiplying the monoid elements on the visited edges yields the identity element. By choosing suitable monoids, a variety of automata models can be obtained as special valence automata. This work is concerned with the accepting power of valence automata. Specifically, we ask for which monoids valence automata can accept only context-free languages or only languages with semilinear Parikh image, respectively. First, we present a characterization of those graph products (of monoids) for which valence automata accept only context-free languages. Second, we provide a necessary and sufficient condition for a graph product of copies of the bicyclic monoid and the integers to yield only languages with semilinear Parikh image when used as a storage mechanism in valence automata. Third, we show that all languages accepted by valence automata over torsion groups have a semilinear Parikh image.

Rational Subsets and Submonoids of Wreath Products
(joint work with Markus Lohrey and Benjamin Steinberg)
Given at ICALP 2013 in Riga, Latvia
Abstract
It is shown that membership in rational subsets of wreath products $H \wr V$ with $H$ a finite group and $V$ a virtually free group is decidable. On the other hand, it is shown that there exists a fixed finitely generated submonoid in the wreath product $\mathbb{Z}\wr\mathbb{Z}$ with an undecidable membership problem.

Silent Transitions in Automata with Storage
Given at ICALP 2013 in Riga, Latvia
Abstract
We consider the computational power of silent transitions in one-way automata with storage. Specifically, we ask which storage mechanisms admit a transformation of a given automaton into one that accepts the same language and reads at least one input symbol in each step.
We study this question using the model of valence automata. Here, a finite automaton is equipped with a storage mechanism that is given by a monoid.
This work presents generalizations of known results on silent transitions. For two classes of monoids, it provides characterizations of those monoids that allow the removal of silent transitions. Both classes are defined by graph products of copies of the bicyclic monoid and the group of integers. The first class contains pushdown storages as well as the blind counters while the second class contains the blind and the partially blind counters.

Valence automata as a generalization of automata with storage
Given at ALFA'13 in Riga, Latvia
Abstract
A valence automaton over a monoid M is a finite automaton in which each edge carries an input word and an element of M. A word is then accepted if there is a run that spells the word such that the product of the monoid elements is the identity. By choosing appropriate monoids M, one can obtain various kinds of automata with storage as special valence automata. Examples include pushdown automata, blind multicounter automata, and partially blind multicounter automata. Therefore, valence automata offer a framework to generalize results on such automata with storage. This talk will present recent advances in this direction. The addressed questions include: For which monoids can we accept non-regular languages? For which monoids can we determinize automata? For which monoids do we have a Parikh's Theorem (as for pushdown automata)?

Valence automata as a generalization of automata with storage
Given at D-CON 2013 in Lübeck, Germany
Abstract
A valence automaton over a monoid $M$ is a finite automaton in which each edge carries an input word and an element of $M$. A word is then accepted if there is a run that spells the word such that the product of the monoid elements is the identity. By choosing appropriate monoids $M$, one can obtain various kinds of automata with storage as special valence automata. Examples include pushdown automata, blind multicounter automata, and partially blind multicounter automata. Therefore, valence automata offer a framework to generalize results on such automata with storage. This talk will present recent results on valence automata. The addressed questions include: For which monoids can we accept non-regular languages? For which monoids can we determinize automata? For which monoids can we avoid silent edges (i.e., those which read no input symbol)?

Valence automata as a generalization of automata with storage
Given at Algebra and Cryptography Seminar at CUNY Graduate Center in New York City, USA
Abstract
A valence automaton over a monoid M is a finite automaton in which each edge carries an input word and an element of M. A word is then accepted if there is a run that spells the word such that the product of the monoid elements is the identity.
By choosing appropriate monoids M, one can obtain various kinds of automata with storage as special valence automata. Examples include pushdown automata, blind multicounter automata, and partially blind multicounter automata. Therefore, valence automata offer a framework to generalize results on such automata with storage.
This talk will present recent results on valence automata. The addressed questions include: For which monoids can we accept non-regular languages? For which monoids can we determinize automata? For which monoids can we avoid silent edges (i.e., those which read no input symbol)?

Silent Transitions in Valence Automata
Given at Seminar "Algebraic and Logical Foundations of Computer Science" at Universität Leipzig in Germany
Abstract
We consider the problem of eliminating silent transitions from one-way automata with storage. It is known that in pushdown automata and in blind multicounter automata (where the counter values can become negative and are only zero-tested in the end), silent transitions can be avoided. On the other hand, in the case of partially blind multicounter automata (where the counter values are always non-negative and are only zero-tested in the end), silent transitions are necessary to accept all languages. In order to study the expressive power of silent transitions in greater generality, we use the model of valence automata. Here, a finite automaton is equipped with a storage mechanism that is given by a monoid. Since many models of automata with storage (including all of the above) arise as special valence automata, our question is: for which monoids can silent transitions be avoided? This work presents generalizations of the results above. For two classes of monoids, it provides characerizations of those monoids that allow the removal of silent transitions. Both classes are defined by graph products of copies of the bicyclic monoid and the group of integers.

Monoid Control for Grammars, Automata, and Transducers
Given at Theorietag "Automaten und formale Sprachen" 2011 in Allrode, Germany
Abstract
During recent decades, classical models in language theory have been extended by control mechanisms defined by monoids. We study which monoids cause the extensions of context-free grammars, finite automata, or finite state transducers to exceed the capacity of the original model. Furthermore, we investigate when, in the extended automata model, the nondeterministic variant differs from the deterministic one in capacity. We show that all these conditions are in fact equivalent and present an algebraic characterization. In particular, the open question of whether every language generated by a valence grammar over a finite monoid is context-free is provided with a positive answer.

A Sufficient Condition for Erasing Productions to Be Avoidable
Given at DLT 2011 in Milano, Italy
Abstract
In each grammar model, it is an important question whether erasing productions are necessary to generate all languages. Using the concept of grammars with control languages by Salomaa, which offers a uniform treatment of a variety of grammar models, we present a condition on the class of control languages that guarantees that erasing productions are avoidable in the resulting grammar model. On the one hand, this generalizes the previous result that in Petri net controlled grammars, erasing productions can be eliminated. On the other hand, it allows us to infer that the same is true for vector grammars.

On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids
Given at ICALP 2011 in Zürich, Switzerland
Abstract
During recent decades, classical models in language theory have been extended by control mechanisms defined by monoids. We study which monoids cause the extensions of context-free grammars, finite automata, or finite state transducers to exceed the capacity of the original model. Furthermore, we investigate when, in the extended automata model, the nondeterministic variant differs from the deterministic one in capacity. We show that all these conditions are in fact equivalent and present an algebraic characterization. In particular, the open question of whether every language generated by a valence grammar over a finite monoid is context-free is provided with a positive answer.

On Erasing Productions in Random Context Grammars
Given at ICALP 2010 in Bordeaux, France
Abstract
Three open questions in the theory of regulated rewriting are addressed. The first is whether every permitting random context grammar has a non-erasing equivalent. The second asks whether the same is true for matrix grammars without appearance checking. The third concerns whether permitting random context grammars have the same generative capacity as matrix grammars without appearance checking. The main result is a positive answer to the first question. For the other two, conjectures are presented. It is then deduced from the main result that at least one of the two holds.

Erasing in Petri Net Languages and Matrix Grammars
Given at DLT 2009 in Stuttgart, Germany
Abstract
It is shown that applying linear erasing to a Petri net language yields a language generated by a non-erasing matrix grammar. The proof uses Petri net controlled grammars. These are context-free grammars, where the application of productions has to comply with a firing sequence in a Petri net. Petri net controlled grammars are equivalent to arbitrary matrix grammars (without appearance checking), but a certain restriction on them (linear Petri net controlled grammars) leads to the class of languages generated by non-erasing matrix grammars. It is also shown that in Petri net controlled grammars (with final markings and arbitrary labeling), erasing rules can be eliminated, which yields a reformulation of the problem of whether erasing rules in matrix grammars can be eliminated.

Labeled Step Sequences in Petri Nets
(joint work with Matthias Jantzen)
Given at PETRI NETS 2008 in Xi'an, China
Abstract
We compare various modes of firing transitions in Petri nets and define classes of languages defined this way. We define languages through steps, i. e. sets of transitions, maximal steps, multi-steps, and maximal multi-steps of transitions in Petri nets, but in a different manner than those defined in [Burk 81a,Burk 83], by considering labeled transitions. We will show that we obtain a hierarchy of families of languages defined by multiple use of transition in firing transitions in a single multistep. Except for the maximal multi-steps all classes can be simulated by sequential firing of transitions.

Concurrent Finite Automata
(joint work with Matthias Jantzen and Manfred Kudlek)
Given at Theorietag "Automaten und formale Sprachen" 2007 in Leipzig, Germany
Abstract
We present a generalization of finite automata using Petri nets as control. Acceptance is defined by final markings of the Petri net. The class of languages obtained by $\lambda$-free concurrent finite automata contains both the class of regular sets and the class of Petri net languages defined by final marking.