Verification, being able to ensure that a piece of software is correct, is both essential to today’s world, and very tedious to do by hand. One of the main goals of theoretical computer science is to address this problem by automating the verification process. Unfortunately, as Turing’s famous result shows, it is impossible to develop a complete algorithm for this purpose. Verifying even the simplest properties of a conventional computer program, e.g. whether it terminates, is undecidable. Even in the face of this undecidability barrier, all hope is not lost: The field of theoretical computer science has developed various approaches to overcome this barrier. One approach is to model the given program as an infinite state system that is weaker than a Turing machine, while still faithfully capturing the aspect we wanted to verify. The research area of infinite state verification aims to develop algorithms for such weaker systems, or show that this is impossible for a given model. As Turing’s undecidability result mandates, these algorithms are guaranteed to be incomplete when translated to the general setting of computer programs. However, an algorithm for such an infinite state system still teaches us an important lesson: how handle the aspects of infinity captured by the system, in a finite way. This lays the groundwork for the future development of practical algorithms that handle these aspects well. Even the negative results, be it undecidability or computational lower bounds, expand our understanding of computation, and its limits. In our institute, we are particularly interested in infinite state systems that model concurrent or recursive behavior, such as well-structured transition systems (WSTS), vector addition systems (VAS), and (higher-order) pushdown systems. We aim to develop algorithms for language theoretical questions (e.g. emptiness, separability, ...) concerning these systems.
For a given infinite state system, the simplest question that can be asked is whether its language is empty, i.e. "Does the given system have an accepting run?". This question can already be algorithmically anwsered for many popular infinite state systems (e.g. vector addition systems under coverability and reachability acceptance conditions, WSTS, pushdown systems). However, this is not the only question that can be asked of such systems. A deeper question is separability, i.e. "Are the languages of two given systems separable?". Interestingly, the insights developed to solve emptiness problems seem to fall short when it comes to separability, the problem requires a deeper understanding. Solving the separability problem also comes with practical benefits, as the insights developed for separability lend themselves well to abstraction-refinement approaches. Our aim is to develop the necessary tools to tackle the separability problem in the context of various systems.
A selection of our work:
(LICS 2024) On the Separability Problem of VASS Reachability Languages, by Eren Keskin, and Roland Meyer
(ICALP 2024) Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities, by Pascal Baumann, Eren Keskin, Roland Meyer, and Georg Zetzsche
(STACS 2023) Regular Separability in Büchi VASS, by Pascal Baumann, Roland Meyer, and Georg Zetzsche
(CONCUR 2018) Regular Separability of Well-Structured Transition Systems, by Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan
Roland Meyer, Eren Keskin