Deterministic finite automaton: Difference between revisions

Revision as of 21:34, 11 April 2023

Revision as of 08:01, 12 April 2023

Line 124:

{{main|Induction of regular languages}}

Given a set of ''positive'' words <math>S^+ \subset \Sigma^*</math> and a set of ''negative'' words <math>S^- \subset \Sigma^*</math> one can construct a DFA that accepts all words from <math>S^+</math> and rejects all words from <math>S^-</math>: this problem is called ''DFA identification'' (synthesis, learning).

While ''some'' DFA can be constructed in linear time, the problem of identifying a DFA with the minimal number of states is NP-complete.<ref name="Complexity of Automaton Identificat">{{cite journal|last1=Gold|first1=E. M.|author1-link=E. Mark Gold|title=Complexity of Automaton Identification from Given Data|journal=Information and Control|volume=37|issue=3|pages=302–320|year=1978|doi=10.1016/S0019-9958(78)90562-4|ref=Gold78|doi-access=free}}</ref>

The first algorithm for minimal DFA identification has been proposed by Trakhtenbrot and Barzdin in <ref>{{Cite book | url=https://books.google.com/books?id=h5XOBQAAQBAJ&pg=PP1 |title = Finite Automata: Behavior and Synthesis|isbn = 9781483297293|last1 = De Vries|first1 = A.|date = 28 June 2014}}</ref> and is called the ''TB-algorithm''.

However, the TB-algorithm assumes that all words from <math>\Sigma</math> up to a given length are contained in either <math>S^+ \cup S^-</math>.

Line 140:

Therefore, Heule and Verwer's initial algorithm has later been augmented with making several steps of the EDSM algorithm prior to SAT solver execution: the DFASAT algorithm.<ref>{{Cite journal |doi = 10.1007/s10664-012-9222-z|title = Software model synthesis using satisfiability solvers|journal = Empirical Software Engineering|volume = 18|issue = 4|pages = 825–856|year = 2013|last1 = Heule|first1 = Marijn J. H.|author-link=Marijn Heule|last2 = Verwer|first2 = Sicco|hdl = 2066/103766|s2cid = 17865020|url = https://lirias.kuleuven.be/handle/123456789/370182|hdl-access = free}}</ref>

This allows reducing the search space of the problem, but leads to loss of the minimality guarantee.

Another way of reducing the search space has been proposed inby Ulyantsev et al.<ref>{{Cite book |doi = 10.1007/978-3-319-15579-1_48|chapter = BFS-Based Symmetry Breaking Predicates for DFA Identification|title = Language and Automata Theory and Applications|volume = 8977|pages = 611–622|series = Lecture Notes in Computer Science|year = 2015|last1 = Ulyantsev|first1 = Vladimir|last2 = Zakirzyanov|first2 = Ilya|last3 = Shalyto|first3 = Anatoly|isbn = 978-3-319-15578-4}}</ref> by means of new symmetry breaking predicates based on the [[breadth-first search]] algorithm:

the sought DFA's states are constrained to be numbered according to the BFS algorithm launched from the initial state. This approach reduces the search space by <math>C!</math> by eliminating isomorphic automata.