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 -