FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals

Radu Constantin Calinescu; Kenneth Harold Anthony Johnson; Colin Alexander Paterson

FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals

Radu Constantin Calinescu, Kenneth Harold Anthony Johnson, Colin Alexander Paterson

Computer Science

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

Abstract

We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016
Publisher	Springer
Pages	540-546
Number of pages	7
ISBN (Print)	9783662496749
Publication status	Published - 2016

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Publisher	Springer, Berlin, Heidelberg
Volume	9636

Bibliographical note

© Springer-Verlag Berlin Heidelberg, 2016. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

Access to Document

tacas2016-camera-ready
© Springer-Verlag Berlin Heidelberg, 2016. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details
Accepted author manuscript, 486 KB

Cite this

@inproceedings{457c371e1a05428cb11410b4ea0fef38,

title = "FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals",

abstract = "We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.",

author = "Calinescu, {Radu Constantin} and Johnson, {Kenneth Harold Anthony} and Paterson, {Colin Alexander}",

note = "{\textcopyright} Springer-Verlag Berlin Heidelberg, 2016. This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details",

year = "2016",

language = "English",

isbn = "9783662496749",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "540--546",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016",

address = "Germany",

}

FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. / Calinescu, Radu Constantin ; Johnson, Kenneth Harold Anthony ; Paterson, Colin Alexander.
Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016. Springer, 2016. p. 540-546 (Lecture Notes in Computer Science (LNCS); Vol. 9636).

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

TY - GEN

T1 - FACT

T2 - A Probabilistic Model Checker for Formal Verification with Confidence Intervals

AU - Calinescu, Radu Constantin

AU - Johnson, Kenneth Harold Anthony

AU - Paterson, Colin Alexander

N1 - © Springer-Verlag Berlin Heidelberg, 2016. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

PY - 2016

Y1 - 2016

N2 - We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.

AB - We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.

UR - http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_32

M3 - Conference contribution

SN - 9783662496749

T3 - Lecture Notes in Computer Science (LNCS)

SP - 540

EP - 546

BT - Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016

PB - Springer

ER -

FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals

Abstract

Publication series

Bibliographical note

Access to Document

Other files and links

Cite this