Quantitative Model Checking

Type product

Quantitative Model Checking

Coursera (CC)
Logo van Coursera (CC)
Opleiderscore: starstarstarstar_halfstar_border 7,2 Coursera (CC) heeft een gemiddelde beoordeling van 7,2 (uit 6 ervaringen)

Tip: meer info over het programma, prijs, en inschrijven? Download de brochure!

Beschrijving

When you enroll for courses through Coursera you get to choose for a paid plan or for a free plan

  • Free plan: No certicification and/or audit only. You will have access to all course materials except graded items.
  • Paid plan: Commit to earning a Certificate—it's a trusted, shareable way to showcase your new skills.

About this course: 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 …

Lees de volledige beschrijving

Veelgestelde vragen

Er zijn nog geen veelgestelde vragen over dit product. Als je een vraag hebt, neem dan contact op met onze klantenservice.

Nog niet gevonden wat je zocht? Bekijk deze onderwerpen: Artificial Intelligence, Blockchain, Machine learning, IBM Watson en Robotic process automation (RPA).

When you enroll for courses through Coursera you get to choose for a paid plan or for a free plan

  • Free plan: No certicification and/or audit only. You will have access to all course materials except graded items.
  • Paid plan: Commit to earning a Certificate—it's a trusted, shareable way to showcase your new skills.

About this course: 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.

Who is this class for: This course is meant for Master students in Computer Science, Electrical Engineering and Embedded Systems as a specialisation in the area of formal models and methods. Note that as a consequence, quiz questions are more like exam questions where you have to construct the answer based on the principles that are taught in the web lectures, rather than to recall the literal text of the teacher.

Created by:  EIT Digital
  • Taught by:  Anne Remke, Prof. dr.

    Computer Science
Level Intermediate Commitment 5 weeks of study, each with around 2.h hours work Language English How To Pass Pass all graded assignments to complete the course. User Ratings 4.4 stars Average User Rating 4.4See what learners said Задания курса

Каждый курс — это интерактивный учебник, который содержит видеоматериалы, тесты и проекты.

Помощь сокурсников

Общайтесь с тысячами других учащихся: обсуждайте идеи, материалы курса и помогайте друг другу осваивать новые понятия.

Сертификаты

Получите документы о прохождении курсов и поделитесь своим успехом с друзьями, коллегами и работодателями.

EIT Digital EIT Digital is a pan-European education and research-based open innovation organization founded on excellence. Its 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 "blended" Innovation and Entrepreneurship education to raise quality, increase diversity and availability of the top-level content provided by 20 reputable universities of technology around Europe. The universities all together 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. These are the courses in the online programme:

Syllabus


WEEK 1


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.


6 videos, 3 readings, 1 practice quiz expand


  1. Video: Welcome!
  2. Video: Introduction
  3. Материал для самостоятельного изучения: Script 1 and 2.1
  4. Video: Semantics of CTL
  5. Материал для самостоятельного изучения: Script 2.2 and 2.3
  6. Video: Model Checking CTL
  7. Video: The Until Operator
  8. Тренировочный тест: Check your understanding of CTL
  9. Video: The Always Operator
  10. Материал для самостоятельного изучения: Script 2.4

Graded: Formulate for yourself
Graded: Test your understanding of CTL semantics
Graded: Model checking eventually, always and until

WEEK 2


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.


5 videos, 2 readings, 2 practice quizzes expand


  1. Video: Introduction to DTMCs
  2. Материал для самостоятельного изучения: Script 3.1 and 3.2
  3. Video: Evolution in Time
  4. Тренировочный тест: Evolution of DTMCs
  5. Video: Transient probabilities
  6. Video: State classification
  7. Материал для самостоятельного изучения: Script 3.3
  8. Тренировочный тест: Classification of DTMC states True or False?
  9. Video: Steady-state probabilities

Graded: Compute transient probabilities
Graded: State classification
Graded: Steady-state computation

WEEK 3


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.


5 videos, 3 readings, 3 practice quizzes expand


  1. Video: Syntax of PCTL
  2. Тренировочный тест: PCTL Syntax
  3. Video: Model checking and the Next operator
  4. Материал для самостоятельного изучения: Script: 4.1 and 4.2
  5. Video: Time-bounded Until
  6. Тренировочный тест: Test your understanding of PCTL Until
  7. Video: Backwards computation
  8. Материал для самостоятельного изучения: Script: 4.3.1 and 4.3.2
  9. Video: Unbounded Until
  10. Материал для самостоятельного изучения: Script 4.3.3
  11. Тренировочный тест: Test your understanding of PCTL

Graded: Checking PCTL next
Graded: Checking time-bounded until
Graded: Checking unbounded until

WEEK 4


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.


5 videos, 2 readings, 3 practice quizzes expand


  1. Video: Definition of a CTMC
  2. Материал для самостоятельного изучения: Script: 5.1 and 5.2
  3. Video: Generator matrix
  4. Тренировочный тест: Test your understanding of CTMCs
  5. Video: Steady-state probabilities
  6. Тренировочный тест: Steady state probability in CTMCs
  7. Video: Triple Modular Redundancy
  8. Материал для самостоятельного изучения: Script: 5.3
  9. Video: Uniformisation
  10. Тренировочный тест: Test your understanding of Uniformisation

Graded: Generator matrix
Graded: Identifying BSCCs
Graded: Uniformisation

WEEK 5


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.


5 videos, 2 readings, 3 practice quizzes expand


  1. Video: Model checking CSL
  2. Video: Model checking and Time-bounded next
  3. Материал для самостоятельного изучения: Script: 6.1
  4. Тренировочный тест: Test your understanding of CSL (I)
  5. Video: Model checking the steady-state operator
  6. Тренировочный тест: Test your understanding of CSL (II)
  7. Материал для самостоятельного изучения: Script: 6.2
  8. Video: Time-bounded Until
  9. Тренировочный тест: Test your understanding of CSL (III)
  10. Video: An application

Graded: Assembly line
Graded: Steady state and next
Graded: Time bounded until in CSL

Blijf op de hoogte van nieuwe ervaringen

Er zijn nog geen ervaringen.

Deel je ervaring

Heb je ervaring met deze cursus? Deel je ervaring en help anderen kiezen. Als dank voor de moeite doneert Springest € 1,- aan Stichting Edukans.

Er zijn nog geen veelgestelde vragen over dit product. Als je een vraag hebt, neem dan contact op met onze klantenservice.

Download gratis en vrijblijvend de informatiebrochure

Aanhef
(optioneel)
(optioneel)
(optioneel)
(optioneel)
(optioneel)

Heb je nog vragen?

(optioneel)
We slaan je gegevens op om je via e-mail en evt. telefoon verder te helpen.
Meer info vind je in ons privacybeleid.