- 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'⊆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*for some_{1}^{*}w_{2}^{*}... w_{m}^{*}*w*Σ_{1},...,w_{m}∈. In particular bounded context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, we give a new construction that shows that each context free language^{*}*L*has a subset*L*that has the same Parikh image as_{N}*L*and that can be represented as a sequence of substitutions on a linear language. Second, we inductively construct a Parikh-equivalent bounded context-free subset of*L*._{N}

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∈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.

@article{GMM-fmsd2012, | ||

author = |
{Ganty, Pierre and Majumdar, Rupak and Monmege, Benjamin}, | |

DOI = |
{10.1007/s10703-011-0136-y}, | |

journal = |
{Formal Methods in System Design}, | |

month = | apr,
| |

number = | {2},
| |

pages = |
{206-231}, | |

publisher = |
{Springer}, | |

title = |
{Bounded underapproximations}, | |

url = |
{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMM-fmsd12.pdf},
| |

volume = |
{40}, | |

year = |
{2012}, | |

} |

- Private Pages
- RSS of the latest LSV publications
- Page maintained by Nicolas Markey.