Journal article

A complete refinement procedure for regular separability of context-free languages

Graeme Gange, Jorge A Navas, Peter Schachte, Harald Sondergaard, Peter J Stuckey



Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present a class of semi-decision procedures for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two effective instances of this approach, one that is complete but relatively expensive, and one that is inexpensive and sound, but for which we do not have a completeness proof. The complete method will prove disjointness whenever the input languages are regularly separable. Both methods will terminate whenever the input languages overlap. We provide an experimental evaluation of these proced..

View full abstract


Awarded by Australian Research Council

Funding Acknowledgements

We wish to thank Pierre Ganty for fruitful discussions, and the anonymous reviewers for their detailed and very constructive feedback; the paper has been greatly improved as a result of these interactions. We also wish to thank Georgel Calin for providing the test programs and the implementation of LCEGAR. Finally we acknowledge support of the Australian Research Council through Linkage Project grant LP140100437.