Record #343625 - GSI Repository

FINABIS

Finite-state abstractions of infinite-state systems

Grant period	2023-01-01 - 2027-12-31
Funding body	European Union
Call number	ERC-2022-STG
Grant number	101077902
Identifier	G:(EU-Grant)101077902

Note: 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.

Recent Publications

There are no publications

Record created 2023-08-27, last modified 2023-08-27

Similar records

Add to personal basket
Export as Author List with IDs BibTeX (UTF-8), EndNote XML, EndNote Text, RIS, MARC, Print MARC, MARCXML, DC,
Request correction
Submit fulltext

GSI Homepage \| GSI Library \| English Deutsch \| guest :: login GSI Repository
Search	Submit	Personalize Your alerts Your baskets Your searches	Help