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

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Contribution to journalArticleResearchpeer-review

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 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 procedures, and demonstrate their practicality on a range of verification and language-theoretic instances.

Original languageEnglish
Pages (from-to)1-24
Number of pages24
JournalTheoretical Computer Science
Volume625
DOIs
Publication statusPublished - 25 Apr 2016
Externally publishedYes

Keywords

  • Abstraction refinement
  • Context-free languages
  • Regular approximation
  • Separability

Cite this