×

Automated symbolic reachability analysis; with application to Delta-Notch signaling automata. (English) Zbl 1032.92500

Maler, Oded (ed.) et al., Hybrid systems: Computation and control. 6th international workshop, HSCC 2003, Prague, Czech Republic, April 3-5, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2623, 233-248 (2003).
Summary: This paper describes the implementation of predicate abstraction techniques to automatically compute symbolic backward reachable sets of high dimensional piecewise affine hybrid automata, used to model Delta-Notch biological cell signaling networks. These automata are analyzed by creating an abstraction of the hybrid model, which is a finite state discrete transition system, and then performing the computation on the abstracted system. All the steps, from model generation to the simplification of the reachable set, have been automated using a variety of decision procedure and theorem-proving tools. The concluding example computes the reach set for a four cell network with 8 continuous and 256 discrete states. This demonstrates the feasibility of using these tools to compute on high dimensional hybrid automata, to provide deeper insight into realistic biological systems.
For the entire collection see [Zbl 1017.00053].

MSC:

92B05 General biology and biomathematics
93A30 Mathematical modelling of systems (MSC2010)

Software:

HyTech
PDFBibTeX XMLCite
Full Text: Link