Skip to main navigation Skip to search Skip to main content

Bayesian Statistical Model-Checking for Complex Stochastic Systems

  • Jia He
  • , Min Zhang
  • , Kangli He
  • , Yannan Guo
  • , Yusi Lei
  • East China Normal University

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Probabilistic Model-Checking is a standard approach for automatically verifying stochastic systems. However, it becomes expensive or even intractable for classic approaches to verify complex systems. Statistical model-checking was proposed to overcome this limitation. In this paper, we propose a novel statistical model-checking approach which is based on Bayesian point estimation. Together with the Bayesian point estimation and a given conjugate prior distribution, we are able to predict the upper bound of sample size before sampling. We implement our techniques in a tool. Experiential results show that our approach is competitive, even better than other standard approaches in several cases.

Original languageEnglish
Title of host publicationProceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages38-41
Number of pages4
ISBN (Electronic)9781509017638
DOIs
StatePublished - 10 Aug 2016
Event10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 - Shanghai, China
Duration: 17 Jul 201619 Jul 2016

Publication series

NameProceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016

Conference

Conference10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
Country/TerritoryChina
CityShanghai
Period17/07/1619/07/16

Keywords

  • Bayesian Point Estimation
  • Complex Stochastic Systems
  • Conjugate Prior
  • Statistical Model-Checking

Fingerprint

Dive into the research topics of 'Bayesian Statistical Model-Checking for Complex Stochastic Systems'. Together they form a unique fingerprint.

Cite this