Statistical model checking: Challenges and perspectives

Axel Legay, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review


Statistical model checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows us to handle requirements that cannot be expressed in classical temporal logics. The approach has been implemented in several toolsets, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. The objectives of this special issue are (1) to survey existing results on SMC, (2) to propose SMC algorithms for a larger class of systems, and (3) to show the applicability of SMC to new emerging applications.

Original languageEnglish (US)
Article numberA011
Pages (from-to)369-376
Number of pages8
JournalInternational Journal on Software Tools for Technology Transfer
Issue number4
StatePublished - Aug 1 2015


  • Overview
  • Quantities statistical model checking

ASJC Scopus subject areas

  • Software
  • Information Systems


Dive into the research topics of 'Statistical model checking: Challenges and perspectives'. Together they form a unique fingerprint.

Cite this