Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KŘETÍNSKÝ Jan

Year of publication 2016
Type Article in Proceedings
Conference Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-47166-2_3
Field Informatics
Keywords verification; statistical model checking; probabilistic systems
Description We survey statistical verification techniques aiming at linear properties with unbounded or infinite horizon, as opposed to properties of runs of fixed length. We discuss statistical model checking of Markov chains and Markov decision processes against reachability, unbounded-until, LTL and mean-payoff properties. Moreover, the respective strategies can be represented efficiently using statistical techniques. Further, we also discuss when it is possible to statistically estimate linear distances between Markov chains.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.