Equivalences, Abstraction, and Partial Order Reduction

Overview

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

Syllabus

Bisimulation Equivalences

This module introduces bisimulation equivalences, its relationship to model checking properties, and algorithms for verifying these equivalences.

Simulation Relations and Equivalences

This module introduces simulations relations and equivalences, their relationship to model checking properties, and algorithms for checking them.

Stutter Relations and Bisimulation

This module introduces stutter linear-time relations, stutter bisimulation, and algorithms for checking them.

Partial Order Reduction

This module introduces partial order reductions that aovid interleaving independent actions, as well as algorithms for performing partial order reduction.