Chris Köcher

About me

I am a postdoctoral researcher at the Max Planck Institute for Software Systems in Kaiserslautern, Germany. Here, I am part of the Models of Computation group headed by Georg Zetzsche and work on the project FINABIS (FINite-state ABstractions of Infinite-state 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 in May 2022.

My pronouns are he / him.

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:
  1. 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.
  2. Distributed queues and stacks, i.e., multiple such memories with a special synchronization in between.
Often we can check the properties of our models by solving the reachability and recurrent reachability problems in our automata models. It is well-known that the decidability of these problems highly depends on the concrete data type of our automata’s memory. Both problems can be solved in polynomial time for automata with one stack. In contrast, these problems are undecidable if we attach a queue or at least two stacks to our automata.
In some special cases we are still able to verify such systems. So, we will consider only special automata with multiple stacks - so-called 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 semi-decide the reachability problem of our queue automata by exploration of the configration space. To this end, we can join multiple consecutive transitions to so-called meta-transformations and simulate them at once. Here, we study meta-transformations 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 meta-transformations 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 Ql(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 Ql(n). With the help of this criterion we can show that Ql(n) does not embed into Ql(m) iff n > m. Additionally we can show that Ql(n) does not embed into Qr(2) (where Qr(2) is the monoid of transformations on a classic reliable queue) as well as Qr(2) does not embed into Ql(n). Finally we investigate into a characterization of the class of trace monoids that embed into Ql(n). As a result we get that the class of embeddings of trace monoids into Ql(n) (for n ≥ 3) is the same class as the embbedings into Qr(2). Furthermore, the class of Ql(2) is a proper subclass of the class of embeddings into Ql(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 NP-complete 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 Σ11-complete for recursive graphs. (2) Existence of a perfect matching and satisfiability of infinite CNF-formulas in propositional calculus are Σ11-complete for both automatic and recursive graphs. (3) Satisfiability of infinite CNF-formulas in propositional calculus without infinite clauses is Π10-complete for automatic graphs and in Π20 for recursive graphs. (4) Satisfiability of infinite CNF-formulas in propositional calculus with finite set of infinite clauses is Σ20-complete for automatic graphs and in Σ40 for recursive graphs. (5) Existence of a coloring with infinite color-set is decidable for automatic graphs and Σ11-complete for recursive graphs. (6) Existence of a coloring with finite color-set is Π10-complete for both automatic and recursive graphs.

Teaching

Lectures

  • Automaten und Komplexität (ST 2021)
  • Automatentheorie (ST 2022)
  • Concurrency Theory (WT 2023/24 - WT 2024/25)
  • 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

  1. The complexity of separability for semilinear sets and Parikh automata (with Elias Rojas Collins and Georg Zetzsche)
    In a separability problem, we are given two sets K and L from a class C, and we want to decide whether there exists a set R from a class S such that K ⊆ R and R ∩ L = ∅. In this case, we speak of separability of sets in C by sets in S.

    We study two types of separability problems. First, we consider separability of semilinear sets by recognizable sets of vectors (equivalently, by sets definable by quantifier-free monadic Presburger formulas). Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity.

    Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕd (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.

Conference Contributions

  1. The Power of Hard Attention Transformers on Data Sequences: A Formal Language Theoretic Perspective (with Pascal Bergsträßer, Anthony Widjaja Lin, and Georg Zetzsche)
    NeurIPS 2024, accepted.
    Formal language theory has recently been successfully employed to unravel the power of transformer encoders. This setting is primarily applicable in Natural Language Processing (NLP), as a token embedding function (where a bounded number of tokens is admitted) is first applied before feeding the input to the transformer. On certain kinds of data (e.g. time series), we want our transformers to be able to handle arbitrary input sequences of numbers (or tuples thereof) without a priori limiting the values of these numbers. In this paper, we initiate the study of the expressive power of transformer encoders on sequences of data (i.e. tuples of numbers). Our results indicate an increase in expressive power of hard attention transformers over data sequences, in stark contrast to the case of strings.
    In particular, we prove that Unique Hard Attention Transformers (UHAT) over inputs as data sequences no longer lie within the circuit complexity class AC0 (even without positional encodings), unlike the case of string inputs, but are still within the complexity class TC0 (even with positional encodings). Over strings, UHAT without positional encodings capture only regular languages. In contrast, we show that over data sequences UHAT can capture non-regular properties. Finally, we show that UHAT capture languages definable in an extension of linear temporal logic with unary numeric predicates and arithmetics.
  2. Regular Separators for VASS Coverability Languages (with Georg Zetzsche)
    FSTTCS 2023, Leibniz International Proceedings in Informatics vol. 284, pages 15:1-15: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.
  3. Forwards- and Backwards-Reachability for Cooperating Multi-Pushdown Systems (with Dietrich Kuske)
    FCT 2023, Springer Lecture Notes in Computer Science vol. 14292, pages 318-332 (2023).
    A cooperating multi-pushdown system consists of a tuple of pushdown systems that can delegate the execution of recursive procedures to sub-tuples; control returns to the calling tuple once all sub-tuples finished their task. This allows the concurrent execution since disjoint sub-tuples can perform their task independently. Because of the concrete form of recursive descent into sub-tuples, the content of the multi-pushdown 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 single-pushdown 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 multi-pushdown systems in polynomial time and the same holds, e.g., for safety and liveness properties given by recognizable sets of configurations.
  4. Reachability Problems on Partially Lossy Queue Automata
    RP 2019, Springer Lecture Notes in Computer Science vol. 11674, pages 149-163 (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.
  5. The Cayley-Graph of the Queue Monoid: Logic and Decidability (with Faried Abu Zaid)
    FSTTCS 2018, Leibniz International Proceedings in Informatics vol. 122, pages 9:1-9:17 (2018).
    We investigate the decidability of logical aspects of graphs that arise as Cayley-graphs of the so-called queue monoids. These monoids model the behavior of the classical (reliable) fifo-queues. We answer a question raised by Huschenbett, Kuske, and Zetzsche and prove the decidability of the first-order theory of these graphs with the help of an - at least for the authors - new combination of the well-known method from Ferrante and Rackoff and an automata-based approach. On the other hand, we prove that the monadic second-order of the queue monoid's Cayley-graph is undecidable.
  6. Rational, Recognizable, and Aperiodic Sets in the Partially Lossy Queue Monoid
    STACS 2018, Leibniz International Proceedings in Informatics vol. 96, pages 45:1-45: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.
  7. The Transformation Monoid of a Partially Lossy Queue (with Dietrich Kuske)
    CSR 2017, Springer Lecture Notes in Computer Science vol. 10304, pages 191-205 (2017).
    We model the behavior of a lossy fifo-queue 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 semi-Thue 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

  1. Backwards-Reachability for Cooperating Multi-Pushdown Systems (with Dietrich Kuske)
    Journal of Computer and System Sciences, vol. 148, pages 1-14 (2025)
    Special Issue on FCT 2023.
    A cooperating multi-pushdown system consists of a tuple of pushdown systems that can delegate the execution of recursive procedures to sub-tuples; control returns to the calling tuple once all sub-tuples finished their task. This allows the concurrent execution since disjoint sub-tuples can perform their task independently. Because of the concrete form of recursive descent into sub-tuples, the content of the multi-pushdown 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 single-pushdown systems. It follows that the reachability relation is decidable for cooperating multi-pushdown systems in polynomial time and the same holds, e.g., for safety and liveness properties given by recognizable sets of configurations.
  2. Rational, Recognizable, and Aperiodic Partially Lossy Queue Languages
    International Journal of Algebra and Computation, vol. 32(3), pages 483-528 (2022).
    Partially lossy queue monoids (or plq monoids) model the behavior of queues that can non-deterministically 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.
  3. Reachability Problems on Reliable and Lossy Queue Automata
    Theory of Computing Systems vol. 65(8), pages 1211-1242 (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.
  4. 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 55-86 (2018).
    We model the behavior of a lossy fifo-queue 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 semi-Thue 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).
Note that the downloads above are submitted or accepted versions of my papers and do not necessarily match their published versions. You can find the published versions by clicking their DOI.

Talks

  1. The Power of Hard Attention Transformers on Data Sequences: A Formal Language Theoretic Perspective
    Highlights of Logic, Games, and Automata 2024, Bordeaux.
    Seminar on Formal Languages and Neural Networks (FLaNN), Online.
  2. 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.
  3. Forwards- and Backwards-Reachability for Cooperating Multi-Pushdown Systems
    24th International Symposium on Fundamentals of Computation Theory 2023, Trier.
    Highlights of Logic, Games, and Automata 2022, Paris.
  4. Reachability Problems on Multi-Queue Automata
    Highlights of Logic, Games, and Automata 2020, Online.
  5. 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.
  6. The Cayley-Graph of the Queue Monoid: Logic and Decidability
    38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 2018, Ahmedabad.
  7. 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.
  8. The Transformation Monoid of a Partially Lossy Queue
    12th International Computer Science Symposium in Russia 2017, Kazan.
  9. Analyse der Entscheidbarkeit diverser Probleme in automatischen Graphen (in German)
    24. Theorietag "Automaten und Formale Sprachen" 2014, Caputh.

Service

As a Reviewer

As an Organizer