| Popis: |
In probabilistic model checking, use discrete time Markov chain (DTMCs) to represent the model and use a branch of the temporal logic called probabilistic computation tree(PCTL) to represent the properties of the model. In this paper, we presents several counterexample generation algorithms for DTMCs violating a PCTL formula, presented as follows: first, according to the transitive closure to reduce the model size against the specific properties of the model, second, using the minimal connected components to generate the equivalent acyclic graph, third, we use the algorithm of the operational research to obtain a shortest path between two points. Experimental results show that our algorithm greatly simplifies the model size and generate more reasonable counterexamples with least states and paths. |
