When you enroll in this course, you'll also be enrolled in this Specialization.
Learn new concepts from industry experts
Gain a foundational understanding of a subject or tool
Develop job-relevant skills with hands-on projects
Earn a shareable career certificate
There are 4 modules in this course
This course introduces methods to utilize abstraction and partial order methods to reduce the complexity of their systems models. The equivalences introduced are based upon bisimulation and simulation relations. These concepts allow one to prove that a model is an abstraction (or simplification) of another model of the same system. Abstraction reduces the complexity of the system model while preserving the ability to correctly verify properties of the system. This course will also introduce the partial order method to further reduce model complexity during verification by enabling the state space exploration to not need to consider all possible interleavings of concurrent events. This approach often provides substantial reductions in the state space of the model being verified.
This course can be taken for academic credit as part of CU Boulder’s Master of Science in Electrical and Computer Engineering (MS-ECE) degree offered on the Coursera platform. The degree offers targeted courses, short 8-week sessions, and pay-as-you-go tuition. Admission is based on performance in three preliminary courses, not academic history. CU degrees on Coursera are ideal for recent graduates or working professionals. Learn more:
MS in Electrical and Computer Engineering: https://www.coursera.org/degrees/msee-boulder
This module introduces bisimulation equivalences, its relationship to model checking properties, and algorithms for verifying these equivalences.
What's included
12 videos5 readings3 assignments
Show info about module content
12 videos•Total 92 minutes
Introduction•5 minutes
Bisimulation Equivalence•11 minutes
Bisimulation Properties•3 minutes
Bisuimulation Quotent•8 minutes
The Bakery Algorithm•14 minutes
CTL* Equivalence•8 minutes
CTL* Equivalence Example•2 minutes
Introduction to Bisimulation-Quotienting Algorithms•11 minutes
Determining the Initial Partition•3 minutes
Refining Partitions•8 minutes
A First Partition Refinement Algorithm•4 minutes
An Efficiency Improvement•14 minutes
5 readings•Total 101 minutes
Course Updates and Accessibility Support•1 minute
Non-Credit Students: Welcome and Where to Find Help•10 minutes
Principles of Model Checking - Sections 7.0 and 7.1•30 minutes
Principles of Model Checking, Section 7.2•30 minutes
Principles of Model Checking, Section 7.3•30 minutes
3 assignments•Total 105 minutes
Bisimulation•30 minutes
Bisimulation and CTL*•30 minutes
Bisimulation-Quotienting Algorithms•45 minutes
Simulation Relations and Equivalences
Module 2•4 hours to complete
Module details
This module introduces simulations relations and equivalences, their relationship to model checking properties, and algorithms for checking them.
What's included
10 videos3 readings3 assignments
Show info about module content
10 videos•Total 61 minutes
Simulation Order•8 minutes
The Use of Simulations•11 minutes
Simulation Equivalence•7 minutes
Bisimulation, Simulation, and Trace Equivalence•7 minutes
Universal Fragment of CTL*•6 minutes
Existential Fragment of CTL*•3 minutes
Introduction to Simulation-Quotienting Algorithms•4 minutes
Simulation Preorder Checking•7 minutes
First Observation and Improved Algorithm•4 minutes
Further Improvements•5 minutes
3 readings•Total 90 minutes
Principles of Model Checking, Section 7.4•30 minutes
Principles of Model Checking, Section 7.5•30 minutes
Principles of Model Checking, Section 7.6•30 minutes
3 assignments•Total 105 minutes
Simulation Relations•30 minutes
Simulation and CTL* Equivalence•45 minutes
Simulation-Quotienting Algorithms•30 minutes
Stutter Relations and Bisimulation
Module 3•4 hours to complete
Module details
This module introduces stutter linear-time relations, stutter bisimulation, and algorithms for checking them.
What's included
9 videos3 readings3 assignments
Show info about module content
9 videos•Total 69 minutes
Motivation•3 minutes
Stutter Trace Equivalence•10 minutes
Stutter Trace and LTL\O Equivalence•5 minutes
Definition and Examples of Stutter Bisimulation•11 minutes
Principles of Model Checking, Section 7.7•30 minutes
Principles of Model Checking, Sections 7.8 - 7.8.3•30 minutes
Principles of Model Checking, Sections 7.8.4 and 7.9•30 minutes
3 assignments•Total 90 minutes
Stutter Linear-Time Relations•30 minutes
Stutter Bisimulation•30 minutes
Stutter Bisimulation Quotienting•30 minutes
Partial Order Reduction
Module 4•3 hours to complete
Module details
This module introduces partial order reductions that aovid interleaving independent actions, as well as algorithms for performing partial order reduction.
What's included
9 videos3 readings3 assignments
Show info about module content
9 videos•Total 73 minutes
Introduction to Partial Order Reduction•7 minutes
Independence of Actions•5 minutes
Independence of Actions Examples•4 minutes
Permuting Independent Actions•8 minutes
The Linear-Time Approach•8 minutes
Ample Set Constraints•10 minutes
Dynamic Partial Order Reduction•11 minutes
Computing Ample Sets•12 minutes
The Branching-Time Approach•8 minutes
3 readings•Total 90 minutes
Principles of Model Checking, Sections 8.0 and 8.1•30 minutes
Principles of Model Checking, Section 8.2•30 minutes
Principles of Model Checking, Sections 8.3 and 8.4•30 minutes
3 assignments•Total 45 minutes
Independence of Actions•15 minutes
The Linear-Time Ample Set Approach•15 minutes
The Branching-Time Ample Set Approach•15 minutes
Earn a career certificate
Add this credential to your LinkedIn profile, resume, or CV. Share it on social media and in your performance review.
CU Boulder is a dynamic community of scholars and learners on one of the most spectacular college campuses in the country. As one of 34 U.S. public institutions in the prestigious Association of American Universities (AAU), we have a proud tradition of academic excellence, with five Nobel laureates and more than 50 members of prestigious academic academies.
When will I have access to the lectures and assignments?
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.
What will I get if I subscribe to this Specialization?
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.
Is financial aid available?
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.