2013 13th International Conference on Application of Concurrency to System Design (ACSD) (2013)
July 8, 2013 to July 10, 2013
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2013.5
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.
Probabilistic logic, Abstracts, Automata, Model checking, Computational modeling, Safety, Algebra
L. Song, L. Zhang, H. Hermanns and J. C. Godskesen, "Incremental Bisimulation Abstraction Refinement," 2013 13th International Conference on Application of Concurrency to System Design (ACSD), Barcelona, Spain, 2013, pp. 11-20.