Finite-state abstractions of infinite-state systems

Introduction

The algorithmic analysis of infinite-state systems is a central topic of theoretical computer science that is part of a popular approach to software verification. While analyzing infinite-state systems is indispensable when verifying software, finite-state systems are far better understood and permit much more efficient analysis.

Project Goals

In this project, I will pursue fundamental questions that arise when we want to abstract infinite-state systems by finite-state systems. The goal is 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.

Broader Impact

In addition to directly attacking well-known deep open problems regarding these fundamental questions, the project will also develop methods that will likely be crucial for resolving further major open problems in infinite-state systems. Moreover, the obtained results would have immediate implications for software verification in settings that combine recursion with concurrency, which is a notoriously difficult task.