Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata

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

Thumbnail PDF


  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Andrzej S. Murawski
  • University of Oxford, UK
Steven J. Ramsay
  • University of Bristol, UK
Nikos Tzevelekos
  • Queen Mary University of London, UK

Cite AsGet BibTex

Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 72:1-72:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Register automata are one of the most studied automata models over infinite alphabets. The complexity of language equivalence for register automata is quite subtle. In general, the problem is undecidable but, in the deterministic case, it is known to be decidable and in NP. Here we propose a polynomial-time algorithm building upon automata- and group-theoretic techniques. The algorithm is applicable to standard register automata with a fixed number of registers as well as their variants with a variable number of registers and ability to generate fresh data values (fresh-register automata). To complement our findings, we also investigate the associated inclusion problem and show that it is PSPACE-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • automata over infinite alphabets
  • language equivalence
  • bisimilarity
  • computational group theory


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. F. Aarts, P. Fiterau-Brostean, H. Kuppens, and F. W. Vaandrager. Learning register automata with fresh value generation. In Proceedings of ICTAC, volume 9399 of Lecture Notes in Computer Science, pages 165-183. Springer, 2015. Google Scholar
  2. L. Babai. On the length of subgroup chains in the symmetric group. Communications in Algebra, 14(9):1729-1736, 1986. Google Scholar
  3. M. Bojańczyk, B. Klin, and S. Lasota. Automata theory in nominal sets. LMCS, 10(3), 2014. Google Scholar
  4. B. Bollig, P. Habermehl, M. Leucker, and B. Monmege. A robust class of data languages and an application to learning. Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  5. S. Cassel, F. Howar, B. Jonsson, and B. Steffen. Active learning for extended finite state machines. Formal Asp. Comput., 28(2):233-263, 2016. Google Scholar
  6. M. L. Furst, J. E. Hopcroft, and E. M. Luks. Polynomial-time algorithms for permutation groups. In Proceedings of FOCS, pages 36-41. IEEE Computer Society, 1980. Google Scholar
  7. R. Grigore, D. Distefano, R. L. Petersen, and N. Tzevelekos. Runtime verification based on register automata. In Proceedings of TACAS, LNCS. Springer, 2013. Google Scholar
  8. J. E. Hopcroft and R. M. Karp. A linear algorithm for testing equivalence of finite automata. Technical Report 114, Cornell University, 1971. Google Scholar
  9. M. Kaminski and N. Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  10. D. E. Knuth. Efficient representation of perm groups. Combinatorica, 11(1):33-43, 1991. Google Scholar
  11. M. Leucker. Learning meets verification. In Proceedings of FMCO, volume 4709 of Lecture Notes in Computer Science, pages 127-151, 2007. Google Scholar
  12. J. Moerman, M. Sammartino, A. Silva, B. Klin, and M. Szynwelski. Learning nominal automata. In Proceedings of POPL, pages 613-625. ACM, 2017. Google Scholar
  13. A. S. Murawski, S. J. Ramsay, and N. Tzevelekos. Bisimilarity in fresh-register automata. In Proceedings of LICS, pages 156-167, 2015. Google Scholar
  14. A. S. Murawski and N. Tzevelekos. Algorithmic nominal game semantics. In Proceedings of ESOP, volume 6602 of Lecture Notes in Computer Science, pages 419-438. Springer-Verlag, 2011. Google Scholar
  15. F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. Google Scholar
  16. H. Sakamoto. Studies on the Learnability of Formal Languages via Queries. PhD thesis, Kyushu University, 1998. Google Scholar
  17. H. Sakamoto and D. Ikeda. Intractability of decision problems for finite-memory automata. Theor. Comput. Sci., 231(2):297-308, 2000. Google Scholar
  18. T. Schwentick. Automata for XML - A survey. J. Comput. Syst. Sci., 73(3):289-315, 2007. Google Scholar
  19. N. Tzevelekos. Full abstraction for nominal general references. Logical Methods in Computer Science, 5(3), 2009. Google Scholar
  20. N. Tzevelekos. Fresh-register automata. In Proceedings of POPL, pages 295-306. ACM Press, 2011. Google Scholar
  21. F. W. Vaandrager. Model learning. Commun. ACM, 60(2):86-95, 2017. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail