Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Conditional Probabilities over Probabilistic and Nondeterministic Systems
verfasst von : Miguel E. Andrés, Peter van Rossum
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper introduces the logic cpCTL, which extends the probabilistic temporal logic pCTL with conditional probability, allowing one to express that the probability that
φ
is true given that
ψ
is true is at least
a
. We interpret cpCTL over Markov Chain and Markov Decision Processes. While model checking cpCTL over Markov Chains can be done with existing techniques, those techniques do not carry over to Markov Decision Processes. We present a model checking algorithm for Markov Decision Processes. We also study the class of schedulers that suffice to find the maximum and minimum probability that
φ
is true given that
ψ
is true. Finally, we present the notion of counterexamples for cpCTL model checking and provide a method for counterexample generation.