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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Ghosh, R., Tiwari, A., & Tomlin, C. (2003). Automated symbolic reachability analysis; with application to delta-notch signaling automata. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2623, 233–248. https://doi.org/10.1007/3-540-36580-x_19
Mendeley helps you to discover research relevant for your work.