Extended Finite-State Machine Induction using SAT-Solver

In the paper we describe the extended finite-state machine (EFSM) induction method which uses SAT-solver. Input data for the induction algorithm is a set of test scenarios. The algorithm consists of several steps: scenarios tree construction, compatibility graph construction, Boolean formula construction, SAT-solver invocation and finite-state machine construction from the satisfying assignment. These extended finite-state machines can be used in automata-based programming, where programs are designed using automated controlled objects. Each controlled object contains a finite-state machine and a controlled object. The described method has been tested on randomly generated scenario sets containing 250 to 1500 elements and on the alarm clock controlling EFSM induction problem where it has greatly outperformed genetic algorithm.