Chennai Mathematical Institute

Seminars




1:15 pm, Lecture Hall 6
PUBLIC VIVA-VOCE NOTIFICATION
Subwords: Automata, Embedding Problems, and Verification

Prateek Karandikar
Chennai Mathematical Institute.
12-02-15


Abstract

The increasing use of software and automated systems has made it important to ensure their correct behaviour. Bugs can not only have significant financial costs, but also catastrophic consequences in mission-critical systems. Testing against a variety of environments and inputs helps with discovering bugs, but cannot guarantee their absence. Formal verification is the technique that establishes correctness of a system or a mathematical model of the system with respect to properties expressed in a formal language.

Regular model checking is a common technique for verification of infinite-state systems - it represents infinite sets of configurations symbolically in a finite manner and manipulates them using these representations. Regular model checking for lossy channel systems (LCS) brings up basic automata-theoretic questions concerning the subword relation on words which models the lossiness of the channels. We address these state complexity and decision problems, and also solve a long-standing problem involving the index of the Simon’s piecewise-testability congruence. The reachability problem for lossy channel systems, though decidable, has very high complexity (it is $F_{\omega_\omega}$-complete), well beyond primitive-recursive. In recent times several problems with this complexity have been discovered, for example in the fields of verification of weak memory models and metric temporal logic. The Post Embedding Problem (PEP) is an algebraic abstraction of the reachability problem on LCS, with the same complexity, and is our champion for a “master” problem for the class $F_{\omega_\omega}$. We provide a common generalization of two known variants of PEP and give a simpler proof of decidability. This allows us to extend the unidirectional channel system (UCS) model with simple channel tests while having decidable reachability.