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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

KŘETÍNSKÝ Jan

Rok publikování 2016
Druh Článek ve sborníku
Konference Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-47166-2_3
Obor Informatika
Klíčová slova verification; statistical model checking; probabilistic systems
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.