Journal article icon

Journal article

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 infinitestate models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is E...

Expand abstract

Actions


Access Document


Publisher copy:
10.1109/LICS.2008.21

Authors


Brázdil, T More by this author
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Kretínský, J More by this author
Publisher:
IEEE Computer Society Publisher's website
Journal:
LICS
Pages:
391-402
Publication date:
2008
DOI:
ISSN:
1043-6871
URN:
uuid:89bb10bc-57e2-4ca1-bdf0-d33d06188c49
Source identifiers:
316492
Local pid:
pubs:316492
Language:
English

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP