A perfect model for bounded verification

DOI10.1109/LICS.2012.39zbMATH Open1362.68168arXiv1201.3194OpenAlexW2006337571MaRDI QIDQ2986805FDOQ2986805

Authors: Javier Esparza, Pierre Ganty, Rupak Majumdar 

Publication date: 16 May 2017

Published in: 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

Full work available at URL: https://arxiv.org/abs/1201.3194

Recommendations

• Bounded underapproximations
• Model-checking bounded multi-pushdown systems
• A perfect class of context-sensitive timed languages
• Budget-bounded model-checking pushdown systems
• Reachability of scope-bounded multistack pushdown systems

zbMATH Keywords

verificationalgorithmscomplexityformal languagesunderapproximation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (15)

• A perfect class of context-sensitive timed languages
• Title not available (Why is that?)
• Verification of Flat FIFO Systems
• Reachability analysis of reversal-bounded automata on series-parallel graphs
• Title not available (Why is that?)
• Unboundedness problems for machines with reversal-bounded counters
• Verification of flat FIFO systems
• Bounded underapproximations
• Unboundedness problems for languages of vector addition systems
• Parameterized verification under TSO with data types
• Coverability in 2-VASS with one unary counter is in NP
• Reachability analysis of reversal-bounded automata on series-parallel graphs
• Non axiomatisability of positive relation algebras with constants, via graph homomorphisms
• On the path-width of integer linear programming
• Bounded context switching for valence systems

This page was built for publication: A perfect model for bounded verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2986805)