Quantitative Model Checking

EIT Digital

À propos de ce cours

19,696 consultations récentes

The integration of ICT (information and communications technology) in different applications is rapidly increasing in e.g. Embedded and Cyber physical systems, Communication protocols and Transportation systems. Hence, their reliability and dependability increasingly depends on software. Defects can be fatal and extremely costly (with regards to mass-production of products and safety-critical systems).
First, a model of the real system has to be built. In the simplest case, the model reflects all possible states that the system can reach and all possible transitions between states in a (labelled) State Transition System. When adding probabilities and discrete time to the model, we are dealing with so-called Discrete-time Markov chains which in turn can be extended with continuous timing to Continuous-time Markov chains. Both formalisms have been used widely for modeling and performance and dependability evaluation of computer and communication systems in a wide variety of domains. These formalisms are well understood, mathematically attractive while at the same time flexible enough to model complex systems. 

Model checking focuses on the qualitative evaluation of the model. As formal verification method, model checking analyzes
the functionality of the system model. A property that needs to be analyzed has to be specified in a logic with consistent syntax and semantics. For every state of the model, it is then checked whether the property is valid or not.
The main focus of this course is on quantitative model checking for Markov chains, for which we will discuss efficient computational algorithms. The learning objectives of this course are as follows:

- Express dependability properties for different kinds of transition systems .
- Compute the evolution over time for Markov chains.
- Check whether single states satisfy a certain formula and compute the satisfaction set for properties.

Certificat partageable

Obtenez un Certificat lorsque vous terminez

100 % en ligne

Commencez dès maintenant et apprenez aux horaires qui vous conviennent.

Dates limites flexibles

Réinitialisez les dates limites selon votre disponibilité.

Niveau intermédiaire

Approx. 11 heures pour terminer

Anglais

Sous-titres : Anglais

Certificat partageable

Obtenez un Certificat lorsque vous terminez

100 % en ligne

Commencez dès maintenant et apprenez aux horaires qui vous conviennent.

Dates limites flexibles

Réinitialisez les dates limites selon votre disponibilité.

Niveau intermédiaire

Approx. 11 heures pour terminer

Anglais

Sous-titres : Anglais

Enseignant

Anne Remke

Offert par

EIT Digital

EIT Digital is a pan-European organization whose mission is to foster digital technology innovation and entrepreneurial talent for economic growth and quality of life. By linking education, research and business, EIT Digital empowers digital top talents for the future.

EIT Digital provides online and blended Innovation and Entrepreneurship education to raise quality, increase diversity and availability of the top-level content provided by 20 leading technical universities around Europe. The universities deliver a unique blend of the best of technical excellence and entrepreneurial skills and mindset to digital engineers and entrepreneurs at all stages of their careers. The academic partners support Coursera’s bold vision to enable anyone, anywhere, to transform their lives by accessing the world’s best learning experience. This means that EIT Digital gradually shares parts of its entrepreneurial and academic education programmes to demonstrate its excellence and make it accessible to a much wider audience. EIT Digital’s online education portfolio can be used as part of blended education settings, in both Master and Doctorate programmes, and for professionals as a way to update their knowledge. EIT Digital offers an online programme in 'Internet of Things through Embedded Systems'. Achieving all certificates of the online courses and the specialization provides an opportunity to enroll in the on campus program and get a double degree. Please visit https://www.eitdigital.eu/eit-digital-academy/

Programme du cours : ce que vous apprendrez dans ce cours

Semaine

Semaine 1

3 heures pour terminer

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.

3 heures pour terminer

6 vidéos (Total 61 min), 3 lectures, 4 quiz

6 vidéos

Welcome!1 min

Introduction13 min

Semantics of CTL13 min

Model Checking CTL9 min

The Until Operator12 min

The Always Operator9 min

3 lectures

Script 1 and 2.110 min

Script 2.2 and 2.310 min

Script 2.420 min

4 exercices pour s'entraîner

Formulate for yourself6 min

Test your understanding of CTL semantics14 min

Check your understanding of CTL20 min

Model checking eventually, always and until22 min

Semaine

Semaine 2

2 heures pour terminer

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.

2 heures pour terminer

5 vidéos (Total 49 min), 2 lectures, 5 quiz

5 vidéos

Introduction to DTMCs7 min

Evolution in Time13 min

Transient probabilities9 min

State classification5 min

Steady-state probabilities12 min

2 lectures

Script 3.1 and 3.210 min

Script 3.310 min

5 exercices pour s'entraîner

Evolution of DTMCs6 min

Compute transient probabilities10 min

Classification of DTMC states True or False?14 min

State classification16 min

Steady-state computation12 min

Semaine

Semaine 3

2 heures pour terminer

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.

2 heures pour terminer

5 vidéos (Total 36 min), 3 lectures, 6 quiz

5 vidéos

Syntax of PCTL8 min

Model checking and the Next operator7 min

Time-bounded Until6 min

Backwards computation4 min

Unbounded Until8 min

3 lectures

Script: 4.1 and 4.210 min

Script: 4.3.1 and 4.3.225 min

Script 4.3.310 min

6 exercices pour s'entraîner

PCTL Syntax8 min

Checking PCTL next4 min

Test your understanding of PCTL Until6 min

Checking time-bounded until16 min

Checking unbounded until10 min

Test your understanding of PCTL6 min

Semaine

Semaine 4

2 heures pour terminer

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.

2 heures pour terminer

5 vidéos (Total 57 min), 2 lectures, 6 quiz

5 vidéos

Definition of a CTMC10 min

Generator matrix11 min

Steady-state probabilities11 min

Triple Modular Redundancy11 min

Uniformisation12 min

2 lectures

Script: 5.1 and 5.220 min

Script: 5.315 min

6 exercices pour s'entraîner

Generator matrix6 min

Test your understanding of CTMCs6 min

Steady state probability in CTMCs10 min

Identifying BSCCs12 min

Test your understanding of Uniformisation6 min

Uniformisation12 min

Foire Aux Questions

Quand aurai-je accès aux vidéos de cours et aux devoirs ?
Une fois que vous êtes inscrit(e) pour un Certificat, vous pouvez accéder à toutes les vidéos de cours, et à tous les quiz et exercices de programmation (le cas échéant). Vous pouvez soumettre des devoirs à examiner par vos pairs et en examiner vous-même uniquement après le début de votre session. Si vous préférez explorer le cours sans l'acheter, vous ne serez peut-être pas en mesure d'accéder à certains devoirs.
À quoi ai-je droit si j'achète le Certificat ?
Lorsque vous achetez un Certificat, vous bénéficiez d'un accès à tout le contenu du cours, y compris les devoirs notés. Lorsque vous avez terminé et réussi le cours, votre Certificat électronique est ajouté à votre page Accomplissements. À partir de cette page, vous pouvez imprimer votre Certificat ou l'ajouter à votre profil LinkedIn. Si vous souhaitez seulement lire et visualiser le contenu du cours, vous pouvez accéder gratuitement au cours en tant qu'auditeur libre.
Quelle est la politique de remboursement ?
Vous avez droit à un remboursement intégral jusqu'à deux semaines après la date de paiement ou (pour les cours qui viennent d'être lancés) jusqu'à deux semaines après le début de la première session du cours, selon la dernière de ces éventualités. Vous ne pouvez pas bénéficier d'un remboursement une fois votre Certificat de Cours obtenu, même si vous terminez le cours pendant la période de remboursement de deux semaines. Consultez notre Politique de remboursement complète.
Une aide financière est-elle possible ?
Oui, Coursera fournit une Aide Financière aux étudiants n'ayant pas les moyens d'acquitter les frais. Pour en faire la demande, cliquez sur le lien Aide Financière situé sous le bouton S'inscrire ci-contre à gauche. Vous serez invité(e) à déposer une demande et vous serez averti(e) si elle est acceptée. En savoir plus.
Puis-je obtenir des crédits universitaires si je réussis le Cours ?
Ce Cours n'est pas associé à des crédits universitaires, mais certaines universités peuvent décider d'accepter des Certificats de Cours pour des crédits. Vérifiez-le auprès de votre établissement pour en savoir plus. Les Diplômes en ligne et les Certificats Mastertrack™ sur Coursera apportent la possibilité d'obtenir des crédits universitaires.

D'autres questions ? Visitez le Centre d'Aide pour les Etudiants.

Quantitative Model Checking