Bounded Model Checking of Continuous Stochastic Logic
AbstractModel 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.