Model checking CSL for markov population models

David Spieler; Ernst Moritz Hahn; Lijun Zhang

doi:10.4204/EPTCS.154.7

Model checking CSL for markov population models

David Spieler, Ernst Moritz Hahn, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

9 Downloads (Pure)

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 language	English
Title of host publication	Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems
Editors	Nathalie Bertrand, Luca Bortolussi
Publisher	ArXiv.org
Pages	93-107
Number of pages	15
DOIs	https://doi.org/10.4204/EPTCS.154.7
Publication status	Published - 2014
Externally published	Yes
Event	12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014 - Grenoble, France Duration: 12 Apr 2014 → 13 Apr 2014 Conference number: 12

Publication series

Name	Electronic Proceedings in Theoretical Computer Science, EPTCS
Publisher	ArXiv
Volume	154
ISSN (Print)	2075-2180

Conference

Conference	12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014
Abbreviated title	QAPL
Country/Territory	France
City	Grenoble
Period	12/04/14 → 13/04/14

Access to Document

10.4204/EPTCS.154.7

Spieler2014modelFinal published version, 149 KB

Cite this

Spieler, D., Hahn, E. M., & Zhang, L. (2014). Model checking CSL for markov population models. In N. Bertrand, & L. Bortolussi (Eds.), Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems (pp. 93-107). (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 154). ArXiv.org. https://doi.org/10.4204/EPTCS.154.7

@inproceedings{a29581acdca04e9b8f5d85e8dbd619ae,

title = "Model checking CSL for markov population models",

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.",

author = "David Spieler and Hahn, {Ernst Moritz} and Lijun Zhang",

year = "2014",

doi = "10.4204/EPTCS.154.7",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

publisher = "ArXiv.org",

pages = "93--107",

editor = "Nathalie Bertrand and Luca Bortolussi",

booktitle = "Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems",

note = "12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, QAPL ; Conference date: 12-04-2014 Through 13-04-2014",

}

Spieler, D, Hahn, EM & Zhang, L 2014, Model checking CSL for markov population models. in N Bertrand & L Bortolussi (eds), Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems. Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 154, ArXiv.org, pp. 93-107, 12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12/04/14. https://doi.org/10.4204/EPTCS.154.7

Model checking CSL for markov population models. / Spieler, David; Hahn, Ernst Moritz; Zhang, Lijun.

Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems. ed. / Nathalie Bertrand; Luca Bortolussi. ArXiv.org, 2014. p. 93-107 (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 154).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Model checking CSL for markov population models

AU - Spieler, David

AU - Hahn, Ernst Moritz

AU - Zhang, Lijun

N1 - Conference code: 12

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84923653515&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.154.7

DO - 10.4204/EPTCS.154.7

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 93

EP - 107

BT - Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems

A2 - Bertrand, Nathalie

A2 - Bortolussi, Luca

PB - ArXiv.org

T2 - 12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014

Y2 - 12 April 2014 through 13 April 2014

ER -

Model checking CSL for markov population models

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this