Get started with custom lists to organize and share courses.

Sign up

Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

Quantitative Model Checking

EIT Digital via Coursera

  • Provider Coursera
  • Subject Electrical Engineering
  • Cost Free Online Course (Audit)
  • Session Upcoming
  • Language English
  • Certificate Paid Certificate Available
  • Start Date
  • Duration 5 weeks long
  • Learn more about MOOCs

Taken this course? Share your experience with other students. Write review

Overview

Sign up to Coursera courses for free Learn how

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.

Taught by

Anne Remke

Help Center

Most commonly asked questions about Coursera Coursera

Reviews for Coursera's Quantitative Model Checking
Based on 0 reviews

  • 5 star 0%
  • 4 star 0%
  • 3 star 0%
  • 2 star 0%
  • 1 star 0%

Did you take this course? Share your experience with other students.

Write a review

Class Central

Get personalized course recommendations, track subjects and courses with reminders, and more.

Sign up for free

Never stop learning Never Stop Learning!

Get personalized course recommendations, track subjects and courses with reminders, and more.