Deterministic finite automaton: Difference between revisions

Revision as of 06:47, 18 November 2021

Revision as of 17:42, 29 January 2022

Line 102:

When the start state and accept states are ignored, a DFA of {{mvar|n}} states and an alphabet of size {{mvar|k}} can be seen as a [[Directed graph|digraph]] of {{mvar|n}} vertices in which all vertices have {{mvar|k}} out-arcs labeled {{math|1, …, ''k''}} (a {{mvar|k}}-out digraph). It is known that when {{math|''k'' ≥ 2}} is a fixed integer, with high probability, the largest [[strongly connected component]] (SCC) in such a {{mvar|k}}-out digraph chosen uniformly at random is of linear size and it can be reached by all vertices.<ref name=Grusho>{{cite journal|last1=Grusho|first1=A. A.|title=Limit distributions of certain characteristics of random automaton graphs|journal=Mathematical Notes of the Academy of Sciences of the USSR|date=1973|volume=4|pages=633–637|doi=10.1007/BF01095785|s2cid=121723743|ref=Grusho1973}}</ref> It has also been proven that if {{mvar|k}} is allowed to increase as {{mvar|n}} increases, then the whole digraph has a phase transition for strong connectivity similar to [[Erdős–Rényi model]] for connectivity.<ref name=Cai>{{cite journal |last1=Cai |first1=Xing Shi |last2=Devroye |first2=Luc |title=The graph structure of a deterministic automaton chosen at random |journal=Random Structures & Algorithms |date=October 2017 |volume=51 |issue=3 |pages=428–458 |doi=10.1002/rsa.20707|arxiv=1504.06238 |s2cid=13013344 }}</ref>

In a random DFA, the maximum number of vertices reachable from one vertex is very close to the number of vertices in the largest [[strongly connected component|SCC]] with high probability.<ref name=Grusho /><ref>{{cite proceedingsconference |last1=Carayol |first1=Arnaud |last2=Nicaud |first2=Cyril |date=February 2012 |title=Distribution of the number of accessible states in a random deterministic automaton |volume=14 |pages=194–205 |conference=STACS'12 (29th Symposium on Theoretical Aspects of Computer Science) |___location=Paris, France |url=https://hal.archives-ouvertes.fr/hal-00678213}}</ref> This is also true for the largest [[Glossary of graph theory#Subgraphs|induced sub-digraph]] of minimum in-degree one, which can be seen as a directed version of [[Degeneracy (graph theory)#k-Cores|{{math|1}}-core]].<ref name=Cai />

==Advantages and disadvantages==

Line 137:

Yet another step forward is due to application of [[Boolean satisfiability problem|SAT]] solvers by [[Marijn Heule|Marjin J. H. Heule]] and S. Verwer: the minimal DFA identification problem is reduced to deciding the satisfiability of a Boolean formula.<ref name=HW1>{{cite conference|last1=Heule|first1=M. J. H.|author-link=Marijn Heule|title=Exact DFA Identification Using SAT Solvers|conference=Grammatical Inference: Theoretical Results and Applications. ICGI 2010. Lecture Notes in Computer Science|date=2010|volume=6339|pages=66–79|doi=10.1007/978-3-642-15488-1_7|ref=Heule2010}}</ref> The main idea is to build a augmented prefix-tree acceptor (a [[trie]] containing all input words with corresponding labels) based on the input sets and reduce the problem of finding a DFA with <math>C</math> states to ''coloring'' the tree vertices with <math>C</math> states in such a way that when vertices with one color are merged to one state, the generated automaton is deterministic and complies with <math>S^+</math> and <math>S^-</math>.

Though this approach allows finding the minimal DFA, it suffers from exponential blow-up of execution time when the size of input data increases.

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 in<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: