Advertisement

Fast Computations on Ordered Nominal Sets

  • David Venhoek
  • Joshua Moerman
  • Jurriaan Rot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

Abstract

We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis. The approach is implemented as the library Ons (Ordered Nominal Sets).

Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets. We evaluate Ons in two applications: minimisation of automata and active automata learning. In both cases, Ons is competitive compared to existing implementations and outperforms them for certain classes of inputs.

Notes

Acknowledgement

We would like to thank Szymon Toruńczyk and Eryk Kopczyński for their prompt help when using the Lois library. For general comments and suggestions we would like to thank Ugo Montanari and Niels van der Weide. At last, we want to thank the anonymous reviewers for their comments.

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.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987).  https://doi.org/10.1016/0890-5401(87)90052-6MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bojańczyk, M., Braud, L., Klin, B., Lasota, S.: Towards nominal computation. In: Proceedings of 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, PA, USA, pp. 401–412. ACM Press, New York (2012).  https://doi.org/10.1145/2103656.2103704
  4. 4.
    Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Log. Methods Comput. Sci. 10(3), Article no. 4 (2014).  https://doi.org/10.2168/lmcs-10(3:4)2014
  5. 5.
    Bojańczyk, M., Lasota, S.: A machine-independent characterization of timed languages. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012. LNCS, vol. 7392, pp. 92–103. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31585-5_12CrossRefzbMATHGoogle Scholar
  6. 6.
    Bollig, B., Habermehl, P., Leucker, M., Monmege, B.: A fresh approach to learning register automata. In: Béal, M.-P., Carton, O. (eds.) DLT 2013. LNCS, vol. 7907, pp. 118–130. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38771-5_12CrossRefGoogle Scholar
  7. 7.
    Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. Formal Asp. Comput. 28(2), 233–263 (2016).  https://doi.org/10.1007/s00165-016-0355-5MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Ciancia, V., Kurz, A., Montanari, U.: Families of symmetries as efficient models of resource binding. Electron. Notes Theor. Comput. Sci. 264(2), 63–81 (2010).  https://doi.org/10.1016/j.entcs.2010.07.014MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Ciancia, V., Montanari, U.: Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput. 208(12), 1349–1367 (2010).  https://doi.org/10.1016/j.ic.2009.10.007MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    D’Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 47–67. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_3CrossRefGoogle Scholar
  11. 11.
    Drews, S., D’Antoni, L.: Learning symbolic automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 173–189. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_10CrossRefGoogle Scholar
  12. 12.
    Ferrari, G.L., Montanari, U., Tuosto, E.: Coalgebraic minimization of HD-automata for the \(\pi \)-calculus using polymorphic types. Theor. Comput. Sci. 331(2–3), 325–365 (2005).  https://doi.org/10.1016/j.tcs.2004.09.021MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454–471. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_25CrossRefGoogle Scholar
  14. 14.
    Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13(3–5), 341–363 (2002).  https://doi.org/10.1007/s001650200016CrossRefzbMATHGoogle Scholar
  15. 15.
    Grigore, R., Tzevelekos, N.: History-register automata. Log. Methods Comput. Sci. 12(1), Article no. 7 (2016).  https://doi.org/10.2168/lmcs-12(1:7)2016
  16. 16.
    Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994).  https://doi.org/10.1016/0304-3975(94)90242-9MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Klin, B., Szynwelski, M.: SMT solving for functional programming over infinite structures. In: Atkey, R., Krishnaswami, N.R. (eds.) Proc. of 6th Workshop on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, Apr. 2016). Electronic Proceedings in Theoretical Computer Science, vol. 207, pp. 57–75. Open Publishing Association, Sydney (2016).  https://doi.org/10.4204/eptcs.207.3MathSciNetCrossRefGoogle Scholar
  18. 18.
    Kopczynski, E., Toruńczyk, S.: LOIS: an application of SMT solvers. In: King, T., Piskac, R. (eds.) Proceedings of 14th International Workshop on Satisfiability Modulo Theories, SMT 2016, Coimbra, July 2016. CEUR Workshop Proceedings, vol. 1617, pp. 51–60. CEUR-WS.org (2016). http://ceur-ws.org/Vol-1617/paper5.pdf
  19. 19.
    Kopczynski, E., Toruńczyk, S.: LOIS: syntax and semantics. In: Proceedings of 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, January 2017, pp. 586–598. ACM Press, New York (2017).  https://doi.org/10.1145/3009837.3009876
  20. 20.
    Maler, O., Mens, I.-E.: A generic algorithm for learning symbolic automata from membership queries. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 146–169. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63121-9_8CrossRefGoogle Scholar
  21. 21.
    Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: Proceedings of 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, January 2017, pp. 613–625. ACM Press, New York (2017).  https://doi.org/10.1145/3009837.3009879
  22. 22.
    Montanari, U., Pistore, M.: An introduction to history dependent automata. Electron. Notes Theor. Comput. Sci. 10, 170–188 (1998).  https://doi.org/10.1016/s1571-0661(05)80696-6MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: Bisimilarity in fresh-register automata. In: Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, July 2015, pp. 156–167. IEEE CS Press (2015).  https://doi.org/10.1109/lics.2015.24
  24. 24.
    Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science, vol. 57. Cambridge University Press, Cambridge (2013).  https://doi.org/10.1017/cbo9781139084673
  25. 25.
    Pitts, A.M.: Nominal techniques. SIGLOG News 3(1), 57–72 (2016). http://doi.acm.org/10.1145/2893582.2893594Google Scholar
  26. 26.
    Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006).  https://doi.org/10.1007/11874683_3CrossRefGoogle Scholar
  27. 27.
    Shinwell, M.R., Pitts, A.M.: Fresh Objective Caml user manual. Technical report, Computer Laboratory, University of Cambridge (2005)Google Scholar
  28. 28.
    Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38–53. Springer, Heidelberg (2005).  https://doi.org/10.1007/11532231_4CrossRefGoogle Scholar
  29. 29.
    Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86–95 (2017).  https://doi.org/10.1145/2967606CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Institute for Computing and Information SciencesRadboud UniversiteitNijmegenThe Netherlands

Personalised recommendations