Quantitative Model Checking
Keep adding new skills with 10,000+ programs for $239 (usually $399). Save now.
Ask Coursera
54 reviews
54 reviews
What you'll learn
Learn the foundations of quantitative model checking for probabilistic and stochastic systems.
Model and analyse systems using Discrete-Time and Continuous-Time Markov Chains.
Apply Computational Tree Logic (CTL) and Probabilistic CTL (PCTL) to formally verify system properties.
Use formal verification techniques to evaluate the reliability, performance, and dependability of embedded, cyber-physical and communication systems
Details to know
See how employees at top companies are mastering in-demand skills
There are 5 modules in this course
Welcome to the cutting-edge course on Quantitative Model Checking for Markov Chains! As technology permeates every aspect of modern life—Embedded Systems, Cyber-Physical Systems, Communication Protocols, and Transportation Systems—the need for dependable software is at an all-time high. One tiny flaw can lead to catastrophic failures and enormous costs. That's where you come in.
The course kicks off with creating a State Transition System, the basic model that captures the intricate dynamics of real-world systems. Soon you'll step into the world of Discrete-time and Continuous-time Markov Chains—powerful mathematical formalisms that are versatile enough to model complex systems yet elegant in their design. These aren't just theories; they are tools actively used across various domains for performance and dependability evaluation. But we won't stop at modelling. The heart of this course is 'Model Checking,' a formal verification method that scrutinizes the functionality of your system model. Learn how to express dependability properties, track the evolution of Markov chains over time, and verify whether states meet particular conditions—all using advanced computational algorithms. By the end of this course, you'll be equipped with the skills to: - Specify dependability properties for a range of transition systems. - Understand the temporal evolution of Markov chains. - Analyze and compute the satisfaction set for multiple properties. Are you ready to become an expert in ensuring the reliability of tomorrow's technologies? Click here to Enroll today and join us in mastering the art and science of model checking.
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 assignments
6 videos•Total 61 minutes
- Welcome!•1 minute
- Introduction•13 minutes
- Semantics of CTL•13 minutes
- Model Checking CTL•10 minutes
- The Until Operator•13 minutes
- The Always Operator•10 minutes
3 readings•Total 40 minutes
- Script 1 and 2.1•10 minutes
- Script 2.2 and 2.3•10 minutes
- Script 2.4•20 minutes
4 assignments•Total 120 minutes
- Formulate for yourself•30 minutes
- Test your understanding of CTL semantics•30 minutes
- Model checking eventually, always and until•30 minutes
- Check your understanding of CTL•30 minutes
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 assignments
5 videos•Total 49 minutes
- Introduction to DTMCs•8 minutes
- Evolution in Time•13 minutes
- Transient probabilities•10 minutes
- State classification•6 minutes
- Steady-state probabilities•12 minutes
2 readings•Total 20 minutes
- Script 3.1 and 3.2•10 minutes
- Script 3.3•10 minutes
5 assignments•Total 130 minutes
- Compute transient probabilities•10 minutes
- State classification•30 minutes
- Steady-state computation•30 minutes
- Evolution of DTMCs•30 minutes
- Classification of DTMC states True or False?•30 minutes
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 assignments
5 videos•Total 36 minutes
- Syntax of PCTL•9 minutes
- Model checking and the Next operator•8 minutes
- Time-bounded Until•7 minutes
- Backwards computation•4 minutes
- Unbounded Until•9 minutes
3 readings•Total 45 minutes
- Script: 4.1 and 4.2•10 minutes
- Script: 4.3.1 and 4.3.2•25 minutes
- Script 4.3.3•10 minutes
6 assignments•Total 50 minutes
- Checking PCTL next•4 minutes
- Checking time-bounded until•16 minutes
- Checking unbounded until•10 minutes
- PCTL Syntax•8 minutes
- Test your understanding of PCTL Until•6 minutes
- Test your understanding of PCTL•6 minutes
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 assignments
5 videos•Total 56 minutes
- Definition of a CTMC•10 minutes
- Generator matrix•11 minutes
- Steady-state probabilities•11 minutes
- Triple Modular Redundancy•11 minutes
- Uniformisation•13 minutes
2 readings•Total 35 minutes
- Script: 5.1 and 5.2•20 minutes
- Script: 5.3•15 minutes
6 assignments•Total 52 minutes
- Generator matrix•6 minutes
- Identifying BSCCs•12 minutes
- Uniformisation•12 minutes
- Test your understanding of CTMCs•6 minutes
- Steady state probability in CTMCs•10 minutes
- Test your understanding of Uniformisation•6 minutes
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 assignments
5 videos•Total 50 minutes
- Model checking CSL•13 minutes
- Model checking and Time-bounded next•8 minutes
- Model checking the steady-state operator•9 minutes
- Time-bounded Until•10 minutes
- An application•9 minutes
2 readings•Total 20 minutes
- Script: 6.1•10 minutes
- Script: 6.2•10 minutes
6 assignments•Total 55 minutes
- Assembly line•10 minutes
- Steady state and next•10 minutes
- Time bounded until in CSL•15 minutes
- Test your understanding of CSL (I)•8 minutes
- Test your understanding of CSL (II)•6 minutes
- Test your understanding of CSL (III)•6 minutes
Instructor
Explore more from Software Development
- Status: Free TrialU
University of Colorado Boulder
Course
- Status: Free TrialU
University of Colorado Boulder
Specialization
- Status: Free TrialU
University of Colorado Boulder
Course
Why people choose Coursera for their career
Learner reviews
- 5 stars
59.25%
- 4 stars
24.07%
- 3 stars
5.55%
- 2 stars
5.55%
- 1 star
5.55%
Showing 3 of 54
Reviewed on Aug 26, 2023
It's not my specialty, just thank you Thanks It's not my specialty, just thank you Thanks It's not my specialty, just thank you Thanks
Frequently asked questions
To access the course materials, assignments and to earn a Certificate, you will need to purchase the Certificate experience when you enroll in a course. You can try a Free Trial instead, or apply for Financial Aid. The course may offer 'Full Course, No Certificate' instead. This option lets you see all course materials, submit required assessments, and get a final grade. This also means that you will not be able to purchase a Certificate experience.
When you enroll in the course, you get access to all of the courses in the Specialization, and you earn a certificate when you complete the work. Your electronic Certificate will be added to your Accomplishments page - from there, you can print your Certificate or add it to your LinkedIn profile.
Yes. In select learning programs, you can apply for financial aid or a scholarship if you can’t afford the enrollment fee. If fin aid or scholarship is available for your learning program selection, you’ll find a link to apply on the description page.
More questions
Financial aid available,