Abstract
Deterministic finite automaton (DFA) is a fundamental concept in the theory of computation. The NP-hard DFA identification problem can be efficiently solved by translation to the Boolean satisfiability problem (SAT). Previously we developed a technique to reduce the problem search space by enforcing DFA states to be enumerated in breadth-first search (BFS) order. We proposed symmetry breaking predicates, which can be added to Boolean formulae representing various automata identification problems. In this paper we continue the study of SAT-based approaches. First, we propose new predicates based on depth-first search order. Second, we present three methods to identify all non-isomorphic automata of the minimum size instead of just one—the 
P-complete problem which has not been solved before. Third, we revisited our implementation of the BFS-based approach and conducted new evaluation experiments. It occurs that BFS-based approach outperforms all other exact algorithms for DFA identification and can be effectively applied for finding all solutions of the problem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Boston (2006)
De La Higuera, C.: A bibliographical study of grammatical inference. Pattern Recogn. 38(9), 1332–1348 (2005)
Gold, E.M.: Complexity of automaton identification from given data. Inf. Control 37(3), 302–320 (1978)
Dupont, P.: Regular grammatical inference from positive and negative samples by genetic search: the GIG method. In: Carrasco, R.C., Oncina, J. (eds.) ICGI 1994. LNCS, vol. 862, pp. 236–245. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58473-0_152
Luke, S., Hamahashi, S., Kitano, H.: Genetic programming. In: Proceedings of the genetic and evolutionary computation conference, vol. 2, pp. 1098–1105 (1999)
Lucas, S.M., Reynolds, T.J.: Learning DFA: evolution versus evidence driven state merging. In: The 2003 Congress on Evolutionary Computation, 2003. CEC 2003, vol. 1, pp. 351–358. IEEE (2003)
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). https://doi.org/10.1007/BFb0054059
Lang, K.J.: Faster algorithms for finding minimal consistent DFAs. Technical report (1999)
Bugalho, M., Oliveira, A.L.: Inference of regular languages using state merging algorithms with search. Pattern Recogn. 38(9), 1457–1467 (2005)
Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., García, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 66–79. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15488-1_7
Lohfert, R., Lu, J.J., Zhao, D.: Solving SQL constraints by incremental translation to SAT. In: Nguyen, N.T., Borzemski, L., Grzech, A., Ali, M. (eds.) IEA/AIE 2008. LNCS (LNAI), vol. 5027, pp. 669–676. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69052-8_70
Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283–1307 (2013)
Ulyantsev, V., Tsarev, F.: Extended finite-state machine induction using SAT-solver. In: Proceedings of ICMLA 2011, vol. 2, pp. 346–349. IEEE (2011)
Zbrzezny, A.: A new translation from ECTL* to SAT. Fundamenta Informaticae 120(3–4), 375–395 (2012)
Walkinshaw, N., Lambeau, B., Damas, C., Bogdanov, K., Dupont, P.: STAMINA: a competition to encourage the development and assessment of software model inference techniques. Empirical Software Engineering 18(4), 791–824 (2013)
Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. KR 96, 148–159 (1996)
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, Cham (2015). https://doi.org/10.1007/978-3-319-15579-1_48
Ulyantsev, V., Buzhinsky, I., Shalyto, A.: Exact finite-state machine identification from scenarios and temporal properties. Int. J. Softw. Tools Technol. Transf. 1–21 (2016)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Biere, A.: Splatz, lingeling, plingeling, treengeling, YalSAT entering the SAT competition 2016. In: Proceedings of SAT Competition, pp. 44–45 (2016)
Acknowledgements
The authors would like to thank Igor Buzhinsky, Daniil Chivilikhin, Maxim Buzdalov for useful comments. This work was financially supported by the Government of Russian Federation, Grant 074-U01.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Zakirzyanov, I., Shalyto, A., Ulyantsev, V. (2018). Finding All Minimum-Size DFA Consistent with Given Examples: SAT-Based Approach. In: Cerone, A., Roveri, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10729. Springer, Cham. https://doi.org/10.1007/978-3-319-74781-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-74781-1_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-74780-4
Online ISBN: 978-3-319-74781-1
eBook Packages: Computer ScienceComputer Science (R0)