EIT Digital

Quantitative Model Checking

Taught in English

Some content may not be translated

6,248 already enrolled

Course

Gain insight into a topic and learn the fundamentals

Anne Remke

Instructor: Anne Remke

4.2

(52 reviews)

Intermediate level
Some related experience required
17 hours to complete
3 weeks at 5 hours a week
Flexible schedule
Learn at your own pace

Details to know

Shareable certificate

Add to your LinkedIn profile

Assessments

27 quizzes

See how employees at top companies are mastering in-demand skills

Placeholder
Placeholder

Earn a career certificate

Add this credential to your LinkedIn profile, resume, or CV

Share it on social media and in your performance review

Placeholder

There are 5 modules in this course

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.

What's included

6 videos3 readings4 quizzes

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.

What's included

5 videos2 readings5 quizzes

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.

What's included

5 videos3 readings6 quizzes

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.

What's included

5 videos2 readings6 quizzes

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.

What's included

5 videos2 readings6 quizzes

Instructor

Instructor ratings
4.3 (5 ratings)
Anne Remke
EIT Digital
2 Courses12,853 learners

Offered by

EIT Digital

Recommended if you're interested in Software Development

Why people choose Coursera for their career

Felipe M.
Learner since 2018
"To be able to take courses at my own pace and rhythm has been an amazing experience. I can learn whenever it fits my schedule and mood."
Jennifer J.
Learner since 2020
"I directly applied the concepts and skills I learned from my courses to an exciting new project at work."
Larry W.
Learner since 2021
"When I need courses on topics that my university doesn't offer, Coursera is one of the best places to go."
Chaitanya A.
"Learning isn't just about being better at your job: it's so much more than that. Coursera allows me to learn without limits."

Learner reviews

Showing 3 of 52

4.2

52 reviews

  • 5 stars

    57.69%

  • 4 stars

    25%

  • 3 stars

    5.76%

  • 2 stars

    5.76%

  • 1 star

    5.76%

RA
5

Reviewed on Aug 26, 2023

New to Software Development? Start here.

Placeholder

Open new doors with Coursera Plus

Unlimited access to 7,000+ world-class courses, hands-on projects, and job-ready certificate programs - all included in your subscription

Advance your career with an online degree

Earn a degree from world-class universities - 100% online

Join over 3,400 global companies that choose Coursera for Business

Upskill your employees to excel in the digital economy

Frequently asked questions