We use \textit{Mealy machines} to represent the state machine of SSH implementations. A Mealy machine is a a 5-tuple $\mathcal{M}=(Q, q_0, I, O, \rightarrow\rangle)$, where

$I$, $O$ and $Q$ are finite sets of \emph{inputs}, \emph{outputs} and \emph{states}, $q_0\in Q$ is the initial state, and $\rightarrow\subseteq Q \times I \times O \times Q$

is the \emph{transition relation}. We say $q \xrightarrow{i/o} q'$ if $(q, i, o, q')\in\rightarrow$.

A \emph{Mealy machine} is a tuple $\M=(I, O, Q, q_0, \delta, \lambda)$, where

$I$ is a finite set of inputs,

$O$ is a finite set of outputs,

$Q$ is a finite set of states,

$q_0\in Q$ is the initial state,

$\delta: Q \times I \rightarrow Q$ is a transition function, and

$\lambda: Q \times I \rightarrow O$ is an output function.

%

Output function $\lambda$ is extended to sequences of inputs by defining,

for all $q \in Q$, $i \in I$ and $\sigma\in I^{\ast}$,

$\lambda(q, \epsilon)=\epsilon$ and $\lambda(q, i \sigma)=\lambda(q, i)\lambda(\delta(q, i), \sigma)$.

%\end{eqnarray*}

%

The behavior of Mealy machine $\M$ is defined by function $A_\M : I^{\ast}\rightarrow O^{\ast}$ with

$A_\M(\sigma)=\lambda(q^0, \sigma)$, for $\sigma\in I^{\ast}$.

Mealy machines $\M$ and $\N$ are \emph{equivalent}, denoted $\M\approx\N$, iff $A_{\M}= A_{\N}$.

Sequence $\sigma\in I^{\ast}$\emph{distinguishes}

$\M$ and $\N$ if and only if $A_{\M}(\sigma)\neq A_{\N}(\sigma)$.

A Mealy machine $\mathcal{M}$ is \emph{input enabled} if for each state $q$ and input $i$, there is a transition $q \xrightarrow{i/o} q'$, for some $o$ and $q'$. Additionally,

a Mealy machine is said to be \emph{deterministic} if there is at most one such transition defined. Our setting restricts the representations of systems to Mealy machines that are both

input enabled and deterministic.

%\begin{figure}[h]

%\centering

...

...

@@ -29,11 +43,10 @@ input enabled and deterministic.

The most efficient algorithms for model learning all follow

the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Angluin1987Learning}.

Here learning is viewed as a game in which a \emph{learner} has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a deterministic Mealy machine $\M$,

Here learning is viewed as a game in which a \emph{learner} has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a Mealy machine $\M$,

also called the System Under Learning ({\dsut}).

Initially, the {\dlearner} only knows the input alphabet $I$ and

output alphabet $O$ of $\M$.

The task of the {\dlearner} is to learn $\M$ through two types of queries:

Initially, the learner only knows the input alphabet $I$ and output alphabet $O$ of $\M$.

The task of the learner is to learn $\M$ through two types of queries:

\begin{itemize}

\item

With a \emph{membership query}, the learner asks what the response is to an input sequence $\sigma\in I^{\ast}$.

...

...

@@ -45,25 +58,21 @@ whether $\CH \approx \M$. The teacher answers \emph{yes} if this is the case. Ot

a different output sequence for both Mealy machines, that is, $A_{\CH}(\sigma)\neq A_{\M}(\sigma)$.

\end{itemize}

%

If $\M$ is treated as a black box, the equivalence query can only be

approximated by a \emph{test query}, which uses conformance testing

\cite{LeeY96} -- more specifically, model-based testing --

to look for a counterexample with a finite number of queries. Note

that this cannot exclude the possibility that there is more behaviour

The MAT framework can be used to learn black box models of software.

If the behavior of a software system, or System Under Learning ({\dsut}), can be described by some unknown Mealy machine $\M$,

then a membership query can be implemented by sending inputs to the software system and observing the resulting outputs.

An equivalence query can be approximated using a conformance testing tool \cite{LeeY96} via a finite number of \emph{test queries}.

A test query consists of asking the {\dsut} for the response to an input sequence

$\sigma\in I^{\ast}$, similar to a membership query.

Note that this cannot exclude the possibility that there is more behaviour

that has not been discovered. For a recent overview of model learning

algorithms for this setting see \cite{Isberner2015}.

in applications where one wants to learn a model of a black-box reactive system, or System Under Learning ({\dsut}). The teacher typically

consists of the {\dsut}, which answers membership queries, and a conformance

testing tool \cite{LeeY96} that approximates equivalence queries using a set

of \emph{test queries}. A test query consists of asking the {\dsut} for the response to an input sequence

$\sigma\in I^{\ast}$, similar to a membership query.

\subsection{Abstraction}\label{ssec:mappers}

Most current learning algorithms are only applicable to Mealy machines with small alphabets comprising abstract messages. Practical systems typically

have parameterized input/output alphabets, whose application triggers updates on the system's state variables. To learn

these systems we place a \emph{mapper} between the {\dlearner} and the {\dsut}. The {\dmapper} is a transducer which translates

concrete inputs to abstract inputs and concrete outputs to abstract outputs. For a thorough definition of mappers, we refer to \cite{AJUV15}.

these systems we place a \emph{mapper} between the learner and the {\dsut}. The mapper is a transducer which translates

concrete inputs to abstract inputs and concrete outputs to abstract outputs. For a thorough discussion of mappers, we refer to \cite{AJUV15}.