Regular separability complexity clarified for bidirected vector systems

Regular Separability for Bidirected VASS

Formal Languages and Automata Theory

Summary

The paper studies a problem about deciding if there’s a simple pattern (a regular language) that can separate the behaviors of two complex systems called bidirected VASS. The authors show that for general bidirected VASS, the problem is very hard to solve, but for a special kind where the input letters reveal the bidirected nature, the problem is easier and matches the difficulty of a known big-complexity class. They also find even simpler cases where the problem is efficiently solvable. However, if certain extra tests are allowed, the problem becomes impossible to decide. These findings help understand the limits of automatically checking and separating behaviors in these mathematical models.

What this means in practice

A theory result. No direct application yet.

Authors

Łukasz Orlikowski, Georg Zetzsche

Abstract

The regular separability problem asks, given two languages, whether there exists a regular language that contains one of them and is disjoint from the other. We study regular separability for bidirected VASS. We first show that the problem remains Ackermann-complete when the input consists of two languages recognised by bidrected VASS. To find a subclass of VASS in which the problem has lower complexity we define alphabetically bidirected VASS as ones where bidirectedness is also visible in the input letters. Our main result establishes that regular separability for alphabetically bidirected VASS is EXPSPACE-complete. The key to this result is that, in this setting, regular separability coincides with disjointness. As a first ingredient in this equivalence, we also show that for alphabetically bidirected Z-VASS, regular separability and disjointness are equivalent. Consequently, regular separability for these systems is in polynomial-time. In fact, it is log-space inter-reducible with non-solvability of integer linear Diophantine equation systems. Finally, we observe that the picture changes dramatically in the presence of a zero test, namely, we show that regular separability for alphabetically bidirected one-counter automata is undecidable.
View PDFOpen arXiv