A perfect model for bounded verification

DOI10.1109/LICS.2012.39MaRDI QIDQ2986805zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

verificationalgorithmscomplexityformal languagesunderapproximation

Mathematics Subject Classification ID

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

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.

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

Cited in

(15)

• Bounded context switching for valence systems
• A perfect class of context-sensitive timed languages
• scientific article; zbMATH DE number 7561313 (Why is no real title available?)
• Reachability analysis of reversal-bounded automata on series-parallel graphs
• Verification of Flat FIFO Systems
• scientific article; zbMATH DE number 7471708 (Why is no real title available?)
• 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

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)