Abstraction refinement techniques in probabilistic model checking are prominent approaches to the verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This paper proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach.
|Tidsskrift||Proceedings of the International Conference on Application of Concurrency to System Design|
|Status||Udgivet - 8 jul. 2013|
|Begivenhed||13th International Conference on Application of Concurrency to System Design: http://acsd.lsi.upc.edu/ - Barcelona, Spanien|
Varighed: 8 jul. 2013 → 10 jul. 2013
|Konference||13th International Conference on Application of Concurrency to System Design|
|Periode||08/07/2013 → 10/07/2013|