Qualitative Logics and Equivalences for Probabilistic Systems
-------------------------------------------------------------

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
\emph{qualitative equivalence}.  % We show that for finite
\emph{alternating} MDPs, where nondeterministic and probabilistic
choice occur in different states, qualitative equivalence coincides
with alternating bisimulation, %when the MDP is viewed as a 2-player
game.  and can thus be computed via efficient partition-refinement
algorithms.  % Surprisingly, the result does not hold for
\emph{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.