Model Checking CSL for Markov Population Models

TL;DR

This paper introduces a comprehensive algorithm for model checking CSL properties in Markov population models, enabling analysis of complex biological measures despite the models' infinite state spaces.

Contribution

It presents the first complete algorithm for CSL model checking in MPMs, expanding the scope of properties that can be analyzed.

Findings

Algorithm effectively verifies CSL properties in MPMs

Experimental results demonstrate practical applicability

Enables analysis of biological measures like reachability and oscillations

Abstract

Markov population models (MPMs) are a widely used modelling formalism in the area of computational biology and related areas. The semantics of a MPM is an infinite-state continuous-time Markov chain. In this paper, we use the established continuous stochastic logic (CSL) to express properties of Markov population models. This allows us to express important measures of biological systems, such as probabilistic reachability, survivability, oscillations, switching times between attractor regions, and various others. Because of the infinite state space, available analysis techniques only apply to a very restricted subset of CSL properties. We present a full algorithm for model checking CSL for MPMs, and provide experimental evidence showing that our method is effective.