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.
CITATION STYLE
Calinescu, R., Johnson, K., & Paterson, C. (2016). FACT: A probabilistic model checker for formal verification with confidence intervals. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 540–546). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_32
Mendeley helps you to discover research relevant for your work.