Skip to main content
SpringerLink
Log in

Learning Moore Machines from Input-Output Traces

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9995))

Included in the following conference series:

Abstract

The problem of learning automata from example traces (but no equivalence or membership queries) is fundamental in automata learning theory and practice. In this paper we study this problem for finite state machines with inputs and outputs, and in particular for Moore machines. We develop three algorithms for solving this problem: (1) the PTAP algorithm, which transforms a set of input-output traces into an incomplete Moore machine and then completes the machine with self-loops; (2) the PRPNI algorithm, which uses the well-known RPNI algorithm for automata learning to learn a product of automata encoding a Moore machine; and (3) the MooreMI algorithm, which directly learns a Moore machine using PTAP extended with state merging. We prove that MooreMI has the fundamental identification in the limit property. We also compare the algorithms experimentally in terms of the size of the learned machine and several notions of accuracy, introduced in this paper. Finally, we compare with OSTIA, an algorithm that learns a more general class of transducers, and find that OSTIA generally does not learn a Moore machine, even when fed with a characteristic sample.

This work was partially supported by the Academy of Finland and the U.S. National Science Foundation (awards #1329759 and #1139138). An extended version of this paper is available as [17].

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 term smallest automaton is used in the exact identification problem, instead of the more well-known term minimal automaton. Among equivalent machines, one with the fewest states is called minimal. Among machines which are all consistent with a set of traces but not necessarily equivalent, one with the fewest states is called smallest.

  2. 2.

    Note, however, that our algorithms perform better in terms of execution time than approaches that solve exact identification problems. For example, [46] report experiments where learning a Mealy machine of 18 states requires more than 29 h. The majority of the execution time here is spent in proving that there exists no machine with fewer than 18 states which is also consistent with the examples. Since we don’t require the smallest machine, our algorithms avoid this penalty.

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, Heidelberg (2015). doi:10.1007/978-3-319-25150-9_11

    Chapter  Google Scholar 

  2. Aarts, F., Vaandrager, F.: Learning I/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71–85. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15375-4_6

    Chapter  Google Scholar 

  3. Akram, H.I., Higuera, C., Xiao, H., Eckert, C.: Grammatical inference algorithms in MATLAB. In: Sempere, J.M., García, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 262–266. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15488-1_22

    Chapter  Google Scholar 

  4. Aleksandrov, A.V., Kazakov, S.V., Sergushichev, A.A., Tsarev, F.N., Shalyto, A.A.: The use of evolutionary programming based on training examples for the generation of finite state machines for controlling objects with complex behavior. J. Comput. Syst. Sci. Int. 52(3), 410–425 (2013)

    Article  MATH  Google Scholar 

  5. Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75–91. Springer, Heidelberg (2014). doi:10.1007/978-3-319-13338-6_7

    Google Scholar 

  6. Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. In: POPL 2002, pp. 4–16. ACM (2002)

    Google Scholar 

  7. Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  8. Berg, T., Grinchtein, O., Jonsson, B., Leucker, M., Raffelt, H., Steffen, B.: On the correspondence between conformance testing and regular inference. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 175–189. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31984-9_14

    Chapter  Google Scholar 

  9. Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Comput. 21(6), 592–597 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  10. Buzhinsky, I.P., Ulyantsev, V.I., Chivilikhin, D.S., Shalyto, A.A.: Inducing finite state machines from training samples using ant colony optimization. J. Comput. Syst. Sci. Int. 53(2), 256–266 (2014)

    Article  MATH  Google Scholar 

  11. Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Learning extended finite state machines. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 250–264. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10431-7_18

    Google Scholar 

  12. Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. 4(3), 178–187 (1978)

    Article  MATH  Google Scholar 

  13. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_39

    Chapter  Google Scholar 

  14. de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. CUP, Cambridge (2010)

    Book  MATH  Google Scholar 

  15. Dorofeeva, R., El-Fakih, K., Maag, S., Cavalli, A.R., Yevtushenko, N.: FSM-based conformance testing methods: a survey annotated with experimental evaluation. Inf. Softw. Technol. 52(12), 1286–1297 (2010)

    Article  Google Scholar 

  16. Dupont, P.: Incremental regular inference. In: Miclet, L., Higuera, C. (eds.) ICGI 1996. LNCS, vol. 1147, pp. 222–237. Springer, Heidelberg (1996). doi:10.1007/BFb0033357

    Chapter  Google Scholar 

  17. Giantamidis, G., Tripakis, S.: Learning Moore machines from input-output traces. ArXiv e-prints, v2, September 2016. http://arxiv.org/abs/1605.07805

  18. Gold, E.M.: Language identification in the limit. Inf. Control 10(5), 447–474 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  19. Gold, E.M.: Complexity of automaton identification from given data. Inf. Control 37(3), 302–320 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  20. Grinchtein, O., Leucker, M.: Learning finite-state machines from inexperienced teachers. In: Sakakibara, Y., Kobayashi, S., Sato, K., Nishino, T., Tomita, E. (eds.) ICGI 2006. LNCS (LNAI), vol. 4201, pp. 344–345. Springer, Heidelberg (2006). doi:10.1007/11872436_30

    Chapter  Google Scholar 

  21. Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: 38th POPL, pp. 317–330 (2011)

    Google Scholar 

  22. Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI 2008, pp. 281–292. ACM (2008)

    Google Scholar 

  23. Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634–640. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_48

    Chapter  Google Scholar 

  24. Heitmeyer, C.L., Pickett, M., Leonard, E.I., Archer, M.M., Ray, I., Aha, D.W., Trafton, J.G.: Building high assurance human-centric decision systems. Autom. Softw. Eng. 22(2), 159–197 (2015)

    Article  Google Scholar 

  25. Heule, M.J., Verwer, S.: Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4), 825–856 (2013)

    Article  Google Scholar 

  26. 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). doi:10.1007/978-3-642-27940-9_17

    Chapter  Google Scholar 

  27. Jin, X., Donz, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 34(11), 1704–1717 (2015)

    Article  Google Scholar 

  28. Jonsson, B.: Learning of automata models extended with data. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 327–349. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21455-4_10

    Chapter  Google Scholar 

  29. Karthik, A.V., Ray, S., Nuzzo, P., Mishchenko, A., Brayton, R., Roychowdhury, J.: ABCD-NL: approximating continuous non-linear dynamical systems using purely Boolean models for analog/mixed-signal verification. In: ASP-DAC, pp. 250–255 (2014)

    Google Scholar 

  30. Kohavi, Z.: Switching and Finite Automata Theory, 2nd edn. McGraw-Hill, New York (1978)

    MATH  Google Scholar 

  31. Lang, K.J., Pearlmutter, B.A., Price, R.A.: Results of the Abbadingo one DFA learning competition and a new evidence-driven state merging algorithm. In: Honavar, V., Slutzki, G. (eds.) ICGI 1998. LNCS, vol. 1433, pp. 1–12. Springer, Heidelberg (1998). doi:10.1007/BFb0054059

    Chapter  Google Scholar 

  32. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proc. IEEE 84(8), 1090–1123 (1996)

    Article  Google Scholar 

  33. Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining. In: Automated Software Engineering (ASE), pp. 81–92, November 2015

    Google Scholar 

  34. Ljung, L. (ed.): System Identification: Theory for the User, 2nd edn. Prentice Hall, Englewood Cliffs (1999)

    MATH  Google Scholar 

  35. Medhat, R., Ramesh, S., Bonakdarpour, B., Fischmeister, S.: A framework for mining hybrid automata from input/output traces. In: Embedded Software (EMSOFT), pp. 177–186 (2015)

    Google Scholar 

  36. Meinke, K.: CGE: a sequential learning algorithm for Mealy automata. In: Sempere, J.M., García, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 148–162. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15488-1_13

    Chapter  Google Scholar 

  37. Mitchell, T.M.: Machine Learning. McGraw-Hill, New York (1997)

    MATH  Google Scholar 

  38. Oncina, J., Garcia, P.: Identifying regular languages in polynomial time. In: Advances in Structural and Syntactic, Pattern Recognition, pp. 99–108 (1992)

    Google Scholar 

  39. Oncina, J., García, P., Vidal, E.: Learning subsequential transducers for pattern recognition interpretation tasks. IEEE Trans. Pattern Anal. Mach. Intell. 15(5), 448–458 (1993)

    Article  Google Scholar 

  40. Ray, B., Posnett, D., Filkov, V., Devanbu, P.: A large scale study of programming languages and code quality in github. In: ACM SIGSOFT, FSE 2014 (2014)

    Google Scholar 

  41. Seshia, S.A.: Sciduction: combining induction, deduction, and structure for verification and synthesis. In: DAC, pp. 356–365, June 2012

    Google Scholar 

  42. Shahbaz, M., Groz, R.: Inferring Mealy machines. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 207–222. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05089-3_14

    Chapter  Google Scholar 

  43. Solar-Lezama, A.: Program sketching. STTT 15(5–6), 475–495 (2013)

    Article  Google Scholar 

  44. Spichakova, M.: An approach to inference of finite state machines based on gravitationally-inspired search algorithm. Proc. Estonian Acad. Sci. 62(1), 39–46 (2013)

    Article  MATH  Google Scholar 

  45. Takahashi, K., Fujiyoshi, A., Kasai, T.: A polynomial time algorithm to infer sequential machines. Syst. Comput. Jpn. 34(1), 59–67 (2003)

    Article  Google Scholar 

  46. Ulyantsev, V., Buzhinsky, I., Shalyto, A.: Exact finite-state machine identification from scenarios and temporal properties. CoRR, abs/1601.06945 (2016)

    Google Scholar 

  47. Ulyantsev, V., Zakirzyanov, I., Shalyto, A.: BFS-based symmetry breaking predicates for DFA identification. In: Dediu, A.-H., Formenti, E., Martín-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 611–622. Springer, Heidelberg (2015). doi:10.1007/978-3-319-15579-1_48

    Google Scholar 

  48. Veelenturf, L.P.J.: Inference of sequential machines from sample computations. IEEE Trans. Comput. 27(2), 167–170 (1978)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aalto University, Espoo, Finland

    Georgios Giantamidis & Stavros Tripakis

  2. University of California, Berkeley, Berkeley, USA

    Stavros Tripakis

Authors
  1. Georgios Giantamidis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stavros Tripakis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Georgios Giantamidis or Stavros Tripakis .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Giantamidis, G., Tripakis, S. (2016). Learning Moore Machines from Input-Output Traces. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation