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.
CITATION STYLE
Křetínský, J. (2016). Survey of statistical verification of linear unbounded properties: Model checking and distances. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9952 LNCS, pp. 27–45). Springer Verlag. https://doi.org/10.1007/978-3-319-47166-2_3
Mendeley helps you to discover research relevant for your work.