Title
Numerical vs. statistical probabilistic model checking
Abstract
Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare the two solution techniques when applied to the verification of time-bounded until formulae in the temporal stochastic logic CSL, both theoretically and through empirical evaluation on a set of case studies. Our study differs from most previous comparisons of numerical and statistical approaches in that CSL model checking is a hypothesis-testing problem rather than a parameter-estimation problem. We can therefore rely on highly efficient sequential acceptance sampling tests, which enables statistical solution techniques to quickly return a result with some uncertainty. We also propose a novel combination of the two solution techniques for verifying CSL queries with nested probabilistic operators.
Year
DOI
Venue
2006
10.1007/s10009-005-0187-8
STTT
Keywords
Field
DocType
dis- crete event simulation,temporal logic,statistical solution technique,hypothesis testing,numerical analysis,hypothesis-testing problem,statistical technique,transient analysis,parameter-estimation problem,stochastic system,statistical probabilistic model checking,statistical approach,verifying csl query,markov chains,model checking,probabilistic verification,csl model checking,uni- formisation,sequential analysis,solution technique,parameter estimation,hypothesis test,markov chain
Model checking,Computer science,Markov chain,Algorithm,Acceptance sampling,Sampling (statistics),Temporal logic,Probabilistic logic,System identification,Statistical hypothesis testing
Journal
Volume
Issue
ISSN
8
3
1433-2787
Citations 
PageRank 
References 
104
4.35
23
Authors
4
Search Limit
100104
Name
Order
Citations
PageRank
Håkan L. S. Younes199660.21
Marta Z. Kwiatkowska26118322.21
Gethin Norman34163193.68
David Parker44018184.00