FINABIS · Finite-state abstractions of infinite-state systems

The algorithmic analysis of infinite-state systems is a central topicof theoretical computer science that is part of a popular approach tosoftware verification. While analyzing infinite-state systems isindispensable when verifying software, finite-state sytems are farbetter understood and permit much more efficient analysis. In thisproject, I will pursue fundamental questions that arise when we wantto abstract infinite-state systems by finite-state systems. The goalis to understand two types of problems:1. Separability problems: Given two infinite-state systems, can we find a finite-state overapproximation of the first system whose behaviors are disjoint from those of the second system? Separability is a basic task for synthesizing certificates for disjointness and therefore safety properties in concurrent systems.2. Closure computation. There are several non-constructive results that guarantee the existence of finite-state overapproximations of infinite-state systems that preserve some particular information. We are interested in how to compute these overapproximations effectively and efficiently. Examples include downward closures and upward closures with respect to the (scattered) subword ordering. Efficient procedures for closure computation would have immediate implications for infinite-state verification tasks that combine recursion with concurrency.In addition to directly attacking well-known deep open problemsregarding these fundamental questions, the project will also developmethods that will likely be crucial for resolving further major openproblems in infinite-state systems. Moreover, the obtained resultswould have immediate implications for software verification insettings that combine recursion with concurrency, which is anotoriously difficult task.