Bounded underapproximations

DOI10.1007/S10703-011-0136-YMaRDI QIDQ453533zbMATH OpenOpenAlexFDO

Authors Pierre Ganty, Benjamin Monmege, Rupak Majumdar

Publication date 27 September 2012

Published in Formal Methods in System Design (Search for Journal in Brave)

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

zbMATH Keywords

context-free grammarbounded languagesmultithreaded reachabilityParikh-boundednessrecursive counter machines

Mathematics Subject Classification ID

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

Abstract: We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L' included in L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w1*w2*...wk* for some finite words w1,...,wk. In particular bounded subsets of context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, using Newton's iterations on the language semiring, we construct a context-free subset Ls of L that can be represented as a sequence of substitutions on a linear language and has the same Parikh image as L. Second, we inductively construct a Parikh-equivalent bounded context-free subset of Ls. We show two applications of this result in model checking: to underapproximate the reachable state space of multithreaded procedural programs and to underapproximate the reachable state space of recursive counter programs. The bounded language constructed above provides a decidable underapproximation for the original problems. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w in L is in some underapproximation of the sequence. In addition, we show that our approach subsumes context-bounded reachability for multithreaded programs.

Recommendations

• A perfect model for bounded verification
• The language theory of bounded context-switching
• On bounded languages and reversal-bounded automata
• On bounded languages and reversal-bounded automata
• Bounded Parikh automata

Cites work

• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 3293666 (Why is no real title available?)
• A generic approach to the static analysis of concurrent programs with procedures
• Automated Technology for Verification and Analysis
• Bounded Algol-Like Languages
• CONCUR 2004 - Concurrency Theory
• Complexity of pattern-based verification for multithreaded programs
• Iterating Octagons
• Newtonian program analysis -- an introduction
• Newton’s Method for ω-Continuous Semirings
• Parikh's theorem: a simple and direct automaton construction
• Programs with Lists Are Counter Automata
• Some decision problems concerning semilinearity and commutation.
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• The context-freeness problem is coNP-complete for flat counter systems
• A perfect model for bounded verification
• Forward analysis and model checking for trace bounded WSTS
• Decidable models of integer-manipulating programs with recursive parallelism
• Unboundedness problems for languages of vector addition systems
• Finite automata for the sub- and superword closure of CFLs: descriptional and computational complexity

Describes a project that uses

Uses Software

• ALGOL 60

This page was built for publication: Bounded underapproximations

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