The Community for Technology Leaders
2013 13th International Conference on Application of Concurrency to System Design (ACSD) (2013)
Barcelona, Spain
July 8, 2013 to July 10, 2013
ISSN: 1550-4808
ISBN: 978-0-7695-5035-0
pp: 11-20
ABSTRACT
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.
INDEX TERMS
Probabilistic logic, Abstracts, Automata, Model checking, Computational modeling, Safety, Algebra
CITATION

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.
doi:10.1109/ACSD.2013.5
83 ms
(Ver 3.3 (11022016))