The Boolean constraint method application for qualitative analysis of the dynamical properties of singular Boolean networks

Abstract

Qualitative study problems of trajectories behaviour for singular Boolean networks functioning on a finite time interval are solved using the method of Boolean constraints. In the form of Boolean constraints, models are built for local dynamical properties, the periodicity property of trajectories, and the property of the reachability of the target state set from the initial state set. Depending on the property, the verification of Boolean models is reduced to the Boolean satisfiability problem or the problem of verifying the truth of a quantified Boolean formula. Several examples demonstrate the technology of qualitative analysis of dynamic properties in a microservice heterogeneous computing environment. The applied software modules for constructing a Boolean model of the dynamical property of singular Boolean networks and verifying the feasibility of the model are implemented in the form of computational microservices. The use of this approach provides independence, reproducibility, autonomy, and scalability of modules. The developed microservices are integrated into the applied microservices package. This package is intended for the qualitative study of binary dynamic systems. The rights to launch microservices are delegated to the managing agents of this package installed in the nodes of the distributed environment. The developed automation tools allow a specialist in automaton dynamics to formulate the problem statement on a computational model of the subject area in meaningful terms.