Statistical Verification of PCTL Using Stratified Samples

Yu Wang; Nima Roohi; Matthew West; Mahesh Viswanathan; Geir E. Dullerud

doi:10.1016/j.ifacol.2018.08.015

Statistical Verification of PCTL Using Stratified Samples

Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, Geir E. Dullerud

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English (US)
Pages (from-to)	85-90
Number of pages	6
Journal	6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018: Oxford, United Kingdom, 11—13 July 2018
Volume	51
Issue number	16
DOIs	https://doi.org/10.1016/j.ifacol.2018.08.015
State	Published - Jan 1 2018

Keywords

Markov chains
PRISM
Sequential probability ratio test
Temporal logic
Variance reduction

ASJC Scopus subject areas

Control and Systems Engineering

Online availability

10.1016/j.ifacol.2018.08.015

Library availability

Discover UIUC Full Text

Cite this

@article{da49b70a86a14da29e671a3b2614b5bf,

title = "Statistical Verification of PCTL Using Stratified Samples",

abstract = "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.",

keywords = "Markov chains, PRISM, Sequential probability ratio test, Temporal logic, Variance reduction",

author = "Yu Wang and Nima Roohi and Matthew West and Mahesh Viswanathan and Dullerud, {Geir E.}",

note = "Publisher Copyright: {\textcopyright} 2018",

year = "2018",

month = jan,

day = "1",

doi = "10.1016/j.ifacol.2018.08.015",

language = "English (US)",

volume = "51",

pages = "85--90",

journal = "6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018: Oxford, United Kingdom, 11—13 July 2018",

issn = "2405-8963",

number = "16",

}

TY - JOUR

T1 - Statistical Verification of PCTL Using Stratified Samples

AU - Wang, Yu

AU - Roohi, Nima

AU - West, Matthew

AU - Viswanathan, Mahesh

AU - Dullerud, Geir E.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

KW - Markov chains

KW - PRISM

KW - Sequential probability ratio test

KW - Temporal logic

KW - Variance reduction

UR - http://www.scopus.com/inward/record.url?scp=85052646695&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85052646695&partnerID=8YFLogxK

U2 - 10.1016/j.ifacol.2018.08.015

DO - 10.1016/j.ifacol.2018.08.015

M3 - Article

AN - SCOPUS:85052646695

SN - 2405-8963

VL - 51

SP - 85

EP - 90

JO - 6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018: Oxford, United Kingdom, 11—13 July 2018

JF - 6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018: Oxford, United Kingdom, 11—13 July 2018

IS - 16

ER -

Statistical Verification of PCTL Using Stratified Samples

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this