Abstract
Language  Undefined 

Awarding Institution 

Supervisors/Advisors 

Thesis sponsors  
Award date  6 Dec 2013 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036535861 
DOIs  
State  Published  6 Dec 2013 
Keywords
 EWI23973
 METIS299026
 IR88033
 Importance sampling
 Dependable systems
 Rare event simulation
 Statistical Model Checking
Cite this
}
Efficient simulation techniques for stochastic model checking. / Reijsbergen, D.P.
Enschede : Universiteit Twente, 2013. 175 p.Research output: Thesis › PhD Thesis  Research UT, graduation UT
TY  THES
T1  Efficient simulation techniques for stochastic model checking
AU  Reijsbergen,D.P.
PY  2013/12/6
Y1  2013/12/6
N2  In this thesis, we focus on methods for speedingup computer simulations of stochastic models. We are motivated by realworld applications in which corporations formulate service requirements in terms of an upper bound on a probability of failure. If one wants to check whether a complex system model satisfies such a requirement, computer simulation is often the method of choice. We aim to aid engineers during the design phase, so a question of both practical and mathematical relevance is how the runtime of the simulation can be minimised. We focus on two settings in which a speedup can be achieved. First, when the probability of failure is low, as is typical in a highly reliable system, the time before the first failure is observed can be impractically large. Our research involves importance sampling; we simulate using a different probability measure under which failure is more likely, which typically decreases the variance of the estimator. In order to keep the estimator unbiased, we compensate for the resulting error using the RadonNikodym theorem. If done correctly, the gains can be huge. However, if the new probability measure is unsuited for the problem setting the negative consequences can be similarly profound (infinite variance is even possible). In our work, we have extended an importance sampling technique with good performance (i.e., proven to have bounded relative error) that was previously only applicable in restricted settings to a broad model class of stochastic (Markovian) Petri nets. We have also proposed methods to alleviate two wellknown problems from the rare event simulation literature: the occurrence of socalled highprobability cycles and the applicability to large time horizons. For the first we use a method based on Dijkstra’s algorithm, for the second we use renewal theory. Second, it often occurs that the number of needed simulation runs is overestimated. As a solution, we use sequential hypothesis testing, which allows us to stop as soon as we can say whether the service requirement is satisfied. This area has seen a lot of recent interest from the model checking community, but some of the techniques used are not always perfectly understood. In our research we have compared the techniques implemented in the most popular model checking tools, identified several common pitfalls and proposed a method that we proved to not have this problem. In particular, we have proposed a new test for which we bounded the probability of an incorrect conclusion using martingale theory.
AB  In this thesis, we focus on methods for speedingup computer simulations of stochastic models. We are motivated by realworld applications in which corporations formulate service requirements in terms of an upper bound on a probability of failure. If one wants to check whether a complex system model satisfies such a requirement, computer simulation is often the method of choice. We aim to aid engineers during the design phase, so a question of both practical and mathematical relevance is how the runtime of the simulation can be minimised. We focus on two settings in which a speedup can be achieved. First, when the probability of failure is low, as is typical in a highly reliable system, the time before the first failure is observed can be impractically large. Our research involves importance sampling; we simulate using a different probability measure under which failure is more likely, which typically decreases the variance of the estimator. In order to keep the estimator unbiased, we compensate for the resulting error using the RadonNikodym theorem. If done correctly, the gains can be huge. However, if the new probability measure is unsuited for the problem setting the negative consequences can be similarly profound (infinite variance is even possible). In our work, we have extended an importance sampling technique with good performance (i.e., proven to have bounded relative error) that was previously only applicable in restricted settings to a broad model class of stochastic (Markovian) Petri nets. We have also proposed methods to alleviate two wellknown problems from the rare event simulation literature: the occurrence of socalled highprobability cycles and the applicability to large time horizons. For the first we use a method based on Dijkstra’s algorithm, for the second we use renewal theory. Second, it often occurs that the number of needed simulation runs is overestimated. As a solution, we use sequential hypothesis testing, which allows us to stop as soon as we can say whether the service requirement is satisfied. This area has seen a lot of recent interest from the model checking community, but some of the techniques used are not always perfectly understood. In our research we have compared the techniques implemented in the most popular model checking tools, identified several common pitfalls and proposed a method that we proved to not have this problem. In particular, we have proposed a new test for which we bounded the probability of an incorrect conclusion using martingale theory.
KW  EWI23973
KW  METIS299026
KW  IR88033
KW  Importance sampling
KW  Dependable systems
KW  Rare event simulation
KW  Statistical Model Checking
U2  10.3990/1.9789036535861
DO  10.3990/1.9789036535861
M3  PhD Thesis  Research UT, graduation UT
SN  9789036535861
PB  Universiteit Twente
CY  Enschede
ER 