Sciweavers

Share
HYBRID
2003
Springer

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

9 years 18 days ago
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.
Ronojoy Ghosh, Ashish Tiwari, Claire Tomlin
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where HYBRID
Authors Ronojoy Ghosh, Ashish Tiwari, Claire Tomlin
Comments (0)
books