Quantitative Model Checking

Por: Coursera . en: ,

  • Module 1: Computational Tree Logic
    • We introduce Labeled Transition Systems (LTS), the syntax and semantics of Computational Tree Logic (CTL) and discuss the model checking algorithms that are necessary to compute the satisfaction set for specific CTL formulas.
  • Discrete Time Markov Chains
    • We enhance transition systems by discrete time and add probabilities to transitions to model probabilistic choices. We discuss important properties of DTMCs, such as the memoryless property and time-homogeneity. State classification can be used to determine the existence of the limiting and / or stationary distribution.
  • Probabilistic Computational Tree Logic
    • We discuss the syntax and semantics of Probabilistic Computational Tree logic and check out the model checking algorithms that are necessary to decide the validity of different kinds of PCTL formulas. We shortly discuss the complexity of PCTL model checking.
  • Continuous Time Markov Chains
    • We enhance Discrete-Time Markov Chains with real time and discuss how the resulting modelling formalism evolves over time. We compute the steady-state for different kinds of CMTCs and discuss how the transient probabilities can be efficiently computed using a method called uniformisation.
  • Continuous Stochastic Logic
    • We introduce the syntax and semantics of Continuous Stochastic Logic and describe how the different kinds of CSL formulas can be model checked. Especially, model checking the time bounded until operator requires applying the concept of uniformisation, which we have discussed in the previous module.

Plataforma