Adapting Grammar Inference Techniques to Mine State Machines - Mining Software Specifications: Methodologies and Applications - page 62

State-based models are usually presumed to be complete; if a particular
transition does not exist in the model, it is assumed to be impossible in prac-
tice. Such models are represented as straightforward LTSs. Although this can
be valid when reasoning about a finished design, in our setting we will be
dealing with unnished models { hypothesized models of system behavior. As
stated by Uchitel et al. [33]: \In this setting the distinction between proscribed
behaviour and behaviour that has not yet been dened is an important one."
To accommodate this, the technique presented here is defined with respect
to an extension of conventional LTSs: partial LTSs (PLTSs) [33]. If they are
known to be incomplete, it is possible to explicitly distinguish between model
transitions that are known to be invalid, and transitions that are simply not
known to exist at all.
Denition 1 (Partial LTS (PLTS)). A PLTS is a tuple A = (Q; ;;q 0 ; ).
This is defined as an LTS, but it is assumed to be only partial. To make the
explicit distinction between unknown and invalid behavior, makes the set of
invalid labels from a given state explicit { Q where (q;) 2 implies
that will be rejected in q.
To define the language of a PLTS, we draw on the inductive definition for
an extended transition function ^ used by Hopcroft et al. [18] to define two
notions of language: prescribed and proscribed which are used below.
Definition 2 (Prescribed and Proscribed Languages). For a state p and a
string w, the extended transition function ^ returns the state p that is reached
when starting in state p and processing sequence w. For the base case ^ (q;) =
q. For the inductive case, let w be of the form xa, where a is the last element,
and x is the prefix. Then ^ (q;w) = ( ^ (q;x);a).
Given the extended transition function, the prescribed language of a PLTS
A can be defined as follows:
PreL(A) = fwj ^ is defined for (q 0 ;w)g.
The proscribed language of a PLTS can be defined as:
ProL(A) = fxasj ^ is defined for (q 0 ;x) and ( ^ (q 0 ;x);a) 2 and s 2 g.
By construction PreL(A) \ProL(A) = ;.
It is important to note that the prescribed language of a PLTS is prefix-
closed. This means that, for every sequence in PreL(A), any prefix of it is
also in PreL(A).
3.2.2 State Merging
Numerous techniques have emerged that attempt to reverse-engineer state
machines from program traces [1, 5, 11, 21{23, 31]. The high-level process they
follow is shown in Figure 3.2. The developer records a set of traces that are
deemed to comprehensively exercise the target program; these are fed to a
machine-learning technique, which produces a hypothesis state machine. Such