loading page

Bounded Model Checking of Continuous Stochastic Logic
  • +1
  • Zhifeng Liu,
  • Yi Gu,
  • Conghua Zhou,
  • Zeeshan Afzal
Zhifeng Liu
Middle Tennessee State University
Author Profile
Yi Gu
Middle Tennessee State University
Author Profile
Conghua Zhou
Jiangsu University
Author Profile
Zeeshan Afzal
University of Lahore - Defence Road Campus

Corresponding Author:[email protected]

Author Profile

Abstract

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.