Wenn Sie sich für diesen Kurs anmelden, werden Sie auch für diese Spezialisierung angemeldet.
Lernen Sie neue Konzepte von Branchenexperten
Gewinnen Sie ein Grundverständnis bestimmter Themen oder Tools
Erwerben Sie berufsrelevante Kompetenzen durch praktische Projekte
Erwerben Sie ein Berufszertifikat zur Vorlage
In diesem Kurs gibt es 4 Module
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.
Das ist alles enthalten
12 Videos5 Lektüren3 Aufgaben
Infos zu Modulinhalt anzeigen
12 Videos•Insgesamt 92 Minuten
Introduction•5 Minuten
Bisimulation Equivalence•11 Minuten
Bisimulation Properties•3 Minuten
Bisuimulation Quotent•8 Minuten
The Bakery Algorithm•14 Minuten
CTL* Equivalence•8 Minuten
CTL* Equivalence Example•2 Minuten
Introduction to Bisimulation-Quotienting Algorithms•11 Minuten
Determining the Initial Partition•3 Minuten
Refining Partitions•8 Minuten
A First Partition Refinement Algorithm•4 Minuten
An Efficiency Improvement•14 Minuten
5 Lektüren•Insgesamt 101 Minuten
Course Updates and Accessibility Support•1 Minute
Non-Credit Students: Welcome and Where to Find Help•10 Minuten
Principles of Model Checking - Sections 7.0 and 7.1•30 Minuten
Principles of Model Checking, Section 7.2•30 Minuten
Principles of Model Checking, Section 7.3•30 Minuten
3 Aufgaben•Insgesamt 105 Minuten
Bisimulation•30 Minuten
Bisimulation and CTL*•30 Minuten
Bisimulation-Quotienting Algorithms•45 Minuten
Simulation Relations and Equivalences
Modul 2•4 Stunden abzuschließen
Moduldetails
This module introduces simulations relations and equivalences, their relationship to model checking properties, and algorithms for checking them.
Das ist alles enthalten
10 Videos3 Lektüren3 Aufgaben
Infos zu Modulinhalt anzeigen
10 Videos•Insgesamt 61 Minuten
Simulation Order•8 Minuten
The Use of Simulations•11 Minuten
Simulation Equivalence•7 Minuten
Bisimulation, Simulation, and Trace Equivalence•7 Minuten
Universal Fragment of CTL*•6 Minuten
Existential Fragment of CTL*•3 Minuten
Introduction to Simulation-Quotienting Algorithms•4 Minuten
Simulation Preorder Checking•7 Minuten
First Observation and Improved Algorithm•4 Minuten
Further Improvements•5 Minuten
3 Lektüren•Insgesamt 90 Minuten
Principles of Model Checking, Section 7.4•30 Minuten
Principles of Model Checking, Section 7.5•30 Minuten
Principles of Model Checking, Section 7.6•30 Minuten
3 Aufgaben•Insgesamt 105 Minuten
Simulation Relations•30 Minuten
Simulation and CTL* Equivalence•45 Minuten
Simulation-Quotienting Algorithms•30 Minuten
Stutter Relations and Bisimulation
Modul 3•4 Stunden abzuschließen
Moduldetails
This module introduces stutter linear-time relations, stutter bisimulation, and algorithms for checking them.
Das ist alles enthalten
9 Videos3 Lektüren3 Aufgaben
Infos zu Modulinhalt anzeigen
9 Videos•Insgesamt 69 Minuten
Motivation•3 Minuten
Stutter Trace Equivalence•10 Minuten
Stutter Trace and LTL\O Equivalence•5 Minuten
Definition and Examples of Stutter Bisimulation•11 Minuten
Principles of Model Checking, Section 7.7•30 Minuten
Principles of Model Checking, Sections 7.8 - 7.8.3•30 Minuten
Principles of Model Checking, Sections 7.8.4 and 7.9•30 Minuten
3 Aufgaben•Insgesamt 90 Minuten
Stutter Linear-Time Relations•30 Minuten
Stutter Bisimulation•30 Minuten
Stutter Bisimulation Quotienting•30 Minuten
Partial Order Reduction
Modul 4•3 Stunden abzuschließen
Moduldetails
This module introduces partial order reductions that aovid interleaving independent actions, as well as algorithms for performing partial order reduction.
Das ist alles enthalten
9 Videos3 Lektüren3 Aufgaben
Infos zu Modulinhalt anzeigen
9 Videos•Insgesamt 73 Minuten
Introduction to Partial Order Reduction•7 Minuten
Independence of Actions•5 Minuten
Independence of Actions Examples•4 Minuten
Permuting Independent Actions•8 Minuten
The Linear-Time Approach•8 Minuten
Ample Set Constraints•10 Minuten
Dynamic Partial Order Reduction•11 Minuten
Computing Ample Sets•12 Minuten
The Branching-Time Approach•8 Minuten
3 Lektüren•Insgesamt 90 Minuten
Principles of Model Checking, Sections 8.0 and 8.1•30 Minuten
Principles of Model Checking, Section 8.2•30 Minuten
Principles of Model Checking, Sections 8.3 and 8.4•30 Minuten
3 Aufgaben•Insgesamt 45 Minuten
Independence of Actions•15 Minuten
The Linear-Time Ample Set Approach•15 Minuten
The Branching-Time Ample Set Approach•15 Minuten
Erwerben Sie ein Karrierezertifikat.
Fügen Sie dieses Zeugnis Ihrem LinkedIn-Profil, Lebenslauf oder CV hinzu. Teilen Sie sie in Social Media und in Ihrer Leistungsbeurteilung.
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.