about this paperpresentation abstract bibitemdownloadseditor link (TBA) extended version on HAL |
Jérôme Feret and Rebecca Ghidini.
Reachability Analysis for Parametric Rule-Based Models.
Abstract:
Kappa is a graph-rewriting language originally developed for modeling molecular interactions in cellular processes. A key feature of Kappa models is that, inspired by organic chemistry, interaction rules operate on patterns i.e., partially specified molecular species, thus allowing compact descriptions of otherwise large or even infinite models.
In this paper, we propose and implement a framework for statistical model checking for stochastic Kappa models against properties written in bounded linear temporal logic (BLTL). A key feature of our approach is that temporal properties operate over Kappa patterns, making the specification language native to Kappa and avoiding the expensive and sometimes theoretically impossible—translation of the model into an equivalent chemical reaction network with a finite number of species. Concretely, given a Kappa model and a property, we first instrument the model by introducing additional variables and observables that track the truth value of each atomic proposition. For each simulated trace, the BLTL formula satisfaction is evaluated using an offline monitoring procedure. Finally, the satisfaction probability is statistically estimated from repeated model simulations.
The proposed model checking framework enables a systematic explo- ration of behavioral properties of Kappa models, that is computationally efficient while able to capture stochastic and finite size effects with any predefined desired accuracy/precision. As such, it can serve in applica- tions for e.g. model selection, property-driven parameter exploration, or robustness analysis. The framework is illustrated on representative case studies from systems biology and swarm robotics.
BibitemTBA