Lorsque vous vous inscrivez à ce cours, vous êtes également inscrit(e) à cette Spécialisation.
Apprenez de nouveaux concepts auprès d'experts du secteur
Acquérez une compréhension de base d'un sujet ou d'un outil
Développez des compétences professionnelles avec des projets pratiques
Obtenez un certificat professionnel partageable
Il y a 4 modules dans ce cours
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.
Inclus
12 vidéos5 lectures3 devoirs
Afficher les informations sur le contenu du module
12 vidéos•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 lectures•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 devoirs•Total 105 minutes
Bisimulation•30 minutes
Bisimulation and CTL*•30 minutes
Bisimulation-Quotienting Algorithms•45 minutes
Simulation Relations and Equivalences
Module 2•4 heures à terminer
Détails du module
This module introduces simulations relations and equivalences, their relationship to model checking properties, and algorithms for checking them.
Inclus
10 vidéos3 lectures3 devoirs
Afficher les informations sur le contenu du module
10 vidéos•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 lectures•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 devoirs•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 heures à terminer
Détails du module
This module introduces stutter linear-time relations, stutter bisimulation, and algorithms for checking them.
Inclus
9 vidéos3 lectures3 devoirs
Afficher les informations sur le contenu du module
9 vidéos•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 devoirs•Total 90 minutes
Stutter Linear-Time Relations•30 minutes
Stutter Bisimulation•30 minutes
Stutter Bisimulation Quotienting•30 minutes
Partial Order Reduction
Module 4•3 heures à terminer
Détails du module
This module introduces partial order reductions that aovid interleaving independent actions, as well as algorithms for performing partial order reduction.
Inclus
9 vidéos3 lectures3 devoirs
Afficher les informations sur le contenu du module
9 vidéos•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 lectures•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 devoirs•Total 45 minutes
Independence of Actions•15 minutes
The Linear-Time Ample Set Approach•15 minutes
The Branching-Time Ample Set Approach•15 minutes
Obtenez un certificat professionnel
Ajoutez ce titre à votre profil LinkedIn, à votre curriculum vitae ou à votre CV. Partagez-le sur les médias sociaux et dans votre évaluation des performances.
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.
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?
Felipe M.
Étudiant(e) depuis 2018
’Pouvoir suivre des cours à mon rythme à été une expérience extraordinaire. Je peux apprendre chaque fois que mon emploi du temps me le permet et en fonction de mon humeur.’
Jennifer J.
Étudiant(e) depuis 2020
’J'ai directement appliqué les concepts et les compétences que j'ai appris de mes cours à un nouveau projet passionnant au travail.’
Larry W.
Étudiant(e) depuis 2021
’Lorsque j'ai besoin de cours sur des sujets que mon université ne propose pas, Coursera est l'un des meilleurs endroits où se rendre.’
Chaitanya A.
’Apprendre, ce n'est pas seulement s'améliorer dans son travail : c'est bien plus que cela. Coursera me permet d'apprendre sans limites.’
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.