Algebraic Model Checking II: Decidability of Semi-Algebraic Model Checking and its Applications to Systems Biology

Motivated by applications to systems biology, and the emergence of semi-algebraic hybrid systems as a natural framework for modeling biochemical networks, we continue exploring the decidability problem for model-checking with TCTL (Timed Computation Tree Logic) over this broad class of semi-algebraic hybrid systems. Previously, we had introduced these models, demonstrated the close connection to the goals of systems biology. However, we had only developed the techniques for bounded reachability, arguing for the adequacy of such an approach in a majority of the biological applications. Here, we present a semi-decidable symbolic algebraic dense-time TCTL model checking algorithm, which satisfies two desirable properties: it can be derived automatically from the symbolic description, and it extends to and generalizes other versions of temporal logics. The main mathematical device at the core of this approach is Tarski-Collins' real quantifier elimination employed at each fixpoint iteration, whose high complexity is the crux of its unfortunate limitation. Along with these results, we prove the undecidability of this problem in the more powerful "real" Turing machine formalism of Blum, Shub and Smale. We then demonstrate a preliminary version of our model-checker Tolque on the Delta-Notch example.