10 papers
The complexity of downward closures of indexed languages
Richard Mandel, Corto Mascle, Georg Zetzsche
Indexed languages are a classical notion in formal language theory, which has attracted attention in recent decades due to its role in higher-order model checking: They are precise…
Infinite-state Games with Energy Objectives Beyond Counters
Irmak SaÄlam, Georg Zetzsche
In the theory of games on infinite-state arenas, there is a stark contrast between (i) recursion-based models such as pushdown systems and extensions on one hand, and (ii) counter-…
The Counting Power of Transformers
Marco Sälzer, Chris Köcher, Alexander Kozachinskiy +2
Counting properties (e.g. determining whether certain tokens occur more than other tokens in a given input text) have played a significant role in the study of expressiveness of tr…
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Kilian Lichtner, Pascal BergsträÃer, Moses Ganardi +2
Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques,…
Bounded treewidth, multiple context-free grammars, and downward closures
C. Aiswarya, Pascal Baumann, Prakash Saivasan +2
The reachability problem in multi-pushdown automata (MPDA) has many applications in static analysis of recursive programs. An example is safety verification of multi-threaded recur…
The complexity of separability for semilinear sets and Parikh automata
Elias Rojas Collins, Chris Köcher, Georg Zetzsche
In a \emph{separability problem}, we are given two sets and from a class , and we want to decide whether there exists a set from a class such…