Survey of statistical verification of linear unbounded properties: Model checking and distances

Jan Křetínský

doi:10.1007/978-3-319-47166-2_3

Survey of statistical verification of linear unbounded properties: Model checking and distances

Jan Křetínský

Informatics 7 - Associate Professorship of Formal Methods for Software Reliability

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

9 Scopus citations

Abstract

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.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publication	Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer Verlag
Pages	27-45
Number of pages	19
ISBN (Print)	9783319471655
DOIs	https://doi.org/10.1007/978-3-319-47166-2_3
State	Published - 2016
Event	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Imperial, Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9952 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Country/Territory	Greece
City	Imperial, Corfu
Period	10/10/16 → 14/10/16

Access to Document

10.1007/978-3-319-47166-2_3

Cite this

Křetínský, J. (2016). Survey of statistical verification of linear unbounded properties: Model checking and distances. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings (pp. 27-45). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9952 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-47166-2_3

Křetínský, Jan. / Survey of statistical verification of linear unbounded properties : Model checking and distances. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer Verlag, 2016. pp. 27-45 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{706c5843e6b0473b8825fcd04e10209e,

title = "Survey of statistical verification of linear unbounded properties: Model checking and distances",

abstract = "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.",

author = "Jan K{\v r}et{\'i}nsk{\'y}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

year = "2016",

doi = "10.1007/978-3-319-47166-2_3",

language = "English",

isbn = "9783319471655",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "27--45",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

}

Křetínský, J 2016, Survey of statistical verification of linear unbounded properties: Model checking and distances. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9952 LNCS, Springer Verlag, pp. 27-45, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, Imperial, Corfu, Greece, 10/10/16. https://doi.org/10.1007/978-3-319-47166-2_3

Survey of statistical verification of linear unbounded properties: Model checking and distances. / Křetínský, Jan.
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer Verlag, 2016. p. 27-45 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9952 LNCS).

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

TY - GEN

T1 - Survey of statistical verification of linear unbounded properties

T2 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016

AU - Křetínský, Jan

N1 - Publisher Copyright: © Springer International Publishing AG 2016.

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84994027714&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-47166-2_3

DO - 10.1007/978-3-319-47166-2_3

M3 - Conference contribution

AN - SCOPUS:84994027714

SN - 9783319471655

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 27

EP - 45

BT - Leveraging Applications of Formal Methods, Verification and Validation

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Verlag

Y2 - 10 October 2016 through 14 October 2016

ER -

Křetínský J. Survey of statistical verification of linear unbounded properties: Model checking and distances. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Springer Verlag. 2016. p. 27-45. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-47166-2_3

Survey of statistical verification of linear unbounded properties: Model checking and distances

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this