Statistical Model Checking : An Overview <s> The Unbounded Case: Until <s> A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs. <s> BIB001 </s> Statistical Model Checking : An Overview <s> The Unbounded Case: Until <s> The verification problem for probabilistic concurrent finite-state program is to decide whether such a program satisfies its linear temporal logic specification. We describe an automata-theoretic approach, whereby probabilistic quantification over sets of computations is reduced to standard quantification over individual computations. Using new determinization construction for ω-automata, we manage to improve the time complexity of the algorithm by two exponentials. The time complexity of the final algorithm is polynomial in the size of the program and doubly exponential in the size of the specification. <s> BIB002 </s> Statistical Model Checking : An Overview <s> The Unbounded Case: Until <s> Symbolic model checking methods have been extended recently to the verification of probabilistic systems. However, the representation of the transition matrix may be expensive for very large systems and may induce a prohibitive cost for the model checking algorithm. In this paper, we propose an approximation method to verify quantitative properties on discrete Markov chains. We give a randomized algorithm to approximate the probability that a property expressed by some positive LTL formula is satisfied with high confidence by a probabilistic system. Our randomized algorithm requires only a succinct representation of the system and is based on an execution sampling method. We also present an implementation and a few classical examples to demonstrate the effectiveness of our approach. <s> BIB003 </s> Statistical Model Checking : An Overview <s> The Unbounded Case: Until <s> Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operator and unbounded until formulas. In this paper, we present a statistical model checking algorithm that also verifies CSL formulas with unbounded untils. The algorithm is based on Monte Carlo simulation of the model and hypothesis testing of the samples, as opposed to sequential hypothesis testing. We have implemented the algorithm in a tool called VESTA, and found it to be effective in verifying several examples. <s> BIB004 </s> Statistical Model Checking : An Overview <s> The Unbounded Case: Until <s> We present MC 2 , what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking. Given a specification S of a finite-state system, an LTL formula φ, and parameters ∈ and 6, MC 2 takes M = ln(δ)/ln(1 - e) random samples (random walks ending in a cycle, i.e lassos) from the Biichi automaton B = B S x B ¬φ to decide if L(B) = θ Let p Z be the expectation of an accepting lasso in B. Should a sample reveal an accepting lasso l, MC 2 returns false with I as a witness. Otherwise, it returns true and reports that the probability of finding an accepting lasso through further sampling, under the assumption that p Z ≥ e, is less than 6. It does so in time O(MD) and space O(D), where D is B's recurrence diameter, using an optimal number of samples M. Our experimental results demonstrate that MC 2 is fast, memory-efficient, and scales extremely well. <s> BIB005 </s> Statistical Model Checking : An Overview <s> The Unbounded Case: Until <s> We propose to perform statistical probabilistic model checking by using perfect simulation in order to verify steady-state and time unbounded until formulas over Markov chains. The model checking of probabilistic models by statistical methods has received increased attention in the last years since it provides an interesting alternative to numerical model checking which is poorly scalable with the increasing model size. In previous statistical model checking works, unbounded until formulas could not be efficiently verified, and steady-state formulas had not been considered due to the burn-in time problem to detect the steady-state. Perfect simulation is an extension of Markov Chain Monte Carlo (MCMC) methods that allows us to obtain exact steady-state samples of the underlying Markov chain, and thus it avoids the burn-in time problem to detect the steady-state. Therefore we suggest to verify time unbounded until and steady-state dependability properties for large Markov chains through statistical model checking by combining perfect simulation and statistical hypothesis testing. <s> BIB006
We are now concerned with the verification of the until property. The property requires that a property φ 1 remains valid until a property φ 2 has been seen. The problem is that we do not know a priori the moment when φ 2 will be satisfied. Hence, one has to reason on infinite execution. There are two works on this topics, one by Sen et al. BIB004 and one more recent work by Pekergin et al. BIB006 . We will not give details on these works, but the reader should know that Sen works by extending the model with extra probabilities, which makes the solution extremely slow. Pekergin uses the new technique of perfect simulation, which is (according to her experiments) not only faster than Sen's one, but also more general as it allows to study the steady-state operator for continuous timed Markov Chains. Remark 5. Contrary to the numerical results BIB002  The above results are not sufficient to verify properties of the form P ≥θ (φ), where φ is a property expressed in Linear Temporal Logic BIB001 . Incomplete results regarding the verification of these properties with simulation-based techniques can be found in BIB003 BIB005 .