Paper Info
Title
The Satisfiability Problem for Probabilistic CTL
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 phi 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 satifiable 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 phi 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 phi has a model with branching degree at most vertical bar phi vertical bar + 2. However this does not yet imply the undecidability of the satisfiability problem for quantitative PCTL, and we in fact conjecture the opposite.
Year
DOI
Venue
2008
10.1109/LICS.2008.21
LICS
Keywords
Field
DocType
markov chain,computational complexity,satisfiability,computational modeling,probabilistic logic,computer science,probabilistic ctl,informatics,markov chains,temporal logic,probability distribution,computability,probabilistic computation tree logic,finite element methods,cost accounting,gold
Discrete mathematics,Combinatorics,Rational number,Boolean satisfiability problem,Probabilistic CTL,Computability,Probability distribution,Conjecture,Mathematics,Computational complexity theory,Undecidable problem
Conference
ISSN
Citations 
PageRank 
1043-6871
11
0.59
References 
Authors
19
4
Name
Order
Citations
PageRank
Tomás Brázdil116116.23
Vojtech Forejt230214.69
Jan Kretínský315916.02
Antonín Kucera465855.69