QUANTIFIED BOOLEAN FUNCTION SATISFIABILITY SOLVING METHODS APPLICATION TO EXTENDED FINITE-STATE MACHINE CREATION BASED ON SCENARIOS AND TEMPORAL PROPERTIES

Ulyantsev Vladimir Igorevich, Elena Panchenko

2013 , VOLUME 13, NUMBER 4 ( JULY-AUGUST )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

QUANTIFIED BOOLEAN FUNCTION SATISFIABILITY SOLVING METHODS APPLICATION TO EXTENDED FINITE-STATE MACHINE CREATION BASED ON SCENARIOS AND TEMPORAL PROPERTIES

V. I. Ulyantsev, E. Panchenko

Read the full article

Abstract

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.

Keywords: quantifiers, Boolean function, control finite-state machines, verification

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License