ENG
РУС
Search
Menu
About the Edition
Open Access Statement
Editorial Board
Editorial Policy
Editorial Ethics
Rules for peer-review
Rules for presentation of papers
Forms of Submitted Documents
Recommendations for the Design of References to Our Journal
Editorial Staff
Information for Subscribers
Summaries of the Issue
List of Authors
Issues
Publishers license agreement
Procedure of work with personal data
Publications
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.
Partners













































doi: 10.17586/2226-1494-2020-20-3-394-401

DETERMINISTIC FINITE AUTOMATA USINGCOUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT

I. T. Zakirzyanov


Read the full article  ';
Article in Russian

For citation:
Deterministic finite automata learning using counterexample guided abstraction refinement. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2020, vol. 20, no. 3, pp. 394–401 (in Russian). doi: 10.17586/2226-1494-2020-20-3-394-401


Abstract
Subject of Research. The paper studies minimum-sized deterministic finite automata inferring problem. A hybrid method is developed and implemented reducing the given problem to Boolean satisfiability (SAT) technique and at the same time applying a counterexample guided abstraction refinement approach. Method. It is proposed to use not all given behavior examples as training data but start with some subset of them and build a consistent automaton, using SAT- based automata inferring method. Then the built automaton is checked against the complete set of behavior examples. The examples not consistent with the automaton are counterexamples. Some subset of counterexamples is added to the current training data and the process is being repeated. Main Results. The proposed method is implemented as a part of deterministic finite automata inferring tool in Python language. Experimental comparison of the developed method and the SAT-based method without abstraction refinement is carried out. Practical Relevance. Experimental research has shown that the developed method is reasonable for application if the number of behavior examples is large enough, at least, two hundred times exceeds the number of the automaton states, and, therefore, the Boolean formula being created contains tens and hundreds of millions of clauses.

Keywords: deterministic finite automata inference, Boolean satisfiability, counterexample guided abstraction refinement, symmetry breaking, grammatical inference, machine learning

Acknowledgements. The reported study was funded by the RFBR according to the research project No. 18-37-00425.

References
  1. Wieman R., Aniche M.F., Lobbezoo W., Verwer S., Van Deursen A. An experience report on applying passive learning in a large-scale payment company. Proc. 33rd IEEE International Conference on Software Maintenance and Evolution (ICSME), Shanghai, China, 2017, pp. 564–573. doi: 10.1109/ICSME.2017.71
  2. Neider D. Applications of Automata Learning in Verification and Synthesis. PhD thesis. Hochschulbibliothek der Rheinisch-Westfälischen Technischen Hochschule Aachen, 2014, 283 p.
  3. Biermann A.W., Feldman J.A. On the synthesis of finite-state machines from samples of their behavior. IEEE Transactions on Computers, 1972, vol. C-21, no. 6, pp. 592–597. doi: 10.1109/TC.1972.5009015
  4. Coste F., Nicolas J. Regular inference as a graph coloring problem. Proc. 14th International Conference on Machine Learning (ICML), Workshop on Grammatical Inference, Automata Induction, and Language Acquisition. Nashville, Tennessee, USA, 1997.
  5. Coste F., Nicolas J. How considering incompatible state mergings may reduce the DFA induction search tree. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1998, vol. 1433, pp. 199–210. doi: 10.1007/BFb0054076
  6. Oliveira A.L., Silva J.P.M. Efficient algorithms for the inference of minimum size DFAs. Machine Learning, 2001, vol. 44, no. 1-2, pp. 93–119. doi: 10.1023/A:1010828029885
  7. Lang K.J. Faster Algorithms for Finding Minimal Consistent DFAs. Technical Report. NEC Research Institute, 1999, 19 p.
  8. 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1998, vol. 1433, pp. 1–12. doi: 10.1007/BFb0054059
  9. Heule M., Verwer S. Exact DFA identification using SAT solvers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2010, vol. 6339, pp. 66–79. doi: 10.1007/978-3-642-15488-1_7
  10. Ulyantsev V., Tsarev F. Extended finite-state machine induction using SAT-solver. Proc. 10th International Conference on Machine Learning and Applications and Workshops, Honolulu, Hawaii, USA, 2011, pp. 346–349. doi: 10.1109/ICMLA.2011.166
  11. Grinchtein O., Leucker M., Piterman N. Inferring network invariants automatically. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2006, vol. 4130, pp. 483–497. doi: 10.1007/11814771_40
  12. Ulyantsev V., Zakirzyanov I., Shalyto A. BFS-based symmetry breaking predicates for DFA identification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2015, vol. 8977, pp. 611–622. doi: 10.1007/978-3-319-15579-1_48
  13. Zakirzyanov I., Morgado A., Ignatiev A., Ulyantsev V., Silva J.M. Efficient symmetry breaking for SAT-based minimum DFA inference. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, vol. 11417, pp. 159–173. doi: 10.1007/978-3-030-13435-8_12
  14. Zakirzyanov I., Shalyto A., Ulyantsev V. Finding all minimum-size DFA consistent with given examples: SAT-based approach. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2018, vol. 10729, pp. 117–131. doi: 10.1007/978-3-319-74781-1_9
  15. Clarke E.M., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 2003, vol. 50, no. 5, pp. 752–794. doi: 10.1145/876638.876643
  16. Angluin D. Learning regular sets from queries and counterexamples. Information and Computation, 1987, vol. 75, no. 2, pp. 87–106. doi: 10.1016/0890-5401(87)90052-6
  17. Handbook of Satisfiability. Ed. by A. Biere, M. Heule, H. van Maaren, T. Walsh. IOS Press, 2009, 980 p., Frontiers in Artificial Intelligence and Applications, vol. 185.
  18. Gold E.M. Complexity of automaton identification from given data. Information and Control, 1978, vol. 37, no. 3, pp. 302–320. doi: 10.1016/S0019-9958(78)90562-4


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2024 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика