Georg Zetzsche

Highlights Conference 2025 Conference Abstract

A complexity dichotomy for reaching semilinear sets in integer 1-VASS

• Georg Zetzsche

KR Conference 2025 Conference Paper

Presburger Functional Synthesis: Complexity and Tractable Normal Forms

• S. Akshay
• A. R. Balasubramanian
• Supratik Chakraborty
• Georg Zetzsche

Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs satisfying the relation. Recently, a rich line of work has emerged tackling this problem for specifications in different theories, from Boolean to general first-order logic. In this paper, we launch an investigation of this problem for the theory of Presburger Arithmetic, that we call Presburger Functional Synthesis (PFnS). We show that PFnS can be solved in EXPTIME and provide a matching exponential lower bound. This is unlike the case for Boolean functional synthesis (BFnS), where only conditional exponential lower bounds are known. Further, we show that PFnS for one input and one output variable is as hard as BFnS in general. We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS. We prove several properties of PSyNF, including how to check and compile to this form, and conditions under which any other form that guarantees poly-time solvability of PFnS can be compiled in poly-time to PSyNF. Finally, we identify a syntactic normal form that is easier to check but is exponentially less succinct than PSyNF.

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.

Highlights Conference 2024 Conference Abstract

Inclusion problems for formal languages

• Georg Zetzsche

It is a classic phenomenon in formal language theory that inclusion between languages is hard to decide: For context-free languages, it is undecidable, and already for NFAs, the problem is PSPACE-complete. However, recent work by various authors has shown that under some restrictions on the input languages, deciding inclusion is surprisingly tractable and admits interesting new techniques. The talk will survey such results (and open problems), with a focus on non-regular languages.

Highlights Conference 2024 Conference Abstract

Slice closures of indexed languages and word equations with counting constraints

• Georg Zetzsche

Indexed languages are a classical notion in formal language theory. As the language equivalent of second-order pushdown automata, they have received considerable attention in higher-order model checking. Unfortunately, counting properties are notoriously difficult to decide for indexed languages: So far, all results about non-regular counting properties show undecidability. In this paper, we initiate the study of slice closures of (Parikh images of) indexed languages. A slice is a set of vectors of natural numbers such that membership of u, u+v, u+w implies membership of u+v+w. Our main result is that given an indexed language L, one can compute a semilinear representation of the smallest slice containing L's Parikh image. We present two applications. First, one can compute the set of all affine relations satisfied by the Parikh image of an indexed language. In particular, this answers affirmatively a question by Kobayashi: Is it decidable whether in a given indexed language, every word has the same number of a's as b's. As a second application, we show decidability of (systems of) word equations with rational constraints and a class of counting constraints: These allow us to look for solutions where a counting function (defined by an automaton) is not zero. For example, one can decide whether a word equation with rational constraints has a solution where the number of occurrences of a differs between variables X and Y. The talk will present a paper accepted for LICS 2024, which is joint work with Laura Ciobanu. The paper is available at https: //arxiv. org/abs/2405. 07911

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.

MFCS Conference 2022 Conference Paper

Membership Problems in Finite Groups

• Markus Lohrey
• Andreas Rosowski
• Georg Zetzsche

We show that the subset sum problem, the knapsack problem and the rational subset membership problem for permutation groups are NP-complete. Concerning the knapsack problem we obtain NP-completeness for every fixed n ≥ 3, where n is the number of permutations in the knapsack equation. In other words: membership in products of three cyclic permutation groups is NP-complete. This sharpens a result of Luks [Eugene M. Luks, 1991], which states NP-completeness of the membership problem for products of three abelian permutation groups. We also consider the context-free membership problem in permutation groups and prove that it is PSPACE-complete but NP-complete for a restricted class of context-free grammars where acyclic derivation trees must have constant Horton-Strahler number. Our upper bounds hold for black box groups. The results for context-free membership problems in permutation groups yield new complexity bounds for various intersection non-emptiness problems for DFAs and a single context-free grammar.

Highlights Conference 2022 Conference Abstract

The Complexity of Bidirected Reachability in Valence Systems

• Georg Zetzsche

An infinite-state system is bidirected (sometimes called reversible) if for every transition, there exists another with opposite effect. We study reachability in bidirected systems in the framework of valence systems, an abstract model featuring finitely many control states and an infinite-state storage that is specified by a finite graph. Picking suitable graphs yields counters as in vector addition systems, pushdowns, integer counters, and combinations. We provide a comprehensive complexity analysis. For example, the complexity of bidirected reachability drops substantially (often to polynomial time) from that of general reachability, for almost every storage mechanism where general reachability is known to be decidable. This is joint work with Moses Ganardi and Rupak Majumdar. See https: //arxiv. org/abs/2110. 03654

Highlights Conference 2020 Conference Abstract

Extensions of -Regular Languages

• Georg Zetzsche

We consider extensions of monadic second-order logic over -words, which are obtained by adding one language that is not -regular. We show that if the added language has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the -regular languages are the only decidable Boolean-closed full trio over -words.

MFCS Conference 2020 Conference Paper

Knapsack and the Power Word Problem in Solvable Baumslag-Solitar Groups

• Markus Lohrey
• Georg Zetzsche

We prove that the power word problem for the solvable Baumslag-Solitar groups BS(1, q) = ⟨ a, t ∣ t a t^{-1} = a^q ⟩ can be solved in TC⁰. In the power word problem, the input consists of group elements g₁, …, g_d and binary encoded integers n₁, …, n_d and it is asked whether g₁^{n₁} ⋯ g_d^{n_d} = 1 holds. Moreover, we prove that the knapsack problem for BS(1, q) is NP-complete. In the knapsack problem, the input consists of group elements g₁, …, g_d, h and it is asked whether the equation g₁^{x₁} ⋯ g_d^{x_d} = h has a solution in ℕ^d.

Highlights Conference 2018 Conference Abstract

Unboundedness problems for languages of vector addition systems

• Georg Zetzsche

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 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. This is joint work with Wojciech Czerwiński and Piotr Hofman and has appeared in the proceedings of ICALP 2018.

MFCS Conference 2013 Conference Paper

Semilinearity and Context-Freeness of Languages Accepted by Valence Automata

• P. Buckheister
• Georg Zetzsche

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.