Temporal Logic Model Checking

Seize the savings! Get 40% off 3 months of Coursera Plus and full access to thousands of courses.

Temporal Logic Model Checking

This course is part of Fundamentals of Model Checking Specialization

Instructor: Hao Zheng

Included with

Learn more

4 modules

Gain insight into a topic and learn the fundamentals.

Beginner level

Recommended experience

5 weeks to complete

at 10 hours a week

Flexible schedule

Learn at your own pace

4 modules

Gain insight into a topic and learn the fundamentals.

Beginner level

Recommended experience

5 weeks to complete

at 10 hours a week

Flexible schedule

Learn at your own pace

What you'll learn

Identify linear time behavior and specify linear time properties using linear time logic (LTL)
Describe basic concepts of LTL model checking
Specify properties using computation tree logic (CTL)
Describe basic concepts of CTL model checking and its symbolic version

Skills you'll gain

Details to know

Shareable certificate

Add to your LinkedIn profile

Assessments

11 assignments

Taught in English

See how employees at top companies are mastering in-demand skills

Learn more about Coursera for Business

logos of Petrobras, TATA, Danone, Capgemini, P&G and L'Oreal

Build your subject-matter expertise

This course is part of the Fundamentals of Model Checking Specialization

When you enroll in this course, you'll also be enrolled in this Specialization.

Learn new concepts from industry experts
Gain a foundational understanding of a subject or tool
Develop job-relevant skills with hands-on projects
Earn a shareable career certificate

There are 4 modules in this course

This course introduces the basic concepts of functional verification and model checking, highlighting their importance in modern system designs. It explains different modeling formalisms for representing the behavior of hardware and software, which are either suitable for automated analysis or can represent data-dependent controls that are common in computing system designs. Additionally, it describes system compositions with respect to different communication models.

This module introduces concepts of linear-time interpretation of transition systems, and shows how to specify various types of properties on the linear-time behavior.

What's included

13 videos5 readings3 assignments

13 videos Total 130 minutes

Deadlock 12 minutes
Linear Time Behavior 13 minutes
Linear Time Properties 17 minutes
Basic Concepts of Invariant Properties 5 minutes
Algorithms for Checking Invariant Properties 12 minutes
Safety Properties 10 minutes
Trace Equivalence and Safety Properties 6 minutes
Liveness Properties 15 minutes
Checking Liveness Properties - Illustration 11 minutes
Safety Vs Liveness 5 minutes
Concepts of Fairness 8 minutes
Fairness Constraints 9 minutes
Fair Satisfaction of LT Properties 9 minutes

5 readings Total 61 minutes

Course Updates and Accessibility Support 1 minute
Non-Credit Students: Welcome and Where to Find Help 10 minutes
Principles of Model Checking - Section 3.2 20 minutes
Principles of Model Checking - Section 3.3 15 minutes
Principles of Model Checking - Sections 3.4, 3.5.1 15 minutes

3 assignments Total 65 minutes

Linear Time Behavior and Properties 25 minutes
Safety Properties and Invariants 20 minutes
Liveness Properties and Fairness 20 minutes

This module introduces linear-time logic (LTL) for specifying linear-time properties and framework for deciding truth of LTL formulas with respect to transition systems.

What's included

26 videos3 readings3 assignments

26 videos Total 289 minutes

Linear Time Logic (LTL): Syntax 18 minutes
Semantics of LTL 10 minutes
Satisfaction of LTL on Transition Systems 13 minutes
Semantics of Negation 6 minutes
Equivalence of LTL Formulas 17 minutes
Positive Normal Form 13 minutes
Fairness in LTL 11 minutes
Overview of LTL Model Checking 9 minutes
Non-Deterministic Buchi Automata (NBA) 10 minutes
Generalize NBA (GNBA) 7 minutes
GNBA to NBA 10 minutes
Persistency Checking - Concepts 7 minutes
Persistency Checking - Example 12 minutes
Closure & Elementary Sets 14 minutes
Translating LTL Formulas to NBA 17 minutes
A Tutorial on SPIN 8 minutes
Overview of Promela 9 minutes
Process Structure 9 minutes
Promela Statements - Part 1 10 minutes
Promela Statements - Part 2 12 minutes
Promela Statements - Part 3 8 minutes
Operational Semantics - Part 1 10 minutes
Operational Semantics - Part 2 7 minutes
Communication Models 18 minutes
Overview of SPIN Model Checker 12 minutes
Property Specifications 12 minutes

3 readings Total 60 minutes

Principles of Model Checking - Section 5.1 20 minutes
Principles of Model Checking - Sections 4.3, 4.4, 5.2 30 minutes
Online SPIN Tutorial 10 minutes

3 assignments Total 125 minutes

Linear Time Logic: Syntax and Semantics 30 minutes
LTL Model Checking 35 minutes
Getting Familiar with SPIN 60 minutes

This module introduces computation tree logic (CTL) for specifying properties and model checking algorithms for deciding truth of CTL formulas with respect to transition systems.

What's included

13 videos3 readings3 assignments

13 videos Total 148 minutes

Introduction to Computation Tree Logic 9 minutes
CTL Syntax 11 minutes
CTL Semantics 13 minutes
CTL Equivalence and Normal Forms 10 minutes
Expressiveness of CTL Vs LTL 14 minutes
Introduction to CTL Model Checking 8 minutes
Computing the Satisfaction Sets of CTL Formulas - Part 1 10 minutes
Computing the Satisfaction Sets of CTL Formulas - Part 2 10 minutes
Fairness in CTL 8 minutes
CTL Model Checking with Fairness 11 minutes
Counterexamples and Witnesses 19 minutes
Generation of Counterexamples and Witnesses 17 minutes
Counterexamples and Witnesses with Fairness 7 minutes

3 readings Total 60 minutes

Principles of Model Checking - Sections 6.1, 6.2, 6.3 20 minutes
Principles of Model Checking - Sections 6.4, 6.5 30 minutes
Principles of Model Checking - Section 6.6 10 minutes

3 assignments Total 100 minutes

Computational Tree Logic 50 minutes
CTL Model Checking 30 minutes
Counterexamples and Witnesses 20 minutes

This module introduces basic concepts of symbolic model checking, how transition systems can be encoded as switch functions, mode checking algorithms based on switch functions, and BDDs as a compact representation of switch functions.

What's included

16 videos3 readings2 assignments1 peer review

16 videos Total 181 minutes

Introduction to Symbolic CTL Model Checking 16 minutes
Symbolic Encoding of Transition Systems 8 minutes
Symbolic Encoding of Transition Systems - An Example 5 minutes
Symbolic Composition of Transition Systems 8 minutes
Symbolic Image Computation 11 minutes
Symbolic Preimage Computation 11 minutes
Symbolic Computation for Existential Until and Existential Always Operators 14 minutes
Symbolic Model Checking - An Example 9 minutes
Overview of Switching Function Representations 18 minutes
Constructing Reduced OBDDs 8 minutes
Considerations of ROBDDs 7 minutes
Variable Ordering Problem 7 minutes
Boolean Operations in OBDDs 12 minutes
NuSMV Overview 16 minutes
Modeling in NuSMV 13 minutes
Uses of NuSMV 17 minutes

3 readings Total 30 minutes

Principles of Model Checking - Section 6.7, (Page 382-392) 10 minutes
Principles of Model Checking - Section 6.7, (Page 392-407) 10 minutes
NuSMV Tutorial 10 minutes

2 assignments Total 50 minutes

Symbolic Representation of Transition Systems 25 minutes
Ordered Binary Decision Diagrams 25 minutes

1 peer review Total 1,440 minutes

Becoming Familiar with NuSMV 1,440 minutes

Earn a career certificate

Add this credential to your LinkedIn profile, resume, or CV. Share it on social media and in your performance review.

Instructor

Hao Zheng

University of Colorado Boulder

3 Courses 773 learners

Offered by

University of Colorado Boulder

Explore more from Algorithms

Status: Free Trial
University of Colorado Boulder
Introduction to Modeling for Formal Verification
Course
Status: Free Trial
University of Colorado Boulder
Fundamentals of Model Checking
Specialization
28DIGITAL
Automated Reasoning: Symbolic Model Checking
Course
28DIGITAL
Quantitative Model Checking
Course

Why people choose Coursera for their career

Felipe M.

Learner since 2018

"To be able to take courses at my own pace and rhythm has been an amazing experience. I can learn whenever it fits my schedule and mood."

Jennifer J.

Learner since 2020

"I directly applied the concepts and skills I learned from my courses to an exciting new project at work."

Larry W.

Learner since 2021

"When I need courses on topics that my university doesn't offer, Coursera is one of the best places to go."

Chaitanya A.

"Learning isn't just about being better at your job: it's so much more than that. Coursera allows me to learn without limits."

Open new doors with Coursera Plus

Unlimited access to 10,000+ world-class courses, hands-on projects, and job-ready certificate programs - all included in your subscription

Learn more

Advance your career with an online degree

Earn a degree from world-class universities - 100% online

Explore degrees

Join over 3,400 global companies that choose Coursera for Business

Upskill your employees to excel in the digital economy

Learn more

Frequently asked questions

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.

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.

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.