2014/11/19 by Graeme Gange, Jorge A. Navas, Gange, Graeme +8
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #cs.FL
paper · pdf · doi:10.48550/arxiv.1411.5131
arxiv created 2014/11/19 · openalex publication_date 2014/11/19 · arxiv updated 2014/11/20 · openalex created_date 2022/10/03 · openalex updated_date 2026/07/28
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.