Abstract.
We study the satisfiability problem for qualitative PCTL
(Probabilistic Computation Tree Logic), which is obtained
from “ordinary” CTL by replacing the EX, AX, EU, and
AU operators with their qualitative counterparts X>0, X=1,
U>0, and U=1, respectively. As opposed to CTL, qualitative
PCTL does not have a small model property, and there are
even qualitative PCTL formulae which have only infinite-
state models. Nevertheless, we show that the satisfiability
problem for qualitative PCTL is EXPTIME-complete and
we give an exponential-time algorithm which for a given
formula φ computes a finite description of a model (if it exists), or answers “not satisfiable” (otherwise). We also consider the finite satisfiability problem and provide analogous
results. That is, we show that the finite satisfiability problem
for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size
which can effectively be constructed in exponential time. Finally, we give some results about the quantitative PCTL,
where the numerical bounds in probability constraints can
be arbitrary rationals between 0 and 1. We prove that the
problem whether a given quantitative PCTL formula φ has
a model of the branching degree at most k, where k ≥ 2 is
an arbitrary but fixed constant, is highly undecidable. We
also show that every satisfiable formula φ has a model with
branching degree at most |φ| + 2. However, this does not
yet imply the undecidability of the satisfiability problem for
quantitative PCTL, and we in fact conjecture the opposite.
|