A complete refinement procedure for regular separability of context-free languages
From MaRDI portal
Publication:264992
DOI10.1016/J.TCS.2016.01.026zbMATH Open1338.68147arXiv1411.5131OpenAlexW1528946883WikidataQ57664979 ScholiaQ57664979MaRDI QIDQ264992FDOQ264992
Peter Schachte, Harald Søndergaard, Peter J. Stuckey, Graeme Gange, Jorge Navas
Publication date: 1 April 2016
Published in: Theoretical Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1411.5131
Recommendations
- On the separability of sparse context-free languages and of bounded rational relations
- Verified Decision Procedures on Context-Free Grammars
- A Note on Decidable Separability by Piecewise Testable Languages
- On separation by locally testable and locally threshold testable languages
- Separating regular languages by locally testable and locally threshold testable languages
Cites Work
- A uniform framework for problems on context-free grammars
- Title not available (Why is that?)
- Regular approximation of CFLs: A grammatical view
- A generic approach to the static analysis of concurrent programs with procedures
- HTML Validation of Context-Free Languages
- Analyzing Context-Free Grammars Using an Incremental SAT Solver
- Visibly pushdown languages
- On the Decidability of Grammar Problems
- Title not available (Why is that?)
- Horn clauses as an intermediate representation for program analysis and transformation
- Nested interpolants
- Unbounded Model-Checking with Interpolation for Regular Language Constraints
- XML Validation for Context-Free Grammars
- Complexity of pattern-based verification for multithreaded programs
- Bounded Algol-Like Languages
- On Decompositions of Regular Events
- Tools and Algorithms for the Construction and Analysis of Systems
Cited In (4)
Uses Software
This page was built for publication: A complete refinement procedure for regular separability of context-free languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q264992)
