Statistical model checking of black-box probabilistic systems

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numerical and statistical analysis methods, we assume that the system under investigation is an unknown, deployed black-box that can be passively observed to obtain sample traces, but cannot be controlled. Given a set of executions (obtained by Monte Carlo simulation) and a property, our algorithm checks, based on statistical hypothesis testing, whether the sample provides evidence to conclude the satisfaction or violation of a property, and computes a quantitative measure (p-value of the tests) of confidence in its answer; if the sample does not provide statistical evidence to conclude the satisfaction or violation of the property, the algorithm may respond with a "don't know" answer. We implemented our algorithm in a Java-based prototype tool called VESTA, and experimented with the tool using case studies analyzed in [15]. Our empirical results show that our approach may, at least in some cases, be faster than previous analysis methods.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRajeev Alur, Doron A. Peled
PublisherSpringer-Verlag Berlin Heidelberg
Pages202-215
Number of pages14
ISBN (Print)3540223428, 9783540223429
DOIs
StatePublished - Jan 1 2004

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Statistical model checking of black-box probabilistic systems'. Together they form a unique fingerprint.

  • Cite this

    Sen, K., Viswanathan, M., & Agha, G. (2004). Statistical model checking of black-box probabilistic systems. In R. Alur, & D. A. Peled (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 202-215). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3114). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_16