Statistical model checking for unbounded until formulas

Nima Roohi, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review


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
Issue number4
StatePublished - Aug 2015


  • PCTL
  • Statistical model checking
  • Unbounded until

ASJC Scopus subject areas

  • Software
  • Information Systems

Cite this