abstract = "In this paper, we describe the method of finite state
machine (FSM) induction using genetic algorithm with
fitness function, cross-over and mutation based on
testing and model checking. Input data for the genetic
algorithm is a set of tests and a set of properties
described using linear time logic. Each test consists
of an input sequence of events and the corresponding
output action sequence. In previous works testing and
model checking were used separately in genetic
algorithms. Usage of such an approach is limited
because the behaviour of system usually cannot be
described by tests only. So, additional validation or
verification is needed. Calculation of fitness function
based only on verification do not perform well because
there are very few possible values of fitness function
(verification gives only yes or no answer). The
approach described is tested on the problem of finite
state machine induction for elevator doors controlling.
Using tests only the genetic algorithm constructs the
finite machine working improperly in some cases. Usage
of verification allows to induct the correct finite
state machine.",
notes = "Also known as \cite{2002085} Distributed on CD-ROM at
GECCO-2011.