Approximation of CFL by Regular Languages for Concurrent Program Verification

Many problems related to verification of concurrent programs can be reduced to the non-empty intersection problem for context-free languages. Since the latter is an undecidable problem, a practical approach for solving the intersection problem is to convert it to a decidable problem of the non-empty intersection of a context-free language and a regular language. This is done by approximating one of the context-free languages in the intersection from above or from below by a regular language. We give an approximation technique from above by modeling a context-free language L in terms of linear integer inequalities and then obtaining the approximating regular language L´ ⊇ L by relaxing the linear inequalities such that each inequality involves at most one variable. Previous approximation techniques focused on approximation below. We also give an alternate technique with a finite-state automata based approach, where we start with an automata M which accepts a suitable finite-subset L₀ of L, and then extend M successively based on the pumping property of L till the language accepted by M contains L.