Sciweavers

QEST
2007
IEEE

Qualitative Logics and Equivalences for Probabilistic Systems

13 years 10 months ago
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...
Luca de Alfaro, Krishnendu Chatterjee, Marco Faell
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where QEST
Authors Luca de Alfaro, Krishnendu Chatterjee, Marco Faella, Axel Legay
Comments (0)