In this work, we study the problem of statistically verifying Probabilistic Computation Tree Logic (PCTL) formulas on discrete-time Markov chains (DTMCs) with stratified and antithetic samples. We show that by properly choosing the representation of the DTMCs, semantically negatively correlated samples can be generated for a fraction of PCTL formulas via the stratified or antithetic sampling techniques. Using stratified or antithetic samples, we propose statistical verification algorithms with asymptotic correctness guarantees based on sequential probability ratio tests, and show that these algorithms are more sample-efficient than the algorithms using independent Monte Carlo sampling. Finally, the efficiency of the statistical verification algorithm with stratified and antithetic samples is demonstrated by numerical experiments on several benchmarks.

Original languageEnglish (US)
Pages (from-to)145-163
Number of pages19
JournalFormal Methods in System Design
Issue number2
StatePublished - Nov 1 2019


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

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


Dive into the research topics of 'Statistical verification of PCTL using antithetic and stratified samples'. Together they form a unique fingerprint.

Cite this