Model checking algorithms for CTMDPs

Peter Buchholz; Ernst Moritz Hahn; Holger Hermanns; Lijun Zhang

doi:10.1007/978-3-642-22110-1_19

Model checking algorithms for CTMDPs

Peter Buchholz^*, Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang

^*Corresponding author for this work

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

27 Citations (Scopus)

Abstract

Continuous Stochastic Logic (CSL) can be interpreted over continuous-time Markov decision processes (CTMDPs) to specify quantitative properties of stochastic systems that allow some external control. Model checking CSL formulae over CTMDPs requires then the computation of optimal control strategies to prove or disprove a formula. The paper presents a conservative extension of CSL over CTMDPs - with rewards - and exploits established results for CTMDPs for model checking CSL. A new numerical approach based on uniformization is devised to compute time bounded reachability results for time dependent control strategies. Experimental evidence is given showing the efficiency of the approach.

Original language	English
Title of host publication	Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Pages	225-242
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-642-22110-1_19
Publication status	Published - 2011
Externally published	Yes
Event	23rd International Conference on Computer Aided Verification, CAV 2011 - Snowbird, UT, United States Duration: 14 Jul 2011 → 20 Jul 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6806 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International Conference on Computer Aided Verification, CAV 2011
Country	United States
City	Snowbird, UT
Period	14/07/11 → 20/07/11

Access to Document

10.1007/978-3-642-22110-1_19

Link to publication in Scopus

Fingerprint Dive into the research topics of 'Model checking algorithms for CTMDPs'. Together they form a unique fingerprint.

Cite this

Buchholz, P., Hahn, E. M., Hermanns, H., & Zhang, L. (2011). Model checking algorithms for CTMDPs. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings (pp. 225-242). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6806 LNCS). https://doi.org/10.1007/978-3-642-22110-1_19

@inproceedings{a7b14baa516a44179a1759f32164fa57,

title = "Model checking algorithms for CTMDPs",

abstract = "Continuous Stochastic Logic (CSL) can be interpreted over continuous-time Markov decision processes (CTMDPs) to specify quantitative properties of stochastic systems that allow some external control. Model checking CSL formulae over CTMDPs requires then the computation of optimal control strategies to prove or disprove a formula. The paper presents a conservative extension of CSL over CTMDPs - with rewards - and exploits established results for CTMDPs for model checking CSL. A new numerical approach based on uniformization is devised to compute time bounded reachability results for time dependent control strategies. Experimental evidence is given showing the efficiency of the approach.",

author = "Peter Buchholz and Hahn, {Ernst Moritz} and Holger Hermanns and Lijun Zhang",

year = "2011",

doi = "10.1007/978-3-642-22110-1_19",

language = "English",

isbn = "9783642221095",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "225--242",

booktitle = "Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings",

note = "23rd International Conference on Computer Aided Verification, CAV 2011 ; Conference date: 14-07-2011 Through 20-07-2011",

}

Buchholz, P, Hahn, EM, Hermanns, H & Zhang, L 2011, Model checking algorithms for CTMDPs. in Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6806 LNCS, pp. 225-242, 23rd International Conference on Computer Aided Verification, CAV 2011, Snowbird, UT, United States, 14/07/11. https://doi.org/10.1007/978-3-642-22110-1_19

Model checking algorithms for CTMDPs. / Buchholz, Peter; Hahn, Ernst Moritz; Hermanns, Holger; Zhang, Lijun.

Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. 2011. p. 225-242 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6806 LNCS).

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

TY - GEN

T1 - Model checking algorithms for CTMDPs

AU - Buchholz, Peter

AU - Hahn, Ernst Moritz

AU - Hermanns, Holger

AU - Zhang, Lijun

PY - 2011

Y1 - 2011

N2 - Continuous Stochastic Logic (CSL) can be interpreted over continuous-time Markov decision processes (CTMDPs) to specify quantitative properties of stochastic systems that allow some external control. Model checking CSL formulae over CTMDPs requires then the computation of optimal control strategies to prove or disprove a formula. The paper presents a conservative extension of CSL over CTMDPs - with rewards - and exploits established results for CTMDPs for model checking CSL. A new numerical approach based on uniformization is devised to compute time bounded reachability results for time dependent control strategies. Experimental evidence is given showing the efficiency of the approach.

AB - Continuous Stochastic Logic (CSL) can be interpreted over continuous-time Markov decision processes (CTMDPs) to specify quantitative properties of stochastic systems that allow some external control. Model checking CSL formulae over CTMDPs requires then the computation of optimal control strategies to prove or disprove a formula. The paper presents a conservative extension of CSL over CTMDPs - with rewards - and exploits established results for CTMDPs for model checking CSL. A new numerical approach based on uniformization is devised to compute time bounded reachability results for time dependent control strategies. Experimental evidence is given showing the efficiency of the approach.

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

U2 - 10.1007/978-3-642-22110-1_19

DO - 10.1007/978-3-642-22110-1_19

M3 - Conference contribution

AN - SCOPUS:79960344528

SN - 9783642221095

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 225

EP - 242

BT - Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings

T2 - 23rd International Conference on Computer Aided Verification, CAV 2011

Y2 - 14 July 2011 through 20 July 2011

ER -