Advertisement

DEQ: Equivalence Checker for Deterministic Register Automata

  • A. S. MurawskiEmail author
  • S. J. Ramsay
  • N. Tzevelekos
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11781)

Abstract

Register automata are one of the most studied automata models over infinite alphabets with applications in learning, systems modelling and program verification. We present an equivalence checker for deterministic register automata, called DEQ, based on a recent polynomial-time algorithm that employs group-theoretic techniques to achieve succinct representations of the search space. We compare the performance of our tool to other available implementations, notably in the learning library RALib and nominal frameworks LOIS and NLambda.

Notes

Acknowledgment

Research funded by EPSRC (EP/J019577/1, EP/P004172/1).

References

  1. 1.
    Aarts, F., Fiterau-Brostean, P., Kuppens, H., Vaandrager, F.: Learning register automata with fresh value generation. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 165–183. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25150-9_11CrossRefGoogle Scholar
  2. 2.
  3. 3.
    Bollig, B., Habermehl, P., Leucker, M., Monmege, B.: A robust class of data languages and an application to learning. LMCS 10(4), (2014)Google Scholar
  4. 4.
    Cassel, S., Howar, F., Jonsson, B.: RALib: a LearnLib extension for inferring EFSMs. In: Proceedings of DIFTS (2015)Google Scholar
  5. 5.
    Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. Formal Asp. Comput. 28(2), 233–263 (2016) MathSciNetCrossRefGoogle Scholar
  6. 6.
    Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260–276. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_19CrossRefGoogle Scholar
  7. 7.
    Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical Report 114, Cornell University (1971)Google Scholar
  8. 8.
    Kaminski, M., Francez, N.: Finite-memory automata. TCS 134(2), 329–363 (1994)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Klin, B., Szynwelski, M.: SMT solving for functional programming over infinite structures. In: Proceedings of MSFP, EPTCS 207, pp. 57–75, 2016MathSciNetCrossRefGoogle Scholar
  10. 10.
    Kopczyński, E., Toruńczyk, S.: LOIS. In: Proceedings of POPL, pp. 586–598 (2017)Google Scholar
  11. 11.
  12. 12.
    Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: Proceedings of POPL, pp. 613–625 (2017)CrossRefGoogle Scholar
  13. 13.
    Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: A contextual equivalence checker for IMJ*. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 234–240. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-24953-7_19CrossRefzbMATHGoogle Scholar
  14. 14.
    Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: Polynomial-time equivalence testing for deterministic fresh-register automata. In: Proceedings of MFCS, pp. 72:1–72:14 (2018)Google Scholar
  15. 15.
    Murawski, A.S., Tzevelekos, N.: Algorithmic nominal game semantics. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 419–438. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19718-5_22CrossRefGoogle Scholar
  16. 16.
    Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403–435 (2004)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Sakamoto, H.: Studies on the Learnability of Formal Languages via Queries. PhD thesis, Kyushu University (1998)Google Scholar
  18. 18.
    Schwentick, T.: Automata for XML. J. Comput. Syst. Sci. 73(3), 289–315 (2007)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Sims, C.C.: Computational methods in the study of permutation groups. In: Computational Problems in Abstract Algebra, pp. 169–183. Pergamon, Oxford (1970)Google Scholar
  20. 20.
  21. 21.
    Tzevelekos, N.: Fresh-register automata. In: Proceedings of POPL, pp. 295–306 (2011)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.University of OxfordOxfordUK
  2. 2.University of BristolBristolUK
  3. 3.Queen Mary University of LondonLondonUK

Personalised recommendations