"The Satisfiability Problem for Probabilistic CTL" . "2008-06-24+02:00"^^ . "[C11FB54C4747]" . . "IEEE Computer Society" . "RIV/00216224:14330/08:00026224!RIV10-MSM-14330___" . "K\u0159et\u00EDnsk\u00FD, Jan" . . "The Satisfiability Problem for Probabilistic CTL" . . "14330" . "000258728700033" . . "Stochastic systems; branching-time temporal logics"@en . . "RIV/00216224:14330/08:00026224" . . "978-0-7695-3183-0" . "Pittsburgh, USA" . . "Los Alamitos, California" . . . "Forejt, Vojt\u011Bch" . "The Satisfiability Problem for Probabilistic CTL"@en . . . "We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from %22ordinary%22 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 %22not satisfiable%22 (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." . "We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from %22ordinary%22 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 %22not satisfiable%22 (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."@en . . "Ku\u010Dera, Anton\u00EDn" . "4"^^ . . . . "4"^^ . "10"^^ . . "23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings" . "The Satisfiability Problem for Probabilistic CTL"@en . . . "P(1M0545), Z(MSM0021622419)" . "Br\u00E1zdil, Tom\u00E1\u0161" . . "393788" . .