The Satisfiability Problem for Probabilistic CTL.
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:
Views and Downloads
If you are the owner of this record, you can report an update to it here: Report update to this record