Active learning of nondeterministic systems from an ioco perspective

Model-based testing allows the creation of test cases from a model of the system under test. Often, such models are difficult to obtain, or even not available. Automata learning helps in inferring the model of a system by observing its behaviour. The model can be employed for many purposes, such as testing other implementations, regression testing, or model checking. We present an algorithm for active learning of nondeterministic, input-enabled, labelled transition systems, based on the well known Angluin’s L* algorithm. Under some assumptions, for dealing with nondeterminism, input-enabledness and equivalence checking, we prove that the algorithm produces a model whose behaviour is equivalent to the one under learning. We define new properties for the structure used in the algorithm, derived from the semantics of labelled transition systems. Such properties help the learning, by avoiding to query the system under learning when it is not necessary