Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata

Abstract. 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 yzed by creating an abstraction of the hybrid model, which is a finite state discrete transition system, and then performing the compun 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.

• Type: Conference
• Year: 2003
• Where: HYBRID
• Authors: Ronojoy Ghosh, Ashish Tiwari, Claire Tomlin
• Keywords: Affine Hybrid Automata, HYBRID 2003, Hybrid Automata, Hybrid Systems, Reachable Set