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

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2024 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика