Binary dynamical systems (BDS) are widely used in bioinformatics [1,2], cryptography [3,4], the study of fault tolerance of computer networks [5,6], and in many other subjects areas. Recently, the BDS study has attracted considerable attention in systems biology. In particular, it is used as a model of genetic regulatory networks [7]. In our research [8], the Boolean constraints method for the qualitative analysis of BDS dynamic properties is proposed. This method is based on the following provisions:
1. Formalization of dynamic properties definitions in the language of predicate logic and the use of bounded quantifiers of existence and universality; 2. Conversion of the logical property formula that includes the equations of the BDS dynamics; 3. Elimination of bounded quantifiers and obtaining a property formula in the applied logic of predicates with unbounded quantifiers.
A model of the dynamic property in the form of a Boolean constraint is obtained using the sequential execution of these three stages. This model has the form of a Boolean equation or quantified Boolean formula (QBF). The verification of the BDS property is reduced to the Boolean satisfiability problem or verifying QBF truth. These problems are solved using modern SAT [9] and QSAT [10] solvers. In recent years, there has been a significant increase in the performance of specialized algorithms for solving SAT and QSAT problems due to using effective heuristics and deep parallelization of the computational process. Therefore, the variables number in the dynamic property model can be thousands.
The Boolean constraint method is a fairly general method for the qualitative analysis of BDS on a finite time interval. In [8], this method is used for qualitative analysis of autonomous systems. This study aims to use this method for a qualitative analysis of the observability property of controlled BDS.
The article is structured as follows. Section 2 provides a brief overview of the use of dynamic models in solving the observability problem. In Section 3, a mathematical model of a controlled BDS and a problem statement for verifying k-observability for this model are presented. In Section 4, a Boolean equation equivalent to the original system and a formal definition of k-observability is given. Also, a Boolean model of this property in the form of a quantified Boolean formula is obtained. The tools and model transformations used for the computer solution of the k-observability problem are indicated in Section 5. In Section 6, the proposed technology of qualitative analysis of the kobservability property for controlled BDS is demonstrated in several examples. The final Section 7 offers the advantages of the proposed method.
Observability is one of the fundamental notions in general control theory [11]. In particular, this applies to the BDS control theory. Observability in control theory is a property that determines the possibility of unambiguous recovery of information about the states of a system from a known output on a finite time interval.
In the last decade, many publications have been devoted to the observability property of BDS (Boolean networks). In [7,12,13,14,15], various definitions and methods for verifying this property have been proposed. In [12][13][14][15], the study of the observability property is based on the approach using the semi-tensor product (STP) of matrices [16]. As noted in [12], such an approach has a disadvantage since the dimension of the obtained matrix is n n 2 2 . This disadvantage is the computation complexity for a high dimension n of the BDS state vector. In [13], an estimate of the acceptable value of the dimension n (n <25) is given. For testing observability, an approach based on the idea of representing BDS in polynomial form was proposed [7]. As the authors noted, computing a Gröbner basis [17] used in this method leads, in the general case, to double exponential complexity. In particular, for loosely coupled genetic regulatory networks, the method proposed in [7] is applicable for significantly larger dimensions of the state vector of their Boolean models comparing with the STP method.
A comparative analysis of different types of observability is presented in [18]. Checking the observability property has high computational complexity. So the problem of reducing and speeding up enumeration is fundamental for all the proposed methods. Based on the authors' Boolean constraints method, this problem is solved by SAT [9] and QSAT [10] solvers efficiently.
A nonlinear BDS of the following form is considered: ) . The value k in the definition of the set T is assumed to be a predetermined constant. This limitation occurs for the following reason. In a qualitative study of the behavior of the trajectories of system (1), of practical interest is the feasibility of some dynamic property for a fixed, not too large k.
For will be denoted by * x . It is necessary to check for system (1) the satisfiability of the k-observability property. We use the following definition of this property, one of several definitions given in [19]. For any two different states 0 0 , x x , there is an input sequence * u of length k such that the corresponding output sequences do not coincide ( * * ỹ y ). is equivalent to one Boolean equation of the following form:
,
H are i-th components of vector-functions F and H; is the addition modulo-2 operation.
For multistep transitions ( 1 k
), system (1) is correspondingly equivalent to the following Boolean equation:
For the initial state 0 x , equation ( 2) takes the form
According to the method of Boolean constraints, we write the formal definition of the kobservability of a BDS in the language of applied logic of predicates with bounded quantifiers:
Let us get rid of the bounded quantifiers of existence and universality and bear in mind the equations of the dynamics of the BDS (2, 3) for various initial conditions. We obtain the following Boolean model of the observability property in the form of a quantified Boolean formula:
where the function E with appropriate arguments satisfies the following Boolean constraint:
This constraint is equivalent to the condition of equality of two Boolean vectors 1 z and 2 z of the dimension p. The total number of subject variables in formula ( 4
The implementation of the proposed approach to the qualitative analysis of the considered dynamic property is based on the Boolean constraints method and performed in the form of an applied microservices package (AMP) [20]. This AMP was created based on the HPCSOMAS framework [21].
The AMP provides the following tools for automating the solving problems of qualitative analysis and structural-parametric synthesis of BDS (Figure 1): Constructing Boolean models of the dynamic properties of autonomous and controlled BDS; Solving a separate problem of the qualitative analysis of BDS (checking the feasibility of a dynamic property); Solving complex problems of qualitative analysis of BDS, including performing several separate tasks with alternating construction of Boolean models and checking their feasibility; Graphic and tabular visualizing of obtained results.
The listed facilities are structured as separate complexes (processors) of the package. Access to the complexes is performed through the user Dew agent [22]. In figure 1, the structural connections of AMP complexes, grouped in these complexes objects and corresponding used layers of knowledge are shown. The conceptual model of AMP, the construction and use of AMP for solving the problems of qualitative analysis of BDS are discussed in detail in [20].
For checking the observability property, complexes for constructing Boolean models and qualitative analysis of controlled BDS are used. For conversing Boolean expressions in dynamic properties models to CNF, the Tseitin transform [23], the Plaisted-Greenbaum transform [24], and the transformation of the Boolean equation ANF = 0 to the form CNF = 1 [25] are used. For solving Boolean satisfiability problems or checking the QBF truth, computational microservices are used. These microservices are implemented based on the AllSAT solver nbc_minisat_all-1.0.2 [26] and the QSAT solver DepQBF [27]. In the case of a high dimension of the BDS state vector, previously developed parallel solvers [28,29] of a similar purpose are used.
The first example shows a detailed computation process.
Let us consider the following controlled BDS (n=3, m=1, l=1):
System ( 5) is equivalent to the following one-step transition equation:
To check the property of 3-observability, we write down the Boolean equation of a two-step transition for the initial state
The Boolean equation 0 ~ for a two-step transition with the initial state
is written similarly. In total, expression (4) contains 26 subject variables and 82 clauses. Boolean encoding of subject variables is given in Table 1. When generating Boolean constraints by expression (4), the Plaisted-Greenbaum transform is used. When applying this transformation, two additional variables are introduced. These variables are coded as 27 and 28.
The expression (4) in QDIMACS format is given in Figure 2. The QBFTV (QBF True Verification) service developed based on the QSAT-solver DepQBF for the quantified Boolean formula (4) returns a message that this formula is TRUE, which means the feasibility of the 3-observability property for system (5). The QBFTV service interface is shown in Figure 3. The QBF in QDIMACS format is used as the input file. The execution result can be viewed on the "Results" tab.
Let us consider the Boolean model of the controlled system from [19] (n=10, m=3, l=7):
The one-step transition equation for system (6)
To check the property of 3-observability, we write down the Boolean equation of a two-step transition (
) for the initial state
, , , ,..., , , ,..., , (
The Boolean equation 0 ~ for a two-step transition with the initial state
is written similarly. In total, expression (4) contains 100 subject variables and 230 clauses.
The QBFTV service for the quantified Boolean formula (4) gives a message that this formula is FALSE, which means that the observability property for system (6) is not satisfied.
Let us consider the Boolean model of the controlled system from [7] (n=37, m=3, l=4):
The solution to the qualitative study problem of the k-observability property of nonlinear BDS on a finite time interval is obtained using the authors' Boolean constraints method. Recently, BDS (Boolean networks) have attracted considerable attention as computational models for genetic and cellular networks. In this article, we consider observability as the feature determining the initial state of the BDS for given input and output sequences of the length k unequivocally. Based on the logic specification of the dynamic property of k-observability and the equations of dynamics of a binary system, a feasibility condition for the k-observability property is obtained in the form of a quantified Boolean formula. The verification of the truth of this formula can be performed using an efficient QSAT solver. An advantage of the developed tools for checking the k-observability property is their orientation to systems with a high dimension of the state, control, and output vectors and a long interval of discrete-time variation. The proposed method implementation allows data parallelism. So high scalability for increasing the number of variables in the Boolean constraint is provided.
The study was supported by the Ministry of Science and Higher Education of the Russian Federation, project «Technologies for the development and analysis of subject-oriented intelligent group control systems in non-deterministic distributed environments».
,..., , ~x x x is written similarly. In total, expression (4) contains 250 subject variables and 515 clauses. The QBFTV service for the quantified Boolean formula (4) gives a message that this formula is FALSE, which means that the observability property for system (7) is not satisfied.