Statistical Model Checking : An Overview <s> Tools and Experiments <s> This paper gives a brief overview of version 2.0 of PRISM, a tool for the automatic formal verification of probabilistic systems, and some of the case studies to which it has already been applied. <s> BIB001 </s> Statistical Model Checking : An Overview <s> Tools and Experiments <s> We present Ymer, a tool for verifying probabilistic transient properties of stochastic discrete event systems. Ymer implements both statistical and numerical model checking techniques. We focus on two features of Ymer: distributed acceptance sampling and statistical model checking of nested probabilistic statements. <s> BIB002 </s> Statistical Model Checking : An Overview <s> Tools and Experiments <s> We give a brief overview of a statistical model-checking and analysis tool VESTA. VESTA is a tool for statistical analysis of probabilistic systems. It supports statistical model-checking and statistical evaluation of expected values of temporal expressions. <s> BIB003 </s> Statistical Model Checking : An Overview <s> Tools and Experiments <s> This paper studies the efficiency of several probabilistic model checkers by comparing verification times and peak memory usage for a set of standard case studies. The study considers the model checkers ETMCC, MRMC, PRISM (sparse and hybrid mode), YMER and VESTA, and focuses on fully probabilistic systems. Several of our experiments show significantly different run times and memory consumptions between the tools-up to various orders of magnitude--without, however, indicating a clearly dominating tool. For statistical model checking YMER clearly prevails whereas for the numerical tools MRMC and PRISM (sparse) are rather close. <s> BIB004
At the origin, there are two tools that implements statistical model checking algorithms, namely Ymer BIB002 and Vesta BIB003 . Vesta implements a variation of the single sampling plan algorithm. The choice of implementing the SSP algorithm is motivated by the fact that it is easier to parallelize as the number of simulations to perform is known in advance. However, in his thesis, Younes showed that sequential algorithms are also easily parallelizable. Ymer is limited to bounded properties while Vesta also incorporate the unbounded until. In BIB004 , the authors conducted several experiments that tend to show that (1) Ymer is faster than Vesta and (2) Vesta makes more false positive (selecting the bad hypothesis) than Ymer. Regarding the unbounded case, it seems that Vesta is not very efficient and can make a lot of false positive. Both Vesta and Ymer have been applied to huge case studies. A comparison of Ymer and Vesta with established tools such PRISM BIB001 can be found in BIB004 . There are a wide range of situations for which the bounded case suffices. We have written a series of recent papers in where we propose applications of SSP and SPRT to interesting problems. In the rest of this section, we briefly recap the content of these papers.