In this paper a novel computational technique for finite discrete approximation of continuous dynamical systems suitable for a significant class of biochemical dynamical systems is introduced. The method is parameterized in order to affect the imposed level of approximation provided that with increasing parameter value the approximation converges to the original continuous system. By employing this approximation technique, we present algorithms solving the reachability problem for biochemical dynamical systems. The presented method and algorithms are evaluated on several exemplary biological models and on a real case study. This is a full version of the paper published in the proceedings of CompMod 2011.
An indirect method based on rectangular abstraction automaton making the finite quotient of the continuous state space has been employed, e.g., in @cite_24 @cite_29 @cite_18 . In general, these methods rely on results @cite_5 @cite_22 and are applicable to (piece-wise) affine or (piece-wise) multi-affine systems. Although not addressed formally in this paper, our technique can be considered as a refinement of @cite_24 . However, we focus on obtaining satisfactory approximate results eliminating the extent of spurious behaviour coming from conservativeness of rectangular abstraction. Our technique can be employed for the recognition of spurious behaviour of the rectangular abstraction transition system.
@cite_18 @cite_22 @cite_29 @cite_24 @cite_5
2049491928 2147970103 2171042116 2114578185
We use hybrid-systems techniques for the analysis of reachability properties of a class of piecewise-affine (PA) differential equations that are particularly suitable for the modeling of genetic regulatory networks. More specifically, we introduce a hyperrectangular partition of the state space that forms the basis for a discrete abstraction preserving the sign of the derivatives of the state variables. The resulting discrete transition system provides a qualitative description of the network dynamics that is well-adapted to available experimental data and that can be efficiently computed in a symbolic manner from inequality constraints on the parameters. Given an affine system on a full-dimensional polytope, the problem of reaching a particular facet of the polytope, using continuous piecewise-affine state feedback is studied. Necessary conditions and sufficient conditions for the existence of a solution are derived in terms of linear inequalities on the input vectors at the vertices of the polytope. Special attention is paid to affine systems on full-dimensional simplices. In this case, the necessary and sufficient conditions are equivalent and a constructive procedure yields an affine feedback control law, that solves the reachability problem under consideration. We propose an abstraction method for medium-scale biomolecular networks, based on hybrid dynamical systems with continuous multi-affine dynamics. This abstraction method follows naturally from the notion of approximating nonlinear rate laws with continuous piecewise linear functions and can be easily automated. An efficient reachability algorithm is possible for the resulting class of hybrid systems. An efficient reachability algorithm is possible for the resulting class of hybrid systems. An approximation for an ordinary differential equation model of the lac operon is constructed, and it is shown that the abstraction passes the same experimental tests as were used to validate the original model. The well studied biological system exhibits bistability and switching behaviour, arising from positive feedback in the expression mechanism of the lac operon. The switching property of the lac system is an example of the major qualitative features that are the building blocks of higher level, more coarse-grained descriptions. The present approach is useful in helping to correctly identify such properties and in connecting them to the underlying molecular dynamical details. Reachability analysis together with the knowledge of the steady-state structure are used to identify ranges of parameter values for which the system maintains the bistable switching property. In this paper, we focus on a particular class of nonlinear affine control systems of the form xdot=f(x)+Bu, where the drift f is a multi-affine vector field (i.e., affine in each state component), the control distribution B is constant, and the control u is constrained to a convex set. For such a system, we first derive necessary and sufficient conditions for the existence of a multiaffine feedback control law keeping the system in a rectangular invariant. We then derive sufficient conditions for driving all initial states in a rectangle through a desired facet in finite time. If the control constraints are polyhedral, we show that all these conditions translate to checking the feasibility of systems of linear inequalities to be satisfied by the control at the vertices of the state rectangle. This work is motivated by the need to construct discrete abstractions for continuous and hybrid systems, in which analysis and control tasks specified in terms of reachability of sets of states can be reduced to searches on finite graphs. We show the application of our results to the problem of controlling the angular velocity of an aircraft with gas jet actuators