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

ral constraint could be: \You cannot save a le unless it has been edited."
Although this rule is relatively straightforward, it is virtually impossible to
ensure that the hypothesis model will conform to the rule without supply-
ing an impractically large number of traces. However, such rules can be suc-
cinctly expressed in well-established formalisms such as linear temporal logic
(LTL) [28].
LTL expressions enable the behavior of a system to be characterised in
terms of propositions that describe the state of a system. A set of temporal
modal operators can be used to describe the temporal relationships between
these propositions. Important operators are listed below:
The next operator , where means that the property has to hold
in the next state.
The global operator , where means that the property has to hold
for every future state.
The eventually operator }, where } means that the property has to
hold eventually.
The until operator U, where 'U means that the property ' has to
hold until property holds.
The release operator R, where 'R means that the property is true
until ' becomes true, or forever if ' is never true.
So, for example, the property that you cannot save a file unless it has been
edited can be expressed as follows:
(editR:save) ^(save !(editR:save))
There exist several powerful model-checking techniques to ensure that a
labeled transition system conforms to such properties [17]. Model checkers
not only state whether or not a model conforms to a particular constraint,
but also provide counter examples of paths in the model that violate a given
constraint. The approach described by the authors [34] shows how the QSM
algorithm can be extended to integrate constraints. Depending on the choice
of initial traces and the constraints provided, the number of questions and
traces can be substantially reduced, whilst increasing the accuracy of the final
machine.
The algorithm is shown in algorithm 5 and assumes the existence of some
model-checker (invoked by the modelCheck function), and the availability of
a set of constraints (provided as a set LTL). Lines 1{4 are the same as the
QSM algorithm; an APTA is constructed, pairs of states are selected to be
merged, and for each merge the hypothesis machine PLTS 0 is checked to
ensure that it is compatible with Neg. Once this has happened, the model
checker is used to check that PLTS 0 is compatible with LTL (line 5). If this