- Authors:
- DOI:
- 10.1109/ACSD.2013.5
- 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.
- Type:
- Conference paper
- Language:
- English
- Published in:
- Proceedings of the International Conference on Application of Concurrency To System Design, 2013, p. 11-20
- Main Research Area:
- Science/technology
- Publication Status:
- Published
- Review type:
- Peer Review
- Conference:
- 13th International Conference on Application of Concurrency to System DesignInternational Conference on Application of Concurrency to System Design, 2013
- Submission year:
- 2013
- Scientific Level:
- Scientific
- ID:
- 245591899
Checking for on-site access...
