Chris Köcher

TCS Journal 2026 Journal Article

Reachability in trace-pushdown systems

• Chris Köcher
• Dietrich Kuske

We consider the reachability relation of pushdown systems whose pushdown holds a Mazurkiewicz trace instead of just a word as in classical systems. Under two natural conditions on the transition structure of such systems, we prove that the reachability relation is lc-rational, a new notion that restricts the class of rational trace relations. We also develop the theory of these lc-rational relations to the point where they allow to infer that forwards-reachability of a trace-pushdown system preserves the rationality and backwards-reachability the recognizability of sets of configurations. As a consequence it is decidable whether one recognizable set of configurations can be reached from some rational set of configurations. All our constructions are polynomial (assuming the dependence alphabet to be fixed). These findings generalize results by Caucal on classical pushdown systems (namely the rationality of the reachability relation of such systems), complement results by Zetzsche (namely the decidability for arbitrary transition structures under severe restrictions on the dependence alphabet), and extend results from our conference papers [1] and [2].

Highlights Conference 2025 Conference Abstract

NoPE: The Counting Power of Transformers with No Positional Encodings

• Chris Köcher

MFCS Conference 2025 Conference Paper

The Complexity of Separability for Semilinear Sets and Parikh Automata

• Elias Rojas Collins
• Chris Köcher
• Georg Zetzsche

In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i. e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. 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.

NeurIPS Conference 2024 Conference Paper

The Power of Hard Attention Transformers on Data Sequences: A formal language theoretic perspective

• Pascal Bergsträßer
• Chris Köcher
• Anthony W. Lin
• Georg Zetzsche

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.

Highlights Conference 2024 Conference Abstract

The Power of Hard Attention Transformers on Data Sequences: A Formal Language Theoretic Perspective

• Chris Köcher

Formal language theory has recently been successfully employed to unravel the power of transformer encoders. This setting is primarily applicable in Natural Languange 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. Here, 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 AC$^0$ (even without positional encodings), unlike the case of string inputs, but are still within the complexity class TC$^0$ (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. This talk is based on joint work with Pascal Bergsträßer, Anthony Widjaja Lin, and Georg Zetzsche. A preprint of this work can be found on arXiv (ID: 2405. 16166).

Highlights Conference 2022 Conference Abstract

Verifying Multi-Pushdown Automata

• Chris Köcher

In this talk we will focus on automata having multiple stacks as their memory. Concretely, our automata consist of multiple local finite automata each having one stack. We additionally allow partial synchronizations between these stacks. This means, whenever we read or write a letter we do this operation on a specified subset of these stacks at the same time. Note that our model also covers automata having one or more stacks without synchronization. It is well-known that automata having at least two stacks are as powerful as Turing-machines implying the undecidability of all non-trivial verification problems of such systems. To circumvent these undecidabilities we consider a special restriction to these automata. So, when applying a transition of our special automata, we read a letter a, execute local transitions simultaneously on each local automaton able to handle the letter a, and we write other letters at most into the stacks associated to the letter a. We can show then that the set of backwards reachable configurations of a recognizable set of configurations of such special multi-pushdown automaton is effectively recognizable again. In contrast we can find a recognizable set of configurations such that the forwards reachable configurations are not recognizable anymore. Anyways, we learn that the reachability problem and even recurrent reachability problem are decidable in polynomial time. We also obtain that the model checking problem of Thiagarajan's LTL for traces is decidable in our multi-pushdown automata. Note that this talk is based on a joint work with Dietrich Kuske.

Highlights Conference 2020 Conference Abstract

Reachability Problems in Multi-Queue Automata

• Chris Köcher

In this talk, we will focus on automata having multiple reliable queues which are partially synchronized. This means, whenever we write or read some letter we do this operation on a specified subset of these queues at the same time. For example, with the help of these machines we can easily simulate networks of finite automata which communicate through some reliable channels, so-called communicating automata. However, these partially synchronized multi-queue automata are more general since we are able to synchronize the contents of two specified channels while other channels can be handled asynchronously. Note that this model also covers automata having one or more queues without any synchronization. Obviously, the reachability problem of these machines is undecidable. Hence, we need some approximation of this problem. This can be done step by step by computation of all configurations after application of n atomic queue operations for some increasing natural number n. Using this approach we obtain an algorithm which semi-decides the reachability problem. However, this approximation is very inefficient since we always explore only a finite space of reachable configurations. Boigelot et al. improved this approximation by introduction of so-called meta-transformations. These are special sets of transformation sequences such that we can easily compute the set of reachable configurations. Boigelot et al. focused on single- and (asynchronous) multi-queue automata looping through a single sequence of transformations t. In other words, given a recognizable set C of configurations and some special transformation sequence t, the authors have proven that the set configurations reachable from C via t^* is effectively recognizable. Here, we generalize this result to our partially synchronized multi-queue automata. We also consider some special recognizable sets T of transformation sequences such that we can compute a recognizable set of configurations which are reachable via the transformation sequences in T^*. Concretely, we consider such recognizable sets of transformation sequences which are alternating between two sets of write actions and read actions. For these sets we prove that, starting from a given recognizable set of configurations we will end up in an effectively recognizable set of configurations after application of these transformation sequences.

Highlights Conference 2018 Conference Abstract

Rational, Recognizable, and Aperiodic Sets in the Partially Lossy Queue Monoid

• Chris Köcher

ABSTRACT. Partially lossy queue monoids (or plq monoids) model the behavior of queues that can forget some parts of their content. Partially lossy queues are a model between reliable and lossy queues. So, these monoids generalize the (reliable) queue monoid~\cite{HusKZ17} and the lossy queue monoid~\cite{Koe16}. While many decision problems like universality, equivalence, or emptiness of intersection 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. To give a Kleene-type characterization of the recognizable sets in the plq monoid we use an approach like the one by Ochma\'{n}ski~\cite{Och85}: we restrict multiplication and iteration in the construction of rational sets. By these restrictions and by allowing complementation we obtain precisely the class of recognizable sets. From these special rational expressions we can also obtain an MSO logic describing the recognizable subsets like in \cite{Bue60, Die95} for regular languages and recognizable trace languages, resp. Moreover, we show connections between star-free sets, aperiodic sets, and an FO logic in the plq monoid similar to the known results for aperiodic word and trace languages~\cite{Sch65, McNP71, DieR95}.