Modular Decomposition of Hierarchical Finite State Machines

TL;DR

This work transfers graph modular decomposition to HFSMs by defining thin modules and constructing a linear-size modular decomposition that represents all equivalent thin HFSMs. It formalizes contraction, restriction, and expansion for FSMs, proving that thin modules yield a unique, linear-sized decomposition with a representative basis, enabling efficient exploration of equivalent HFSMs. An $O(n^2k)$ algorithm computes the decomposition for an $n$-state, $k$-symbol FSM and enables greedy solutions to bottleneck width minimisation, as demonstrated on Harel's wristwatch HFSM. The approach offers practical benefits for reducing model width and guiding modular redesign, with open questions on languages and HFSM compression. The results also suggest using modular decomposition as a preprocessing step for model checking.

Abstract

Hierarchical Finite State Machines (HFSMs) are a standard software-modelling concept which extends the classical Finite State Machine (FSM) notion with the useful abstraction of hierarchical nesting. That is, an HFSM is an FSM whose states can be other FSMs. The hierarchy in HFSMs is provided at design time, and can be removed by expanding nested states, allowing HFSMs to inherit the semantics of FSMs. However, because hierarchy is a useful representation of the structure of an FSM, we would like to be able to invert this operation: given an FSM, can we compute equivalent HFSMs? This is the topic of this paper. By adapting the analogous theory of `modular decomposition' from graph theory into automata theory, we are able to compute an efficient representation of the space of equivalent HFSMs to a given one. Specifically, we first define a module of an FSM, which is a collection of nodes which can be treated as a nested FSM. Unlike modules in graphs, some modules in FSMs are lacking in algebraic structure. We identify a simple and natural restriction of the modules, called thin modules, which regain many of the critical properties from modules in graphs. We then construct a linear-space directed graph which uniquely represents every thin module, and hence every equivalent (thin) HFSM. We call this graph the modular decomposition. The modular decomposition makes clear the significant common structure underlying equivalent thin HFSMs. We provide an $O(n^2k)$ algorithm for constructing the modular decomposition of an $n$-state $k$-symbol FSM. We demonstrate the applicability of this theory on the following `bottleneck' problem: given an HFSM, find an equivalent one where the size of the largest component FSM is minimised. The modular decomposition gives a simple greedy algorithm for the bottleneck problem on thin HFSMs, which we demonstrate on a wristwatch HFSM example from Harel (1987).

Figures (7)

• Figure 1: A graphical depiction of the contribution of this paper. The left column shows the modular decomposition of a graph $G$, which constructs a hierarchical representation of $G$ which captures all other such representations gallai1967transitiv. The right column shows our analogous theory for FSMs. The main contribution is the modular decomposition of an FSM (Fig. \ref{['fig:Z tree']}), a tree-like structure which represents all HFSMs equivalent to a given FSM.
• Figure 2: A transition $\psi(a,x) = b$ in an HFSM, defined by the hierarchical transition function (Definition \ref{['def hierarchical transition']}). Here, $a$ has no $x$-arc, and nor do any of the containing FSMs $A_1,\dots,A_{n-1}$. An $x$-arc exists out of $A_n$, which transitions to the superstate $B_1$. The state $b$ is $\mathop{\mathrm{start}}\nolimits(B_1)$ (Definition \ref{['def:nested start state']}), the nested start state of $B_1$.
• Figure 3: An example of FSM expansion (Definition \ref{['defn:expansion']})
• Figure 4: This FSM has two non-trivial modules, $\{1,2,3\}$ and $\{2,3,4\}$ (represented by grey rectangles), neither of which are thin; they both contain an $x$-cycle and have an $x$-exit. These modules overlap, but neither their union $\{1,2,3,4\}$ nor their intersection $\{2,3\}$ are modules.
• Figure 5: Two HFSMs equivalent to $Z$ (Figure \ref{['fig:Z']}), constructed by contracting different choices of modules from $Z$. Comparing to Figure \ref{['fig:Z tree']}, the modular decomposition of $Z$, we see that $W_1$ and $W_2$ represent different ways to extend the modular decomposition to a tree form.

Theorems & Definitions (70)

• Definition 3.1: Overlapping Sets
• Definition 3.2: Finite state machine, eilenberg1974automata
• Definition 3.3: Output Function of FSMs
• Definition 3.4: Hierarchical Finite State Machine
• Definition 3.5
• Definition 3.6: Hierarchical Transition Function
• Definition 3.7: Output Function of HFSMs
• Definition 3.8: (H)FSM Equivalence
• Theorem 3.9
• Definition 4.1: $x$-Exit and $x$-Entrance