A Complete Refinement Procedure for Regular Separability of Context-Free Languages

TL;DR

This paper introduces a semi-decision procedure for determining if two context-free languages can be separated by a regular language, utilizing counter-example guided refinement methods, and demonstrates its practical effectiveness.

Contribution

It presents a novel refinement procedure for regular separability of context-free languages, including both incomplete and complete methods, with experimental validation.

Findings

The semi-decision procedure effectively distinguishes separable languages.

The complete refinement method guarantees correctness but is more computationally intensive.

Experimental results show practical applicability on verification problems.

Abstract

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 an effective semi-decision procedure for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two refinement methods, one inexpensive but incomplete, and the other complete but more expensive. We provide an experimental evaluation of this procedure, and demonstrate its practicality on a range of verification and language-theoretic instances.