FSM Inference from Long Traces
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.
KeywordsMachine inference Machine identification SAT solver
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.
- 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
- 5.Audemard, G., Simon, L.: The glucose SAT solver (2013)Google Scholar
- 10.Een, N., Sörensson, N.: MiniSat: a SAT solver with conflict-clause minimization. In: 8th SAT-5 (2005)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
- 20.Soos, M.: Cryptominisat 2.5.0. SAT Race competitive event booklet (2010)Google Scholar