Model Learning as a Satisfiability Modulo Theories Problem

  • Rick Smetsers
  • Paul Fiterău-Broştean
  • Frits Vaandrager
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10792)


We explore an approach to model learning that is based on using satisfiability modulo theories (SMT) solvers. To that end, we explain how DFAs, Mealy machines and register automata, and observations of their behavior can be encoded as logic formulas. An SMT solver is then tasked with finding an assignment for such a formula, from which we can extract an automaton of minimal size. We provide an implementation of this approach which we use to conduct experiments on a series of benchmarks. These experiments address both the scalability of the approach and its performance relative to existing active learning tools.


  1. 1.
    Aarts, F., et al.: Generating models of infinite-state communication protocols using regular inference with abstraction. FMSD 46(1), 1–41 (2015)zbMATHGoogle Scholar
  2. 2.
    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). CrossRefGoogle Scholar
  3. 3.
    Aarts, F., de Ruiter, J., Poll, E.: Formal models of bank cards for free. In: ICST Workshops, pp. 461–468. IEEE (2013)Google Scholar
  4. 4.
    Aarts, F., Schmaltz, J., Vaandrager, F.: Inference and abstraction of the biometric passport. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6415, pp. 673–686. Springer, Heidelberg (2010). CrossRefGoogle Scholar
  5. 5.
    Angluin, D.: Learning regular sets from queries and counterexamples. I&C 75(2), 87–106 (1987)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Angluin, D.: Negative results for equivalence queries. Mach. Learn. 5, 121–150 (1990)Google Scholar
  7. 7.
    Bruynooghe, M., et al.: Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3. TPLP 15(6), 783–817 (2015)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. FAOC 28(2), 233–263 (2016)MathSciNetzbMATHGoogle Scholar
  9. 9.
    De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. CACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
  10. 10.
    Florêncio, C.C., Verwer, S.: Regular inference as vertex coloring. TCS 558, 18–34 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Gold, E.: Language identification in the limit. I&C 10(5), 447–474 (1967)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Heule, M., Verwer, S.: Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4), 825–856 (2013)CrossRefGoogle Scholar
  13. 13.
    De la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, Cambridge (2010)CrossRefzbMATHGoogle Scholar
  14. 14.
    Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251–266. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  15. 15.
    Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307–322. Springer, Cham (2014). Google Scholar
  16. 16.
    Lee, D., Yannakakis, M.: Testing finite-state machines: state identification and verification. IEEE Trans. Comput. 43(3), 306–320 (1994)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines—a survey. Proc. IEEE 84(8), 1090–1123 (1996)CrossRefGoogle Scholar
  18. 18.
    Neider, D.: Computing minimal separating DFAs and regular invariants using SAT and SMT solvers. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 354–369. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  19. 19.
    Peled, D., Vardi, M., Yannakakis, M.: Black box checking. In: FORTE, pp. 225–240. Kluwer (1999)Google Scholar
  20. 20.
    Petrenko, A., Avellaneda, F., Groz, R., Oriat, C.: From passive to active FSM inference via checking sequence construction. In: Yevtushenko, N., Cavalli, A.R., Yenigün, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 126–141. Springer, Cham (2017). CrossRefGoogle Scholar
  21. 21.
    Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393–407 (2009)CrossRefGoogle Scholar
  22. 22.
    Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: an industrial experience report. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 311–325. Springer, Cham (2016). CrossRefGoogle Scholar
  23. 23.
    Smeenk, W., Moerman, J., Vaandrager, F., Jansen, D.N.: Applying automata learning to embedded control software. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 67–83. Springer, Cham (2015). CrossRefGoogle Scholar
  24. 24.
    Smetsers, R.: Grammatical Inference as a Satisfiability Modulo Theories Problem. arXiv preprint arXiv:1705.10639 (2017)
  25. 25.
    Vaandrager, F.: Model learning. CACM 60(2), 86–95 (2017)CrossRefGoogle Scholar
  26. 26.
    Walkinshaw, N., Derrick, J., Guo, Q.: Iterative refinement of reverse-engineered models by model-based testing. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 305–320. Springer, Heidelberg (2009). CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Rick Smetsers
    • 1
  • Paul Fiterău-Broştean
    • 1
  • Frits Vaandrager
    • 1
  1. 1.Institute for Computing and Information SciencesRadboud UniversityNijmegenThe Netherlands

Personalised recommendations