University of Colorado Boulder
Verification and Synthesis of Autonomous Systems
University of Colorado Boulder

Verification and Synthesis of Autonomous Systems

Majid Zamani

Instructor: Majid Zamani

Included with Coursera Plus

Gain insight into a topic and learn the fundamentals.
Intermediate level

Recommended experience

10 hours to complete
3 weeks at 3 hours a week
Flexible schedule
Learn at your own pace
Build toward a degree
Gain insight into a topic and learn the fundamentals.
Intermediate level

Recommended experience

10 hours to complete
3 weeks at 3 hours a week
Flexible schedule
Learn at your own pace
Build toward a degree

What you'll learn

  • Analyze stability properties of linear systems

  • Compute over-approximations of reachable sets for some classes of systems

  • Perform model checking for finite systems

  • Synthesize controllers for safety and reachability specifications for finite systems using fixed-point algorithms

Details to know

Shareable certificate

Add to your LinkedIn profile

Assessments

6 assignments

Taught in English

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

Placeholder

Build your subject-matter expertise

This course is part of the Foundations of Autonomous Systems 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
Placeholder
Placeholder

Earn a career certificate

Add this credential to your LinkedIn profile, resume, or CV

Share it on social media and in your performance review

Placeholder

There are 4 modules in this course

Welcome to the beginning of our exploration into formal verification and synthesis within the model-based design framework. In this introductory module, we will guide you through the key processes of specification, design, verification, and refinement of systems. We will delve into the vital role of formal methods in guaranteeing the correctness of systems. Through captivating examples, we will demonstrate the importance of formal verification, especially in safety-critical and life-critical applications. This module lays the foundation for the more advanced topics we will address throughout the course.

What's included

3 videos7 readings

In this module, we focus on the verification of finite systems, particularly emphasizing regular safety properties and ω-regular properties (including those expressed as linear temporal logic formulae). We will explore a variety of verification techniques and delve into the theoretical underpinnings essential for understanding how finite systems are verified. Through detailed examples and clear, comprehensive explanations, we aim to provide a deep understanding of how these properties are verified in the context of finite systems.

What's included

13 videos1 reading2 assignments

In this module, we explore the synthesis of controllers for finite systems, focusing on enforcing certain linear temporal logic (LTL) formulas, including safety, reachability, persistence, and recurrence. We aim to understand how controllers can be designed to render specific LTL formulas for closed-loop systems. The module provides essential theoretical frameworks and practical algorithms necessary for synthesizing such controllers, with an emphasis on the roles of fixed-point operators and algorithms in the computation processes. Additionally, we will discuss various synthesis techniques that depend on the properties of the system and the involved LTL formulas.

What's included

12 videos1 reading2 assignments

In this module, we will explore the concepts of abstraction and refinement within the context of control systems. We will delve into feedback refinement relations to understand how controllers can be modified or replaced to meet new specifications without altering the overall system behavior. The module also covers the computation of abstractions, demonstrating how we derive abstract models from complex systems to facilitate analysis and design. Additionally, we will discuss practical methods for abstracting different types of control systems, equipping us with the skills to apply theoretical concepts in real-world scenarios.

What's included

9 videos2 readings2 assignments

Instructor

Majid Zamani
University of Colorado Boulder
3 Courses1,216 learners

Offered by

Recommended if you're interested in Software Development

Build toward a degree

This course is part of the following degree program(s) offered by University of Colorado Boulder. If you are admitted and enroll, your completed coursework may count toward your degree learning and your progress can transfer with you.¹

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."

New to Software Development? Start here.

Placeholder

Open new doors with Coursera Plus

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

Advance your career with an online degree

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

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

Upskill your employees to excel in the digital economy

Frequently asked questions