Qualitative Logics and Equivalences for Probabilistic Systems

We investigate logics and equivalence relations that capture the qualitative behavior of Markov Decision Processes (MDPs). We present Qualitative Randomized Ctl (Qrctl): formulas of this logic can express the fact that certain temporal properties hold over all paths, or with probability 0 or 1, but they do not distinguish among intermediate probability values. We present a symbolic, polynomial time model-checking algorithm for Qrctl on MDPs. The logic Qrctl induces an equivalence relation over states of an MDP that we call qualitative equivalence: informally, two states are qualitatively equivalent if the sets of formulas that hold with probability 0 or 1 at the two states are the same. We show that for finite alternating MDPs, where nondeterministic and probabilistic choices occur in different states, qualitative equivalence coincides with alternating bisimulation, and can thus be computed via efficient partition-refinement algorithms. On the other hand, in nonalternating MDPs the e...

• Type: Conference
• Year: 2007
• Where: QEST
• Authors: Luca de Alfaro, Krishnendu Chatterjee, Marco Faella, Axel Legay
• Keywords: Equivalence Relations, QEST 2007, Qualitative Equivalence, Qualitative Equivalence Coincides, Quantitative Evaluation Of Systems