11institutetext:  Computer Science Department,
Quaid i Azam University, Islamabad 45320, Pakistan,
<EMAIL_ADDRESS>
# An Efficient Model Inference Algorithm
for Learning-based Testing of Reactive Systems

Muddassar A. Sindhu

###### Abstract

Learning-based testing (LBT) is an emerging methodology to automate iterative
black-box requirements testing of software systems. The methodology involves
combining model inference with model checking techniques. However, a variety
of optimisations on model inference are necessary in order to achieve scalable
testing for large systems.

In this paper we describe the IKL learning algorithm which is an active
incremental learning algorithm for deterministic Kripke structures. We
formally prove the correctness of IKL. We discuss the optimisations it
incorporates to achieve scalability of testing. We also evaluate a black box
heuristic for test termination based on convergence of IKL learning.

##  1 Introduction

A heuristic approach to automated test case generation (ATCG) from formal
requirements specifications known as learning-based testing (LBT) was
introduced in [13], [14] and [17]. Learning-based testing is an iterative
approach to automate specification-based black-box testing. It encompasses
both test case generation, execution and evaluation (the oracle step). The aim
of LBT is to automatically generate a large number of high-quality test cases
by combining a model checking algorithm with an optimised model inference
algorithm (aka. learning algorithm). For both procedural ([14]) and reactive
systems ([15], [17]) it has been shown that LBT can significantly outperform
random testing in the speed with which it finds errors in a system under test
(SUT). This is because random test suites generally contain a large degree of
redundancy, which can be reduced by using learning algorithms and model
checkers to execute a more directed search for software errors.

An efficient and practical implementation of learning-based testing for
reactive systems has been developed in the LBTest tool [18]. In this paper we
describe the IKL (Incremental Kripke Learning) algorithm implemented in
LBTest. IKL is an algorithm for active incremental learning of deterministic
Kripke structures. The reliability of LBTest for producing correct test
results depends crucially on the correctness of this learning algorithm. So we
give a formal definition of IKL and prove its correctness. The IKL algorithm
involves a number of optimisations necessary to achieve scalability of testing
for large software systems. We discuss these optimisations from the
perspective of learning and testing.

The problems of coverage, and termination criteria for black-box testing, are
complex and different solutions have been proposed. In LBT, convergence of
learning can sometimes be used as a criterion to terminate testing. However,
heuristics are needed to estimate convergence in the context of black box
testing. We will empirically evaluate the reliability of a simple heuristic
for IKL.

In the remainder of Section 1, we discuss the general paradigm of LBT, and
specific requirements on learning for efficient testing of reactive systems.
In Section 2, we review some essential mathematical preliminaries. In Section
3, we present the architecture of the IKL learning algorithm and its main
components. These three main components are defined and analysed in detail in
Sections 4, 5 and 6. In Section 4, we consider a learning algorithm for
families of DFA which supports incremental learning and projection (to be
discussed in Section 1.2). In Section 5, we consider integrating a family of
DFA into a single Kripke structure using a subdirect product construction. In
Section 6, we consider an efficient minimisation algorithm for deterministic
Kripke structures based on Hopcroft’s DFA minimisation algorithm [12]. This is
needed by the IKL algorithm to produce hypothesis models that can be
efficiently model checked. In Section 7, we empirically evaluate a black box
heuristic to detect convergence of IKL, that can be used as a test termination
criterion. Finally, in Section 8 we draw some conclusions and suggest
prospects for further research on learning and testing.

###  1.1 Learning-Based Testing

The basic LBT paradigm requires three components: (1) a (black-box) system
under test (SUT) $S$, (2) a formal requirements specification ${\it Req}$ for
$S$, and (3) a learned model $M$ of $S$. Now (1) and (2) are common to all
specification-based testing, and it is really (3) that is distinctive.
Learning-based testing is a heuristic iterative method to automatically
generate a sequence of test cases. The heuristic concept is to learn a black-
box system using tests as queries.

In general, an LBT algorithm iterates the following four steps: (Step 1)
Suppose that $n$ test case inputs $i_{1},\hskip 3.0pt\ldots,\hskip 3.0pti_{n}$
have been executed on $S$ yielding the system outputs $o_{1},\hskip
3.0pt\ldots,\hskip 3.0pto_{n}$. The $n$ input/output observations
$(i_{1},\hskip 3.0pto_{1}),\hskip 3.0pt\ldots,\hskip 3.0pt$ $(i_{n},\hskip
3.0pto_{n})$ can be synthesized into a learned model $M_{n}$ of $S$ using an
incremental learning algorithm (see Section 1.2). This step involves
generalization from the observed behaviour, (which represents an incomplete
description of $S$) to all possible behaviour. This generalisation step gives
the possibility to predict previously unseen errors in $S$ during Step 2.
(Step 2) The system requirements ${\it Req}$ are checked against the learned
model $M_{n}$ derived in Step 1 (aka. model checking). This process searches
for a counterexample $i_{n+1}$ to the requirements. (Step 3) The
counterexample $i_{n+1}$ is executed as the next test case on $S$, and if $S$
terminates then the output $o_{n+1}$ is obtained. If $S$ fails this test case
(i.e. the observation $(i_{n+1},\hskip 3.0pto_{n+1})$ does not satisfy ${\it
Req}$) then $i_{n+1}$ was a true negative and we proceed to Step 4. Otherwise
$S$ passes the test case $i_{n+1}$ so the model $M_{n}$ was inaccurate, and
$i_{n+1}$ was a false negative. In this latter case, the effort of executing
$S$ on $i_{n+1}$ is not wasted. We return to Step 1 and apply the learning
algorithm once again to $n+1$ pairs $(i_{1},\hskip 3.0pto_{1}),\hskip
3.0pt\ldots,\hskip 3.0pt(i_{n+1},\hskip 3.0pto_{n+1})$ to infer a refined
model $M_{n+1}$ of $S$. (Step 4) We terminate with a true negative test case
($i_{n+1}$, $o_{n+1}$) for $S$.

Thus an LBT algorithm iterates Steps $1\dots$ 3 until an SUT error is found
(Step 4) or execution is terminated. Practical criteria for termination of
testing include a bound on the maximum testing time, or a bound on the maximum
number of test cases to be executed. However, it also seems possible to derive
more theoretically well-founded criteria for termination based on learning
theory. One simple approach will be discussed in Section 7. A more
sophisticated proposal can be found in [25].

This iterative approach to automated test case generation yields a sequence of
increasingly accurate models $M_{0}$, $M_{1}$, $M_{2}$, $\ldots$, of $S$. (We
usually take $M_{0}$ to be a null hypothesis about $S$.) So, with increasing
values of $n$, it becomes more and more likely that model checking in Step 2
will produce a true negative if one exists.

Notice, if Step 2 does not produce any counterexamples at all then to proceed
with the next iteration, we must construct the next test case $i_{n+1}$ by
some other method. Now active learning algorithms can be devised to generate
queries that efficiently learn an unknown system in polynomial time. So for
LBT there is clearly an advantage to combine model checking with active
learning and generate both types of test cases. More generally, it is useful
to have access to as wide a variety of query generation techniques as
possible. So in practice, model checker and active learning queries are
augmented with random queries when necessary. However, these different types
of queries need to be combined carefully to achieve efficient and scalable
testing.

###  1.2 Learning for Efficient Testing

As has already been suggested in Section 1.1, for LBT to be effective at
finding errors, it is important to use the right kind of learning algorithm.
As well as active learning, several other principles for efficient testing can
be found. To motivate the design of the IKL algorithm we will discuss two of
them. For this purpose, we focus specifically on automata learning for testing
reactive systems. (LBT has also been successfully applied to testing other
types of systems, see e.g. [14]). Learning algorithms for automata are also
known as regular inference algorithms in the literature (e.g. [8]).

####  1.2.1 Incremental Learning

One efficiency principle is that a good learning algorithm should maximise the
opportunity of the model checker in Step 2 above to find a true counterexample
$i_{n+1}$ to the requirements ${\it Req}$ as soon as possible. An automata
learning algorithm $L$ is said to be incremental if it can produce a sequence
of hypothesis automata ${\mathcal{A}}_{0},\hskip 3.0pt{\mathcal{A}}_{1},\hskip
3.0pt\ldots$ which are approximations to an unknown automata ${\mathcal{A}}$,
based on a sequence of observations of the input/output behaviour of
${\mathcal{A}}$. The sequence ${\mathcal{A}}_{0},\hskip
3.0pt{\mathcal{A}}_{1},\hskip 3.0pt\ldots$ must finitely converge to
${\mathcal{A}}$, at least up to behavioural equivalence. In addition, the
computation of each new approximation ${\mathcal{A}}_{i+1}$ by $L$ should
reuse as much information as possible about the previous approximation
${\mathcal{A}}_{i}$ (e.g. equivalences between states). Incremental learning
algorithms are necessary for two reasons. (1) Real world systems are often too
big to be completely learned and tested within a feasible timescale. This is
mainly due to: (i) the time complexity of learning and model checking
algorithms, and (ii) the time needed to execute the individual test cases on a
large SUT.

(2) Testing of specific requirements such as use cases may not require
learning and analysing the entire SUT $S$, but only the relevant fragment of
$S$ which implements the requirement ${\it Req}$.

For these two reasons, the IKL learning algorithm used in LBTest is based on
incremental learning.

This concept of a relevant fragment of an SUT for testing a requirement ${\it
Req}$ raises the question of the relative efficiency of different types of
queries (test cases). We have already seen that in LBT, test cases can be
generated by model checking, by active learning, or by some other process
entirely such as random querying.

As indicated in (1) above, the overhead of SUT execution time to answer an
individual query can be large compared with the execution time of learning and
model checking. There are examples of industrial systems where this execution
time is of the order of minutes. So realistically, queries should be seen as
“expensive”. From the viewpoint of relevance therefore, as many queries as
possible should be derived from model checking the hypothesis automaton, since
these queries are all based on checking the requirements ${\it Req}$.
Conversely as few queries as possible should be derived from the active
learning algorithm. Active learning queries have no way to reference the
requirement ${\it Req}$, and therefore can only uncover an SUT error by
accident. Furthermore, active learning queries may explore parts of the SUT
which are irrelevant to checking ${\it Req}$, thereby leading the search for
errors in a fruitless direction. Ideally, every query would represent a
relevant and interesting requirements-based test case.

However, there is conflicting issue involved here, which is the computational
effort needed to generate different types of queries. Model checker generated
queries are generally computationally expensive relative to active learner
generated queries, often by several orders of magnitude. Therefore, if too
many (perhaps even all) queries are generated by model checking, then the LBT
process may slow so much that random testing is simply faster. In a practical
LBT tool, the ratio between the number of model checker generated queries, and
the number of active learning queries must be controlled to achieve a balance
between relevance and speed. The IKL algorithm implements a pragmatic balance
between these two types of queries that we have found to be reasonably
efficient in practise.

Interestingly, when the balance of active learning queries becomes very high,
and model checking queries are almost eliminated, we might think that LBT
becomes similar to random testing. However [26] shows that this is not the
case. Thus using active learner queries alone, LBT can achieve better
functional coverage than random testing.

####  1.2.2 Projection

When we consider the output variables of the SUT $S$ that appear in a specific
formal black box requirement ${\it Req}$, we often see just a small subset of
the set of all output variables of $S$. This observation points to a powerful
abstraction technique for learning that can be termed bit-slicing (for
propositional variables) or more generally projection.

Like incremental learning, projection is another abstraction method that
concentrates on learning only the relevant SUT behavior needed to test the
requirement ${\it Req}$. Essentially, projection involves learning a quotient
model of the SUT by observing just the output variables appearing in ${\it
Req}$. Since quotient models of $S$ may be dramatically smaller than $S$
itself, the time needed for learning and testing may be considerably reduced.
Therefore, projection seems to be an essential component of a scalable LBT
system. Indeed, the combination of incremental learning and projection seems
to be particularly powerful. The IKL algorithm incorporates both these
features, and they will be discussed in further detail in Sections 3 and 4.

###  1.3 Literature Survey

Several previous works, (for example Peled et al. [22], Groce et al. [11] and
Raffelt et al. [23]) have considered a combination of learning and model
checking to achieve testing and/or formal verification of reactive systems.
Within the model checking community the verification approach known as
counterexample guided abstraction refinement (CEGAR) also combines learning
and model checking, (see e.g. Clarke et al. [7] and Chauhan et al. [6]). The
LBT approach can be distinguished from these other approaches by: (i) an
emphasis on testing rather than verification, and (ii) the use of incremental
learning and other abstraction techniques specifically chosen to achieve
scalable testing and faster error discovery (c.f. Section 1.2).

In practise, most of the well-known classical regular inference algorithms
such as L* (Angluin [2]) or ID (Angluin [1]) are designed for complete rather
than incremental learning. Among the much smaller number of known incremental
learning algorithms, we can mention the RPNII algorithm (Dupont [9]) and the
IID algorithm (Parekh et al. [21]) which learn Moore automata, and the ICGE
algorithm (Meinke and Fei [16]) which learns Mealy automata over abstract data
types. No algorithm which combines incremental learning and projection has
been published in the literature. The problem of integrating active learning
queries with model checker generated queries (which in some sense take over
the role of Angluin’s equivalence checker [2]) has also not been considered.
Thus: (i) the design of the IKL algorithm, (ii) its formal proof of
correctness, and (iii) its motivation by efficient test case generation
represent the main novel contributions of our paper.

The use of minimisation algorithms in automata learning also seems not to have
been considered. This is mainly because most DFA learning algorithms naturally
infer the canonical minimal automaton. However, our use of projection as an
abstraction method for learning large Kripke structures does not lead
immediately to minimal structures. In fact, inferring non-minimal automata can
even lead to efficiency gains as we have shown elsewhere in [16].

For different automata models and different notions of equivalence, the
complexity of the minimisation problem can vary considerably. The survey [3]
considers minimisation algorithms for DFA up to language equivalence, with
time complexities varying between $\mathcal{O}(n^{2})$ and
$\mathcal{O}(n\;log\;n)$. Kripke structures represent a generalisation of DFA
to allow non-determinism and multiple outputs. They have been widely used to
model concurrent and embedded systems. An algorithm for mimimizing Kripke
structures has been given in [5]. In the presence of non-determinism, the
complexity of minimisation is quite high. Minimisation up to language
equivalence requires exponential time, while minimisation up to a weaker
simulation equivalence can be carried out polynomial time (see [5]). By
contrast, we will show that deterministic Kripke structures can be efficiently
minimized even up to language equivalence with a worst case time complexity of
$\mathcal{O}(kn\log_{2}n)$. Our generalisation of Hopcroft’s DFA minimisation
algorithm to deterministic Kripke structures in Section 6 is fairly simple and
straightforward. Nevertheless, this algorithm has not been previously
published in the literature, and represents another novel contribution.

##  2 Mathematical Preliminaries and Notation

In this section we introduce some basic concepts and notations needed to
define and prove the correctness of the IKL learning algorithm. Let $\Sigma$
be any set of symbols then $\Sigma^{*}$ denotes the set of all finite strings
over $\Sigma$ including the empty string $\varepsilon$. The length of a string
$\alpha\in\Sigma^{*}$ is denoted by $|\alpha|$ and $|\varepsilon|=0$. For
strings $\alpha,\beta\in\Sigma^{*}$, $\alpha{\hskip 3.0pt.\hskip 3.0pt}\beta$
denotes their concatenation.

For $\alpha,\beta,\gamma\in\Sigma^{*}$, if $\alpha=\beta\gamma$ then $\beta$
is termed a prefix of $\alpha$ and $\gamma$ is termed a suffix of $\alpha$. We
let ${\it Pref}(\alpha)$ denote the prefix closure of $\alpha$, i.e. the set
of all prefixes of $\alpha$. We can also apply prefix closure pointwise to any
set of strings. The set difference operation between two sets $U,V$, denoted
by $U-V$, is the set of all elements of $U$ which are not members of $V$. The
symmetric difference operation on pairs of sets is defined by $U\oplus
V=(U-V)\cup(V-U)$.

A deterministic finite automaton (DFA) is a five-tuple
${\mathcal{A}}=(\Sigma,Q,F,q_{0},\delta)$ where: $\Sigma$ is the input
alphabet, $Q$ is the state set, $F\subseteq Q$ is the accepting state set and
$q_{0}\in Q$ is the starting state. The state transition function of
${\mathcal{A}}$ is a mapping $\delta:Q\times\Sigma\to Q$ with the usual
meaning, and can be inductively extended to a mapping
$\delta^{*}:Q\times\Sigma^{*}\to Q$ where $\delta^{*}(q,\hskip
3.0pt\varepsilon)=q$ and $\delta^{*}(q,\hskip 3.0pt\sigma_{1},\hskip
3.0pt\ldots\sigma_{n+1})=\delta(\delta^{*}(q,\hskip 3.0pt\sigma_{1},\hskip
3.0pt\ldots\sigma_{n}),\hskip 3.0pt\sigma_{n+1})$.

A dead state is a state from which no accepting state can be reached, and a
state which is not dead is termed live. Since input strings can be used to
name states, given any distinguished dead state $d_{0}$ we define string
concatenation modulo the dead state $d_{0}$,
$f:\Sigma^{*}\cup\\{d_{0}\\}\times\Sigma\to\Sigma^{*}\cup\\{d_{0}\\}$, by
$f(d_{0},\hskip 3.0pt\sigma)=d_{0}$ and $f(\alpha,\hskip
3.0pt\sigma)=\alpha{\hskip 3.0pt.\hskip 3.0pt}\sigma$ for
$\alpha\in\Sigma^{*}$. This function is used for automaton learning in Section
4.

The language $L({\mathcal{A}})$ accepted by ${\mathcal{A}}$ is the set of all
strings $\alpha\in\Sigma^{*}$ such that $\delta^{*}(q_{0},\hskip
3.0pt\alpha)\in F$. A language $L\subseteq\Sigma^{*}$ is accepted by a DFA if
and only if, $L$ is regular, i.e. $L$ can be defined by a regular grammar.

A generalisation of DFA to allow multi-bit outputs on states is given by
deterministic Kripke structures.

2.1. Definition. Let $\Sigma=\\{\hskip 5.0pt\sigma_{1},\hskip
3.0pt\ldots,\hskip 3.0pt\sigma_{n}\hskip 5.0pt\\}$ be a finite input alphabet.
By a $k$-bit deterministic Kripke structure ${\mathcal{A}}$ we mean a five-
tuple

${\mathcal{A}}=(\hskip 3.0ptQ_{\mathcal{A}},\hskip 3.0pt\Sigma,\hskip
3.0pt\delta_{\mathcal{A}}:Q_{\mathcal{A}}\times\Sigma\to
Q_{\mathcal{A}},\hskip 3.0ptq_{\mathcal{A}}^{0},\hskip
3.0pt\lambda_{\mathcal{A}}:Q_{\mathcal{A}}\to{\mathbb{B}}^{k}\hskip 3.0pt)$

where $Q_{\mathcal{A}}$ is a state set, $\delta_{\mathcal{A}}$ is the state
transition function, $q_{\mathcal{A}}^{0}$ is the initial state and
$\lambda_{\mathcal{A}}$ is the output function.

As before we let $\delta_{\mathcal{A}}^{*}:Q_{\mathcal{A}}\times\Sigma^{*}\to
Q_{\mathcal{A}}$ denote the iterated state transition function, where
$\delta_{\mathcal{A}}^{*}(q,\hskip 3.0pt\varepsilon)=q$ and
$\delta_{\mathcal{A}}^{*}(q,\hskip 3.0pt\sigma_{1},\hskip 3.0pt\ldots,\hskip
3.0pt\sigma_{i+1})=\delta_{\mathcal{A}}(\delta_{\mathcal{A}}^{*}(q,\hskip
3.0pt\sigma_{1},\hskip 3.0pt\ldots,\hskip 3.0pt\sigma_{i}),\hskip
3.0pt\sigma_{i+1})$. Also we let
$\lambda_{\mathcal{A}}^{*}:\Sigma^{*}\to{\mathbb{B}}^{k}$ denote the iterated
output function $\lambda_{\mathcal{A}}^{*}(\sigma_{1},\hskip
3.0pt\ldots,\hskip
3.0pt\sigma_{i})=\lambda_{\mathcal{A}}(\delta_{\mathcal{A}}^{*}(q_{\mathcal{A}}^{0},\hskip
3.0pt\sigma_{1},\hskip 3.0pt\ldots,\hskip 3.0pt\sigma_{i}))$. More generally
for any $q\in Q$ define
$\lambda_{q}^{*}(\sigma_{1},...,\sigma_{i})=\lambda_{\mathcal{A}}(\delta_{\mathcal{A}}^{*}(q,\hskip
3.0pt\sigma_{1},\hskip 3.0pt\ldots,\hskip 3.0pt\sigma_{i}))$. Given any
$R\subseteq Q$ we write $\lambda(R)=\cup_{r\in R}\lambda(r)$. We let
$q.\sigma$ denote $\delta(q,\sigma)$ and $R.\sigma$ denotes
$\\{r.\sigma\;|\;r\in R\\}$ for $R\subseteq Q$.

Note that a $1$-bit deterministic Kripke structure ${\mathcal{A}}$ is
isomorphic to a DFA ${\mathcal{A}}^{\prime}=(\hskip
3.0ptQ_{{\mathcal{A}}^{\prime}},\hskip 3.0pt\Sigma,\hskip
3.0pt\delta_{{\mathcal{A}}^{\prime}}:Q_{{\mathcal{A}}^{\prime}}\times\Sigma\to
Q_{{\mathcal{A}}^{\prime}},\hskip 3.0ptq_{{\mathcal{A}}^{\prime}}^{0},\hskip
3.0ptF_{{\mathcal{A}}^{\prime}}\hskip 3.0pt)$, where
$F_{{\mathcal{A}}^{\prime}}\subseteq Q_{{\mathcal{A}}^{\prime}}$ and
$\lambda_{{\mathcal{A}}^{\prime}}(q)={\it true}$ if, and only if $q\in
F_{{\mathcal{A}}^{\prime}}$.

In the context of Boolean valued output variables, the concept of projection
on a set of output variables will also be termed bit slicing. Let us make
precise the concept of a bit-slice or projection of a Kripke structure. 2.2.
Definition. Let ${{\mathcal{A}}}$ be a $k$-bit Kripke structure over a finite
input alphabet $\Sigma$,

${{\mathcal{A}}}=(\hskip 3.0ptQ_{{\mathcal{A}}},\hskip 3.0pt\Sigma,\hskip
3.0pt\delta_{{\mathcal{A}}}:Q_{{\mathcal{A}}}\times\Sigma\to
Q_{{\mathcal{A}}},\hskip 3.0ptq_{{\mathcal{A}}}^{0},\hskip
3.0pt\lambda_{{\mathcal{A}}}:Q_{{\mathcal{A}}}\to{\mathbb{B}}^{k}\hskip
3.0pt).$

For each $1\leq i\leq k$ define the $i$-th projection ${{\mathcal{A}}}_{i}$ of
${{\mathcal{A}}}$ to be the $1$-bit Kripke structure where

${{\mathcal{A}}}_{i}=(\hskip 3.0ptQ_{{\mathcal{A}}},\hskip 3.0pt\Sigma,\hskip
3.0pt\delta_{{\mathcal{A}}}:Q_{{\mathcal{A}}}\times\Sigma\to
Q_{{\mathcal{A}}},\hskip 3.0ptq_{{\mathcal{A}}}^{0},\hskip
3.0pt\lambda_{{{\mathcal{A}}}_{i}}:Q_{{\mathcal{A}}}\to{\mathbb{B}}\hskip
3.0pt),$

and $\lambda_{{{\mathcal{A}}}_{i}}(q)=\lambda_{{\mathcal{A}}}(q)_{i}$, i.e.
$\lambda_{{{\mathcal{A}}}_{i}}(q)$ is the $i$-th bit of
$\lambda_{{\mathcal{A}}}(q)$.

A family of $k$ individual $1$-bit Kripke structures can be combined into a
single $k$-bit Kripke structure using a subdirect product construction. This
will be discussed in Section 5.

A Kripke structure ${{\mathcal{A}}}$ is minimal if it has no proper
subalgebra. This is equivalent to all states of ${{\mathcal{A}}}$ being
reachable from the initial state by means of some input string. If
${{\mathcal{A}}}$ is a Kripke structure then ${{\mathcal{A}}}$ always has a
minimal subalgebra which we denote by $Min({{\mathcal{A}}})$.

##  3 Architecture of the IKL Algorithm

As discussed in Section 1, IKL is an algorithm for incrementally inferring a
deterministic $k$-bit Kripke structure from observational data. For efficient
testing, it also implements projection on output variables. An architectural
view of the IKL algorithm is given in Figure 1. The basic idea of the
algorithm is to learn a $k$-bit Kripke structure as a family of $k$ $1$-bit
Kripke structures (i.e. DFA) using an incremental DFA learning algorithm for
each of the $k$ individual DFA.

Figure 1: Architecture of the IKL algorithm.

For DFA learning, we use an incremental refinement of Angluin’s ID algorithm
[1]. The dead state $d_{0}$ used in the ID algorithm can be used in
incremental learning as an abstraction for all currently unknown information
about the system to be learned. Our refinement of ID differs from the IID
learning algorithm described in [21] in ways which have been discussed in
[24]. Note that the IKL architecture is modular, in the sense that other DFA
learning algorithms could be used instead of ID. These might alter the overall
performance of IKL from a testing perspective (see Section 8).

As Figure 1 indicates, these $k$ incremental DFA learning algorithms must co-
operate in order to jointly learn an entire family of DFA. This co-operation
between the DFA learners is termed lazy learning. It is used to support more
frequent model checking during testing, which is desirable for the reasons
explained in Section 1.2. The goal of lazy learning then is to learn the DFA
family in a way that can produce new $k$-bit hypothesis Kripke structures with
maximum frequency.

The $k$ individual DFA are assembled into a single $k$-bit Kripke structure
using a generalisation of the direct product construction known as a subdirect
product. Without minimisation, the state space of the product automaton would
be very large. However, the state space can be reduced on the fly, resulting
in a subalgebra of the direct product. This removes all states which are not
reachable from the initial state, using some input string. The state space of
this subdirect product is typically still very large. In order to minimise the
state space even further, we finally apply a minimisation algorithm for Kripke
structures. For this we adapt Hopcroft’s minimisation algorithm for DFA [12],
and generalise it to Kripke structures. We will discuss the state space sizes
achieved by the intermediate Kripke structures during the incremental learning
process in Section 7.

In the next three sections we define and prove correct the three major
components of the IKL algorithm:

(i) the DFA family learning algorithm ${FID}$ (Section 4),

(ii) the subdirect product construction (Section 5), and

(iii) a Kripke structure minimisation algorithm (Section 6)

##  4 Incremental Learning of DFA Families

In this section we define and prove correct an algorithm ${FID}$ for
incremental lazy learning of a family of DFA that share a common input. This
approach supports bit-sliced learning of a large Kripke structure by
projection of specific output variables (c.f. Section 1.2). Our algorithm is
derived from the ${\it ID}$ learning algorithm for DFA described in [1], and
our correctness proof makes use of the correctness property of ${\it ID}$.
Therefore, we begin by reviewing the ${\it ID}$ algorithm itself, before
turning our attention to DFA family learning.

###  4.1 The ${\it ID}$ Algorithm

The ${\it ID}$ algorithm and its correctness have been discussed at length in
[1]. Therefore our own presentation can be brief. A finite set
$P\subseteq\Sigma^{*}$ of input strings is said to be live complete for a DFA
${\mathcal{A}}$ if for every live state $q\in Q$ there exists a string
$\alpha\in P$ such that $\delta^{*}(q_{0},\hskip 3.0pt\alpha)=q$. Given a live
complete set $P$ for a target automaton ${\mathcal{A}}$, the essential idea of
the ${\it ID}$ algorithm is to first construct the set
$T^{\prime}=P\cup\\{f(\alpha,b)|(\alpha,b)\in P\times\Sigma\\}\cup\\{d_{0}\\}$
of all one element extensions of strings in $P$ as a set of state names for
the hypothesis automaton.

A symbol $d_{0}$ is added as a name for the canonical dead state. Now this
dead state can be used for incremental learning of a DFA, since parts of the
DFA which have not yet been learned can be "hidden" inside the dead state.
This is a key idea in the ${FID}$ incremental learning algorithm described in
Section 4.2

The set of state names is then iteratively partitioned into sets
$E_{i}(\alpha)\subseteq T^{\prime}$ for $i=0,1,\ldots$ such that elements
$\alpha$, $\beta$ of $T^{\prime}$ that denote the same state in
${\mathcal{A}}$ will occur in the same partition set, i.e.
$E_{i}(\alpha)=E_{i}(\beta)$. This partition refinement can be proven to
terminate and the resulting collection of sets forms a congruence on
$T^{\prime}$. Finally the ${\it ID}$ algorithm constructs the hypothesis DFA
as the resulting quotient DFA. The method used to refine the partition set is
to iteratively construct a set $V$ of distinguishing strings, such that no two
distinct states of ${\mathcal{A}}$ have the same behaviour on all of $V$.

Input: A live complete set $P\subseteq\Sigma^{*}$ and a DFA ${{\mathcal{A}}}$
to act as a teacher answering membership queries $\alpha\in
L({{\mathcal{A}}})?$
Output: A $DFA$ $M$ language equivalent to the target DFA ${{\mathcal{A}}}$.

  1. 1.

begin

  2. 2.

//Perform Initialization

  3. 3.

$i=0,$ $v_{i}=\lambda,$ $V=\\{\hskip 5.0ptv_{i}\hskip 5.0pt\\},$

  4. 4.

$T=P\cup\\{f(\alpha,b)|(\alpha,b)\in P\times\Sigma\\},$
$T^{\prime}=T\cup\\{\hskip 5.0ptd_{0}\hskip 5.0pt\\}$

  5. 5.

Construct function $E_{0}$ for $v_{0}=\lambda,$

  6. 6.

$E_{0}(d_{0})=\emptyset$

  7. 7.

$\forall\alpha\in T$

  8. 8.

{ pose the membership query $``\alpha\in L({{\mathcal{A}}})?"$

  9. 9.

if the teacher’s response is $yes$

  10. 10.

then $E_{0}(\alpha)=\\{\lambda\\}$

  11. 11.

else $E_{0}(\alpha)=\emptyset$

  12. 12.

end if

  13. 13.

}

  14. 14.

//Refine the partition of the set $T^{\prime}$

  15. 15.

while $(\exists\alpha,\beta\in P^{\prime}$ and $b\in\Sigma$ such that
$E_{i}(\alpha)=E_{i}(\beta)$ but $E_{i}(f(\alpha,b))\not\neq
E_{i}(f(\beta,b)))$

  16. 16.

do

  17. 17.

Let $\gamma\in E_{i}(f(\alpha,b))\oplus E_{i}(f(\beta,b))$

  18. 18.

$v_{i+1}=b\gamma$

  19. 19.

$V=V\cup\\{v_{i+1}\\}$, $i=i+1$

  20. 20.

$\forall\alpha\in T_{k}$ pose the membership query $"\alpha v_{i}\in
L({{\mathcal{A}}})?"$

  21. 21.

{

  22. 22.

if the teacher’s response is $yes$

  23. 23.

then $E_{i}(\alpha)=E_{i-1}(\alpha)\cup\\{v_{i}\\}$

  24. 24.

else $E_{i}(\alpha)=E_{i-1}(\alpha)$

  25. 25.

end if

  26. 26.

}

  27. 27.

end while

  28. 28.

//Construct the representation $M$ of the target DFA ${{\mathcal{A}}}$.

  29. 29.

The states of $M$ are the sets $E_{i}(\alpha)$, where $\alpha\in T$

  30. 30.

The initial state $q_{0}$ is the set $E_{i}(\lambda)$

  31. 31.

The accepting states are the sets $E_{i}(\alpha)$ where $\alpha\in T$ and
$\lambda\in E_{i}(\alpha)$

  32. 32.

The transitions of $M$ are defined as follows:

  33. 33.

$\quad\forall\alpha\in P^{\prime}$

  34. 34.

if $E_{i}(\alpha)=\emptyset$

  35. 35.

then add self loops on the state $E_{i}(\alpha)$ for all $b\in\Sigma$

  36. 36.

else $\forall b\in\Sigma$ set the transition
$\delta(E_{i}(\alpha),b)=E_{i}(f(\alpha,b))$

  37. 37.

end if

  38. 38.

end.

Algorithm 1 ${\it ID}$ Learning Algorithm

In Section 4.2, we present the DFA family learning algorithm ${FID}$ so that
similar variables in the ${FID}$ and ${\it ID}$ algorithms share similar
names. This pedagogic device emphasises some similarity in the behaviour of
both algorithms. However, there are also important differences of behaviour.
Thus, when analysing the behavioural properties of similar program variables,
we will try to distinguish their context as $v_{n}^{\it ID}$, ${{\it
E}_{n}^{ID}{(\alpha)}},\ldots$ etc, (for the ${\it ID}$ algorithm) and
correspondingly $v_{n}^{c}$, $E_{n}^{c}(\alpha),\ldots$ etc, (for the ${FID}$
algorithm). Our basic argument in the proof of correctness of ${FID}$ is to
show how the learning behaviour of ${FID}$ on a sequence of input strings
$s_{1},\hskip 3.0pt\ldots s_{n}\in\Sigma^{*}$ can be simulated by the
behaviour of ${\it ID}$ on the prefix closure ${\it Pref}(\\{\hskip
5.0pts_{1},\hskip 3.0pt\ldots s_{n}\hskip 5.0pt\\})$ of the corresponding set
of inputs $\\{\hskip 5.0pts_{1},\hskip 3.0pt\ldots s_{n}\hskip 5.0pt\\}$. Once
this is established one can apply the correctness of ${\it ID}$ to establish
the correctness of ${FID}$. The correctness of the ${\it ID}$ algorithm can be
stated as follows.

4.1.1. Theorem.
(i) Let $P\subseteq\Sigma^{*}$ be a live complete set for a DFA
${\mathcal{A}}$ containing $\lambda$. Then given $P$ and ${\mathcal{A}}$ as
input, the ${\it ID}$ algorithm terminates and the automaton $M$ returned is
the canonical minimum state automaton for $L({\mathcal{A}})$.
(ii) Let $l\in{\mathbb{N}}$ be the maximum value of program variable $i^{{\it
ID}}$ given $P$ and ${\mathcal{A}}$. For all $0\leq n\leq l$ and for all
$\alpha\in T$,

${{\it E}_{n}^{ID}{(\alpha)}}=\\{\hskip 5.0ptv_{j}^{{\it ID}}\in V^{{\it
ID}}\hskip 5.0pt|\hskip 5.0pt0\leq j\leq n,\hskip 5.0pt\alpha v_{j}^{{\it
ID}}\in L({\mathcal{A}})\hskip 5.0pt\\}.$

Proof. (i) See [1] Theorem 3.
(ii) By induction on $n$.

Basis. Suppose $n=0$. Then $v_{0}^{{\it ID}}=\lambda$. For any $\alpha\in T$,
if $\alpha v_{0}^{{\it ID}}\in L({\mathcal{A}})$ then $\alpha\in
L({\mathcal{A}})$ so ${{\it E}_{0}^{ID}{(\alpha)}}=\\{\hskip 5.0ptv_{0}^{{\it
ID}}\hskip 5.0pt\\}$. If $\alpha v_{0}^{ID}\not\in L({\mathcal{A}})$ then
$\alpha\not\in L({\mathcal{A}})$ so ${{\it E}_{0}^{ID}{(\alpha)}}=\emptyset$.
Thus ${{\it E}_{0}^{ID}{(\alpha)}}=\\{\hskip 5.0ptv_{j}^{{\it ID}}\hskip
5.0pt|\hskip 5.0pt0\leq j\leq 0,\hskip 5.0pt\alpha v_{j}^{ID}\in
L({\mathcal{A}})\hskip 5.0pt\\}$.

Induction Step. Suppose $l\geq n>0$. Consider any $\alpha,\hskip 3.0pt\beta\in
P^{\prime}$ and $b\in\Sigma$ such that ${{\it E}_{n-1}^{ID}{(\alpha)}}={{\it
E}_{n-1}^{ID}{(\beta)}}$ but ${{\it E}_{n-1}^{ID}{(f(\alpha,b))}}\not={{\it
E}_{n-1}^{ID}{(f(\beta,b))}}$. Since $n-1<l$ then $\alpha$, $\beta$ and $b$
exist. Then

${{\it E}_{n-1}^{ID}{(f(\alpha,b))}}{\oplus}{{\it
E}_{n-1}^{ID}{(f(\beta,b))}}\not=\emptyset.$

Consider any $\gamma\in{{\it E}_{n-1}^{ID}{(f(\alpha,b))}}{\oplus}{{\it
E}_{n-1}^{ID}{(f(\beta,b))}}$ and let $v_{n}^{{\it ID}}=b\gamma$. For any
$\alpha\in T$, if $\alpha v_{n}^{{\it ID}}\in L({\mathcal{A}})$ then ${{\it
E}_{n}^{ID}{(\alpha)}}={{\it E}_{n-1}^{ID}{(\alpha)}}\cup\\{\hskip
5.0ptv_{n}^{{\it ID}}\hskip 5.0pt\\}$ and if $\alpha v_{n}^{{\it ID}}\not\in
L({\mathcal{A}})$ then ${{\it E}_{n}^{ID}{(\alpha)}}={{\it
E}_{n-1}^{ID}{(\alpha)}}$. So by the induction hypothesis ${{\it
E}_{n}^{ID}{(\alpha)}}=\\{\hskip 5.0ptv_{j}^{{\it ID}}\in V^{{\it ID}}\hskip
5.0pt|\hskip 5.0pt0\leq j\leq n,\hskip 5.0pt\alpha v_{j}^{{\it ID}}\in
L({\mathcal{A}})\hskip 5.0pt\\}$.

###  4.2 The ${FID}$ Algorithm

We can now present the ${FID}$ algorithm for incremental lazy learning of a
family of DFA. We give a rigorous proof that ${FID}$ correctly learns in the
limit in the sense of [10] (Correctness Theorem 4.2.6).

Algorithm 2 is the main component of the ${FID}$ algorithm. It learns a
sequence $F_{0},\hskip 3.0pt\ldots,\hskip 3.0ptF_{l}$ of families
$F_{i}=(M_{i}^{1},\hskip 3.0pt\ldots,\hskip 3.0ptM_{i}^{n})$ of $n$ DFA driven
by a sequence of input strings (queries) $s_{1},\hskip 3.0pt\ldots,\hskip
3.0pts_{l}$. The teacher is a single $n$-bit Kripke structure
${{\mathcal{A}}}$. Then $F_{0}$ is a null hypothesis about the projections
${{\mathcal{A}}}_{1},\hskip 3.0pt\ldots,\hskip 3.0pt{{\mathcal{A}}}_{n}$ of
${{\mathcal{A}}}$. We claim that the sequence $F_{0},\hskip 3.0ptF_{1},\hskip
3.0pt\ldots$ finitely converges to the projections
$({{\mathcal{A}}}_{1},\hskip 3.0pt\ldots,\hskip 3.0pt{{\mathcal{A}}}_{n})$
given enough information about ${{\mathcal{A}}}$, i.e when $s_{1},\hskip
3.0pt\ldots,\hskip 3.0pts_{l}$ contains a live complete set of queries for
each projection ${{\mathcal{A}}}_{i}$.

Input: A file $S=s_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}$ of input strings
$s_{i}\in\Sigma^{*}$ and an $n$-bit Kripke structure ${{\mathcal{A}}}$ as
teacher to answer queries $\lambda_{{\mathcal{A}}}^{*}(s_{i})=\hskip 3.0pt?$
Output: A sequence of families $F_{t}=(M_{t}^{1},\hskip 3.0pt\ldots,\hskip
3.0ptM_{t}^{n})$ of DFA for $t=0,\hskip 3.0pt\ldots,\hskip 3.0ptl$.

  1. 1.

begin

  2. 2.

//Perform Initialization

  3. 3.

for c = 1 to n do $\\{\hskip 5.0pt$ $i_{c}=0,$ $v_{i_{c}}^{c}=\varepsilon$,
$V_{c}=\\{v_{i_{c}}^{c}\\}\hskip 5.0pt\\}$

  4. 4.

$k=0,$ $t=0,$

  5. 5.

$P_{0}=\\{\varepsilon\\}$, $P^{\prime}_{0}=P_{0}\cup\\{d_{0}\\}$,
$T_{0}=P_{0}\cup\Sigma$

  6. 6.

//Build equivalence classes for the dead state $d_{0}$

  7. 7.

for c = 1 to n do $\\{\hskip 5.0ptE_{0}^{c}(d_{0})=\emptyset\hskip 5.0pt\\}$

  8. 8.

//Build equivalence classes for input strings of length zero and one

  9. 9.

$\forall\alpha\in T_{0}$ $\\{$

  10. 10.

$(b_{1},\hskip 3.0pt\ldots,\hskip
3.0ptb_{n})=\lambda_{{\mathcal{A}}}^{*}(\alpha)$

  11. 11.

for c = 1 to n do

  12. 12.

if $b_{c}$ then $E_{i_{c}}^{c}(\alpha)=\\{v_{i_{c}}^{c}\\}$ else
$E_{i_{c}}^{c}(\alpha)=\emptyset$

  13. 13.

}

  14. 14.

//Refine the initial equivalence relations $E_{0}^{1},\hskip
3.0pt\ldots,\hskip 3.0ptE_{0}^{n}$

  15. 15.

//into congruences using Algorithm 3

  16. 16.

  17. 17.

//Synthesize an initial family $F_{0}$ approximating ${{\mathcal{A}}}$

  18. 18.

//using Algorithm 4.

  19. 19.

  20. 20.

//Process the file of examples.

  21. 21.

while  $S\not=empty$ do $\\{$

  22. 22.

read( S, $\alpha$ )

  23. 23.

k = k+1, t = t+1

  24. 24.

$P_{k}=P_{k-1}\cup Pref(\alpha)$ //prefix closure

  25. 25.

$P_{k}^{\prime}=P_{k}\cup\\{d_{0}\\}$

  26. 26.

$T_{k}=P_{k}\cup\\{f(\alpha,\hskip 3.0ptb)\hskip 5.0pt|\hskip 5.0pt\alpha\in
P_{k}-P_{k-1},b\in\Sigma\\}$ //for prefix closure

  27. 27.

$T^{\prime}_{k}=T_{k}\cup\\{d_{0}\\}$

  28. 28.

$\forall\alpha\in T_{k}-T_{k-1}\hskip 5.0pt\\{$

  29. 29.

for c = 1 to n do $E_{0}^{c}(\alpha)=\emptyset$ //initialise the new
equivalence class $E_{0}^{c}(\alpha)$

  30. 30.

for j = 0 to $i_{c}$ do $\\{$

  31. 31.

// Consider adding previous distinguishing string $v_{j}^{c}\in V_{c}$

  32. 32.

// to the new equivalence class $E_{j}^{c}(\alpha)$

  33. 33.

$(b_{1},\hskip 3.0pt\ldots,\hskip
3.0ptb_{n})=\lambda_{{\mathcal{A}}}^{*}(\alpha{\hskip 3.0pt.\hskip
3.0pt}v_{j}^{c})$

  34. 34.

if $b_{c}$ then $E_{j}^{c}(\alpha)=E_{j}^{c}(\alpha)\cup\\{\hskip
5.0ptv_{j}^{c}\hskip 5.0pt\\}$

  35. 35.

}

  36. 36.

}

  37. 37.

//Refine the current equivalence relations $E_{i_{1}}^{1},\hskip
3.0pt\ldots,\hskip 3.0ptE_{i_{n}}^{n}$

  38. 38.

// into congruences using Algorithm 3

  39. 39.

  40. 40.

if $\alpha$ is consistent with $F_{t-1}$

  41. 41.

then $F_{t}=F_{t-1}$

  42. 42.

else synthesize the family $F_{t}$ using Algorithm 4.

  43. 43.

$\\}$

  44. 44.

end.

Algorithm 2 FID: a DFA Family Learning Algorithm

The basic idea of Algorithm 2 is to construct in parallel a family

$(E_{i_{1}}^{1},\hskip 3.0pt\ldots,\hskip 3.0ptE_{i_{n}}^{n})$

of $n$ individual equivalence relations on the same set $T_{k}$ of state
names. For each equivalence relation $E_{i_{j}}^{j}$, a set $V_{j}$ of
distinguishing strings is incrementally generated to split pairs of
equivalence classes in $E_{i_{j}}^{j}$ until a congruence is achieved. Then a
quotient DFA $M^{j}$ can be constructed from the partition of $T_{k}$ by the
congruence $E_{i_{j}}^{j}$. The congruences are constructed so that
$E_{i}^{j}\subseteq E_{i+1}^{j}$ and thus the ${FID}$ algorithm is
incremental, and fully reuses information about previous approximations, which
is efficient.

Each DFA family $F_{i}=(M_{i}^{1},\hskip 3.0pt\ldots,\hskip 3.0ptM_{i}^{n})$
is constructed from the partition family $(E_{i_{1}}^{1},\hskip
3.0pt\ldots,\hskip 3.0ptE_{i_{n}}^{n})$ using Synthesis Algorithm 4. When the
${FID}$ algorithm is applied to the problem of LBT, the input strings
$s_{i}\in\Sigma^{*}$ to ${FID}$ are generated as counterexamples to
correctness (i.e. test cases). For this we execute a model checker on a Kripke
structure ${{\mathcal{A}}}_{i-1}$ which is a minimised subdirect product of
$(M_{i-1}^{1},\hskip 3.0pt\ldots,\hskip 3.0ptM_{i-1}^{n})$ using a
requirements specification $\phi$ expressed in temporal logic. (The
construction of ${{\mathcal{A}}}_{i-1}$ will be detailed in Sections 5 and 6.)
In the case that no counterexamples to $\phi$ can be found in
${{\mathcal{A}}}_{i-1}$ then $s_{i}$ is randomly chosen, taking care to avoid
all previously used input strings.

Algorithm 3 implements lazy partition refinement, to extend
$E_{i_{1}}^{1},\hskip 3.0pt\ldots,\hskip 3.0ptE_{i_{n}}^{n}$ from being
equivalence relations on states to being a family of congruences with respect
to the state transition functions $\delta_{1},\hskip 3.0pt\ldots,\hskip
3.0pt\delta_{n}$ for the synthesized DFA $M^{1},\hskip 3.0pt\ldots,\hskip
3.0ptM^{n}$.

Thus line 1 in Algorithm 3 searches for congruence failure in any one of the
equivalence relations $E_{i_{1}}^{1},\hskip 3.0pt\ldots,\hskip
3.0ptE_{i_{n}}^{n}$. In lines 6-14 of Algorithm 3 we apply lazy partition
refinement. This technique implies reusing the new distinguishing string $v$
wherever possible to refine each equivalence relation $E_{i_{j}}^{j}$ that is
not yet a congruence. On the other hand, any equivalence relation
$E_{i_{j}}^{j}$ that is already a congruence is not refined, even though the
result $b_{j}$ of the new query $\alpha{\hskip 3.0pt.\hskip 3.0pt}v$ might add
some new information to $M^{j}$. This brings the set of relations
$E_{i_{1}}^{1},\hskip 3.0pt\ldots,\hskip 3.0ptE_{i_{n}}^{n}$ to a simultaneous
fixed point of $n$ congruence constructions as soon as possible. It therefore
helps to reduce the number of active learner queries and raise the number of
model checker queries used during learning based testing (cf. Section 1.2).

  1. 1.

while $(\exists\hskip 3.0pt1\leq c\leq n,\exists\alpha,\beta\in
P_{k}^{\prime}$ and $\exists\sigma\in\Sigma$ such that
$E_{i_{c}}^{c}(\alpha)=E_{i_{c}}^{c}(\beta)$ but
$E_{i_{c}}^{c}(f(\alpha,\hskip 3.0pt\sigma))\not\neq
E_{i_{c}}^{c}(f(\beta,\hskip 3.0pt\sigma))$ do $\\{$

  2. 2.

//Equivalence relation $E_{i_{c}}^{c}$ is not a congruence w.r.t. $\delta_{c}$

  3. 3.

//so add a new distinguishing sequence.

  4. 4.

Choose $\gamma\in E_{i_{c}}^{c}(f(\alpha,\hskip 3.0pt\sigma))\oplus
E_{i_{c}}^{c}(f(\beta,\hskip 3.0pt\sigma))$

  5. 5.

$v=\sigma{\hskip 3.0pt.\hskip 3.0pt}\gamma$

  6. 6.

$\forall\alpha\in T_{k}$ $\\{$

  7. 7.

$(b_{1},\hskip 3.0pt\ldots,\hskip 3.0ptb_{n})=\lambda_{A}^{*}(\alpha{\hskip
3.0pt.\hskip 3.0pt}v)$

  8. 8.

for c = 1 to n do $\\{$

  9. 9.

if $E_{i_{c}}^{c}(\alpha)=E_{i_{c}}^{c}(\beta)$ and
$E_{i_{c}}^{c}(f(\alpha,\hskip 3.0pt\sigma))\not\neq
E_{i_{c}}^{c}(f(\beta,\hskip 3.0pt\sigma))$ then $\\{$

  10. 10.

// Lazy refinement of equivalence relation $E_{i_{c}}^{c}$

  11. 11.

$i_{c}=i_{c}+1$, $v_{i_{c}}=v$, $V_{c}=V_{c}\cup\\{v_{i_{c}}\\}$

  12. 12.

if $b_{c}$ then
$E_{i_{c}}^{c}(\alpha)=E_{i_{c}-1}^{c}(\alpha)\cup\\{v_{i_{c}}\\}$ else
$E_{i_{c}}^{c}(\alpha)=E_{i_{c}-1}^{c}(\alpha)$

  13. 13.

$\\}$

  14. 14.

}

  15. 15.

$\\}$

Algorithm 3 Lazy Partition Refinement

  1. 1.

for c = 1 to n do $\\{\hskip 5.0pt$

  2. 2.

// Synthesize the quotient DFA $M^{c}$

  3. 3.

The states of $M^{c}$ are the sets $E_{i_{c}}^{c}(\alpha)$, where $\alpha\in
T_{k}$

  4. 4.

Let $q_{0}^{c}=E_{i_{c}}^{c}(\varepsilon)$

  5. 5.

The accepting states are the sets $E_{i_{c}}^{c}(\alpha)$ where $\alpha\in
T_{k}$ and $\varepsilon\in E_{i_{c}}^{c}(\alpha)$

  6. 6.

The transition function $\delta_{c}$ of $M^{c}$ is defined as follows:

  7. 7.

$\forall\alpha\in P_{k}^{\prime}$ $\\{$

  8. 8.

if $E_{i_{c}}^{c}(\alpha)=\emptyset$ then $\forall b\in\Sigma$ $\\{$ let
$\delta_{c}(E_{i_{c}}^{c}(\alpha),b)=E_{i_{c}}^{c}(\alpha)$ $\\}$

  9. 9.

else $\forall b\in\Sigma$ $\\{$
$\delta_{c}(E_{i_{c}}^{c}(\alpha),b)=E_{i_{c}}^{c}(\alpha{\hskip 3.0pt.\hskip
3.0pt}b)$ $\\}$

  10. 10.

$\\}$

  11. 11.

$\forall\beta\in T_{k}-P_{k}^{\prime}$ $\\{$

  12. 12.

if $\forall\alpha\in P_{k}^{\prime}$ $\\{$ $E_{i_{c}}^{c}(\beta)\neq
E_{i_{c}}^{c}(\alpha)$ $\\}$ and $E_{i_{c}}^{c}(\beta)\neq\emptyset$ then

  13. 13.

$\forall b\in\Sigma$ $\\{$ $\delta_{c}(E_{i_{c}}^{c}(\beta),b)=\emptyset$
$\\}$

  14. 14.

$\\}$

  15. 15.

$\\}$

  16. 16.

return $F=(M^{1},\hskip 3.0pt\ldots,\hskip 3.0ptM^{n})$

Algorithm 4 DFA Family Synthesis

We begin an analysis of the correctness of the ${FID}$ algorithm by confirming
that the construction of hypothesis DFA carried out by Algorithm 4 is well
defined.

4.2.1. Proposition. For each $t\geq 0$ the hypothesis DFA $M^{1},\hskip
3.0pt\ldots,\hskip 3.0ptM^{n}$ constructed by the DFA Family Synthesis
Algorithm 4 after $t$ input strings have been applied to ${{\mathcal{A}}}$ are
all well defined DFA.  Proof. The main task is to show $\delta$ to be well
defined function and uniquely defined for every state $E_{i}(\alpha)$, where
$\alpha\in T_{k}$.

Proposition 4.2.1 establishes that Algorithm 4 will generate families of well
defined DFA. However, to show that the ${FID}$ algorithm learns correctly in
the limit, we must prove that this sequence of DFA families finitely converges
to the $n$ individual projections ${\mathcal{A}}_{i}$ of the target Kripke
structure ${\mathcal{A}}$. It will suffice to show that the behaviour of
${FID}$ can be simulated by the behaviour of ${\it ID}$, since ${\it ID}$ is
known to learn correctly given a live complete set of input strings (c.f.
Theorem 4.4.1.(i)). The first step in this proof is to show that the sequences
of sets of state names ${\it P}_{k}$ and ${\it T}_{k}$ generated by ${FID}$
converge to the sets ${\it P}^{ID}$ and ${\it T}^{{\it ID}}$ of ${\it ID}$.

4.2.2. Proposition. Let $S=s_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}$ be any
non-empty sequence of input strings $s_{i}\in\Sigma^{*}$ for ${FID}$ and let
${\it P}^{ID}={\it Pref}(\\{\hskip 5.0pt\lambda,\hskip 3.0pts_{1},\hskip
3.0pt\ldots,\hskip 3.0pts_{l}\hskip 5.0pt\\})$ be the prefix closure of the
corresponding input set for ${\it ID}$.

(i) For all $0\leq k\leq l$, ${\it P}_{k}={\it Pref}(\\{\hskip
5.0pt\lambda,\hskip 3.0pts_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{k}\hskip
5.0pt\\})\subseteq{\it P}^{ID}$.

(ii) For all $0\leq k\leq l$, ${\it T}_{k}={\it P}_{k}\cup\\{\hskip
5.0ptf(\alpha,\hskip 3.0ptb)\hskip 5.0pt|\hskip 5.0pt\alpha\in{\it
P}_{k},\hskip 3.0ptb\in\Sigma\hskip 5.0pt\\}\subseteq{\it T}^{{\it ID}}$.

(iii) ${\it P}_{l}={\it P}^{ID}$ and ${\it T}_{l}={\it T}^{{\it ID}}$.

Proof. Clearly (iii) follows from (i) and (ii). Then (i) and (ii) are easily
proved by induction on $k$. Observe that unlike ${FID}$, the ${\it ID}$
algorithm does not compute any prefix closure of input strings. Therefore,
prefix closure must be added explicitly in Proposition 4.2.2, to make a
correspondence between the behaviour of ${FID}$ and ${\it ID}$.

Next we turn our attention to proving some fundamental loop invariants for
Algorithm 2. Since this algorithm in turn calls the Lazy Partition Refinement
Algorithm 3 then we have in effect a doubly nested loop structure to analyse.
Clearly the outer loop counter $k$ in Algorithm 2 and the family of inner loop
counters $i_{c}$ (for $1\leq c\leq n$) in Algorithm 3 both increase on each
iteration. However, the relationships between these counter variables are not
easily defined. Nevertheless, since all variables increase from an initial
value of zero, we can assume the existence of some family of $n$ monotone re-
indexing functions that capture their relationships.

4.2.3. Definition. Let $S=s_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}$ be any
non-empty sequence of strings $s_{i}\in\Sigma^{*}$. The re-indexing function
${\it K}_{c}^{S}:{\mathbb{N}}\to{\mathbb{N}}$ for ${FID}$ on input $S$ (for
each $1\leq c\leq n$) is the unique monotonically increasing function such
that for each $n\in{\mathbb{N}}$, ${\it K}_{c}^{S}(n)$ is the least integer
$m$ such that program variable $k$ has value $m$ while the program variable
$i_{c}$ has value $n$. Thus, for example, ${\it K}_{c}^{S}(0)=0$ for all
$1\leq c\leq n$. When $S$ is clear from the context, we may simply write ${\it
K}_{c}$ for ${\it K}_{c}^{S}$.

With the help of these re-indexing functions we can express important
invariant properties of the distinguishing sequence variables $v_{j}^{c}$ and
partition set variables $E_{n}^{c}(\alpha)$. Using Proposition 4.2.2 their
relationship to the corresponding variables $v_{j}^{\it ID}$ and ${{\it
E}_{n}^{ID}{(\alpha)}}$ of ${\it ID}$ can be established. Since Algorithm 2
has a doubly nested loop structure, the proof of Simulation Theorem 4.2.4
below makes use of a doubly nested induction argument.

4.2.4. Simulation Theorem. Let $S=s_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}$
be any non-empty sequence of strings $s_{i}\in\Sigma^{*}$. For any execution
of ${FID}$ on $S$ and the $n$-bit Kripke structure ${{\mathcal{A}}}$ there
exists an execution of ${\it ID}$ on ${\it Pref}(\\{\hskip 5.0pt\lambda,\hskip
3.0pts_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}\hskip 5.0pt\\})$ and the
$c$-th projection ${{\mathcal{A}}}_{c}$ (for each $1\leq c\leq n$) such that
for all $m\geq 0$:

(i) For all $n\geq 0$, if ${\it K}_{c}(n)=m$ then:

(a) for all $0\leq j\leq n$, $v_{j}^{c}=v_{j}^{\it ID}$,

(b) for all $0\leq j<n$, $v_{n}^{c}\not=v_{j}^{c}$,

(c) for all $\alpha\in{\it T}_{m}$, $E_{n}^{c}(\alpha)=\\{\hskip
5.0ptv_{j}^{c}\in V_{c}\hskip 5.0pt|\hskip 5.0pt0\leq j\leq n,\hskip
5.0pt\alpha v_{j}^{c}\in L({{\mathcal{A}}}_{c})\hskip 5.0pt\\}$.

(ii) If $m>0$ then let $p\in{\mathbb{N}}$ be the greatest integer such that
${\it K}_{c}(p)=m-1$. Then for all $\alpha\in{\it T}_{m}$,
$E_{p}^{c}(\alpha)=\\{\hskip 5.0ptv_{j}^{c}\in V_{c}\hskip 5.0pt|\hskip
5.0pt0\leq j\leq p,\hskip 5.0pt\alpha v_{j}^{c}\in
L({{\mathcal{A}}}_{c})\hskip 5.0pt\\}$.

(iii) The $m$th partition refinement of ${FID}$ terminates.  Proof. By
induction on $m$ using Proposition 4.2.2.(i).

Part (i.a) above asserts that the same distinguishing sequences are produced
in the same order by ${FID}$ and ${\it ID}$. Part (i.b) asserts that a
distinguishing sequence is never produced twice by ${FID}$. Part (i.c) and
(ii) characterise the partition sets $E_{n}^{c}(\alpha)$ as sets of all
distinguishing sequences $v_{j}^{c}$ that lead to an accepting state of
${{\mathcal{A}}}_{c}$ from $\alpha$.

Note that both ${\it ID}$ and ${FID}$ are non-deterministic algorithms (due to
the non-deterministic choice on line 17 of Algorithm 1 and line 4 of Algorithm
3). Therefore in the statement of Theorem 4.2.4 above, we can only talk about
the existence of some correct simulation. Clearly there are also simulations
of ${FID}$ by ${\it ID}$ which are not correct, but this does not affect the
basic correctness argument.

4.2.5. Corollary. Let $S=s_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}$ be any
non-empty sequence of strings $s_{i}\in\Sigma^{*}$. Any execution of ${FID}$
on $S$ and an $n$-bit Kripke structure ${{\mathcal{A}}}$ terminates with the
program variable $k$ having value $l$.  Proof. Follows from Simulation Theorem
4.2.4.(iii) since clearly the while loop of Algorithm 2 terminates when the
input sequence $S$ is empty.

Using the detailed analysis of the invariant properties of the program
variables ${\it P}_{k}$ and ${\it T}_{k}$ in Proposition 4.2.2 and $v_{j}^{c}$
and $E_{n}^{c}(\alpha)$ in Simulation Theorem 4.2.4 it is now a simple matter
to establish correctness of learning for the ${FID}$ Algorithm.

4.2.6. Correctness Theorem. Let $S=s_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}$
be any non-empty sequence of strings $s_{i}\in\Sigma^{*}$ such that $\\{\hskip
5.0pt\lambda,\hskip 3.0pts_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{l}\hskip
5.0pt\\}$ contains a live complete set for each projection ${\mathcal{A}}_{i}$
of ${\mathcal{A}}$. Then ${FID}$ terminates on $S$. Also for each $1\leq i\leq
n$ the hypothesis DFA $M_{l}^{i}$ is a canonical representation of
${\mathcal{A}}_{i}$ .  Proof. By Corollary 4.2.5, ${FID}$ terminates on $S$
with the variable $k$ having value $l$. By Simulation Theorem 4.2.4.(i) and
Theorem 4.1.1.(ii), there exists an execution of ${\it ID}$ on ${\it
Pref}(\\{\hskip 5.0pt\lambda,\hskip 3.0pts_{1},\hskip 3.0pt\ldots,\hskip
3.0pts_{l}\hskip 5.0pt\\})$ such that $E_{n}^{i}(\alpha)={{\it
E}_{n}^{ID}{(\alpha)}}$ for all $\alpha\in{\it T}_{l}$ and any $n$ such that
${\it K}(n)=l$. By Proposition 4.2.2.(iii), ${\it T}_{l}={\it T}^{{\it ID}}$
and ${\it P^{\prime}}_{l}={\it P^{\prime}}$. So letting $M_{i}^{\it ID}$ be
the canonical representation of ${\mathcal{A}}_{i}$ constructed by ${\it ID}$
using ${\it Pref}(\\{\hskip 5.0pt\lambda,\hskip 3.0pts_{1},\hskip
3.0pt\ldots,\hskip 3.0pts_{l}\hskip 5.0pt\\})$ then $M_{i}^{\it ID}$ and
$M_{l}^{i}$ have the same state sets, initial states, accepting states and
transitions.

Our next result confirms that each hypothesis DFA $M_{t}^{i}$ generated after
$t$ input strings have been applied to ${{\mathcal{A}}}$ is consistent with
all currently known observations about the $i$th projection
${\mathcal{A}}_{i}$. This is quite straightforward in the light of Simulation
Theorem 4.2.4.

4.2.7. Compatibility Theorem. Let $S=s_{1},\hskip 3.0pt\ldots,\hskip
3.0pts_{l}$ be any non-empty sequence of strings $s_{i}\in\Sigma^{*}$. For
each $0\leq t\leq l$ and each string $s\in\\{\hskip 5.0pt\lambda,\hskip
3.0pts_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{t}\hskip 5.0pt\\}$, the
hypothesis automaton $M_{t}^{i}$ accepts $s$ if, and only if the $i$th
projection ${\mathcal{A}}_{i}$ of ${\mathcal{A}}$ does.  Proof. By definition,
$M_{t}^{i}$ is compatible with ${\mathcal{A}}_{i}$ on $\\{\hskip
5.0pt\lambda,\hskip 3.0pts_{1},\hskip 3.0pt\ldots,\hskip 3.0pts_{t}\hskip
5.0pt\\}$ if, and only if, for each $0\leq j\leq t$, $s_{j}\in
L({\mathcal{A}}_{i})\hskip 5.0pt\Leftrightarrow\hskip 5.0pt\lambda\in
E_{i_{t}}^{i}({s_{j}})$, where ${i_{t}}$ is the greatest integer such that
${\it K}({i_{t}})=t$ and the sets $E_{i_{t}}^{i}({\alpha})$ for $\alpha\in{\it
T}_{t}$ are the states of $M_{t}^{i}$. Now $v_{0}=\lambda$. So by Simulation
Theorem 4.2.4.(i).(c), if $s_{j}\in L({\mathcal{A}}_{i})$ then $s_{j}v_{0}\in
L({\mathcal{A}}_{i})$ so $v_{0}\in{{\it E}_{i_{t}}{(s_{j})}}$, i.e.
$\lambda\in E_{i_{t}}^{i}({s_{j}})$, and if $s_{j}\not\in
L({\mathcal{A}}_{i})$ then $s_{j}v_{0}\not\in L({\mathcal{A}}_{i})$ so
$v_{0}\not\in E_{i_{t}}^{i}({s_{j}})$, i.e. $\lambda\not\in
E_{i_{t}}^{i}({s_{j}})$.

We have now established a reliable method for decomposing the problem of
learning a $k$-bit Kripke structure ${\mathcal{A}}$ into the problem of
learning a family of $k$ individual DFA. This approach supports projection, as
defined in Section 1.2 and Definition 2.2.

##  5 Subdirect Product Construction

We next turn our attention to problem of efficiently recombining a family of
$k$ individual DFA (the projections) into a single $k$-bit deterministic
Kripke structure. For this we use a well known algebraic construction known as
a subdirect product. Informally, a subdirect product of a family
$F={\langle\hskip 3.0pt}A_{i}\hskip 5.0pt|\hskip 5.0pti\in I{\hskip
3.0pt\rangle}$ of algebraic structures, is any subalgebra of the direct
product $\Pi F=\Pi_{i\in I}A_{i}$ which projects onto (surjectively) each of
its co-ordinate algebras $A_{i}$. The subdirect product construction was
introduced in [4] as a universal decomposition method applicable to any
algebraic structures. The reader may consult [19] for basic facts about
subdirect products and their universal properties. A specific definition for
deterministic Kripke structures is given below.

To begin with, we observe that for black-box testing it suffices to learn a
Kripke structure up to behavioural equivalence.

5.1. Definition. Let ${{\mathcal{A}}}$ and ${{\mathcal{B}}}$ be $k$-bit Kripke
structures over a finite input alphabet $\Sigma$. We say that
${{\mathcal{A}}}$ and ${{\mathcal{B}}}$ are behaviourally equivalent, and
write ${{\mathcal{A}}}\equiv{{\mathcal{B}}}$ if, and only if, for every finite
input sequence $\sigma_{1},\hskip 3.0pt\ldots,\hskip
3.0pt\sigma_{i}\in\Sigma^{*}$ we have

$\lambda_{{\mathcal{A}}}^{*}(\hskip 3.0pt\sigma_{1},\hskip 3.0pt\ldots,\hskip
3.0pt\sigma_{i}\hskip 3.0pt)=\lambda_{{\mathcal{B}}}^{*}(\hskip
3.0pt\sigma_{1},\hskip 3.0pt\ldots,\hskip 3.0pt\sigma_{i}\hskip 3.0pt).$

Clearly, by the isomorphism identified in Section 2 between $1$-bit Kripke
structures and DFA, for such structures we have
${{\mathcal{A}}}\equiv{{\mathcal{B}}}$ if, and only if,
$L({{\mathcal{A}}}^{\prime})=L({{\mathcal{B}}}^{\prime})$. Furthermore, if
$Min({{\mathcal{A}}})$ is the minimal subalgebra of ${{\mathcal{A}}}$ then
$Min({{\mathcal{A}}})\equiv{{\mathcal{A}}}$.

A family of $k$ individual $1$-bit Kripke structures (DFA) can be combined
into a single $k$-bit Kripke structure using the following instance of the
subdirect product construction.

5.2. Definition. Let ${{\mathcal{A}}}_{1},\hskip 3.0pt\ldots,\hskip
3.0pt{{\mathcal{A}}}_{k}$ be a family of 1-bit Kripke structures,

${{\mathcal{A}}}_{i}=(\hskip 3.0ptQ_{i},\hskip 3.0pt\Sigma,\hskip
3.0pt\delta_{i}:Q_{i}\times\Sigma\to Q_{i},\hskip 3.0ptq_{i}^{0},\hskip
3.0pt\lambda_{i}:Q\to{\mathbb{B}}\hskip 3.0pt)$

for $i=1,\hskip 3.0pt\ldots,\hskip 3.0ptk$. Define the direct product Kripke
structure

$\prod_{i=1}^{k}{{\mathcal{A}}}_{i}=(\hskip 3.0ptQ,\hskip 3.0pt\Sigma,\hskip
3.0pt\delta:Q\times\Sigma\to Q,\hskip 3.0ptq^{0},\hskip
3.0pt\lambda:Q\to{\mathbb{B}}^{k}\hskip 3.0pt),$

where $Q=\prod_{i=1}^{k}Q_{i}=Q_{1}\times\ldots\times Q_{k}$ and
$q^{0}=(\hskip 3.0ptq_{1}^{0},\hskip 3.0pt\ldots,\hskip 3.0ptq_{k}^{0}\hskip
3.0pt)$. Also

$\delta(q_{1},\hskip 3.0pt\ldots,\hskip 3.0ptq_{k},\hskip 3.0pt\sigma)=(\hskip
3.0pt\delta_{1}(q_{1},\hskip 3.0pt\sigma),\hskip 3.0pt\ldots,\hskip
3.0pt\delta_{k}(q_{k},\hskip 3.0pt\sigma)\hskip 3.0pt),$ $\lambda(q_{1},\hskip
3.0pt\ldots,\hskip 3.0ptq_{k})=(\hskip 3.0pt\lambda_{1}(q_{1}),\hskip
3.0pt\ldots,\hskip 3.0pt\lambda_{k}(q_{k})\hskip 3.0pt).$

Associated with the direct product $\prod_{i=1}^{k}{{\mathcal{A}}}_{i}$ we
have $i$-th projection mapping

${\it proj}_{i}:Q_{1}\times\ldots\times Q_{k}\to Q_{i},\hskip 3.0pt\quad{\it
proj}_{i}(q_{1},\hskip 3.0pt\ldots,\hskip 3.0ptq_{k})=q_{i},\hskip 3.0pt1\leq
i\leq k$

Define the subdirect product ${\it Min}(\hskip
3.0pt\prod_{i=1}^{k}{{\mathcal{A}}}_{i}\hskip 3.0pt)$ be the minimal
subalgebra of $\prod_{i=1}^{k}{{\mathcal{A}}}_{i}$. The reason for taking the
subdirect product of the ${{\mathcal{A}}}_{i}$ as the minimal subalgebra of
the direct product $\prod_{i=1}^{k}{{\mathcal{A}}}_{i}$ is to avoid the state
space explosion due to a large number of unreachable states in the direct
product itself. The state space size of $\prod_{i=1}^{k}{{\mathcal{A}}}_{i}$
grows exponentially with $k$. On the other hand, since most of these states
are unreachable from the initial state, then from the point of view of
requirements testing they are irrelevant. This subdirect product can be
computed from its components ${{\mathcal{A}}}_{i}$ in time $O(k.m.|\Sigma|)$
where $m$ is the number of states in the resulting subdirect product and
$|\Sigma|$ is the size of the input alphabet. A naive algorithm based on
systematic path exploration starting from the initial state can be used. We
leave the definition of this algorithm as an exercise for the reader.

As is well known from universal algebra, the $i$-th projection mapping ${\it
proj}_{i}$ is a homomorphism. 5.3. Proposition. Let
${{\mathcal{A}}}_{1},\hskip 3.0pt\ldots,\hskip 3.0pt{{\mathcal{A}}}_{k}$ be
any minimal 1-bit Kripke structures.
(i) For each $1\leq i\leq k$, the projection mapping ${\it proj}_{i}:{\it
Min}(\hskip 3.0pt\prod_{i=1}^{k}{{\mathcal{A}}}_{i}\hskip
3.0pt)\to{{\mathcal{A}}}_{i}$ is an epimorphism. Hence ${\it Min}(\hskip
3.0pt\prod_{i=1}^{k}{{\mathcal{A}}}_{i}\hskip 3.0pt)$ is a subdirect product
of the ${{\mathcal{A}}}_{i}$. (ii) ${\it Min}(\hskip
3.0pt\prod_{i=1}^{k}{{\mathcal{A}}}_{i}\hskip
3.0pt)\equiv\prod_{i=1}^{k}{{\mathcal{A}}}_{i}.$ Proof. (i) Immediate since
the ${{\mathcal{A}}}_{i}$ are minimal. (ii) Follows from the fact that
$Min({{\mathcal{A}}})\equiv{{\mathcal{A}}}$. The following theorem justifies
bit-sliced learning of $k$-bit Kripke structures using conventional regular
inference methods for a family of DFA. It constitutes the correctness argument
for the subdirect product component of the IKL architecture, as presented in
Section 3. 5.4. Theorem. Let ${{\mathcal{A}}}$ be a $k$-bit Kripke structure
over a finite input alphabet $\Sigma$. Let ${{\mathcal{A}}}_{1},\hskip
3.0pt\ldots,\hskip 3.0pt{{\mathcal{A}}}_{k}$ be the $k$ individual 1-bit
projections of ${{\mathcal{A}}}$. For any 1-bit Kripke structures
${{\mathcal{B}}}_{1},\hskip 3.0pt\ldots,\hskip 3.0pt{{\mathcal{B}}}_{k}$, if,
${{\mathcal{A}}}_{1}\equiv{{\mathcal{B}}}_{1}\hskip 3.0pt\&\ldots\&\hskip
3.0pt{{\mathcal{A}}}_{k}\equiv{{\mathcal{B}}}_{k}$ then

${{\mathcal{A}}}\equiv{\it Min}(\hskip
3.0pt\prod_{i=1}^{k}{{\mathcal{B}}}_{i}\hskip 3.0pt).$

Proof. Use Proposition 5.3. By Correctness Theorem 4.2.6, the assumptions of
Theorem 5.4 on the 1-bit Kripke structures ${{\mathcal{B}}}_{1},\hskip
3.0pt\ldots,\hskip 3.0pt{{\mathcal{B}}}_{k}$ are fulfilled by the IKL
architecture, since these are the canonical representations of
${{\mathcal{A}}}_{1},\hskip 3.0pt\ldots,\hskip 3.0pt{{\mathcal{A}}}_{k}$. So
by Theorem 5.4, the output of the IKL algorithm, after DFA family learning has
converged and the subdirect product construction has been applied is a $k$-bit
Kripke structure ${{\mathcal{B}}}$ that is behaviourally equivalent with the
input Kripke structure ${{\mathcal{A}}}$.

Despite the canonical DFA ${{\mathcal{B}}}_{1},\hskip 3.0pt\ldots,\hskip
3.0pt{{\mathcal{B}}}_{k}$ being minimal, the reduced product ${{\mathcal{B}}}$
may still be much larger in state space size than ${{\mathcal{A}}}$. This can
slow down the process of model checking the output of IKL considerably. So it
is important to reduce the state space size of ${{\mathcal{B}}}$ even further.
This last step of the IKL algorithm will be discussed in the next section.

##  6 Kripke Structure Minimisation.

In this section we introduce an efficient algorithm for the minimisation of
deterministic Kripke structures with $\mathcal{O}(|\Sigma|.n\log_{2}n)$ time
complexity. Here $n$ is the state space size of the Kripke structure
${{\mathcal{A}}}$ and $|\Sigma|$ is the size of its input alphabet. This
algorithm is applied on the back end of the IKL learning algorithm in order to
speed up model checking of the learned hypothesis automata during testing.

To define a minimisation algorithm, we need to generalise the concepts of
right language and Nerode congruence from DFA to deterministic Kripke
structures. We then show how Hopcroft’s DFA minimisation algorithm of [12] can
be generalised to compute the Nerode congruence $\equiv$ of a deterministic
Kripke structure ${{\mathcal{A}}}$. The quotient Kripke structure
${{\mathcal{A}}}/\equiv$ is minimal and language equivalent to
${{\mathcal{A}}}$. This fact is the final result needed to prove the
correctness of the IKL architecture. We will prove the correctness and
complexity properties of our minimisation algorithm from first principles.

###  6.1 Minimal Deterministic Kripke Structures

Let us consider a DFA ${{\mathcal{A}}}=(Q,\Sigma,\delta,q_{0},F)$ . For each
state $q\in Q$ of ${{\mathcal{A}}}$ there corresponds a subautomaton of
${{\mathcal{A}}}$ rooted at $q$ which accepts the regular language
$\mathcal{L}_{q}({{\mathcal{A}}})\subseteq\Sigma^{*}$, consisting of just
those words accepted by the subautomaton with $q$ as initial state. Thus
$\mathcal{L}_{q_{0}}({{\mathcal{A}}})$ is the language accepted by
${{\mathcal{A}}}$. The language $\mathcal{L}_{q}({{\mathcal{A}}})$ is called
either the _future_ of state _q_ or the _right language_ of _q._
${{\mathcal{A}}}$ is _minimal_ (i.e. _state minimal_ as opposed to
_algebraically minimal_) if for each pair of distinct states _$p,q\in Q$_ , we
have, $\mathcal{L}_{p}({{\mathcal{A}}})\neq\mathcal{L}_{q}({{\mathcal{A}}})$.
For any regular language $\mathcal{L}\subseteq\Sigma^{*}$ there is a smallest
DFA (in terms of the number of states) accepting $\mathcal{L}$. This DFA is
minimal, and is unique up to isomorphism.

An equivalence relation $\equiv$ can be defined on the states of a DFA by
$p\equiv q$ if and only if
$\mathcal{L}_{p}({{\mathcal{A}}})=\mathcal{L}_{q}({{\mathcal{A}}})$. This
relation is a congruence, i.e. if $p\equiv q$ then $p.\sigma\equiv q.\sigma$
for all $\sigma\in\Sigma^{*}$. It is known as the _Nerode congruence_.
Consider the quotient DFA ${{\mathcal{A}}}/\equiv$. This is the unique
smallest DFA which accepts the regular language
$\mathcal{L}_{q_{0}}({{\mathcal{A}}})$. The problem of minimizing a DFA
${{\mathcal{A}}}$ is therefore to compute its Nerode congruence, which will be
the identity relation if, and only if ${{\mathcal{A}}}$ is a minimal
automaton.

The problem of computing a minimal Kripke structure ${{\mathcal{A}}}$ is an
analogous but more general problem. In this case, the right language
$\mathcal{L}_{q}({{\mathcal{A}}})$ associated with a state $q$ of
${{\mathcal{A}}}$ can be defined by

$\mathcal{L}_{q}({{\mathcal{A}}})=\\{\hskip
5.0pt(\sigma_{1},...,\sigma_{n},a)\in\Sigma^{*}\times\mathbb{B}^{k}\hskip
3.0pt|\hskip 3.0pt\lambda_{q}^{*}(\sigma_{1},...,\sigma_{n})=a\hskip
5.0pt\\}.$

As before, ${{\mathcal{A}}}$ is _minimal_ if for each pair of distinct states
_$p,q\in Q$_ we have,
$\mathcal{L}_{p}({{\mathcal{A}}})\neq\mathcal{L}_{q}({{\mathcal{A}}})$. There
is again a smallest Kripke structure associated with a right language
$\mathcal{L}\subseteq\Sigma^{*}\times\mathbb{B}^{k}$. This Kripke structure is
also minimal, and unique up to isomorphism. The Nerode congruence for a Kripke
structure ${{\mathcal{A}}}$ is now defined by:

$p\equiv q$ if and only if
$\lambda_{p}^{*}(\sigma_{1},...,\sigma_{n})=\lambda_{q}^{*}(\sigma_{1},...,\sigma_{n})$
for all $(\sigma_{1},...,\sigma_{n})\in\Sigma^{*}$.

and ${{\mathcal{A}}}/\equiv$ is the unique smallest Kripke structure
associated with the right language $\mathcal{L}_{q_{0}}({{\mathcal{A}}})$. So
the problem of minimising ${{\mathcal{A}}}$ is to compute this congruence.

###  6.2 A Kripke Structure Minimisation Algorithm

Algorithm 5 Kripke Structure Minimisation

Input: A deterministic Kripke structure ${{\mathcal{A}}}$ with no unreachable
states and $k$ output bits.

Output: The Nerode congruence $\equiv$ for ${{\mathcal{A}}}$, i.e. equivalence
classes of states for the minimized structure ${{\mathcal{A}}}_{min}$
behaviourally equivalent to ${{\mathcal{A}}}$.

Create an initial state partition $P=\\{B_{q}=\\{q^{\prime}\in
Q\;|\;\lambda(q)=\lambda(q^{\prime})\\}\;|\;q\in Q\\}$. Let $n=|P|$. Let
$B_{1},...,B_{n}$ be an enumeration of P.

if $n=|Q|$ then go to line 5.

foreach  _$\sigma\in\Sigma$_ do

2 for  _$i\leftarrow 1$ to $n$ _ do

3 $B(\sigma,i)=\\{q\in B_{i}\;|\;\exists r\in Q\;s.t\;\delta(r,\sigma)=q\\}.$
/*This constitutes the subset of states in block $B_{i}$ which have
predecessors through input $\sigma$. */

4

5 $count=n+1$; foreach  _$\sigma\in\Sigma$_ do

6 choose all the subsets $B(\sigma,i)$ (excluding any empty subsets) and put
their block numbers $i$ on a waiting list (i.e. an unordered set) $W(\sigma)$
to be processed.

7 Boolean splittable = true; while  _splittable_ do

8 foreach  _$\sigma\in\Sigma$ _ do

9 foreach  _$i\in$ $W(\sigma)$_ do

10 Delete i from $W(\sigma)$ for  _$j\leftarrow 1$ to $count-1$ s.t. $\exists
t\in B_{j}$ with $\delta(t,\sigma)\in B(\sigma,i)$_ do

11 Create $B_{j}^{\prime}=\\{t\in B_{j}\;|\;\delta(t,\sigma)\in
B(\sigma,i)\\}$ if  _$B_{j}^{\prime}\subset B_{j}$_ then

12 $B_{count}=B_{j}-B_{j}^{\prime}$; $B_{j}=B_{j}^{\prime}$ foreach
_$\sigma\in\Sigma$_ do

13 $B(\sigma,count)=\\{q\in B(\sigma,j)\;|\;q\in B_{count}\\}$;
$B(\sigma,j)=\\{q\in B(\sigma,j)\;|\;q\in B_{j}\\}$ if  _$j\notin W(\sigma)$
and $0<|B(\sigma,j)|\leq|B(\sigma,count)|$_ then

14 $W(\sigma)=W(\sigma)\cup\\{j\\}$

15 else

16 $W(\sigma)=W(\sigma)\cup\\{count\\}$

17

18 $count=count+1$;

19

20

21

22 splittable = false; foreach  _$\sigma\in\Sigma$_ do

23 if  _$W(\sigma)\not=\emptyset$_ then

24 splittable=true;

25

26

Return partition blocks $B_{1},...,B_{count}$.

Algorithm 5 presents an efficient algorithm to compute the Nerode congruence
$\equiv$ of a deterministic Kripke structure ${{\mathcal{A}}}$, which is the
same as the state set of the associated quotient Kripke structure
${{\mathcal{A}}}/\equiv$. We will give a rigorous but simple proof of the
correctness of this algorithm. By means of a new induction argument, we have
simplified the correctness argument compared with [3] and [12]. First let us
establish termination of the algorithm by using an appropriate well-founded
ordering for the main loop variant.

6.2.1. Definition. Consider any pair of finite sets of finite sets
$A=\\{A_{1},...,A_{m}\\}$ and $B=\\{B_{1},...,B_{n}\\}$. We define an ordering
relation $\leq$ on $A$ and $B$ by $A\leq B$ iff $\forall 1\leq i\leq m$,
$\exists 1\leq j\leq n$ such that $A_{i}\subseteq B_{j}$. Define $A<B\iff
A\leq B\;\&\;A\neq B$. Clearly $\leq$ is a reflexive, transitive relation.
Furthermore $\leq$ is well-founded, i.e. there are no infinite descending
chains $A_{1}>A_{2}>A_{3}...$ , since $\emptyset$ is the smallest element
under $\leq$.

6.2.2. Proposition. Algorithm 5 always terminates.

Proof. We have two cases for the termination of the algorithm as a result of
the partition formed on line 5 of the algorithm: (1) when $n=|Q|$, and (2)
when $n<|Q|$.

Consider the case when $n=|Q|$ then each block in the partition corresponds to
a state of the given Kripke structure with a unique bit-label and hence in
this case the algorithm will terminate on line 5 by providing the description
of these blocks.

Now consider the case when $n<|Q|$. Then the waiting sets $W(\sigma)$ for all
$\sigma\in\Sigma$ will be initialized on lines 5, 5 and the termination of the
algorithm depends on proving the termination of the loop on line 5. Now
$W(\sigma)$ is intialized by loading the block numbers of the split sets on
line 5. There are only two possiblities after any execution of the loop. Let
$W_{m}(\sigma)$ and $W_{m+1}(\sigma)$ represent the state of the variable
$W(\sigma)$ before and after one execution of the loop respectively at any
given time. Then either $W_{m}(\sigma)=W_{m+1}(\sigma)\cup\\{i\\}$ and no
splitting has taken place and _i_ is the deleted block number, or
$W_{m}(\sigma)\cup\\{j\\}=W_{m+1}(\sigma)\cup\\{i\\}$ or
$W_{m}(\sigma)\cup\\{k\\}=W_{m+1}(\sigma)\cup\\{i\\}$ where j and k represent
the split blocks and one of them goes into $W_{m}(\sigma)$ if it has fewer
incoming transitions. In either case $W_{m}(\sigma)>W_{m+1}(\sigma)$ by
Definition 5. Therefore $W(\sigma)$ strictly decreases with each iteration of
the loop on line 5. Since the ordering $\leq$ is well-founded, Algorithm 5
must terminate.

Now we only need to show that when Algorithm 5 has terminated, it returns the
Nerode congruence $\equiv$ on states.

6.2.3. Proposition. Let $P_{i}$ be the partition (block set) on the $ith$
iteration of Algorithm 5. For any blocks $B_{j},B_{k}\in P_{i}$ and any states
$p\in B_{j},q\in B_{k}$ if $j\neq k$ then $p\not\equiv q$.

Proof. By induction on the number $i$ of times the loop on line 5 is executed.
Basis: Suppose $i=0$ then clearly the result holds because each block created
at line 5 is distinguishable by the empty string $\epsilon$. Induction Step:
Suppose $i=m>0$. Let us assume that the proposition holds after $m$ executions
of the loop.

Consider any $B_{j},B_{k}\in P_{m}$. During the $m+1$th execution of the loop
on line 5 either block $B_{j}$ is split into $B_{j}^{\prime}$ and
$B_{j}^{\prime\prime}$ or $B_{k}$ is split into $B_{k}^{\prime}$ and
$B_{k}^{\prime\prime}$ but not both during one execution of the loop (due to
line 5).

Consider the case when $B_{j}$ is split then for any $p\in B_{j}$, either
$p\in B_{j}^{\prime}$ or $p\in B_{j}^{\prime\prime}$. But for any $p\in B_{j}$
and $q\in B_{k}$, $p\not\equiv q$ by the induction hypothesis. Therefore, for
$p\in B_{j}^{\prime}$ or $p\in B_{j}^{\prime\prime}$ $p\not\equiv q$. Hence
the proposition is true for $m+1$th execution of the loop in this case.

By symmetry the same argument holds when $B_{k}$ is split.

The following Lemma gives a simple, but very effective way to understand
Algorithm 5. Note that this analysis is more like a temporal logic argument
than a loop invariant approach. This approach reflects the non-determinism
inherent in the algorithm.

6.2.4. Lemma. For any states $p,q\in Q$, if $p\not\equiv q$ and initially $p$
and $q$ are in the same block $p,q\in B_{i_{0}}$ then eventually $p$ and $q$
are split into different blocks, $p\in B_{j}$ and $q\in B_{k}$ for $j\not=k$.

Proof. Suppose that $p\not\equiv q$ and that initially $p,q\in B_{i_{0}}$ for
some block $B_{i_{0}}$. Since $p\not\equiv q$ then for some $n\geq 0$, and
$\sigma_{1},\ldots,\sigma_{n}\in\Sigma$,

$\lambda^{*}(p,\sigma_{1},\ldots,\sigma_{n})\not=\lambda^{*}(q,\sigma_{1},\ldots,\sigma_{n}).$

We prove the result by induction on $n$. Basis Suppose $n=0$, so that
$\lambda(p)\not=\lambda(q)$. By line 5, $p\in B_{p}$ and $q\in B_{q}$ and
$B_{p}\not=B_{q}$. So the implication holds vacuously. Induction Step Suppose
$n>0$ and for some $\sigma_{1},\ldots,\sigma_{n}\in\Sigma$,

$\lambda^{*}(p,\sigma_{1},\ldots,\sigma_{n})\not=\lambda^{*}(q,\sigma_{1},\ldots,\sigma_{n}).$

(a) Suppose initially $\delta(p,\sigma_{1})\in B(\sigma_{1},\alpha)$ and
$\delta(q,\sigma_{1})\in B(\sigma_{1},\beta)$ for $\alpha\neq\beta$.

Consider when $\sigma=\sigma_{1}$ on the first iteration of the loop on line
5. Clearly, $B(\sigma_{1},\alpha),B(\sigma_{1},\beta)\in W(\sigma)$ at this
point. Choosing $i=\alpha$ and $j=i_{0}$ on this iteration then since
$\delta(p,\sigma_{1})\in B(\sigma_{1},\alpha)$ we have

$B_{i_{0}}^{\prime}=\\{t\in B_{i_{0}}\;|\;\delta(t,\sigma_{1})\in
B(\sigma_{1},\alpha)\\}\subset B_{i_{0}}$

This holds because $q\in B_{i_{0}}$ but $\delta(q,\sigma_{1})\in
B(\sigma_{1},\beta)$ and $B(\sigma_{1},\alpha)\not=B(\sigma_{1},\beta)$ so
$B(\sigma_{1},\alpha)\cap B(\sigma_{1},\beta)=\emptyset$ and hence $q\not\in
B^{\prime}_{i_{0}}$. Therefore $p$ and $q$ are split into different blocks on
the first iteration so that $p\in B^{\prime}_{i_{0}}$ and $q\in
B_{i_{0}}-B^{\prime}_{i_{0}}$.

By symmetry, choosing $i=\beta$ and $j={i_{0}}$ then $p$ and $q$ are split on
the first loop iteration with $q\in B^{\prime}_{i_{0}}$ and $p\in
B_{i_{0}}-B^{\prime}_{i_{0}}$.

(b) Suppose initially $\delta(p,\sigma_{1}),\delta(q,\sigma_{1})\in
B(\sigma_{1},\alpha)$ for some $\alpha$. Now

$\lambda^{*}(\;\delta(p,\sigma_{1}),\sigma_{2},\ldots,\sigma_{n}\;)\not=\lambda^{*}(\;\delta(q,\sigma_{1}),\sigma_{2},\ldots,\sigma_{n}\;).$

So by the induction hypothesis, eventually $\delta(p,\sigma_{1})$ and
$\delta(q,\sigma_{1})$ are split into different blocks,
$\delta(p,\sigma_{1})\in B_{\alpha}$ and $\delta(p,\sigma_{1})\in B_{\beta}$.
At that time one of $B_{\alpha}$ or $B_{\beta}$ is placed in a waiting set
$W(\sigma)$. Then either on the same iteration of the loop on line 5 or on the
next iteration, we can apply the argument of part (a) again to show that $p$
and $q$ are split into different blocks.

Observe that only one split block is loaded into $W(\sigma)$ on lines 5-5.
From the proof of Lemma 5 we can see that it does not matter logically which
of these two blocks we insert into $W(\sigma)$. However, by choosing the
subset with fewest incoming transitions we can obtain a worst case time
complexity of order $O(|\Sigma|.n\hskip 3.0ptlog_{2}\hskip 3.0ptn)$, as we
will show.

6.2.5. Corollary. For any states $p,q\in Q$, if $p\not\equiv q$ then $p$ and
$q$ are in different blocks when the algorithm terminates.

Proof. Assume that $p\not\equiv q$.

(a) Suppose at line 3 that $n=|Q|$. Then initially, all blocks $B_{i}$ are
singleton sets and so trivially $p$ and $q$ are in different blocks when the
algorithm terminates.

(b) Suppose at line 3 that $n<|Q|$.

(b.i) Suppose that $p$ and $q$ are in different blocks initially. Since blocks
are never merged then the result holds.

(b.ii) Suppose that $p$ and $q$ are in the same block initially. Since
$p\not\equiv q$ then the result follows by Lemma 5.

We conclude this section by verifying that our generalisation of Hopcroft’s
minimisation algorithm does not actually change its time complexity.

6.2.6. Proposition. If ${{\mathcal{A}}}$ has $n$ states then Algorithm 5 has
worst case time complexity $O(|\Sigma|.n\log_{2}n)$.

Proof. Creating the initial block partition on line 5 requires at most $O(n)$
assignments. The block subpartitioning in the loop on line 5 requires at most
$O(kn)$ moves of states. Also the the initialisation of the waiting lists
$W(\sigma)$ in the loop on line 5 requires at most $O(kn)$ assignments.

Consider one execution of the body of the loop starting on line 5, i.e. lines
5 \- 5. Consider any states $p,\hskip 3.0ptq\in Q$ and suppose that
$\delta(p,\hskip 3.0pt\sigma)=q$ for some $\sigma\in\Sigma$. Then the state
$p$ can be: (i) moved into $B^{\prime}_{j}$ (line 5), (ii) removed from
$B_{j}$ (line 5), or (iii) moved into $B(\sigma,\hskip 3.0pti)$ or
$B(\sigma,\hskip 3.0ptcount)$ (lines 5, 5) if, and only if, a block $i$ is
being removed from $W(\sigma)$ such that $q\in B(\sigma,\hskip 3.0pti)$ at
that time. (Such a block sub-partition $B(\sigma,\hskip 3.0pti)$ can be termed
a splitter of $q$.)

Now each time a block $i$ containing $q$ is removed from $W(\sigma)$ its size
is less than half of the size when it was originally entered into $W(\sigma)$,
by lines 5-5. So $i$ can be removed from $W(\sigma)$ at most $O(log_{2}\hskip
3.0ptn)$ times. Since there are at most $|\Sigma|$ values of $\sigma$ and $n$
values of $p$, then the total number of state moves between blocks and block
sub-partitions is at most $O(|\Sigma|.n\hskip 3.0ptlog_{2}\hskip 3.0ptn)$.

##  7 Heuristic Estimation of IKL Convergence

When the IKL learning algorithm is applied to the problem of learning based
testing of software, the question naturally arises, when should we stop
testing? When the system under test (SUT) is sufficiently small, exhaustive
testing can be achieved if we continue until the IKL algorithm converges. But
how can we detect convergence?

Traditionally, in automata learning theory, this question is answered by
executing an equivalence oracle on the SUT and the hypothesis automaton such
as [20]. For a DFA learning algorithm such as L* [2], learning is continued if
the equivalence oracle can return a string that is incorrectly learned by the
hypothesis DFA, otherwise learning is terminated. However, in the context of
black-box testing a glass box equivalence oracle, based on direct comparison
of the SUT and the hypothesis automaton, is not acceptable for two reasons:
(1) the principles of black-box testing do not allow us to expose the SUT for
glass box equivalence checking, and (2) even if we ignore (1), in practise
there are no glass box equivalence checkers that can compare an arbitrary
piece of software (the SUT implementation) with the hypothesis automaton for
equivalence. Of course, a glass box equivalence oracle can be stochastically
approximated by a black-box equivalence oracle based on random queries. Random
queries are even necessary during LBT when no counterexamples can be found by
model checking. However, a purely stochastic solution to equivalence checking
is not possible, as we will discuss below. Therefore problems (1) and (2)
force us to consider other black-box heuristics for estimating convergence of
the IKL algorithm.

Figure 2:  Graph for True and Estimated Convergence for Elevator

Figure 2 depicts the state space size of successive hypothesis automata
$H_{i}$ ($i=1,...104$) generated by the IKL algorithm while learning and
testing a small reactive system against a simple temporal logic specification.
In this controlled experiment the SUT was a simplified model of an elevator,
with a state space size of 38 states and an input alphabet of 4 symbols. This
model is well within the scope of complete learning using IKL, which converges
quickly.

It is natural to consider whether any features of a graph such as Figure 2 can
be used to estimate the point of convergence. This graph is comparable in its
structure for all similar experiments that were conducted. It shows a
succession of peaks, each one well above the state space size of the
underlying SUT. However at some point these peaks die out and a steady state
space size is reached. Each peak and trough seem to indicate a distinct new
phase in learning, and therefore they do shed some light on the learning
activity. However, they clearly do not indicate convergence, which first
appears in hypothesis automaton $H_{55}$. (In controlled experiments we can
apply a glass box equivalence checker to accurately determine convergence.)

Although we cannot apply glass box equivalence checking between the SUT and
hypothesis automata $H_{i}$, we can apply it to pairs of successive hypothesis
automata $H_{i}$ and $H_{i-1}$, since the representations of these are known
and visible. We can even iterate this test across $n$ successive hypothesis
automata $H_{i},...,H_{i-n}$ (by conjunction of the outcomes) which we term
$n$-equivalence checking. After convergence has been achieved, $n$-equivalence
checking will be positive for every value of $n$. This gives a heuristic for
black box equivalence checking that is more complex than stochastic
equivalence checking, since the queries used to generate successive hypothesis
automata are not always random. Many arise from model checking
counterexamples. It is difficult to say that queries generated by model
checking are randomised, since they are always counterexamples to a specific
temporal logic formula, which can strongly bias their structure.

We therefore decided to empirically evaluate the reliability of
$n$-equivalence checking as a heuristic indicator of convergence. For this
evaluation we considered different SUTs with different state space sizes,
different temporal logic formulas, and different values of $n$.

We chose two different SUTs, which were models of a simple cruise controller
and a simple elevator. The cruise controller model was an 8-state 5-bit Kripke
structure with an input alphabet size of 5. The elevator model was a 38-state
8-bit Kripke structure with an input alphabet size of 4. We considered four
different temporal logic test requirements for the cruise controller and six
for the elevator. These gave a total of ten convergence experiments for the
two SUTs.

Each of these ten experiments was then used to evaluate the $n$-equivalence
heuristic for $n=1,2,10,50$. For $n=1,2$ the heuristic completely failed to
identify convergence (i.e. the indicator always triggered too early) for all
ten experiments. For $n=10$, just two experiments with the cruise controller
(the smaller case study) correctly identified convergence , while eight still
failed. Using $n=50$ all experiments correctly identified convergence.
However, note that for increasingly large values of $n$ we tended to
overestimate the convergence point by an increasing margin. Table 1 summarises
the relationship between true convergence and estimated convergence for
$n=50$.

Requirement |  True Convergence |  Estimated Convergence
---|---|---
1 |  $H_{55}$ |  $H_{104}$
2 |  $H_{16}$ |  $H_{66}$
3 |  $H_{44}$ |  $H_{94}$
4 |  $H_{32}$ |  $H_{82}$
5 |  $H_{18}$ |  $H_{68}$
6 |  $H_{25}$ |  $H_{66}$
Table 1: True and Estimated Convergence

These simple experiments suggest that for sufficiently large $n$,
$n$-equivalence, can be used as a reliable heuristic indicator for
convergence. However, further empirical and theoretical analysis still seems
necessary to predict the smallest reliable value of $n$ which minimises the
problem of overestimation.

##  8 Conclusions

We have defined and analysed a learning algorithm IKL for deterministic Kripke
structures which is efficient for applications in software testing. This
algorithm extends active incremental learning with new features such as lazy
learning and projection. We have formally proved the correctness of the IKL
algorithm and its main components. We have also empirically evaluated a black
box heuristic for detecting convergence of learning, which can be used to
terminate testing for small systems under test.

Incremental learning and projection combine to make IKL scalable to larger
systems under test. Also, incremental and lazy learning combine to support
frequent generation of hypothesis automata with which we can discover SUT
errors much faster than random testing by model checking. These claims have
been empirically evaluated and supported in [17] and [28]. The IKL algorithm
has been implemented in the LBTest tool [18] for learning based testing of
reactive systems.

We believe that the efficiency of learning-based testing can be even further
improved by more research on model inference. For example, the modular
architecture of the IKL algorithm can support experiment with other
incremental DFA learning algorithms instead of the ID learning algorithm of
Section 4, (e.g. RPNI2 [9]). The impact of the frequency of hypothesis
automata generation on testing efficiency could then be further investigated.
When hypothesis generation is very frequent the overhead of model checking is
high, and this overhead can slow down the entire LBT process. However, if
generation is very infrequent, then little use is made of the model checker to
conduct a directed search for SUT errors using queries that can falsify the
user requirements. This is also inefficient. (Recall the discussion of Section
1.2.) More generally, we could consider an optimal tuning of the rate of
hypothesis automata generation, e.g. based on the estimated density of SUT
errors.

The relationship between computational learning and software testing has been
a fruitful line of research ever since Weyuker’s thesis [27]. Many fundamental
questions remain within the context of learning-based testing. For example,
the execution of any automata learning algorithm can always be associated with
a prefix tree construction (see e.g. [8]) based on the query set used. How can
we influence the choice between breadth-first and depth-first search for SUT
errors using this prefix tree? Another important question is whether we can
find other techniques to generate active learner queries besides congruence
construction? Such techniques should be aimed at reducing the need for random
queries, which can be very inefficient in practise.

We gratefully acknowledge financial support for this research from the Swedish
Research Council (VR), the Higher Education Commission (HEC) of Pakistan, and
the European Union under project HATS FP7-231620.

## References

  * [1] D. Angluin.  A note on the number of queries needed to identify regular languages.  Information and Control, 51(1):76–87, October 1981.
  * [2] D. Angluin.  Learning regular sets from queries and counterexamples.  Information and Computation, 75(1):87–106, November 1987.
  * [3] J. Berstel, L. Boasson, O. Carton, and I. Fagnot.  Minimization of Automata.  ArXiv e-prints, October 2010.
  * [4] G. Birkhoff.  Subdirect unions in universal algebra.  Bull. Amer. Math. Soc, 50:764–768, 1944.
  * [5] D. Bustan and O. Grumberg.  Simulation-based minimization.  ACM Trans. Comput. Logic, 4(2):181–206, April 2003.
  * [6] P. Chauhan, E. M. Clarke, J. H. Kukula, S. Sapra, H. Veith, and D. Wang.  Automated abstraction refinement for model checking large state spaces using sat based conflict analysis.  In Proc. 14th International Conference On Formal Methods in Computer-Aided Design (FMCAD02), 2002.
  * [7] E. Clarke, A. Gupta, J. Kukula, and O. Strichman.  Sat-based abstraction refinement using ilp and machine learning.  In Proc. 21st International Conference On Computer Aided Verification (CAV’02), 2002.
  * [8] C. de la Higuera.  Grammatical Inference.  Cambridge University Press, 2010.
  * [9] P. Dupont.  Incremental regular inference.  In Proceedings of the Third ICGI-96, number 1147 in LNAI, 1996.
  * [10] E.M. Gold.  Language identification in the limit.  Information and Control, 10(5):447–474, 1967.
  * [11] A. Groce, D. Peled, and M. Yannakakis.  Adaptive model checking.  Logic Journal of the IGPL, 14(5):729–744, 2006.
  * [12] J. E Hopcroft.  An n log n algorithm for minimizing states in a finite automaton.  In Z. Kohavi and A. Paz, editors, Theory of Machines and Computations, pages 189–196. Academic Press, 1971.
  * [13] K. Meinke.  Automated black-box testing of functional correctness using function approximation.  In ISSTA ’04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, pages 143–153, New York, NY, USA, 2004. ACM.
  * [14] K. Meinke and F. Niu.  A learning-based approach to unit testing of numerical software.  In Proc. Twenty Second IFIP Int. Conf. on Testing Software and Systems (ICTSS 2010), number 6435 in LNCS, pages 221–235. Springer, 2010.
  * [15] K. Meinke and F. Niu.  Learning-based testing for reactive systems using term rewriting technology.  In Proc. 23rd IFIP Int. Conf. on Testing Software and Systems (ICTSS 2011), number 7019 in LNCS, pages 97–114. Springer, 2011.
  * [16] K. Meinke and F. Niu.  An incremental learning algorithm for extended mealy automata.  In Proc. 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, number 7610 in LNCS. Springer, 2012.
  * [17] K. Meinke and M. Sindhu.  Incremental learning-based testing for reactive systems.  In Proc Fifth Int. Conf. on Tests and Proofs (TAP2011), number 6706 in LNCS, pages 134–151. Springer, 2011.
  * [18] K. Meinke and M.A. Sindhu.  Lbtest: A learning-based testing tool for reactive systems.  In Software Testing, Verification and Validation (ICST), 2013 IEEE Sixth International Conference on, pages 447–454, March 2013.
  * [19] K. Meinke and J.V. Tucker.  Universal algebra.  In Handbook of Logic in Computer Science: Volume 1, pages 189–411. Oxford University Press, 1993.
  * [20] D.A. Norton.  Algorithms for testing equivalence of finite state automata, with a grading tool for jflap.  Technical report, Rochester Institute of Technology, Department of Computer Science, 2009.
  * [21] R.G. Parekh, C. Nichitiu, and V.G. Honavar.  A polynomial time incremental algorithm for regular grammar inference.  In Proc. Fourth Int. Colloq. on Grammatical Inference (ICGI 98), LNAI. Springer, 1998.
  * [22] D. Peled, M.Y. Vardi, and M. Yannakakis.  Black-box checking.  In Formal Methods for Protocol Engineering and Distributed Systems FORTE/PSTV, pages 225–240. Kluwer, 1999.
  * [23] H. Raffelt, B. Steffen, and T. Margaria.  Dynamic testing via automata learning.  In Hardware and Software: Verification and Testing, number 4899 in LNCS, pages 136–152. Springer, 2008.
  * [24] M. A. Sindhu and K. Meinke.  IDS: An Incremental Learning Algorithm for Finite Automata.  ArXiv e-prints, June 2012.
  * [25] N. Walkinshaw.  Assessing test adequacy for black-box systems without specifications.  In Proc. Twenty Third IFIP Int. Conf. on Testing Software and Systems (ICTSS 2011), number 7019 in LNCS, pages 209–224. Springer, 2011.
  * [26] N. Walkinshaw, K. Bogdanov, J. Derrick, and J. Paris.  Increasing functional coverage by inductive testing: a case study.  In Proc. Twenty Second IFIP Int. Conf. on Testing Software and Systems (ICTSS 2010), number 6435 in LNCS, pages 126–141. Springer, 2010.
  * [27] E. Weyuker.  Assessing test data adequacy through program inference.  ACM Trans. Program. Lang. Syst, 5(4):641–655, 1983.
  * [28] Peter Y. Wong, Richard Bubel, Frank S. Boer, Miguel Gómez-Zamalloa, Stijn Gouw, Reiner Hähnle, Karl Meinke, and Muddassar Azam Sindhu.  Testing abstract behavioral specifications.  Int. J. Softw. Tools Technol. Transf., 17(1):107–119, February 2015\.