Open Systems Laboratory at Illinois

Statistical model checking of black-box probabilistic systems

By Koushik Sen, Mahesh Viswanathan, and Gul Agha. In CAV, volume 3114 of Lecture Notes in Computer Science, 202–215. Springer, 2004.

Full Text:
Download PDF
Publisher Link:


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.


    author = "Sen, Koushik and Viswanathan, Mahesh and Agha, Gul",
    editor = "Alur, Rajeev and Peled, Doron",
    title = "Statistical Model Checking of Black-Box Probabilistic
    booktitle = "CAV",
    crossref = "conf/cav/2004",
    ee = "",
    keywords = "formal methods, sensor networks, real-time systems",
    pages = "202-215",
    year = "2004",

    editor = "Alur, Rajeev and Peled, Doron",
    title = "Computer Aided Verification, 16th International
             Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004,
    isbn = "3-540-22342-8",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "3114",
    year = "2004",