Open Systems Laboratory at Illinois

On statistical model checking of stochastic systems

By Koushik Sen, Mahesh Viswanathan, and Gul Agha. In CAV, volume 3576 of Lecture Notes in Computer Science, 266–280. Springer, 2005.

Full Text:
Download PDF
Publisher Link:


Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operator and unbounded until formulas. In this paper, we present a statistical model checking algorithm that also verifies CSL formulas with unbounded untils. The algorithm is based on Monte Carlo simulation of the model and hypothesis testing of the samples, as opposed to sequential hypothesis testing. We have implemented the algorithm in a tool called VESTA, and found it to be effective in verifying several examples.


    author = "Sen, Koushik and Viswanathan, Mahesh and Agha, Gul",
    editor = "Etessami, Kousha and Rajamani, Sriram K.",
    title = "On Statistical Model Checking of Stochastic Systems",
    booktitle = "CAV",
    crossref = "conf/cav/2005",
    ee = "",
    keywords = "formal methods",
    pages = "266-280",
    year = "2005",

    editor = "Etessami, Kousha and Rajamani, Sriram K.",
    title = "Computer Aided Verification, 17th International
             Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005,
    isbn = "3-540-27231-3",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "3576",
    year = "2005",