---
res:
bibo_abstract:
- '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 non-alternating MDPs the equivalence relations cannot be computed via partition-refinement
algorithms, but rather, they require non-local computation. Finally, we consider
QRCTL*, that extends QRCTL with nested temporal operators in the same manner in
which CTL* extends CTL. 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 finitely-branching.@eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Krishnendu Chatterjee
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Luca
foaf_name: de Alfaro, Luca
foaf_surname: De Alfaro
- foaf_Person:
foaf_givenName: Marco
foaf_name: Faella, Marco
foaf_surname: Faella
- foaf_Person:
foaf_givenName: Axel
foaf_name: Legay, Axel
foaf_surname: Legay
bibo_doi: 10.2168/LMCS-5(2:7)2009
bibo_issue: '2'
bibo_volume: 5
dct_date: 2009^xs_gYear
dct_publisher: International Federation of Computational Logic@
dct_title: Qualitative logics and equivalences for probabilistic systems@
...