Bisimilarity in Fresh-Register Automata

DOI10.1109/LICS.2015.24zbMATH Open1401.68164arXiv2005.06411MaRDI QIDQ4635800FDOQ4635800

Authors: Andrzej S. Murawski, S. J. Ramsay, Nikos Tzevelekos 

Publication date: 23 April 2018

Published in: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2005.06411

Recommendations

• On-the-fly bisimilarity checking for fresh-register automata
• Bisimulation of automata
• Fresh-register automata
• Bisimulations for fuzzy automata
• Bisimulations and behaviour of nondeterministic automata
• scientific article; zbMATH DE number 2020181
• On symmetric higher-dimensional automata and bisimilarity
• Bisimulation Equivalence of First-Order Grammars
• An efficient algorithm for computing bisimulation equivalence
• Polynomial-time equivalence testing for deterministic fresh-register automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Cited In (4)

• Polynomial-time equivalence testing for deterministic fresh-register automata
• On-the-fly bisimilarity checking for fresh-register automata
• Fast computations on ordered nominal sets
• Synthesis of Data Word Transducers

This page was built for publication: Bisimilarity in Fresh-Register Automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635800)