logo              Stochastic Models:
Scalable Model Checking.
Home Members Meetings Tasks Publications Bibliography

Project Blanc ANR-13-BS02-0011-01 [2014-2018]

  • Aim: develop scalable model checking techniques that can handle large stochastic systems.
    Large stochastic systems arise naturally in many different contexts: from networks to system biology.

  • Application: we will demonstrate the techniques on two stochastic biomodels:
    A model for Hela cells death and a model of stress response in yeast.

  • Technique: approximate the system, monitor the accuracy of the approximation, and decide whether to recompute with a better accuracy according to the interval of behaviors obtained.
  • proto

  • Context:Model Checking is a mature field of research (Turing award in 2007).
    It consists in describing formally a system in the form of a mathematical model, specifying the properties it has to fulfill in a formal logic, and providing algorithms to decide whether the model satisfies the property.

    Model checking started with Boolean systems and properties (sequential finite state models...).
    To handle large realistic systems: use abstraction
    CEGAR counter example guided abstraction refinement
    Abstract interpretation from Cousot et al.

    Work extremely well for verifying (large, sequential) programs with Boolean predicates (x\leq a).

  • State of the Art: Current abstraction techniques are not suited to the verification of large stochastic systems. To verify large stochastic systems, techniques such as Statistical Model Checking (based on Monte Carlo property testing) can be used. However, the latter do not give sure answers, but only answers correct up to some confidence level. To date, there is no (sure) Model Checking method which scales to large stochastic systems (e.g. Markov Chains with 10^20 states and over, for instance 20 variables which can take 10 different values each). For instance, the PRISM model checker and other comparable tools scale up to 10^10 states.