Abstract：
Bounded model checking has been proven to be a powerful technique for the verification of reactive systems, since it can avoid the space blow up of BDDs(Binary Decision Diagrams). To avoid the space blow up of MTBDDs(Multi Terminal Binary Decision Diagrams), a bounded model checking technique for Markov decision processes is proposed. The biggest feature of Markov decision processes is able to describe the nondeterministic choice. For this feature, the bounded semantics of the probabilistic computation tree logic is first presented, and its correctness is proven. Second, based on the evolution trend of the sequence consisting of probability measure calculated by the bounded model checking procedure,three termination criterions are given. Third, the bounded model checking procedure of the probabilistic computation tree logic is transformed into a linear equation. Finally, the experiment results show that compared with the unbounded model checking if the length of the witness is short then the bounded model checking needs less space.

ReleaseDate：2014-07-21 17:04:09

PDF