QUANTIFIED BOOLEAN FUNCTION SATISFIABILITY SOLVING METHODS APPLICATION TO EXTENDED FINITE-STATE MACHINE CREATION BASED ON SCENARIOS AND TEMPORAL PROPERTIES
Read the full article
The question of automatic control systems application for design of systems with complex behavior is considered. A method of control state machine design for a given set of scenarios and temporal properties that must be met in the resulting automaton is proposed. The method is based on the reduction to the problem of quantified Boolean function satisfiability. The algorithm of function construction and the basic components of the resulting Boolean formula are described.