Bounded Underapproximations

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

′ ⊆ 

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

$w_1^*w_2^*\cdots w_k^*$

for some

$w_1,\ldots,w_k\in\Sigma^*$

. In particular bounded 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

L

N

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

L

N

.

As an application of this result in model checking, we show how to underapproximate the reachable state space of multithreaded procedural programs. The bounded language constructed above provides a decidable underapproximation for the original problem. 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

 ∈ 

L

is in some underapproximation of the sequence, and hence, a program bug is guaranteed to be found. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded programs.