Statistical model checking for rule-based models in the Kappa language

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 talk, 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 framework is illustrated on representative case studies from systems biology and swarm robotics. This work is done in collaboration with Jérôme Feret (ENS-Paris) and Tatjana Petrov (U. Trieste).