Mealy and Moore machines are widely used to model reactive systems. A restriction of these frameworks, however, is that each input generates exactly one output. In real-world systems, some inputs do not induce any output, whereas others induce several consecutive outputs. In order to model such behaviors, De Alfaro and Henzinger [AH01] introduced interface automata, a modeling framework related to the I/O automata of Lynch \& Tuttle [LT87], and the I/O transition systems of Tretmans [Tre08] . Interface automata refine labelled transition systems by declaring actions to be either inputs or outputs. The definition below is a simplified version of the definition of [AH01] without internal actions.
An interface automaton (IA) is a tuple $T = \langle Q, Q_0, \Sigma, \Gamma, \rightarrow \rangle$, where $Q$ is a set of states, $Q_0 \subseteq Q$ is a nonempty set of initial states, $\Sigma$ is a set of input symbols, $\Gamma$ is a set of output symbols with $\Sigma \cap \Gamma = \emptyset$, and $\rightarrow \subseteq Q \times (\Sigma \cup \Gamma) \times Q$ is a transition relation. We call an interface automaton deterministic (resp. finite) if its underlying labelled transition system is deterministic (resp. finite), and refer to finite deterministic interface automata as DFIAs.
A DFIA is encoded as a dot file where input actions are always of the form ?a, whereas output actions are always of the form !x. For instance, the dot encoding for the DFIA toy benchmark is:
digraph S {
__start0 [label="" shape="none"]
s0 [shape="circle" label="s0"]
s1 [shape="circle" label="s1"]
s2 [shape="circle" label="s2"]
__start0 -> s1
s0 -> s0 [label="?a"]
s0 -> s1 [label="!x"]
s0 -> s2 [label="?b"]
s1 -> s0 [label="?a"]
s1 -> s2 [label="?b"]
s2 -> s0 [label="?a"]
s2 -> s1 [label="!y"]
s2 -> s2 [label="?b"]
}