Bounded Model Checking of Continuous Stochastic Logic

Model checking continuous stochastic logic has been proven to be a powerful technique for analyzing the dependability and performance of stochastic systems. The state space explosion is the main obstacle making the technique more practical. To avoid the state explosion, a bounded model checking technique of continuous stochastic logic is proposed. First of all, the bounded semantics of continuous stochastic logic is presented, and its correctness is proven. Secondly, an effective method for computing the transient probability and steady-state probability bounded by the path length is proposed. Finally, for different operators bounded model checking procedures based on the computation of the transient probability and steady-state probability bounded by the path length are proposed. The experiment results show that if the property can be verified in local reachable space with small depth, then the bounded model checking is better than global model checking in time and space consumption.