A recent doctoral thesis has brought to light a novel algorithmic framework focussing on the inclusion of infinite-word languages, a fundamental problem in automata theory and applications in the broader field of software verification.
IMDEA Software researcher Kyveli Doveri, supervised by Pierre Ganty, presented her doctoral thesis: “A Uniform Approach to Language Containment Problems” last Friday, February 16 at the ETSIINF of the Polytechnic University of Madrid.
Context
In an increasingly digitized world, software verification is a crucial aspect of software development that ensures the correctness, reliability, and quality of software systems. It involves the process of checking whether a software system meets its specified requirements and behaves as expected under various conditions. Furthermore, in the realm of theorem proving, particularly within formal methods and automated reasoning, understanding formal languages that describe system behaviors or properties becomes imperative. These languages serve as a foundation for expressing and reasoning about complex system properties, making the language inclusion problem a vital tool for verifying intricate theorems and ensuring the integrity of formal proofs.
Thesis
Kyveli’s research focuses on developing computational tools to solve language inclusion problems for formal languages.
The IMDEA Software researcher has developed algorithms for decidable cases of inclusion between Büchi automata, a challenge known for its complexity. These algorithms, such as BAIT and FORKLIFT, are based on quasiorder relations to optimize the search for counterexamples, which makes it a valuable tool for software verification. Central to their efficacy is a fixed-point characterization of the languages, which allows them to manipulate finite sets of states efficiently.
In addition, the thesis establishes a theorem similar to the Myhill-Nerode theorem for specific subclasses of timed languages accepted by one-clock timed automata. This advance is fundamental to a better understanding of the properties of regular languages and has important implications for the practical modeling of computer systems.
In short, these new algorithms and theorems not only extend our theoretical understanding, but also have the potential to positively impact diverse areas of computer science, from program verification to theorem proving in word combinatorics. A step forward in the age of automated computing.
