Model Checking CSL for Markov Population Models
This work provides a complete solution for verifying CSL properties on MPMs, addressing a key bottleneck in computational biology and related fields.
The paper presents a full algorithm for model checking Continuous Stochastic Logic (CSL) on infinite-state Markov population models (MPMs), enabling analysis of properties like probabilistic reachability and survivability. Experimental results demonstrate the method's effectiveness.
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.