TY - JOUR
T1 - Aggregation-based minimization of finite state automata
AU - Björklund, Johanna
AU - Cleophas, Loek
PY - 2021/6
Y1 - 2021/6
N2 - We present a minimization algorithm for non-deterministic finite state automata that finds and merges bisimulation-equivalent states. The bisimulation relation is computed through partition aggregation, in contrast to existing algorithms that use partition refinement. The algorithm simultaneously generalises and simplifies an earlier one by Watson and Daciuk for deterministic devices. We show the algorithm to be correct and run in time O(n2r2|Σ|), where n is the number of states of the input automaton M, r is the maximal out-degree in the transition graph for any combination of state and input symbol, and |Σ| is the size of the input alphabet. The algorithm has a higher time complexity than derivatives of Hopcroft’s partition-refinement algorithm, but represents a promising new solution approach that preserves language equivalence throughout the computation process. Furthermore, since the algorithm essentially computes the maximal model of a logical formula derived from M, optimisation techniques from the field of model checking become applicable.
AB - We present a minimization algorithm for non-deterministic finite state automata that finds and merges bisimulation-equivalent states. The bisimulation relation is computed through partition aggregation, in contrast to existing algorithms that use partition refinement. The algorithm simultaneously generalises and simplifies an earlier one by Watson and Daciuk for deterministic devices. We show the algorithm to be correct and run in time O(n2r2|Σ|), where n is the number of states of the input automaton M, r is the maximal out-degree in the transition graph for any combination of state and input symbol, and |Σ| is the size of the input alphabet. The algorithm has a higher time complexity than derivatives of Hopcroft’s partition-refinement algorithm, but represents a promising new solution approach that preserves language equivalence throughout the computation process. Furthermore, since the algorithm essentially computes the maximal model of a logical formula derived from M, optimisation techniques from the field of model checking become applicable.
UR - http://www.scopus.com/inward/record.url?scp=85077537325&partnerID=8YFLogxK
U2 - 10.1007/s00236-019-00363-5
DO - 10.1007/s00236-019-00363-5
M3 - Article
SN - 0001-5903
VL - 58
SP - 177
EP - 194
JO - Acta Informatica
JF - Acta Informatica
IS - 3
ER -