Reachability algorithm for biological piecewise-affine hybrid systems

We consider a class of qualitative biological models which describe species (e.g. protein) interactions in terms of promotion or inhibition, from which a piecewise-affine (PWA) hybrid system model can be generated. These models have a special structure under which negative feedback is a necessary condition for the presence of limit cycles, centers, and foci. We describe modifications to reachability algorithms to take advantage of this special structure, and we give conditions on the qualitative model for termination of the algorithm. An example of applying the algorithm to a simple biological system is given.