К содержимому
learnspaceYOUR NEXT CHAPTER
ПРОСТРАНСТВО ОБУЧЕНИЯ
ГлавнаяКаталог курсовМоё обучениеCoursera

Знания без границ

Учитесь у лучших университетов и компаний мира.

Открыть Coursera
Интеграция
Пространство университета
Моё пространствоСтраница курса
↵
ЯЛичный кабинетСтудент
© 2026 LearnSpaceКаждый день — возможность узнать больше.Помощь
Equivalences, Abstraction, and Partial Order Reduction · LearnSpace
Назад в каталог
courseraПрограммирование

Equivalences, Abstraction, and Partial Order Reduction

Курс от University of Colorado Boulder
Начальный≈ 16.9 чАнглийский
О курсеНавыкиПрограммаПреподаватели

О курсе

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

Навыки, которые вы освоите

Verification And ValidationComputer ArchitectureComputational ThinkingLogical ReasoningSoftware Quality (SQA/SQC)Software DesignSystems AnalysisModel OptimizationSystems Design

Программа курса

4 модулей · 66 учебных материалов

01Bisimulation Equivalences20 материалов

Bisimulation

Course Updates and Accessibility SupportЧтениеNon-Credit Students: Welcome and Where to Find HelpЧтениеIntroductionВидеоBisimulation EquivalenceВидео

Учитесь у экспертов

Chris Myers

Professor

Equivalences, Abstraction, and Partial Order Reduction
В каталоге вашей программы

Инвестируйте в себя

Новые знания — в удобное для вас время.

Начать на Coursera

Обучение откроется на Coursera
в новой вкладке

Обучение на Coursera

≈ 16.9 ч

4 модулей

Язык: Английский

Часть программы вашего университета
Bisimulation PropertiesВидео
Bisuimulation QuotentВидео
The Bakery AlgorithmВидео
Principles of Model Checking - Sections 7.0 and 7.1Чтение
BisimulationЗадание

Bisimulation and CTL* Equivalences

CTL* EquivalenceВидеоCTL* Equivalence ExampleВидеоPrinciples of Model Checking, Section 7.2ЧтениеBisimulation and CTL*Задание

Bisimulation-Quotienting Algorithms

Introduction to Bisimulation-Quotienting AlgorithmsВидеоDetermining the Initial PartitionВидеоRefining PartitionsВидеоA First Partition Refinement AlgorithmВидеоAn Efficiency ImprovementВидеоPrinciples of Model Checking, Section 7.3ЧтениеBisimulation-Quotienting AlgorithmsЗадание
02Simulation Relations and Equivalences16 материалов

Simulation Relations

Simulation OrderВидеоThe Use of SimulationsВидеоSimulation EquivalenceВидеоBisimulation, Simulation, and Trace EquivalenceВидеоPrinciples of Model Checking, Section 7.4ЧтениеSimulation RelationsЗадание

Simulation and CTL* Equivalence

Universal Fragment of CTL*ВидеоExistential Fragment of CTL*ВидеоPrinciples of Model Checking, Section 7.5ЧтениеSimulation and CTL* EquivalenceЗадание

Simulation-Quotienting Algorithms

Introduction to Simulation-Quotienting AlgorithmsВидеоSimulation Preorder CheckingВидеоFirst Observation and Improved AlgorithmВидеоFurther ImprovementsВидеоPrinciples of Model Checking, Section 7.6ЧтениеSimulation-Quotienting AlgorithmsЗадание
03Stutter Relations and Bisimulation15 материалов

Stutter Linear-Time Relations

MotivationВидеоStutter Trace EquivalenceВидеоStutter Trace and LTL\O EquivalenceВидеоPrinciples of Model Checking, Section 7.7ЧтениеStutter Linear-Time RelationsЗадание

Stutter Bisimulation

Definition and Examples of Stutter BisimulationВидеоDivergence-Sensitive Stutter BisimulationВидеоStutter Bisimulation and CTL*\O EquivalenceВидеоPrinciples of Model Checking, Sections 7.8 - 7.8.3ЧтениеStutter BisimulationЗадание

Stutter Bisimulation Quotienting

Stutter Bisimulation QuotientingВидеоDivergence-Sensitive Stutter Bisimulation QuotientingВидеоSummaryВидеоPrinciples of Model Checking, Sections 7.8.4 and 7.9ЧтениеStutter Bisimulation QuotientingЗадание
04Partial Order Reduction15 материалов

Independence of Actions

Introduction to Partial Order ReductionВидеоIndependence of ActionsВидеоIndependence of Actions ExamplesВидеоPermuting Independent ActionsВидеоPrinciples of Model Checking, Sections 8.0 and 8.1ЧтениеIndependence of ActionsЗадание

The Linear-Time Ample Set Approach

The Linear-Time ApproachВидеоAmple Set ConstraintsВидеоDynamic Partial Order ReductionВидеоComputing Ample SetsВидеоPrinciples of Model Checking, Section 8.2ЧтениеThe Linear-Time Ample Set ApproachЗадание

The Branching-Time Ample Set Approach

The Branching-Time ApproachВидеоPrinciples of Model Checking, Sections 8.3 and 8.4ЧтениеThe Branching-Time Ample Set ApproachЗадание