Technical Reports
The report FIMU-RS-2008-03
The Satisfiability Problem for Probabilistic CTL
by
Tomáš Brázdil,
Vojtěch Forejt,
Jan Křetínský,
Antonín Kučera,
A full version of the paper presented at LICS 2008. June 2008, 34 pages.
FIMU-RS-2008-03.
Available as Postscript,
PDF.
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 > 1 is an arbitrary but fixed constant, is highly undecidable.
We also show that every satisfiable formula F has a model with
branching degree at most |F| + 2. However, this does not yet
imply the undecidability of the satisfiability problem for
quantitative PCTL, and we in fact conjecture the opposite.
