Reachability analysis of delta-notch lateral inhibition using predicate abstraction

Abstract. This paper examines the feasibility of predicate abstraction as a method for the reachability analysis of hybrid systems. A hybrid system can be abstracted into a purely discrete system by mapping the continuous state space into an equivalent finite discrete state space using a set of Boolean predicates and a decision procedure in the theory of real closed fields. It is then possible to find the feasible transitions between these states. In this paper, we propose new conditions for predicate abstraction which greatly reduce the number of transitions in the abstract discrete system. We also develop a computational technique for reachability analysis and apply it to a biological system of interest (the Delta-Notch lateral inhibition problem).