Language Equivalence is Undecidable in VASS with Restricted Nondeterminism

TL;DR

It is shown that the languages of two history-deterministic VASSs are equal if and only if each can simulate the other, which allows the undecidability to be extended to any equivalence relation between two-sided simulation and language equivalence.

Abstract

In this work, we extend undecidability of language equivalence for two-dimensional Vector Addition System with States (VASS) accepting by coverability condition. We show that the problem is undecidable even when one of the two-dimensional VASSs is deterministic and the other is history-deterministic. Moreover, we observe, that the languages of two history-deterministic VASSs are equal if and only if each can simulate the other. This observation allows us to extend the undecidability to any equivalence relation between two-sided simulation and language equivalence.

Figures (3)

• Figure 1: Example of the construction of $2$-VASSs $A$ and $B$ and auxiliary $2$-VASS $N$ from 2CM $M$. Effects on the counters corresponds to letters except from two transitions: the first transition from $q_{1_B}$ to $q_{1_B}'$ which decrements second counter by $1$ and the second transition from $q_{1_B}'$ to $q_{f_A}^B$ which increments second counter by $1$.
• Figure 2: Situation in $A$ on the left and situation in $B$ on the right. $X_i -=1$ and $X_i+=1$ means respectively decrementing and incrementing $i$-th counter by one.
• Figure 3: Situation in VASS $B$. We have that $q_1'$ comes from $A$ and was created as a copy of state $q_3$ which is a copy of the same state of $N$ as $q_2'$. Labels $X_i -=1$ and $X_i+=1$ mean decrementing and incrementing $i$-th counter by one, respectively

Theorems & Definitions (15)

• Theorem 1
• proof
• Lemma 2
• proof
• Corollary 3
• proof
• Corollary 4
• proof
• Corollary 5
• proof