Observable Non-deterministic Finite State Machines (ONFSM)

An Observable Non-deterministic Finite State Machine (ONFSM) is a finite-state machine that extends Mealy machines with a limited form of non-determinism. Given the same state and input, multiple transitions with different outputs are possible.

Formal definition

An ONFSM is a tuple $M = (\Sigma_i,\Sigma_o,Q,q_0,h)$ where:

• $\Sigma_i$ is the input alphabet
• $\Sigma_o$ is the output alphabet
• $Q$ is a finite set of states
• $q_0 \in Q$ is the initial state
• $h\subseteq Q\times\Sigma_i\times\Sigma_o\times Q$ is the transition relation

A transition $(q, i, o, q’) \in h$ means that in state $q$, on input $i$, the machine may produce output $o$ and move to state $q’$.

Syntax

An ONFSM is encoded as a dot file where the label on a transition has the syntax "input/output", identical to Mealy machines. Non-determinism is expressed by multiple transitions from the same state with the same input but different output labels. For instance, the dot encoding for the MQTT benchmark? is:

  digraph g {
    __start0 [label="" shape="none"];
    q0 [shape="circle" margin=0 label="q0"];
    q1 [shape="circle" margin=0 label="q1"];
    q0 -> q0 [label="a/1"];
    q0 -> q1 [label="b/0"];
    q1 -> q1 [label="b/O"];
    q1 -> q1 [label="a/1"];
    __start0 -> q0;
  }.