A complete refinement procedure for regular separability of context-free languages
| Autor: | Harald Søndergaard, Peter J. Stuckey, Graeme Gange, Peter Schachte, Jorge A. Navas |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
FOS: Computer and information sciences
Class (computer programming) Theoretical computer science General Computer Science Formal Languages and Automata Theory (cs.FL) Programming language Context-free language Computer Science - Formal Languages and Automata Theory 020207 software engineering 02 engineering and technology computer.software_genre Theoretical Computer Science Separable space Range (mathematics) Completeness (order theory) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Abstraction refinement computer Software verification Mathematics Abstraction (linguistics) |
| Zdroj: | Theoretical Computer Science. 625:1-24 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/j.tcs.2016.01.026 |
| Popis: | 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. We give a novel semi-decision procedure for regular separability of CFLs.The procedure makes use of counter-example guided abstraction refinement.It halts for pairs of CFLs that either overlap or are regularly separable.We show the method's utility on practical software verification tasks. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect