Debugging of Markov Decision Processes (MDPs) Models
In model checking, a counterexample is considered as a valuable tool for debugging. In Probabilistic Model Checking (PMC), counterexample generation has a quantitative aspect. The counterexample in PMC is a set of paths in which a path formula holds, and their accumulative probability mass violates...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1608.07881v1 |