Gennady A. Oparin, Vera G. Bogdanova, Sergey A. Gorsky

Matrosov Institute for System Dynamics and Control Theory Siberian Branch of the Russian Academy of Sciences

The high computational complexity of some problems in the analysis of dynamics and structural-parametric synthesis for different classes of dynamic controlled systems leads to the development of methods and software for their parallel solution. Based on the Boolean constraints method, problems of qualitative analysis of the trajectories behavior of binary dynamical systems, whose operation is considered on a finite time interval, are reduced to solving Boolean satisfiability problems and checking the validity of quantified Boolean formulas. A mathematical model of the studied dynamic property is constructed as a system of Boolean equations, taking into account both the property specification and the equations of the dynamics of a specific object. Such an approach is declarative and provides the possibility of data parallelism. For verifying the validity of the quantified Boolean formulas, a parallel solver Hpc2qall was implemented. Unlike similar solvers, Hpc2qall not only produces the answer (SAT or UNSAT) but finds all values sets of universally quantified variables leading to this answer. An example is given of applying a constructive approach to solving the problem of the synthesis of stabilizing feedback.

binary dynamic system, Boolean model, parallel 2QBF solver, qualitative analysis