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 allow-
ing 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).