DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT
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 approac...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)
2020-07-01
|
| Series: | Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki |
| Subjects: | |
| Online Access: | https://ntv.ifmo.ru/file/article/19638.pdf |
| _version_ | 1818772856874467328 |
|---|---|
| author | Ilya T. Zakirzyanov |
| author_facet | Ilya T. Zakirzyanov |
| author_sort | Ilya T. Zakirzyanov |
| collection | DOAJ |
| description | 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 SATbased 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. |
| first_indexed | 2024-12-18T10:16:00Z |
| format | Article |
| id | doaj.art-70032e1e980641bb92545a0b6dbb174a |
| institution | Directory Open Access Journal |
| issn | 2226-1494 2500-0373 |
| language | English |
| last_indexed | 2024-12-18T10:16:00Z |
| publishDate | 2020-07-01 |
| publisher | Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University) |
| record_format | Article |
| series | Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki |
| spelling | doaj.art-70032e1e980641bb92545a0b6dbb174a2022-12-21T21:11:17ZengSaint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki2226-14942500-03732020-07-0120339440110.17586/2226-1494-2020-20-3-394-401DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENTIlya T. Zakirzyanov0https://orcid.org/0000-0002-3460-3489Postgraduate, Software Engineer, ITMO University, Saint Petersburg, 197101, Russian FederationSubject 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 SATbased 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.https://ntv.ifmo.ru/file/article/19638.pdfdeterministic finite automata inferenceboolean satisfiabilitycounterexample guided abstraction refinementsymmetry breakinggrammatical inference |
| spellingShingle | Ilya T. Zakirzyanov DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki deterministic finite automata inference boolean satisfiability counterexample guided abstraction refinement symmetry breaking grammatical inference |
| title | DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT |
| title_full | DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT |
| title_fullStr | DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT |
| title_full_unstemmed | DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT |
| title_short | DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT |
| title_sort | deterministic finite automata learning using counterexample guided abstraction refinement |
| topic | deterministic finite automata inference boolean satisfiability counterexample guided abstraction refinement symmetry breaking grammatical inference |
| url | https://ntv.ifmo.ru/file/article/19638.pdf |
| work_keys_str_mv | AT ilyatzakirzyanov deterministicfiniteautomatalearningusingcounterexampleguidedabstractionrefinement |