Bisimilarity in fresh-register automata

TL;DR

This work provides a unified complexity landscape for bisimilarity over automata on infinite alphabets, covering both register and fresh-register systems under all major discipline variations (duplication, emptiness, and freshness). It introduces a robust symbolic-bisimulation framework and leverages permutation-group theory to obtain tight $EXPTIME$ upper and lower bounds for the general case, while showcasing $PSPACE$-completeness for single-assignment-no-erasure and $NP$-completeness for single-assignment-with-filled-registers in deterministic settings. The results close gaps in language-equivalence complexity for deterministic finite-memory like models and reveal a sharp boundary: freshness per se does not alter the complexity class, but erasure and pushdown storage can dramatically change decidability. The paper also demonstrates the practical utility of group-theoretic methods for reasoning about symmetries in bisimulation relations, and connects these findings to longstanding conjectures and undecidability results in the presence of pushdown storage. Collectively, the contributions advance the theory of automata over infinite alphabets and provide concrete complexity characterizations for a broad spectrum of bisimilarity problems.

Abstract

Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies. Furthermore, they enable a highly succinct representation of the corresponding bisimulations. By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines. In each case, we find that freshness does not affect the complexity class of the problem. The results allow us to close a complexity gap for language equivalence of deterministic register automata. We show that deterministic language inequivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto. Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.

Figures (4)

• Figure 1: Relationship between the main bisimilarity problems considered in this work.
• Figure 2: Alternating algorithm determining whether Attacker wins the $N$-bisimulation game.
• Figure 3: Encoding of a bounded tape of length $9$ (top) using $18$ registers (bottom, registers 2-19). The first register stores an auxiliary name which is used in the reduction of ALBA-Mem to $\boldsymbol{\sim}$-RA($S\#$).
• Figure 4: Defender forcing gadget $\mathsf{DF}(p_1,p_2,\ell,\ell_1,\ell_2,q_1,q_2,q'_1,q'_2)$. Labels $\ell_1$ and $\ell_2$ must be semantically distinct.

Theorems & Definitions (64)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Remark 2.4
• Definition 2.5
• Lemma 2.6
• proof
• Lemma 2.7
• proof
• Theorem 3.1