# From Passive to Active FSM Inference via Checking Sequence Construction

Alexandre Petrenko, Florent Avellaneda, Roland Groz, Catherine Oariat

► To cite this version:

Alexandre Petrenko, Florent Avellaneda, Roland Groz, Catherine Oariat. From Passive to Active FSM Inference via Checking Sequence Construction. 29th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2017, St. Petersburg, Russia. pp.126-141, 10.1007/978-3-319-67549-7_8 . hal-01678991

HAL Id: hal-01678991

https://inria.hal.science/hal-01678991

Submitted on 9 Jan 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# From Passive to Active FSM Inference via Checking
Sequence Construction

Alexandre Petrenko¹, Florent Avellaneda¹, Roland Groz², and Catherine Oriat²

¹CRIM, Canada

{Alexandre.Petrenko, Florent.Avellaneda}@crim.ca

²Univ. Grenoble Alpes, LIG, France

{Roland.Groz, Catherine.Oriat}@imag.fr

**Abstract.** The paper focuses on the problems of passive and active FSM inference as well as checking sequence generation. We consider the setting where an FSM cannot be reset so that its inference is constrained to a single trace either given a priori in passive inference scenario or to be constructed in active inference scenario or aiming at obtaining checking sequence for a given FSM. In each of the last two cases, the expected result is a trace representing a checking sequence for an inferred machine, if it was not given. We demonstrate that this can be achieved by a repetitive use of a procedure that infers an FSM from a given trace (identifying a minimal machine consistent with a trace) avoiding equivalent conjectures. We thus show that FSM inference and checking sequence construction can be seen as two sides of the same coin. Following an existing approach of constructing conjectures by SAT solving, we elaborate first such a procedure and then based on it the methods for obtaining checking sequence for a given FSM and inferring a machine from a black box. The novelty of our approach is that it does not use any state identification facilities. We only assume that we know initially the input set and a bound on the number of states of the machine. Experiments with a prototype implementation of the developed approach using as a backend an existing SAT solver indicate that it scales for FSMs with up to a dozen of states and requires relatively short sequences to identify the machine.

**Keywords:** FSM testing, machine inference, machine identification, active learning, checking experiments, checking sequences.

## 1 Introduction

Model-based testing from finite state models of systems, when it is only possible to interact with the system through its input/output interfaces, relies on traversing transitions of the model and being able to check that states reached after transitions in the system are consistent with those expected from the model. At the end of the test, the goal is to be able to guarantee that the system under test behaves as expected in the model. So the test must be built as a checking sequence of inputs that can uniquely identify (up to equivalence) a given model machine.
Computing a checking sequence from a finite state model dates back to the very early history of automata in computer science, starting with the work of Moore [15] and many approaches have been proposed to generate checking sequences for various types of models under various assumptions for the machine w.r.t determinism, completeness, and the existence of specific sequences for a machine such as distinguishing sequences [10], signatures [21], state identifiers [17] etc.

More recently, at the turn of the century, model-based approaches have led to an interest in inference techniques. Instead of checking whether a system behaves as specified by a model, it works the other way round: we try to build a model, called a conjecture that will predict as accurately as possible the behaviour of a system. This can be based on a corpus of given observed behaviours of the system (passive inference), or on the ability to submit test sequences (active inference). One key driver for such approaches is that experience in industrial context have shown that building and maintaining accurate and up-to-date models was complicated, and needed specific expertise. Being able to derive models automatically relieves the burden of creating and maintaining them.

Building a checking sequence can be seen as a top-down approach (from model to implementation) and inference as bottom-up approach (from implementation to conjectured model). The two are in fact closely linked: in active inference, if a sequence is built that uniquely identifies a machine, then this sequence is a checking sequence for this machine. The main difference is in the starting point: for checking sequence generation, we assume we know the (specification) machine to be identified. For inference, the machine is unknown.

In this paper, we propose an iterative approach that alternates passive inference with construction of checking experiments. Initially, an input sequence will be too short to uniquely identify a machine. But one can exhibit one of many possible conjectures that would match the observed input/output sequence (the running trace). So the idea is to build a checking experiment that will distinguish among conjectures, and which is appended to the current trace. Following this experiment, the set of potential conjectures is reduced, and the process is iterated until we get to a point where the set is reduced to a singleton, at which point the input projection of the observed trace is a checking sequence.

Interestingly, this theoretical framework had already been envisioned by J. Kella, in one of the early papers on passive inference [14]. Let us quote the end of his introduction (our comments in brackets): “When the machine has no distinguishing sequences the reducing technique can help in minimizing the length of the checking experiment by iterative construction of the experiment. An initial sequence is applied to the machine and the resulting input-output sequence is reduced [by state merging]; the result will indicate a family of machines responding in the same way. An additional sequence which eliminates nondesired machines is then applied and another reduction is performed; by repeated application of the basic iteration the sequence will reduce uniquely to the checked machine [up to the initial state]. This method of checking experiment construction was tried for some examples but there is no proof yet to whether it is more efficient than other methods [10] and whether it will converge in all cases.”
Our approach shows that it is indeed possible to uniquely identify a non-resettable
deterministic complete machine, while building a checking sequence for it, with no
priori knowledge apart from a bound on the number of states, and the input set of the
machine. Contrary to previous work [9], it does not require a characterization set or
another assumption on sequences to distinguish states in the machine.

Section 2 will provide precise definitions for our formal framework, while Section
3 will define the inference problems and checking sequence generation in our context,
i.e. from a single trace for a non-resettable machine, in relation with the state of the art.
Section 4 shows how passive inference, i.e. the computation of a conjecture from a
single trace can be encoded into a Boolean formula, so that a SAT solver can be used
to efficiently get a conjecture. Sections 5 and 6 present our iterative approaches, show-
ing the two sides of the coin: checking sequence generation and active inference. Sec-
tion 7 presents experiments that show that the algorithms can work with middle-sized
automata. Section 8 concludes.

## 2 Definitions

A *Finite State Machine* (FSM) *M* is a 5-tuple (*S*, *s*₀, *I*, *O*, *T*), where *S* is a finite set of states with an initial state *s*₀; *I* and *O* are finite non-empty disjoint sets of inputs and outputs, respectively; *T* is a transition relation *T* ⊆ *S* × *I* × *O* × *S*, (*s*, *a*, *o*, *s*') ∈ *T* is a transition. When we need to refer to the machine *M* in a state *s* ∈ *S*, we write *M/s*.

*M* is completely specified (complete) if for each tuple (*s*, *a*) ∈ *S* × *I* there exists transition (*s*, *x*, *o*, *s*') ∈ *T*. It is deterministic if for each (*s*, *a*) ∈ *S* × *I* there exists at most one transition (*s*, *a*, *o*, *s*') ∈ *T*, otherwise it is nondeterministic. We consider in this paper only deterministic FSMs.

An *execution* of *M/s* is a sequence of transitions forming a path from *s* in the state transition diagram of *M*. The machine *M* is *initially* connected, if for any state *s* ∈ *S* there exists an execution from *s*₀ to *s*. *M* is *strongly* connected, if the state transition diagram of *M* is a strongly connected graph.

A *trace* of *M/s* is a string of input-output pairs which label an execution from *s*. Let *Tr*(*s*) denote the set of all traces of *M/s* and *Tr*<sub>*M*</sub> denote the set of traces of *M/s*₀. For trace ω ∈ *Tr*(*s*), we use *s*-after-ω to denote the state *M* reached after the execution of ω, for an empty trace ε, *s*-after-ε = *s*. When *s* is the initial state then we write *M*-after-ω instead of *M/s*₀-*after*-ω.

Let also *out*(*s*, α) be an output sequence produced by the input sequence α ∈ I* in *M/s*. For input sequence α applied in state *s*, we let *tr*<sub>s</sub>(*α*) denote the trace with the input projection α; we will omit the subscript when no confusion occurs.

Given an input sequence α, states *s*, *s'* ∈ *S* are *equivalent w.r.t.* α, if *out*(*s*, α) = *out*(*s'*, α), denoted *s* ≅ α *s'*, they are *distinguishable* by α, if *out*(*s*, α) ≠ *out*(*s'*, α), denoted *s* ≠ α *s'* or simply *s* ≠ *s'*. A *distinguishing sequence* of *M* is an input sequence α for which the output sequence produced by *M* in response to α identifies the state of *M*: for all *s*, *s'* ∈ *S*, *out*(*s*, α) ≠ *out*(*s'*, α). A *characterization set* of *M* is a set input sequences such that every *s*, *s'* ∈ *S*, there exists a sequence α in the set such that *out*(*s*, α) ≠ *out*(*s'*, α).
α). States $s$ and $s'$ are equivalent if they are equivalent w.r.t. all input sequences, thus $\mathrm{Tr}(s) = \mathrm{Tr}(s')$, denoted $s \cong s'$. The equivalence and distinguishability relations between FSMs is similarly defined. Two FSMs are equivalent if their initial states are equivalent. A complete FSM is *minimal*, if it has no equivalent states.

Given two FSMs $M = (S, s_0, I, O, T)$ and $M' = (S', s'_0, I, O, T')$, their product $M \times M'$ is an FSM $(P, p_0, I, O, H)$, where $p_0 = (s_0, s'_0)$ is such that $P$ and $H$ are the smallest sets satisfying the following rule: If $(s, s') \in P$, $(s, x, o, t) \in T$, $(s', x, o', t') \in T'$, and $o = o'$, then $(t, t') \in P$ and $((s, s'), x, o, (t, t')) \in H$.

**Lemma.** If $M$ and $M'$ are complete machines then they are equivalent iff the product $M \times M'$ is complete in the input set $I$.

Two complete FSMs $M = (S, s_0, I, O, T)$ and $M' = (S', s'_0, I, O, T')$ are called *isomorphic* if there exists a bijection $f: S \to S'$ such that $f(s_0) = s'_0$ and for all $a \in I, o \in O$, and $s \in S, f(s\text{-after-ao}) = f(s\text{-after-ao})$. Isomorphic FSMs are equivalent, but the converse does not necessarily hold. Note that we do not require equivalent machines to be minimal.

Given a trace $\omega \in (IO)^*$ of length $|\omega|$, let $\mathrm{Pref}(\omega)$ be the set of all prefixes of $\omega$. We define a linear FSM $W = (X, x_0, I, D_\omega)$, where $D_\omega$ is a transition relation, such that $|X| = |\omega| + 1$, and there exists a bijection $f: X \to \mathrm{Pref}(\omega)$, such that $f(x_0) = \varepsilon$, $(x_i, ao, x_{i+1}) \in D_\omega$ iff $f(x_i)ao = f(x_{i+1})$ for all $i = 0, \dots, |\omega| - 1$, in other words, $\mathrm{Tr}_W = \mathrm{Pref}(\omega)$. We call it an $\omega$-machine $W$.

While the set of traces of the $\omega$-machine is $\mathrm{Pref}(\omega)$, there are many FSMs which have the trace $\omega$ among other traces. We restrict our attention to the class of FSMs with at most $n$ states and alphabets $I$ and $O$, denoted $\mathfrak{J}(n, I, O)$. An FSM $C = (S, s_0, I, O, T)$, $C \in \mathfrak{J}(n, I, O)$ is called an $\omega$-conjecture, if $\omega \in \mathrm{Tr}_C$. Let $\mathfrak{J}_\omega(n, I, O)$ be the set of all $\omega$-conjectures in the set $\mathfrak{J}(n, I, O)$. Clearly, the $\omega$-machine is also an $\omega$-conjecture, if $|\omega| < n$.

The states of the $\omega$-machine $W = (X, x_0, I, D_\omega)$ and an $\omega$-conjecture $C = (S, s_0, I, O, T)$, $C \in \mathfrak{J}_\omega(n, I, O)$ are closely related to each other. A state of the $\omega$-machine reached after any prefix of the trace $\omega$ corresponds to a unique state of the $\omega$-conjecture that is reached after that prefix. Formally, there exists a mapping $\mu: X \to S$, such that $\mu(x) = s_0$-after-$f(x)$, the state reached by $C$ when the trace $f(x) \in \mathrm{Pref}(\omega)$ is executed. The mapping $\mu$ induces a partition $\pi_C$ on the set $X$ such that $x$ and $x'$ belong to the same block of the partition $\pi_C$, denoted $x =_{\pi_C} x'$, iff $\mu(x) = \mu(x')$.

Given an $\omega$-conjecture $C$ with the partition $\pi_C$, let $D$ be an $\omega'$-conjecture with the partition $\pi_D$, such that $\omega' \in \mathrm{Pref}(\omega)$, we say that the partition $\pi_C$ is an *expansion* of the partition $\pi_D$, if its projection to $\omega'$ coincides with the partition $\pi_D$; viz $\pi_D = \{P \cap X' | P \in \pi_C\}$ where $X' = \{x_i \in X | i \le |\omega'|\}$.

An input sequence $\alpha \in I^*$ is a *checking sequence* for a complete FSM $M$ with $n$ states if for each FSM $N \in \mathfrak{J}(n, I, O)$, such that $N \cong_\alpha M/s$, where $s \in S$, it holds that $N \cong M/s$. The trace $\mathrm{tr}_s(\alpha)$, where $\alpha$ is a checking sequence, is called a *checking trace* of $M$. In this definition, we allow uncertainty in the initial state of $M$ since it may have other states which converge with the initial state on a checking trace (an example of such an FSM can be found in Section 5).
Checking sequence is a special type of checking experiments for FSM, it is usually considered for FSM based testing when a reset operation in FSM implementations is unavailable or formidably costly to execute.

# 3 Problem Statement and Related Work

We consider the following closely related problems, passive and active FSM inference as well as checking sequence construction. Significantly, we restrict our setting to the case where a FSM may not be reset, so that the definitions we give here refer to a single trace. Actually, if a FSM can be reliably reset, the reset sequences can be included in the trace, so the definitions below can cover the general case. We state the problems using the definitions given above.

Passive inference is a classical problem whereby given a trace $ω$ we need to build an $ω$-conjecture with a minimal number of states [14][6][2].

Active inference, aka active automata learning, is another problem addressed in the literature [5]. Restated in our FSM context, given a black box, which behaves as an unknown minimal complete strongly connected FSM with the input alphabet *I* and the number of states equal to *n*, infer the FSM, i.e. build an $ω$-conjecture equivalent to the FSM and its checking trace $ω$.

The checking sequence problem differs from active inference in assuming that the expected behavior of a black box with at most *n* states submitted for testing is given as a strongly connected FSM *M* called a specification machine (which is unknown in active inference) and we need to determine its checking trace $ω$. The relation to passive inference is direct, once $ω$ is constructed, any $ω$-conjecture must be equivalent to *M*.

In this section, we briefly discuss the existing approaches addressing these problems which do not rely on the existence of a reset operation.

## 3.1 Passive Inference from a Single Trace

Passive FSM inference problem is stated by Kella in 1971 [14] as sequential machine identification and later as system/automaton identification problem by Gold [6]. The problem has been studied ever since. The problem is known to be computationally very hard, nevertheless, numerous proposals have been made, mainly on developing state merging techniques to transform an $ω$-machine into an $ω$-conjecture as small as possible, see, e.g., [14] [27] etc. The most recent approaches are based on satisfiability (SAT) solvers [1][11].

In Section 4, we propose an approach to build an $ω$-conjecture within a bound on the number of states using a SAT solver that avoids obtaining conjectures which were already considered.

## 3.2 Checking Sequence Problem

The problem of checking sequence generation from an FSM has a long history starting from work of Moore [15] and Hennie [10]. Almost all existing methods require a
machine be complete and minimal. Moreover, the vast majority of the proposed meth-
ods only apply to FSMs which have distinguishing sequences or distinguishing sets,
see, e.g. [4][7][12][22][23][26]. Not all FSMs possess these sequences and their con-
struction is a non-trivial problem. Only few methods can generate checking sequence
from complete and minimal FSM which has just characterization set and no other dis-
tinguishing sets, see [10][19][18]. Moreover, they cannot be called efficient, since the
size of a checking sequence generated by using characterization set grows exponen-
tially with the length and number of sequences in characterization set [25].

The problem of checking sequence generation without even checking the existence
of distinguishing sequences or finding an “optimal” or any other characterization set
remains open, to the best our knowledge. In Section 5 we propose an approach that does
not assume any distinguishing or characterization set computation.

3.3 Active Inference without Reset

Active inference has most often been addressed in the context of learning from samples and queries [5][8], so that the problem of dealing with a single trace has not received a lot of attention. An early attempt was proposed by [20], as an adaptation to Angluin's L\* algorithm. It assumes that an external oracle can be queried to provide a counterexample (hence an input sequence to distinguish the black box and the conjecture), and starts with the knowledge of a homing sequence. More recently an approach was proposed that does not require an external oracle, but still assumes knowledge of a characterization set [9].

However, the assumptions about the existence of an external oracle, knowledge of
homing or state characterizing sequences, such as distinguishing sequences and char-
acterization sets, are not easy to justify in practice, therefore the problem of active in-
ference of FSMs with neither reset operation nor strong assumptions about a given back
box remains open. In Section 6 we propose an approach that does not require such
assumptions.

4 Passive Inference with SAT solving

Since an ω-machine is itself an ω-conjecture, the minimization problem boils down to merging states of the ω-machine without introducing traces that would contradict the trace ω. Therefore by encoding a trace into a Boolean formula, and expressing state merging possibilities in that formula, we may use a SAT solver to determine acceptable mergers.

**4.1 Problem Encoding**

Here we present a procedure for encoding a trace into a Boolean formula, and at the
same time express a constraint on the number of states.

Let $W = (X, x_0, I, D_\omega)$ be an $\omega$-machine. To find an $\omega$-conjecture with at most $n$ states amounts to determine a partition $\pi$ on the set of states $X$ such that the number of blocks
does not exceed *n*. This problem can be casted as a constraint satisfaction problem (CSP) [3]. Let X be {$x_0, ..., x_{|O|}$}, so each integer variable represents a state of theomega-machine. Since theomega-machine is deterministic, the state variables satisfy the following constraint:

$$ \forall x_i, x_j \in X: $$

if $x_i \neq x_j$ then $x_i \neq x_j$ and

$$ \text{if } \exists a \in I \text{ s.t. } out(x_i, a) = out(x_j, a) = o \text{ then } x_i = x_j \Rightarrow x_i\text{-after-ao} = x_j\text{-after-ao} \quad (1) $$

If the number of states in anomega-conjecture to be constructed should be at most *n* then each state variable $x_i \in \{0, ..., n - 1\}$. Then an assignment of values to variables in {$x_0, ..., x_{|O|}$} such that the formula (1) is satisfied defines a mapping $\mu: X \to S$, where S is the set of states of anomega-conjecture, i.e., the mapping $\mu$ defines a partition of X into *n* blocks.

These formulas can be translated to SAT using unary coding for each integer variable $x \in X$, such that $x$ is represented by *n* Boolean variables $v_{x,0}, ..., v_{x,n-1}$. For each $x \in X$, we have the clause:

$$ v_{x,0} \lor \dots \lor v_{x,n-1} \quad (2) $$

These clauses mean that each state of theomega-machine W should be in at least one block.

For each state $x \in X$ and all $i, j \in \{0, ..., n - 1\}$ such that $i \neq j$, we have the clauses:

$$ \neg v_{x,i} \lor \neg v_{x,j} \quad (3) $$

The clauses mean that each state of theomega-machine W should be in at most one block.

Since a sought-afteromega-conjecture must be deterministic, the formula (1) is encoded into the following clauses. First, distinguishable states of W should be in different blocks, so for every $x, y \in X$ such that $x \neq y$ and all $i \in \{0, ..., n - 1\}$

$$ \neg v_{x,i} \lor \neg v_{y,i} \quad (4) $$

Second, states of W equivalent w.r.t. to some input if placed in the same block must have their successors also in one block. Hence for all $x_i, x_j \in X$ such that $out(x_i, a) = out(x_j, a) = o$ and all $i, j \in \{0, ..., n - 1\}$ we have a formula which can directly be translated into clauses

$$ (v_{x,i} \land v_{x',i}) \Rightarrow (v_{(x\text{-after-ao}),i} \Rightarrow v_{(x'\text{-after-ao}),i}) \quad (5) $$

To simplify learning that $x = y$ for some $x, y \in X$ we further rewrite the clauses (4) and (5) using auxiliary variables $e_{x,y}$ modeling the fact that $x = y$. For every $x, y \in X$ such that $x \neq y$ we have

$$ \neg e_{x,y} \quad (6) $$

For all $x, y \in X$ such that $out(x, a) = out(x, a) = o$, we have

$$ e_{x,y} \Rightarrow e_{x\text{-after-ao},y\text{-after-ao}} \quad (7) $$

The relation between auxiliary state variables is expressed in the following clauses. For every $x, y \in X$ and all $i \in \{0, ..., n - 1\}$

$$ e_{x,y} \land v_{x,i} \Rightarrow v_{y,i} \quad (8) $$

$$ \neg e_{x,y} \land v_{x,i} \Rightarrow \neg v_{y,i} \quad (9) $$

The resulting Boolean formula is the conjunction of clauses (2), (3), (6), (7), (8) and (9). To check its satisfiability one can use any of the existing solvers. If a solution exists
then we have an $\omega$-conjecture with $n$ or fewer states. The latter is obtained from the determined partition on $X$. In the context of passive inference, we are usually interested in finding an $\omega$-conjecture as small as possible. This requires several trials with varying values of $n$.

## 4.2 Passive Inference of Different (new) Conjectures

In the context of active inference as well as checking sequence construction we aim at obtaining a single $\omega$-conjecture while avoiding constructing isomorphic conjectures. A key building block will be provided by the following procedure to infer a conjecture that differs from already considered conjectures. We identify isomorphic conjectures by their common partition, hence we add as a constraint that we look for an $\omega$-conjecture that does not expand a set of “forbidden” partitions. If such $\omega$-conjectures are found they will be used in Sections 5 and 6 to augment the trace $\omega$ by adding suffixes that eliminate distinguishable conjectures until only one remains.

**Algorithm 1.** Infer_conjecture($\omega$, $n$, $\Pi$)

**Input:** A trace $\omega$, an integer $n$, and a set of partitions $\Pi$

**Output:** An $\omega$-conjecture with at most $n$ states such that its partition does not expand any partition in $\Pi$, or False.

1. *formula* = conjunction of the clauses (2), (3), (6), (7), (8) and (9)

2. **for all** $\pi \in \Pi$ **do**

3. &nbsp;&nbsp;&nbsp;&nbsp;*clause* = False

4. &nbsp;&nbsp;&nbsp;&nbsp;**for all** $x, y$ such that $x =_{\pi} y$ **do**

5. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*clause* = *clause* $\lor \neg e_{x,y}$

6. &nbsp;&nbsp;&nbsp;&nbsp;**end for**

7. *formula* = *formula* $\land$ *clause*

8. **end for**

9. **return** *call-solver*(*formula*)

# 5 Checking Sequence Construction

The idea of the proposed method for checking sequence (trace) generation is to find an FSM that reacts as the given specification FSM to a current input sequence using passive inference and eliminate it by extending the sequence with a suffix distinguishing the two machines or forbidding the passive inference from further regeneration if they cannot be distinguished any further. This process iterates until no more conjectures distinguishable from the given FSM can be found. The procedure is implemented in Algorithm 2.

**Algorithm 2.** Generating checking trace

**Input:** A complete strongly-connected FSM $M$ with $n$ states

**Output:** A checking trace $\omega$
1. $\omega := \varepsilon$

2. $\Pi := \emptyset$

3. **while** an $\omega$-conjecture $C$ is returned by Infer_conjecture($\omega, n, \Pi$) **do**

4. **if** $C$-after-$\omega \times M$-after-$\omega$ is complete **then**

5. $\Pi := \Pi \cup \{\pi_C\}$

6. **else**

7. Determine an input sequence $\beta a$ such that $\beta$ is a shortest transfer sequence from the state $C$-after-$\omega$ to a state with the undefined input $a$ in $C$-after-$\omega \times M$-after-$\omega$

8. $\omega := \omega\mathrm{tr}(\beta a)$, where $\mathrm{tr}(\beta a)$ is the trace of $M$-after-$\omega$

9. **end if**

10. **end while**

11. **return** $\omega$

Algorithm 2 calls Infer_conjecture($\omega, n, \Pi$), which in turn calls a SAT solver constraining it to avoid solutions of already considered conjectures.

Note that the Boolean formula used by the SAT solver is built incrementally by saving a current formula and adding only new clauses each time a trace $\omega$ or a set of partitions $\Pi$ is augmented.

**Theorem 1.** Given an FSM $M$ with $n$ states, Algorithm 2 returns a checking trace $\omega$.

*Sketch of the proof.* When Algorithm 2 terminates the resulting trace $\omega$ is indeed a checking one, since by the post-condition of Infer_conjecture no conjecture exists that is distinguishable from the given FSM $M$, after having executed $\omega$. Note that all complete conjectures equivalent to $M$ are excluded because as soon as one if found (including possibly $M$ itself), according to the Lemma, its partition is added to $\Pi$. Algorithm 2 always terminates, because the number of all possible conjectures with the fixed input alphabet within a given bound on the number of states $n$ is finite.

*Example.* Consider the FSM in Fig.1, it has no distinguishing sequence, its characterization set is $\{a, b\}$.

<figure><img src="image_2.png" /><figcaption>Fig.1. The FSM $M$</figcaption></figure>

This example is used in [18], where a method for checking sequence generation from a minimal FSM without distinguishing sequence is proposed. Using this example the authors of [18] compare their method with those of [10][19] and report that the length of checking sequence obtained by their method is 120, while that of [10] is 171 and 248 of [19].
Algorithm 1 implemented in a prototype tool presented in Section 6 returns the checking sequence $\omega = a0a1a0a1b0b1b0a0b0b1a0a1b0a0a1$ of length 15. Fig. 2 shows intermediate complete $\omega$-conjectures obtained executing Algorithm 1. Notice that the last but one conjecture is actually the FSM $M$, though, the same trace is also accepted by another conjecture, which is eliminated using the suffix $b0a0a1$.

<figure><img src="image_3.png" /><figcaption>Fig. 2. The $\omega$-conjectures generated by Algorithm 1 along with their versions of $\omega$; suffixes in bold show how $\omega$ grows.</figcaption></figure>

Note that the algorithm does not require the FSM to be minimal, moreover, it can be adapted to accept even a partial FSM. We are not aware of any method for checking sequence construction for FSMs which are partially defined and have compatible states, i.e., machines without characterization set. The only existing method which deals with such machines is [17], but it relies on the usage of the reset operation, as opposed to the approach proposed here.

# 6 Active Inference Approach

The iterative approach of Algorithm 2, which relied on computing a checking experiment for an $\omega$-conjecture that was consistent with the current prefix trace can be adapted to active inference. The trick is to find a checking experiment not between the reference
FSM *M* and the ω-conjecture, but between two possible ω-conjectures and retain the one that is consistent with the observations on the black box.

Given a black box BB, which behaves as an unknown minimal complete strongly connected FSM with the input alphabet *I* and a number of states equal to *n*, Algorithm 3 infers the FSM and constructs its checking trace.

**Algorithm 3.** Inferring BB and determining its checking trace

**Input** A black box BB, input set *I* and integer *n*

**Output** A minimal complete ω-conjecture with *n* states and a checking trace ω

1: ω := ε

2: Π := ∅

3: C := Infer_conjecture(ω, n, Π)

4: **while** an ω-conjecture *D* is returned by *Infer_conjecture*(ω, *n*, Π) **do**

5: if *D*/*D*-after-ω × *C*/*C*-after-ω is complete in the input set *I* then

6: Π := Π ∪ {π_D}

7: **else**

8: Determine an input sequence βa such that β is a shortest transfer sequence from the state C-after-ω to a state with the undefined input a in D/D-after-ω × C/C-after-ω

9: ω := ωtr(βa), where tr(βa) is the trace obtained by applying βa to BB

10: **if** ω ∉ Tr_C **then**

11: C := Infer_conjecture(ω, n, Π)

12: **end if**

13: **end if**

14: **end while**

15: **return** *C* and ω

**Theorem 2.** If a black box behaves as a minimal complete strongly connected FSM with the input alphabet *I* and the number of states equal to *n*, Algorithm 3 infers it and constructs a checking sequence and trace for it.

*Sketch of the proof.* Algorithm 3 follows the steps of Algorithm 2, just replacing the FSM *M* by a current conjecture. This does not influence its termination since it only occurs when no more distinguishable conjecture can be found. And at some point, because the black box behaves as a FSM with *n* states, it will be returned by *Infer_conjecture*, so that the remaining conjecture is equivalent to the FSM of the black box initialized in some state. The resulting trace accepted by that state is a checking one, as in Theorem 1.

*Example.* Consider that the FSM *M* in Fig.1 is a BB. Six intermediate complete ω-conjectures shown in Fig. 3 are obtained executing Algorithm 3. The last two conjectures both accept ω = a0a1a0b0b1b0b1a0a1b0a0a1a0a1. Both end up in state 2 from which they cannot be distinguished. The algorithm returns ω as a checking trace and the last but one conjecture which is isomorphic to FSM *M*/2. The last conjecture is isomorphic to FSM *M*/0. Indeed this trace is accepted by *M* in two states, 0 and 2.
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** The $\omega$-conjectures generated by Algorithm 3 along with their versions of $\omega$; suffixes in bold show how $\omega$ grows.</figcaption></figure>

The expected complexity of the proposed approach could be estimated by viewing it as a mutation-based technique which kills mutants. In our approach at each iteration only a mutant surviving a current trace can be generated and then killed, drastically reducing the complexity of mutation-based techniques. A naive worst-case estimation based on number of (potential) mutants would be grossly overestimated. This explains why we provide in the next section experimental results on the observed complexity with random machines.

# 7 Experiments

The prototype was developed on C++ depending only on a SAT Solver Cryptominisat [24], as a backend. All the experiments were performed on a virtual machine (VirtualBox) with 8 GiB of RAM and one CPU used. The computer has the processor 7-3770 and 16 GiB of RAM.

Table 1 presents experimental results on randomly generated FSMs. The numbers of inputs as well as outputs are fixed to two, while the number of state is varied. For each state number, 101 complete strongly connected machines are generated; they are not
necessarily minimal, since the approach does not require any state distinguishability. Each generated machine playing role of a specification FSM is used to construct checking sequence, and acting as a black box system is used for inference. Median values are collected for the length of resulting checking sequences |ω|, the number of times the solver is called (#solver), and execution time in seconds. The prototype scales for up to a dozen of states. This matches the state-of-the-art, see, e.g., [16].

<table><caption>Table 1. Experimental results with randomly generated FSMs with two inputs and outputs.</caption><thead><tr><th rowspan="3">n</th><th colspan="6">RANDOM FSMs</th></tr><tr><th colspan="3">Checking</th><th colspan="3">Inferring</th></tr><tr><th>|ω|</th><th>#solver</th><th>time</th><th>|ω|</th><th>#solver</th><th>time</th></tr></thead><tbody><tr><td>1</td><td>2</td><td>3</td><td>0.01</td><td>2</td><td>3</td><td>0.01</td></tr><tr><td>2</td><td>7</td><td>8</td><td>0.01</td><td>7</td><td>9</td><td>0.01</td></tr><tr><td>3</td><td>17</td><td>14</td><td>0.01</td><td>18</td><td>18</td><td>0.01</td></tr><tr><td>4</td><td>26</td><td>20</td><td>0.01</td><td>30</td><td>24</td><td>0.01</td></tr><tr><td>5</td><td>37</td><td>26</td><td>0.01</td><td>43</td><td>32</td><td>0.02</td></tr><tr><td>6</td><td>47</td><td>32</td><td>0.03</td><td>57</td><td>39</td><td>0.05</td></tr><tr><td>7</td><td>63</td><td>39</td><td>0.07</td><td>69</td><td>45</td><td>0.13</td></tr><tr><td>8</td><td>76</td><td>44</td><td>0.17</td><td>83</td><td>54</td><td>0.32</td></tr><tr><td>9</td><td>100</td><td>53</td><td>0.59</td><td>107</td><td>72</td><td>2.4</td></tr><tr><td>10</td><td>118</td><td>58</td><td>1.7</td><td>119</td><td>70</td><td>9.0</td></tr><tr><td>11</td><td>146</td><td>69</td><td>18.5</td><td>146</td><td>83</td><td>161</td></tr></tbody></table>

To assess the performance of the prototype to various numbers of inputs and outputs, another series of experiments reported in Table 2 were performed for machines with five states. Our experiments by varying their numbers separately show, unsurprisingly, that increasing number of inputs or outputs have opposite effects on the effectiveness, the more inputs the more complex the solutions (the search space is larger) but the more outputs the easier the solutions (more outputs increase distinguishability).

In addition, we performed another series of experiments using randomly generated lock machines (Table 3). A lock FSM (aka Moore lock, defined by him) with *n* states has a unique “locking” input sequence of length *n* which executes the “remotest” transition, the transitions not covered by this sequence all lead to the initial state resetting the lock. We consider lock machines as ultimate test for active inference and checking sequence generation methods. As before for each number of states we generate 101 random locks with two inputs and two outputs and collect the same parameters as above. Clearly, for a fixed number of states, locks differ only in labelling of unlocking sequences, which effects the performance of the prototype, since it chooses inputs completing and distinguishing conjectures following the lexicographical order.
<table><caption>Table 2. Experimental results with randomly generated arbitrary FSMs with five states.</caption><thead><tr><th rowspan="3">#inputs = #outputs</th><th colspan="6">RANDOM FSMs</th></tr><tr><th colspan="3">Checking</th><th colspan="3">Inferring</th></tr><tr><th>|ω|</th><th>#solver</th><th>time</th><th>|ω|</th><th>#solver</th><th>time</th></tr></thead><tbody><tr><td>2</td><td>37</td><td>26</td><td>0.01</td><td>43</td><td>32</td><td>0.02</td></tr><tr><td>3</td><td>51</td><td>40</td><td>0.03</td><td>57</td><td>47</td><td>0.05</td></tr><tr><td>4</td><td>68</td><td>53</td><td>0.04</td><td>70</td><td>58</td><td>0.09</td></tr><tr><td>5</td><td>74</td><td>62</td><td>0.05</td><td>81</td><td>71</td><td>0.12</td></tr><tr><td>6</td><td>88</td><td>73</td><td>0.07</td><td>95</td><td>85</td><td>0.2</td></tr><tr><td>7</td><td>101</td><td>83</td><td>0.09</td><td>109</td><td>99</td><td>0.3</td></tr><tr><td>8</td><td>113</td><td>95</td><td>0.12</td><td>121</td><td>111</td><td>0.38</td></tr><tr><td>9</td><td>121</td><td>102</td><td>0.12</td><td>127</td><td>122</td><td>0.5</td></tr><tr><td>10</td><td>138</td><td>114</td><td>0.18</td><td>145</td><td>136</td><td>0.72</td></tr><tr><td>20</td><td>257</td><td>212</td><td>0.63</td><td>276</td><td>261</td><td>3.2</td></tr><tr><td>30</td><td>377</td><td>312</td><td>1.3</td><td>425</td><td>391</td><td>10</td></tr><tr><td>40</td><td>525</td><td>412</td><td>2.5</td><td>517</td><td>571</td><td>22</td></tr></tbody></table>

<table><caption>Table 3. Experimental results with randomly generated lock FSMs.</caption><thead><tr><th rowspan="3">n</th><th colspan="6">RANDOM LOCKS</th></tr><tr><th colspan="3">Checking</th><th colspan="3">Inferring</th></tr><tr><th>|ω|</th><th>#solver</th><th>time</th><th>|ω|</th><th>#solver</th><th>time</th></tr></thead><tbody><tr><td>1</td><td>2</td><td>3</td><td>0.01</td><td>2</td><td>3</td><td>0.01</td></tr><tr><td>2</td><td>7</td><td>8</td><td>0.01</td><td>7</td><td>7</td><td>0.01</td></tr><tr><td>3</td><td>22</td><td>16</td><td>0.01</td><td>23</td><td>22</td><td>0.01</td></tr><tr><td>4</td><td>57</td><td>28</td><td>0.04</td><td>58</td><td>61</td><td>0.05</td></tr><tr><td>5</td><td>110</td><td>40</td><td>0.41</td><td>127</td><td>164</td><td>0.79</td></tr><tr><td>6</td><td>255</td><td>58</td><td>7.8</td><td>269</td><td>514</td><td>21</td></tr><tr><td>7</td><td>488</td><td>456</td><td>870</td><td>456</td><td>2202</td><td>970</td></tr></tbody></table>

It is interesting to notice that active inference and checking sequence construction have comparable lengths of the resulting input sequences. After all, in both cases a checking sequence for the same machine is generated.

We observe that the length of resulting sequences grows polynomially, the number of times the solver is called linearly and time exponentially with the number of states.

## 8 Conclusions

We have presented a method that can infer a model of a non-resettable black box FSM for which we only know an upper bound *n* on the number of states. It produces the model along with the input sequence that was used for inferring it. The algorithm terminates on a final model that is equivalent to the black-box FSM up to initialization,
and since it identifies a unique machine such that the input sequence is a checking sequence for this FSM.

The main benefit of this approach is that it only requires a bound on the number of states, no other assumption is needed, and the system does not have to be reset. This implies that it may have a wide spectrum of applications. The performance of active inference methods is usually assessed through the number of interactions with a system that are needed to infer it. Experiments have shown that the length of the input sequence implied by our approach is quite good. Another issue comes from the internal computations needed by the inference algorithm to build the model of the system. The method relies on a SAT solver to propose conjecture FSMs that are consistent with an observed trace. Unfortunately, this induces an exponential growth in the number of states, and this has been the limiting factor in our experiments. However, being able to infer state machines of up to a dozen states is in itself interesting for a large range of applications (many systems have relatively small state-space for the control part of their computations).

The approach seems promising, and can be improved in several directions. First, we have encoded the constraints for passive inference in a straightforward way, which puts a high burden on the constraint solver. It should be possible to encode the problem with more elements from the trace and FSM-structure to help the solver, with some guidance. Another direction we are investigating is to extract more information from previous conjectures and observations so as to reduce the number of calls to the solver to a minimum. In many cases, the calls to the solver can be avoided because it is possible to derive further checking experiments from the structure of the past conjecture(s). Instead of calling the solver to identify a new conjecture, it could be possible to refine the current conjecture.

**Acknowledgements.** This work was partially supported by MESI (Ministère de l'Économie, Science et Innovation) of Gouvernement du Québec and NSERC of Canada.

**References**

1. Abel, A., Reineke, J. MeMin SAT-based exact minimization of incompletely specified mealy machines. In IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 94-101 (2015)

2. Biermann, A. W., Feldman, J. A. On the synthesis of finite-state machines from samples of their behavior. IEEE transactions on Computers, 100(6), 592-597 (1972)

3. Carbonnel, C., Cooper, M.C. Tractability in constraint satisfaction problems: a survey. Constraints, 21(2), 115-144 (2016)

4. Boute, R.T. Distinguishing sets for optimal state identification in checking experiments. IEEE Transactions on Computers 23, 874-877 (1974)

5. De la Higuera, C. Grammatical inference: learning automata and grammars. Cambridge University Press (2010)

6. Gold, E. M. Complexity of automaton identification from given data. Information and control, 37(3), 302-320 (1978)

7. Gonenc, G. A method for the design of fault detection experiments. IEEE Transactions on Computers 19, 551-558 (1970)
8. Groz, R., Li, K., Petrenko, A., Shahbaz, M. Modular system verification by inference, testing and reachability analysis. In Testing of Software and Communicating Systems, Springer Berlin Heidelberg, 216-233 (2008)

9. Groz, R., Simao, A., Petrenko, A. and Oriat, C. November. Inferring finite state machines without reset using state identification sequences. In IFIP International Conference on Testing Software and Systems. Springer International Publishing, 161-177 (2015)

10. Hennie, F.C.: Fault-Detecting Experiments for Sequential Circuits. Proc. Fifth Annual Symp. On Circuit Theory and Logical Design, pp. 95–110 (1965)

11. Heule, M.J., Verwer, S. Exact DFA identification using SAT solvers. In International Colloquium on Grammatical Inference. Springer Berlin Heidelberg, 66-79 (2010)

12. Hierons, R.M., Ural, H. Optimizing the length of checking sequences. IEEE Transactions on Computers 55, 618–629 (2006)

13. C. de la Higuera, Grammatical Inference: Learning Automata and Grammars, Cambridge University Press, 2010.

14. Kella, J. Sequential machine identification. IEEE Transactions on Computers, 100(3), 332-338 (1971)

15. Moore, E.F. Gedanken experiments on sequential machines. In: Automata Studies. Annals of Mathematical Studies, vol. 34, pp. 129–153 (1956)

16. Oliveira, A. L., João PM Silva. "Efficient algorithms for the inference of minimum size dfas." Machine Learning 44, no.1, 93-119 (2001)

17. Petrenko A., Yektushenko. N. Testing from partial deterministic FSM specifications, IEEE Transactions on Computers, 54(9), 1154-1165 (2005)

18. Porto F.R., Endo A.T., Simao A. Generation of checking sequences using identification sets. In: ICFEM 2013. LNCS, vol. 8144. Springer, Berlin, Heidelberg (2013)

19. Rezaki, A., Ural, H.: Construction of checking sequences based on characterization sets. Computer Communications 18, 911–920 (1995)

20. Rivest, R.L., Schapire, R.E. Inference of finite automata using homing sequences. In Machine Learning: From Theory to Applications. Springer Berlin Heidelberg, 51-73 (1993)

21. Sabnani, K., Dahbura, A. A protocol test generation procedure. Computer Networks 15: 285-297 (1988)

22. Simao, A.S., Petrenko, A. Generating checking sequences for partial reduced finite state machines. TestCom/FATES 2008. LNCS, vol. 5047, Springer, Heidelberg, 153–168 (2008)

23. Simao, A., Petrenko, A. Checking sequence generation using state distinguishing subsequences. In: The IEEE ICST Workshops, 48–56 (2009)

24. Soos, M. CryptoMiniSat – a SAT solver for cryptographic problems. http://www.msoos.org/cryptominisat (2009).

25. Vasilevski, M. P. Failure diagnosis of automata. Cybernetics, Plenum Publishing Corporation, New York, No 4, 653-665, (1973)

26. Yannakakis, M. and Lee, D. Testing finite state machines: fault detection. Journal of Computer and System Sciences, 50, 209-227 (1995)

27. Yao, M., Petrenko, A. and Bochmann, G.V. Conformance testing of protocol machines without reset. In Proceedings of the IFIP Thirteenth International Symposium on Protocol Specification, Testing and Verification. North-Holland Publishing Co. 241-256 (1993)