Chris Köcher
Researcher
About me
I am a postdoctoral researcher at the Max Planck Institute for Software Systems in Kaiserslautern. Here, I am part of the Models of Computation group headed by Georg Zetzsche's and work on the project FINABIS (FINitestate ABstractions of Infinitestate Systems) funded by the ERC.
Before that, I was a doctoral student at the Technische Universität Ilmenau in the Automata and Logics group led by Dietrich Kuske. I defended my dissertation on May 18th, 2022.
Photo by: Chris Liebold
Contact
Research Interests
 Automata with various storage mechanisms
 Formal verification of infinite state systems
 Algebraic automata theory
 Computability and Complexity
Work Experience
2023  present
Researcher @ Max Planck Institute for Software Systems, Kaiserslautern, Germany
2016  2022
Researcher and Doctoral Student @ Technische Universität Ilmenau, Germany
2014  2016
Student Assistant @ Technische Universität Ilmenau, Germany
Education
2016  2022
Doctor rerum naturalium (Dr. rer. nat.) @ Technische Universität Ilmenau, Germany
Thesis: Verification of Automata with Storage Mechanisms (supervised by Dietrich Kuske)
An important research topic in computer science is the verification, i.e., the analysis of systems towards their correctness. This analysis consists of two parts: first we have to formalize the system and the desired properties. Afterwards we have to find algorithms to check whether the properties hold in the system. In many cases we can model the system as a finite automaton with a suitable storage mechanism, e.g., functional programs with recursive calls can be modeled as automata with a stack (or pushdown).
Here, we consider automata with two variations of stacks and queues:
In some special cases we are still able to verify such systems. So, we will consider only special automata with multiple stacks  socalled asynchronous pushdown automata. These are multiple (local) automata each having one stack. Whenever these automata try to write something into at least one stack, we require a read action on these stacks right before these actions. We will see that the (recurrent) reachability problem is decidable for such asynchronous pushdown automata in polynomial time.
We can also semidecide the reachability problem of our queue automata by exploration of the configration space. To this end, we can join multiple consecutive transitions to socalled metatransformations and simulate them at once. Here, we study metatransformations alternating between writing words from a given regular language into the queues and reading words from another regular language from the queues. We will see that such metatransformations can be applied in polynomial time.
We will prove the aforementioned results with the help of several algebraic properties of the storage mechanisms. To this end, we will first study the monoid of all action sequences which can be applied on such memories. This monoid is also known as the transformation monoid or action monoid. So, we will see for each of our considered storage mechanisms that for each sequence of basic actions we can construct in any case another action sequence which is somewhat “simple” and has the same effect as the original sequence. Furthermore, we will characterize several classes of languages in these transformation monoids and analyze their algorithmic properties.
Here, we consider automata with two variations of stacks and queues:
 Partially lossy queues and stacks, which are allowed to forget some specified parts of their contents at any time. We are able to model unreliable systems with such memories.
 Distributed queues and stacks, i.e., multiple such memories with a special synchronization in between.
In some special cases we are still able to verify such systems. So, we will consider only special automata with multiple stacks  socalled asynchronous pushdown automata. These are multiple (local) automata each having one stack. Whenever these automata try to write something into at least one stack, we require a read action on these stacks right before these actions. We will see that the (recurrent) reachability problem is decidable for such asynchronous pushdown automata in polynomial time.
We can also semidecide the reachability problem of our queue automata by exploration of the configration space. To this end, we can join multiple consecutive transitions to socalled metatransformations and simulate them at once. Here, we study metatransformations alternating between writing words from a given regular language into the queues and reading words from another regular language from the queues. We will see that such metatransformations can be applied in polynomial time.
We will prove the aforementioned results with the help of several algebraic properties of the storage mechanisms. To this end, we will first study the monoid of all action sequences which can be applied on such memories. This monoid is also known as the transformation monoid or action monoid. So, we will see for each of our considered storage mechanisms that for each sequence of basic actions we can construct in any case another action sequence which is somewhat “simple” and has the same effect as the original sequence. Furthermore, we will characterize several classes of languages in these transformation monoids and analyze their algorithmic properties.
2014  2016
Master of Science in Computer Science @ Technische Universität Ilmenau, Germany
Thesis: Einbettungen in das Transformationsmonoid einer vergesslichen Warteschlange (supervised by Dietrich Kuske)
In this thesis we model so called lossy queues (also called “lossy channels”) as monoids of transformations denoted by Q_{l}^{(n)}, where n is the size of the underlying alphabet of write and read operations. These queues can randomly forget some parts of their content at any time. Our focus is the study of embeddings into this monoid. At first we give a common criterion on embeddings into Q_{l}^{(n)}. With the help of this criterion we can show that Q_{l}^{(n)} does not embed into Q_{l}^{(m)} iff n > m. Additionally we can show that Q_{l}^{(n)} does not embed into Q_{r}^{(2)} (where Q_{r}^{(2)} is the monoid of transformations on a classic reliable queue) as well as Q_{r}^{(2)} does not embed into Q_{l}^{(n)}. Finally we investigate into a characterization of the class of trace monoids that embed into Q_{l}^{(n)}. As a result we get that the class of embeddings of trace monoids into Q_{l}^{(n)} (for n ≥ 3) is the same class as the embbedings into Q_{r}^{(2)}. Furthermore, the class of Q_{l}^{(2)} is a proper subclass of the class of embeddings into Q_{l}^{(3)}.
2011  2014
Bachelor of Science in Computer Science @ Technische Universität Ilmenau, Germany
Thesis: Analyse der Entscheidbarkeit diverser Probleme in automatischen Graphen (supervised by Dietrich Kuske)
We investigate the decidability of different NPcomplete problems in automatic and recursive graphs and determine the completeness of the concrete level in arithmetic and analytic hierarchy. The results are the following: (1) Existence of an independent node set, existence of an infinite path in an order tree, existence of an set covering and set packing are decidable for automatic graphs and Σ_{1}^{1}complete for recursive graphs. (2) Existence of a perfect matching and satisfiability of infinite CNFformulas in propositional calculus are Σ_{1}^{1}complete for both automatic and recursive graphs. (3) Satisfiability of infinite CNFformulas in propositional calculus without infinite clauses is Π_{1}^{0}complete for automatic graphs and in Π_{2}^{0} for recursive graphs. (4) Satisfiability of infinite CNFformulas in propositional calculus with finite set of infinite clauses is Σ_{2}^{0}complete for automatic graphs and in Σ_{4}^{0} for recursive graphs. (5) Existence of a coloring with infinite colorset is decidable for automatic graphs and Σ_{1}^{1}complete for recursive graphs. (6) Existence of a coloring with finite colorset is Π_{1}^{0}complete for both automatic and recursive graphs.
Teaching
Lectures
 Automaten und Komplexität (ST 2021)
 Automatentheorie (ST 2022)
 Concurrency Theory (WT 2023/24)
 Logik und Logikprogrammierung (ST 2021)
 Verifikation (WT 2021/22)
Tutorials
 Automaten, Sprachen und Komplexität (WT 2015/16  WT 20/21)
 Automaten und Komplexität (ST 2020  ST 2021)
 Automatentheorie (ST 2019  ST 2022)
 Logik und Logikprogrammierung (ST 2017  ST 2019)
 Verifikation (WT 2016/17  WT 2019/20)
Seminars
 Logic and Verification Seminar: Formal Languages and Neural Networks (ST 2024)
Publications
Submitted Articles

BackwardsReachability for Cooperating MultiPushdown Systems (with Dietrich Kuske)
Invited for a special issue of JCSS for FCT 2023.
A cooperating multipushdown system consists of a tuple of pushdown systems that can delegate the execution of recursive procedures to subtuples; control returns to the calling tuple once all subtuples finished their task. This allows the concurrent execution since disjoint subtuples can perform their task independently. Because of the concrete form of recursive descent into subtuples, the content of the multipushdown does not form an arbitrary tuple of words, but can be understood as a Mazurkiewicz trace.
For such systems, we prove that the backwards reachability relation efficiently preserves recognizability, generalizing a result and proof technique by Bouajjani et al. for singlepushdown systems. It follows that the reachability relation is decidable for cooperating multipushdown systems in polynomial time and the same holds, e.g., for safety and liveness properties given by recognizable sets of configurations.
Conference Contributions

Regular Separators for VASS Coverability Languages (with Georg Zetzsche)
FSTTCS 2023, Leibniz International Proceedings in Informatics vol. 284, pages 15:115:19 (2023).
We study regular separators of vector addition systems (VASS, for short) with coverability semantics. A regular language R is a regular separator of languages K and L if K ⊆ R and L ∩ R = ∅. It was shown by Czerwiński, Lasota, Meyer, Muskalla, Kumar, and Saivasan (CONCUR 2018) that it is decidable whether, for two given VASS, there exists a regular separator. In fact, they show that a regular separator exists if and only if the two VASS languages are disjoint. However, they provide a triply exponential upper bound and a doubly exponential lower bound for the size of such separators and leave open which bound is tight.
We show that if two VASS have disjoint languages, then there exists a regular separator with at most doubly exponential size. Moreover, we provide tight size bounds for separators in the case of fixed dimensions and unary/binary encodings of updates and NFA/DFA separators. In particular, we settle the aforementioned question.
The key ingredient in the upper bound is a structural analysis of separating automata based on the concept of basic separators, which was recently introduced by Czerwiński and the second author. This allows us to determinize (and thus complement) without the powerset construction and avoid one exponential blowup. 
Forwards and BackwardsReachability for Cooperating MultiPushdown Systems (with Dietrich Kuske)
FCT 2023, Springer Lecture Notes in Computer Science vol. 14292, pages 318332 (2023).
A cooperating multipushdown system consists of a tuple of pushdown systems that can delegate the execution of recursive procedures to subtuples; control returns to the calling tuple once all subtuples finished their task. This allows the concurrent execution since disjoint subtuples can perform their task independently. Because of the concrete form of recursive descent into subtuples, the content of the multipushdown does not form an arbitrary tuple of words, but can be understood as a Mazurkiewicz trace.
For such systems, we prove that the backwards reachability relation efficiently preserves recognizability, generalizing a result and proof technique by Bouajjani et al. for singlepushdown systems. While this preservation does not hold for the forwards reachability relation, we can show that it efficiently preserves the rationality of a set of configurations; the proof of this latter result is inspired by the work by Finkel et al. It follows that the reachability relation is decidable for cooperating multipushdown systems in polynomial time and the same holds, e.g., for safety and liveness properties given by recognizable sets of configurations. 
Reachability Problems on Partially Lossy Queue Automata
RP 2019, Springer Lecture Notes in Computer Science vol. 11674, pages 149163 (2019).
We study the reachability problem for queue automata and lossy queue automata. Concretely, we consider the set of queue contents which are forwards resp. backwards reachable from a given set of queue contents. Here, we prove the preservation of regularity if the queue automaton loops through some special sets of transformations. This is a generalization of the results by Boigelot et al. and Abdulla et al. regarding queue automata looping through a single sequence of transformations. We also prove that our construction is effective and efficient. 
The CayleyGraph of the Queue Monoid: Logic and Decidability (with Faried Abu Zaid)
FSTTCS 2018, Leibniz International Proceedings in Informatics vol. 122, pages 9:19:17 (2018).
We investigate the decidability of logical aspects of graphs that arise as Cayleygraphs of the socalled queue monoids. These monoids model the behavior of the classical (reliable) fifoqueues. We answer a question raised by Huschenbett, Kuske, and Zetzsche and prove the decidability of the firstorder theory of these graphs with the help of an  at least for the authors  new combination of the wellknown method from Ferrante and Rackoff and an automatabased approach. On the other hand, we prove that the monadic secondorder of the queue monoid's Cayleygraph is undecidable. 
Rational, Recognizable, and Aperiodic Sets in the Partially Lossy Queue Monoid
STACS 2018, Leibniz International Proceedings in Informatics vol. 96, pages 45:145:14 (2018).
Partially lossy queue monoids (or plq monoids) model the behavior of queues that can forget arbitrary parts of their content. While many decision problems on recognizable subsets in the plq monoid are decidable, most of them are undecidable if the sets are rational. In particular, in this monoid the classes of rational and recognizable subsets do not coincide. By restricting multiplication and iteration in the construction of rational sets and by allowing complementation we obtain precisely the class of recognizable sets. From these special rational expressions we can obtain an MSO logic describing the recognizable subsets. Moreover, we provide similar results for the class of aperiodic subsets in the plq monoid. 
The Transformation Monoid of a Partially Lossy Queue (with Dietrich Kuske)
CSR 2017, Springer Lecture Notes in Computer Science vol. 10304, pages 191205 (2017).
We model the behavior of a lossy fifoqueue as a monoid of transformations that are induced by sequences of writing and reading. To have a common model for reliable and lossy queues, we split the alphabet of the queue into two parts: the forgettable letters and the letters that are transmitted reliably.
We describe this monoid by means of a confluent and terminating semiThue system and then study some of the monoids algebraic properties. In particular, we characterize completely when one such monoid can be embedded into another as well as which trace monoids occur as submonoids. The resulting picture is far more diverse than in the case of reliable queues studied before.
Fully Refereed Journal Articles

Rational, Recognizable, and Aperiodic Partially Lossy Queue Languages
International Journal of Algebra and Computation, vol. 32(3), pages 483528 (2022).
Partially lossy queue monoids (or plq monoids) model the behavior of queues that can nondeterministically forget specified parts of their content at any time. We call the subsets of this monoid partially lossy queue languages (or plq languages). While many decision problems on recognizable plq languages are decidable, most of them are undecidable if the languages are rational. In particular, in this monoid the classes of rational and recognizable languages do not coincide. This is due to the fact that the class of recognizable plq languages is not closed under multiplication and iteration. However, we can generate the recognizable plq languages using special rational expressions consisting of the Boolean operations and restricted versions of multiplication and iteration. From these special rational expressions we can also obtain an MSO logic describing the recognizable plq languages. Moreover, we provide similar results for the class of aperiodic languages in the plq monoid. 
Reachability Problems on Reliable and Lossy Queue Automata
Theory of Computing Systems vol. 65(8), pages 12111242 (2021).
We study the reachability problem for queue automata and lossy queue automata. Concretely, we consider the set of queue contents which are forwards resp. backwards reachable from a given set of queue contents. Here, we prove the preservation of regularity if the queue automaton loops through some special sets of transformation sequences. This is a generalization of the results by Boigelot et al. and Abdulla et al. regarding queue automata looping through a single sequence of transformations. We also prove that our construction is possible in polynomial time. 
The Inclusion Structure of Partially Lossy Queue Monoids and their Trace Submonoids (with Dietrich Kuske and Olena Prianychnykova)
RAIRO  Theoretical Informatics and Applications vol. 52(1), pages 5586 (2018).
We model the behavior of a lossy fifoqueue as a monoid of transformations that are induced by sequences of writing and reading. To have a common model for reliable and lossy queues, we split the alphabet of the queue into two parts: the forgettable letters and the letters that are transmitted reliably.
We describe this monoid by means of a confluent and terminating semiThue system and then study some of the monoid's algebraic properties. In particular, we characterize completely when one such monoid can be embedded into another as well as which trace monoids occur as submonoids. Surprisingly, these are precisely those trace monoids that embed into the direct product of two free monoids  which gives a partial answer to a question raised by Diekert, Muscholl, and Reinhardt (STACS 1995).
Talks

Regular Separators for VASS Coverability Languages
43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 2023, Hyderabad.
33. Theorietag "Automaten und Formale Sprachen" 2023, Kaiserslautern. 
Forwards and BackwardsReachability for Cooperating MultiPushdown Systems
24th International Symposium on Fundamentals of Computation Theory 2023, Trier.
Highlights of Logic, Games and Automata 2022, Paris. 
Reachability Problems on MultiQueue Automata
Highlights of Logic, Games and Automata 2020, Online. 
Reachability Problems on Partially Lossy Queue Automata
Highlights of Logic, Games and Automata 2019, Warsaw.
13th International Conference on Reachability Problems 2019, Brussels.
28. Theorietag "Automaten und Formale Sprachen" 2018, Wittenberg. 
The CayleyGraph of the Queue Monoid: Logic and Decidability
38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 2018, Ahmedabad. 
Rational, Recognizable, and Aperiodic Sets in the Partially Lossy Queue Monoid
Highlights of Logic, Games and Automata 2018, Berlin.
35th Symposium on Theoretical Aspects of Computer Science 2018, Caen.
27. Theorietag "Automaten und Formale Sprachen" 2017, Bonn. 
The Transformation Monoid of a Partially Lossy Queue
12th International Computer Science Symposium in Russia 2017, Kazan. 
Analyse der Entscheidbarkeit diverser Probleme in automatischen Graphen (in German)
24. Theorietag "Automaten und Formale Sprachen" 2014, Caputh.