Statistical model checking for unbounded until formulas

Nima Roohi, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review

Abstract

Statistical model checking of unbounded time properties is challenging, because it requires an algorithm to estimate the measure of paths satisfying an unbounded until property from samples of finite length paths. In this paper, we survey all proposed algorithms for this problem, and critically evaluate them.

Original languageEnglish (US)
Article numberA008
Pages (from-to)417-427
Number of pages11
JournalInternational Journal on Software Tools for Technology Transfer
Volume17
Issue number4
DOIs
StatePublished - Aug 2015

Keywords

  • PCTL
  • Statistical model checking
  • Unbounded until

ASJC Scopus subject areas

  • Software
  • Information Systems

Cite this