آموزش مدل‌سازی کمّی مدل (Quantitative Model Checking) - آخرین آپدیت

Module 1: Computational Tree Logic Module 1: Computational Tree Logic

• Welcome! Welcome!

• Introduction Introduction

• Semantics of CTL Semantics of CTL

• Model Checking CTL Model Checking CTL

• The Until Operator The Until Operator

• The Always Operator The Always Operator

Discrete Time Markov Chains Discrete Time Markov Chains

• Introduction to DTMCs Introduction to DTMCs

• Evolution in Time Evolution in Time

• Transient probabilities Transient probabilities

• State classification State classification

• Steady state probabilities Steady-state probabilities

Probabilistic Computational Tree Logic Probabilistic Computational Tree Logic

• Syntax of PCTL Syntax of PCTL

• Model checking and the Next operator Model checking and the Next operator

• Time bounded Until Time-bounded Until

• Backwards computation Backwards computation

• Unbounded Until Unbounded Until

Continuous Time Markov Chains Continuous Time Markov Chains

• Definition of a CTMC Definition of a CTMC

• Generator matrix Generator matrix

• Steady state probabilities Steady-state probabilities

• Triple Modular Redundancy Triple Modular Redundancy

• Uniformisation Uniformisation

Continuous Stochastic Logic Continuous Stochastic Logic

• Model checking CSL Model checking CSL

• Model checking and Time bounded next Model checking and Time-bounded next

• Model checking the steady state operator Model checking the steady-state operator

• Time bounded Until Time-bounded Until

• An application An application