Bounded underapproximations

DOI10.1007/S10703-011-0136-YzbMATH Open1247.68140arXiv0809.1236OpenAlexW2914181030MaRDI QIDQ453533FDOQ453533

Pierre Ganty, Benjamin Monmege, Rupak Majumdar

Publication date: 27 September 2012

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

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.

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

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

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)

Cites Work

• Title not available (Why is that?)
• Some decision problems concerning semilinearity and commutation.
• A generic approach to the static analysis of concurrent programs with procedures
• Complexity of pattern-based verification for multithreaded programs
• Bounded Algol-Like Languages
• Title not available (Why is that?)
• CONCUR 2004 - Concurrency Theory
• Automated Technology for Verification and Analysis
• Title not available (Why is that?)
• Programs with Lists Are Counter Automata
• Parikh's theorem: a simple and direct automaton construction
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Newton’s Method for ω-Continuous Semirings
• Iterating Octagons

Cited In (4)

• Unboundedness Problems for Languages of Vector Addition Systems.
• Forward analysis and model checking for trace bounded WSTS
• Decidable models of integer-manipulating programs with recursive parallelism
• Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity

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)