The Library
Bisimilarity in fresh-register automata
Tools
Tools
Tools
Murawski, Andrzej S., Ramsay, Steven J. and Tzevelekos, Nikos (2015) Bisimilarity in fresh-register automata. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Kyoto, 6-10 Jul 2015. Published in: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science LICS 2015 pp. 156-167. doi:10.1109/LICS.2015.24 ISSN 1043-6871.
|
PDF
WRAP_1271755-cs-010416-ra-bisim.pdf - Accepted Version - Requires a PDF viewer. Download (700Kb) | Preview |
Official URL: http://dx.doi.org/10.1109/LICS.2015.24
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 in equivalence 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.
| Item Type: | Conference Item (Paper) | ||||||
|---|---|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
| Library of Congress Subject Headings (LCSH): | Bisimulation, Group theory | ||||||
| Journal or Publication Title: | 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science LICS 2015 | ||||||
| Publisher: | IEEE | ||||||
| ISSN: | 1043-6871 | ||||||
| Book Title: | 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science | ||||||
| Official Date: | 2015 | ||||||
| Dates: |
|
||||||
| Page Range: | pp. 156-167 | ||||||
| DOI: | 10.1109/LICS.2015.24 | ||||||
| Status: | Peer Reviewed | ||||||
| Publication Status: | Published | ||||||
| Access rights to Published version: | Restricted or Subscription Access | ||||||
| Date of first compliant deposit: | 8 April 2016 | ||||||
| Date of first compliant Open Access: | 8 April 2016 | ||||||
| Funder: | Engineering and Physical Sciences Research Council (EPSRC), Royal Academy of Engineering (Great Britain) | ||||||
| Grant number: | EP/J019577/1 (EPSRC) | ||||||
| Conference Paper Type: | Paper | ||||||
| Title of Event: | 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | ||||||
| Type of Event: | Other | ||||||
| Location of Event: | Kyoto | ||||||
| Date(s) of Event: | 6-10 Jul 2015 |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
