loading...
Qualitative Logics and Equivalences for Probabilistic Systems
Edinburgh, Scotland, UK September 17-September 19
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2007.15Fourth International Conference on th ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Luca de Alfaro, University of California, Santa Cruz, USA
Krishnendu Chatterjee, University of California, Berkeley, USA
Marco Faella, Universita di Napoli "Federico II", Italy
Axel Legay, University of Liege, Belgium
We present Qualitative Randomized CTL (QRCTL), a qualitative version of pCTL, for specifying properties of Markov Decision Processes (MDPs). QRCTL formulas can express the fact that certain temporal properties hold with probability 0 or 1, but they do not distinguish other probabilities values.

We present a symbolic, polynomial time model-checking algorithm for QRCTL on MDPs. Then, we study the equivalence relation induced by QRCTL, called qualitative equivalence. We show that for finite alternating MDPs, where nondeterministic and probabilistic choice occur in different states, qualitative equivalence coincides with alternating bisimulation, and can thus be computed via efficient partition-refinement algorithms. Surprisingly, the result does not hold for non-alternating MDPs. Indeed, we show that no local partition refinement algorithm can compute qualitative equivalence on non-alternating MDPs. Finally, we consider QRCTL*, that is the "star extension" of QRCTL. We show that QRCTL and QRCTL* induce the same qualitative equivalence on alternating MDPs, while on non-alternating MDPs, the equivalence arising from QRCTL* can be strictly finer. We also provide a full characterization of the relation between qualitative equivalence, bisimulation, and alternating bisimulation, according to whether the MDPs are finite, and to whether their transition relations are finite-branching.

Citation:
Luca de Alfaro, Krishnendu Chatterjee, Marco Faella, Axel Legay, "Qualitative Logics and Equivalences for Probabilistic Systems," qest, pp.237-248, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.