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.
Discrete approximation methods are commonly used in continuous and hybrid systems analysis (see @cite_19 for an overview regarding reachability) to handle the uncountability of the state space. Direct methods work on the original system and rely on a successor operation iteratively computing the reachable set whereas indirect methods abstract from the continuous model by a finite structure for which the analysis is simpler. Our method belongs to the latter class, since it uses numerical simulations and creates the abstraction automaton. Considering a fixed set of initial conditions, there is a certain overhead with generating states of the automaton in comparison with simple numerical simulations. However, the advantage of constructing the automaton is obtaining a global view of the dynamics. Moreover, in addition to rectangular abstraction, the automaton is augmented with weighted transitions which represent quantitative information describing volumes of subsets of initial conditions belonging to attraction basins of different parts of the phase space.
@cite_19
2110910849
Set-based reachability analysis computes all possible states a system may attain, and in this sense provides knowledge about the system with a completeness, or coverage, that a finite number of simulation runs can not deliver. Due to its inherent complexity, the application of reachability analysis has been limited so far to simple systems, both in the continuous and the hybrid domain. In this paper we present recent advances that, in combination, significantly improve this applicability, and allow us to find better balance between computational cost and accuracy. The presentation covers, in a unified manner, a variety of methods handling increasingly complex types of continuous dynamics (constant derivative, linear, nonlinear). The improvements include new geometrical objects for representing sets, new approximation schemes, and more flexible combinations of graph-search algorithm and partition refinement. We report briefly some preliminary experiments that have enabled the analysis of systems previously beyond reach.