Skip to main content
SpringerLink
Log in

FSM Inference from Long Traces

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

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

Included in the following conference series:

Abstract

Inferring a minimal finite state machine (FSM) from a given set of traces is a fundamental problem in computer science. Although the problem is known to be NP-complete, it can be solved efficiently with SAT solvers when the given set of traces is relatively small. On the other hand, to infer an FSM equivalent to a machine which generates traces, the set of traces should be sufficiently representative and hence large. However, the existing SAT-based inference techniques do not scale well when the length and number of traces increase. In this paper, we propose a novel approach which processes lengthy traces incrementally. The experimental results indicate that it scales sufficiently well and time it takes grows slowly with the size of traces.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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

References

  1. Abel, A., Reineke, J.: Memin: SAT-based exact minimization of incompletely specified mealy machines. In: 2015 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 94–101. IEEE (2015)

    Google Scholar 

  2. Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: Proceedings of the 39th annual Design Automation Conference, pp. 731–736. ACM (2002)

    Google Scholar 

  3. Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. IEEE Trans. Comput. 55(5), 549–558 (2006)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  5. Audemard, G., Simon, L.: The glucose SAT solver (2013)

    Google Scholar 

  6. Biere, A.: Picosat essentials. J. Satisfiability Boolean Model. Comput. 4, 75–97 (2008)

    MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  8. Brown, C.A., Finkelstein, L., Purdom Jr., P.W.: Backtrack searching in the presence of symmetry. In: Mora, T. (ed.) AAECC 1988. LNCS, vol. 357, pp. 99–110. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51083-4_51

    Chapter  Google Scholar 

  9. Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)

    Article  Google Scholar 

  10. Een, N., Sörensson, N.: MiniSat: a SAT solver with conflict-clause minimization. In: 8th SAT-5 (2005)

    Google Scholar 

  11. Giantamidis, G., Tripakis, S.: Learning moore machines from input-output traces. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 291–309. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_18

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  14. Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 483–497. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_40

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  16. Kella, J.: Sequential machine identification. IEEE Trans. Comput. 100(3), 332–338 (1971)

    Article  Google Scholar 

  17. Oliveira, A.L., Silva, J.P.M.: Efficient algorithms for the inference of minimum size DFAS. Mach. Learn. 44(1), 93–119 (2001)

    Article  Google Scholar 

  18. Oncina, J., García, P.: Identifying regular languages in polynomial time. Adv. Struct. Syntactic Pattern Recogn. 5(99–108), 15–20 (1992)

    Google Scholar 

  19. Smetsers, R., Fiterău-Broştean, P., Vaandrager, F.: Model learning as a satisfiability modulo theories problem. In: Klein, S.T., Martín-Vide, C., Shapira, D. (eds.) LATA 2018. LNCS, vol. 10792, pp. 182–194. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77313-1_14

    Chapter  Google Scholar 

  20. Soos, M.: Cryptominisat 2.5.0. SAT Race competitive event booklet (2010)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  22. 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). https://doi.org/10.1007/978-3-642-05089-3_20

    Chapter  Google Scholar 

Download references

Acknowledgements

This work was partially supported by MESI (Ministère de l’Économie, Science et Innovation) of Gouvernement du Québec, NSERC of Canada and CAE.

Author information

Authors and Affiliations

  1. CRIM, Montreal, Canada

    Florent Avellaneda & Alexandre Petrenko

Authors
  1. Florent Avellaneda
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandre Petrenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Florent Avellaneda or Alexandre Petrenko .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Avellaneda, F., Petrenko, A. (2018). FSM Inference from Long Traces. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation