
Evènement pour le groupe Modélisation et Verification
Date  20121206 10:1511:15 
Titre  A perfect model for bounded verification 
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 contextfree languages is undecidable, no class containing them can be perfect.In practice, verification problems for language classes that are not perfect are often underapproximated 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. 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 multihead pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We also show that bounded languages form a maximal class for which perfection is obtained. We show that computations of several known models of systems, such as recursive multithreaded programs, recursive counter machines, and communicating finitestate machines can be encoded as multihead pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages. 
Lieu  Salle Patio  Bat C4 "Hautcarré" 
Orateur  Javier Esparza 
Url  TUM, Germany 
Aucun document lié à cet événement. RetourRetour à l'index
 