*salle A. Turing CE4*

9 mai 2012 - 14h00

A Perfect Model for Bounded Verification

par Pierre Ganty de IMDEA (Madrid)

Résumé : A class of languages C is perfect if it is closed under

Boolean operations and the emptiness problem is decidable. Perfect

language classes are the basis for the automata-theoretic approach to

model checking: a system is correct if the language generated by the

system is disjoint from the language of bad traces. Regular languages

are perfect, but because the disjointness problem for CFLs is

undecidable, no class containing the CFLs can be perfect.

In practice, verification problems for language classes that are

not perfect are often under-approximated by checking if the property

holds for all behaviors of the system belonging to a fixed subset. A

general way to specify a subset of behaviors is by using bounded

languages (languages of the form w1* ... wk* for fixed words

w1,...,wk). A class of languages C is perfect modulo bounded languages

if it is closed under Boolean operations relative to every bounded

language, and if the emptiness problem is decidable relative to every

bounded language.

We consider finding perfect classes of languages modulo bounded

languages. We show that the class of languages accepted by multi-head

pushdown automata are perfect modulo bounded languages, and

characterize the complexities of decision problems. We show that

computations of several known models of systems, such as recursive

multi-threaded programs, recursive counter machines, and communicating

finite-state machines can be encoded as multi-head pushdown automata,

giving uniform and optimal underapproximation algorithms modulo

bounded languages.

[Joint work with Javier Esparza and Rupak Majumdar]