Model checking CSL for markov population models

David Spieler, Ernst Moritz Hahn, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems
EditorsNathalie Bertrand, Luca Bortolussi
PublisherArXiv
Pages93-107
Number of pages15
DOIs
Publication statusPublished - 2014
Externally publishedYes
Event12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014 - Grenoble, France
Duration: 12 Apr 201413 Apr 2014
Conference number: 12

Publication series

NameElectronic Proceedings in Theoretical Computer Science, EPTCS
PublisherArXiv
Volume154
ISSN (Print)2075-2180

Conference

Conference12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014
Abbreviated titleQAPL
CountryFrance
CityGrenoble
Period12/04/1413/04/14

Fingerprint Dive into the research topics of 'Model checking CSL for markov population models'. Together they form a unique fingerprint.

Cite this