Abstract

is a statistical model checker that uses antithetic and stratified sampling techniques to reduce the number of samples and, hence, the amount of time required before making a decision. The tool is capable of statistically verifying any black-box probabilistic system thatcan simulate, against probabilistic bounds on any property thatcan evaluate over individual executions of the system. We have evaluated our tool on many examples and compared it with both symbolic and statistical algorithms. When the number of strata is large, our algorithms reduced the number of samples more than 3 times on average. Furthermore, being a statistical model checker makesable to verify models that are well beyond the reach of current symbolic model checkers. On large systems (up to states)was able to check 100% of benchmark systems, compared to existing symbolic methods in, which only succeeded on 13% of systems. The tool, installation instructions, benchmarks, and scripts for running the benchmarks are all available online as open source.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
EditorsShuvendu K. Lahiri, Chao Wang
PublisherSpringer
Pages448-460
Number of pages13
ISBN (Print)9783030532901
DOIs
StatePublished - 2020
Event32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States
Duration: Jul 21 2020Jul 24 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12225 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference32nd International Conference on Computer Aided Verification, CAV 2020
CountryUnited States
CityLos Angeles
Period7/21/207/24/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'STMC: Statistical Model Checker with Stratified and Antithetic Sampling'. Together they form a unique fingerprint.

Cite this