Skip to main content
SpringerLink
Log in

DEQ: Equivalence Checker for Deterministic Register Automata

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The tool and its source are available at http://github.com/stersay/deq.

  2. 2.

    We used an unreleased implementation of the equivalence checking algorithm that was kindly communicated to us by F. Howar.

  3. 3.

    The encoding used for the comparison with RALib-EqCheck was slightly modified to reflect certain structural constraints imposed by that tool. This alternative encoding is larger and hence runtimes are not comparable with the other two experiments. Note that the timing data for RALib-EqCheck contains JVM start-up time.

References

  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_11

    Chapter  Google Scholar 

  2. Amos, D.: http://hackage.haskell.org/package/HaskellForMaths

  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. Cassel, S., Howar, F., Jonsson, B.: RALib: a LearnLib extension for inferring EFSMs. In: Proceedings of DIFTS (2015)

    Google Scholar 

  5. Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. Formal Asp. Comput. 28(2), 233–263 (2016)

    Article  MathSciNet  Google Scholar 

  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_19

    Chapter  Google Scholar 

  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. Kaminski, M., Francez, N.: Finite-memory automata. TCS 134(2), 329–363 (1994)

    Article  MathSciNet  Google Scholar 

  9. Klin, B., Szynwelski, M.: SMT solving for functional programming over infinite structures. In: Proceedings of MSFP, EPTCS 207, pp. 57–75, 2016

    Article  MathSciNet  Google Scholar 

  10. Kopczyński, E., Toruńczyk, S.: LOIS. In: Proceedings of POPL, pp. 586–598 (2017)

    Google Scholar 

  11. http://hackage.haskell.org/package/containers

  12. Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: Proceedings of POPL, pp. 613–625 (2017)

    Article  Google Scholar 

  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_19

    Chapter  MATH  Google Scholar 

  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. 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_22

    Chapter  Google Scholar 

  16. Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403–435 (2004)

    Article  MathSciNet  Google Scholar 

  17. Sakamoto, H.: Studies on the Learnability of Formal Languages via Queries. PhD thesis, Kyushu University (1998)

    Google Scholar 

  18. Schwentick, T.: Automata for XML. J. Comput. Syst. Sci. 73(3), 289–315 (2007)

    Article  MathSciNet  Google Scholar 

  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. Snoyman, M., Breitkreuz, A.: http://hackage.haskell.org/package/xml-conduit

  21. Tzevelekos, N.: Fresh-register automata. In: Proceedings of POPL, pp. 295–306 (2011)

    Article  Google Scholar 

Download references

Acknowledgment

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

Author information

Authors and Affiliations

  1. University of Oxford, Oxford, UK

    A. S. Murawski

  2. University of Bristol, Bristol, UK

    S. J. Ramsay

  3. Queen Mary University of London, London, UK

    N. Tzevelekos

Authors
  1. A. S. Murawski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. S. J. Ramsay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. N. Tzevelekos
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to A. S. Murawski .

Editor information

Editors and Affiliations

  1. Institute of Information Science, Academia Sinica, Taipei, Taiwan

    Yu-Fang Chen

  2. DENSO AUTOMOTIVE Deutschland GmbH, Eching, Germany

    Chih-Hong Cheng

  3. Institute of Computer Science, TU München, Munich, Germany

    Javier Esparza

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Murawski, A.S., Ramsay, S.J., Tzevelekos, N. (2019). DEQ: Equivalence Checker for Deterministic Register Automata. In: Chen, YF., Cheng, CH., Esparza, J. (eds) Automated Technology for Verification and Analysis. ATVA 2019. Lecture Notes in Computer Science(), vol 11781. Springer, Cham. https://doi.org/10.1007/978-3-030-31784-3_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31784-3_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31783-6

  • Online ISBN: 978-3-030-31784-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation