Bounded underapproximations

作     者：Ganty, Pierre Majumdar, Rupak Monmege, Benjamin 

作者机构：ENS Cachan CNRS LSV F-94235 Cachan France INRIA F-94235 Cachan France Fac Informat UPM IMDEA Software Madrid 28660 Spain MPI SWS D-67663 Kaiserslautern Germany UC Los Angeles Los Angeles CA USA 

出 版 物：《FORMAL METHODS IN SYSTEM DESIGN》 (系统设计中的形式方法)

年 卷 期：2012年第40卷第2期

页      面：206-231页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：NSF [CCF-0546170, CCF-0702743] DARPA [HR0011-09-1-0037] Comunidad de Madrid [S2009TIC-1465] PEOPLE-COFUND's program AMAROUT [PCOFUND-2008-229599] Spanish Ministry of Science and Innovation [TIN2010-20639] 

主　　题：Context-free grammar Bounded languages Parikh-boundedness Multithreaded reachability Recursive counter machines 

摘      要：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 subset of 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)...w(m)* for some w(1),...,w(m) is an element of Sigma*. 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-N that has the same Parikh image as 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 iteratof underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w is an element of 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 *** the construction, we get a semi-algorithm for the original problems that constructs a sequence