Finite-state abstractions of infinite-state systems

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 sytems are far

better understood and permit much more efficient analysis. 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.

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.