Learning and Adaptive Testing of Nondeterministic State Machines

The paper addresses the problems of active learning and conformance testing of systems modeled by nondeterministic Mealy machines (NFSM). It presents a unified SAT-based approach originally proposed by the authors for deterministic FSMs and now generalized to partial nondeterministic machines and checking experiments. Learning a nondeterministic black box, the approach neither needs a Teacher nor uses it a conformance tester to approximate equivalence queries. The idea behind this approach is to infer from a current set of traces not one, but two inequivalent conjectures, use an input sequence distinguishing them in an output query, and update the current trace set with an observed trace to obtain a new pair of distinguishable conjectures, if possible. The classical active learning problem is further generalized by adding a nondeterministic specification FSM, which defines the solution space. The setup unifies the learning and adaptive testing problems and makes them equisolvable with the proposed approach.