Statistical probabilistic model checking with a focus on time-bounded properties

Probabilistic verification of continuous-time stochastic processes has received increasing attention in the model-checking community in the past five years, with a clear focus on developing numerical solution methods for model checking of continuous-time Markov chains. Numerical techniques tend to s...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2006-09, Vol.204 (9), p.1368-1409
Main Authors: Younes, Håkan L.S., Simmons, Reid G.
Format: Article
Language:English
Subjects:
Acceptance sampling
Exact sciences and technology
General logic
Hypothesis testing
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Numerical analysis
Numerical analysis. Scientific computation
Numerical methods in probability and statistics
Probabilistic verification
Probability and statistics
Probability theory and stochastic processes
Sampling theory, sample surveys
Sciences and techniques of general use
Statistics
Stochastic processes
Temporal logic
Transient analysis
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Probabilistic verification of continuous-time stochastic processes has received increasing attention in the model-checking community in the past five years, with a clear focus on developing numerical solution methods for model checking of continuous-time Markov chains. Numerical techniques tend to scale poorly with an increase in the size of the model (the “state space explosion problem”), however, and are feasible only for restricted classes of stochastic discrete-event systems. We present a statistical approach to probabilistic model checking, employing hypothesis testing and discrete-event simulation. Since we rely on statistical hypothesis testing, we cannot guarantee that the verification result is correct, but we can at least bound the probability of generating an incorrect answer to a verification problem.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2006.05.002