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 infinitestate models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is E...Expand abstract
- Publisher copy:
- Copyright date:
The Satisfiability Problem for Probabilistic CTL.
If you are the owner of this record, you can report an update to it here: Report update to this record