Equivalences, Abstraction, Partial Order Reduction

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

• Explain and analyze equivalences of transition system models based on bisimulation
• Explain and compare equivalences of transition system models based on simulation relations
• Apply bisimulation and simulation relations to construct and justify abstractions of transition systems
• Analyze independence of concurrent actions and apply this information to perform partial order reductions

• No deep prior experience is required, but basic computer and internet skills are helpful
• Ability to read course instructions in English and complete short practice activities