In this work, we propose a stratified sampling method to statistically check Probabilistic Computation Tree Logic (PCTL) formulas on discrete-time Markov chains with sequential probability ratio test. Distinct from previous statistical verification methods using independent Monte Carlo sampling, our algorithm uses stratified samples that are negatively correlated, thus give lower variance. The experiments demonstrate that the new algorithm uses a smaller number of samples for a given confidence level on several benchmark examples.

Original languageEnglish (US)
Pages (from-to)85-90
Number of pages6
Journal6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018: Oxford, United Kingdom, 11—13 July 2018
Issue number16
StatePublished - Jan 1 2018


  • Markov chains
  • Sequential probability ratio test
  • Temporal logic
  • Variance reduction

ASJC Scopus subject areas

  • Control and Systems Engineering


Dive into the research topics of 'Statistical Verification of PCTL Using Stratified Samples'. Together they form a unique fingerprint.

Cite this