test for $MathJaxURL
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.