Regular Separability in Büchi VASS

2023/01/26 by Pascal Baumann, Baumann, Pascal, Roland Meyer +3
Biochemistry, Genetics and Molecular Biology · Computer Science · #Algorithms and Data Compression #DNA and Biological Computing #F.1.1 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2301.11242

openalex publication_date 2023/01/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We study the (ω-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages L₁ and L₂, check whether there is a regular language that fully contains L₁ while remaining disjoint from L₂. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from L₂. Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of L₁. Finally, we show how to symbolically represent inseparability witnesses and how to check their existence.

Related

• Regular Separability and Intersection Emptiness are Independent Problems
• Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities
• Separating regular languages by piecewise testable and unambiguous languages
• The separation problem for regular languages by piecewise testable languages
• An Approach to Regular Separability in Vector Addition Systems