Verifying pCTL model checking

Johannes Hölzl; Tobias Nipkow

doi:10.1007/978-3-642-28756-5_24

Verifying pCTL model checking

Johannes Hölzl
, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

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

5 Scopus citations

Abstract

Probabilistic model checkers like PRISM check the satisfiability of probabilistic CTL (pCTL) formulas against discrete-time Markov chains. We prove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings
Publisher	Springer Verlag
Pages	347-361
Number of pages	15
ISBN (Print)	9783642287558
DOIs	https://doi.org/10.1007/978-3-642-28756-5_24
State	Published - 2012
Event	18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia Duration: 24 Mar 2012 → 1 Apr 2012

Publication series

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

Conference

Conference	18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Country/Territory	Estonia
City	Tallinn
Period	24/03/12 → 1/04/12

Access to Document

10.1007/978-3-642-28756-5_24

Cite this

Hölzl, J., & Nipkow, T. (2012). Verifying pCTL model checking. In Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings (pp. 347-361). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7214 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-28756-5_24

Hölzl, Johannes ; Nipkow, Tobias. / Verifying pCTL model checking. Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings. Springer Verlag, 2012. pp. 347-361 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a02af6ae73aa480c9ab788c0be0ac41d,

title = "Verifying pCTL model checking",

abstract = "Probabilistic model checkers like PRISM check the satisfiability of probabilistic CTL (pCTL) formulas against discrete-time Markov chains. We prove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.",

author = "Johannes H{\"o}lzl and Tobias Nipkow",

year = "2012",

doi = "10.1007/978-3-642-28756-5\_24",

language = "English",

isbn = "9783642287558",

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

publisher = "Springer Verlag",

pages = "347--361",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings",

note = "18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 ; Conference date: 24-03-2012 Through 01-04-2012",

}

Hölzl, J & Nipkow, T 2012, Verifying pCTL model checking. in Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7214 LNCS, Springer Verlag, pp. 347-361, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 24/03/12. https://doi.org/10.1007/978-3-642-28756-5_24

Verifying pCTL model checking. / Hölzl, Johannes; Nipkow, Tobias.
Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings. Springer Verlag, 2012. p. 347-361 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7214 LNCS).

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

TY - GEN

T1 - Verifying pCTL model checking

AU - Hölzl, Johannes

AU - Nipkow, Tobias

PY - 2012

Y1 - 2012

N2 - Probabilistic model checkers like PRISM check the satisfiability of probabilistic CTL (pCTL) formulas against discrete-time Markov chains. We prove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.

AB - Probabilistic model checkers like PRISM check the satisfiability of probabilistic CTL (pCTL) formulas against discrete-time Markov chains. We prove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.

UR - https://www.scopus.com/pages/publications/84859356719

U2 - 10.1007/978-3-642-28756-5_24

DO - 10.1007/978-3-642-28756-5_24

M3 - Conference contribution

AN - SCOPUS:84859356719

SN - 9783642287558

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

SP - 347

EP - 361

BT - Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings

PB - Springer Verlag

T2 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012

Y2 - 24 March 2012 through 1 April 2012

ER -

Hölzl J, Nipkow T. Verifying pCTL model checking. In Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings. Springer Verlag. 2012. p. 347-361. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-28756-5_24

Verifying pCTL model checking

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this