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

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

doi:10.1016/j.tcs.2016.01.026

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 journal › Article › Research › peer-review

1 Citation (Scopus)

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 language	English
Pages (from-to)	1-24
Number of pages	24
Journal	Theoretical Computer Science
Volume	625
DOIs	https://doi.org/10.1016/j.tcs.2016.01.026
Publication status	Published - 25 Apr 2016
Externally published	Yes

Keywords

Abstraction refinement
Context-free languages
Regular approximation
Separability

Access to Document

10.1016/j.tcs.2016.01.026

Cite this

@article{46c0d21209774c2b88c7dcfdef9d4ee8,

title = "A complete refinement procedure for regular separability of context-free languages",

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.",

keywords = "Abstraction refinement, Context-free languages, Regular approximation, Separability",

author = "Graeme Gange and Navas, {Jorge A.} and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",

year = "2016",

month = apr,

day = "25",

doi = "10.1016/j.tcs.2016.01.026",

language = "English",

volume = "625",

pages = "1--24",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

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

AU - Gange, Graeme

AU - Navas, Jorge A.

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

PY - 2016/4/25

Y1 - 2016/4/25

N2 - 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.

AB - 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.

KW - Abstraction refinement

KW - Context-free languages

KW - Regular approximation

KW - Separability

UR - http://www.scopus.com/inward/record.url?scp=84960346910&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2016.01.026

DO - 10.1016/j.tcs.2016.01.026

M3 - Article

AN - SCOPUS:84960346910

SN - 0304-3975

VL - 625

SP - 1

EP - 24

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

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

Abstract

Keywords

Access to Document

Other files and links

Cite this