Sciweavers

Share
IANDC
2006

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

9 years 5 months ago
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 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. Key words: Probabilistic verification, Stochastic processes, Temporal logic, Hypothesis testing, Acceptance sampling, Transient analysis
Håkan L. S. Younes, Reid G. Simmons
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where IANDC
Authors Håkan L. S. Younes, Reid G. Simmons
Comments (0)
books