Foundations of Autonomous Systems (CSCI 4830, CSCI 7000)

General information:

  • Instructor: Majid Zamani

  • During fall semesters

  • Days: Tuesdays and Thursdays

  • Time: 2:00 PM – 3:15 PM

  • Room: ECES 112

  • Office hours: Mondays, 10:00-11:00, ECCE 1B09

Course Description:

This course will provide an end-to-end overview of different topics involved in designing or analyzing autonomous systems. It begins with explaining the core structure in any autonomous system which includes sensors, actuators, and potentially communication networks. Then, it will cover different formal modeling frameworks used for autonomous systems including state-space representations (difference equations), hybrid automata, and in general labeled transition systems. It also discusses different ways of formally modeling properties of interest for such systems. Examples of such properties include stability, invariance, reachability, and temporal logic properties.

After students get familiar with formally modeling autonomous systems and their properties of interest, the course will cover different techniques on the verification of such systems including Lyapunov functions, reachability, barrier certificates, and potentially model checking. Finally, the course will introduce students with several techniques (e.g. reactive synthesis) on designing controllers (or policies) enforcing properties of interest over the original autonomous systems.

Prerequisites:

  • Basic principles of embedded systems design and some knowledge of differential equations, linear algebra, and calculus.

List of principal topics includes:

  • Formal modeling of autonomous systems:

    • State-space modeling framework

    • Automata

    • Labeled transitions systems

  • Formal pecifications:

    • Stability

    • Invariance

    • Reachability

    • Temporal logic

  • Formal analysis:

    • Lyapunov theory

    • Reachability analysis

    • Barrier certificate

    • Model checking

  • Formal synthesis:

    • Stabilizing feedback controllers

    • Abstraction-based synthesis

    • Control barrier certificate

    • Sampling-based motion planning

Lecture Notes:

  • All lecture notes will be posted on Canvas. Your identikey is needed for signing in.

Recommended textbooks:

  • E. A. Lee and S. A. Seshia. Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, 2017.

  • C. Belta, B. Yordanov, and E. Göl. Formal Methods for Discrete-Time Dynamical Systems. Springer International Publishing, 2017.

  • C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press, 2008.

  • R. Alur. Principles of Cyber-Physical Systems. MIT Press, 2015.

  • P. Tabuada. Verification and Control of Hybrid Systems. Springer US, 2009.

Tentative grading:

  • Assignments: 40%

  • Participation: 10%

  • Midterm exam: 25%

  • Final project: 25%

  • Accommodation for Disabilities
    If you qualify for accommodations because of a disability, please submit your accommodation letter from Disability Services to your faculty member in a timely manner so that your needs can be addressed. Disability Services determines accommodations based on documented disabilities in the academic environment. Information on requesting accommodations is located on the Disability Services website. Contact Disability Services at 303-492-8671 or dsinfo@colorado.edu for further assistance. If you have a temporary medical condition or injury, see Temporary Medical Conditions under the Students tab on the Disability Services website.

  • Classroom Behavior
    Students and faculty each have responsibility for maintaining an appropriate learning environment. Those who fail to adhere to such behavioral standards may be subject to discipline. Professional courtesy and sensitivity are especially important with respect to individuals and topics dealing with race, color, national origin, sex, pregnancy, age, disability, creed, religion, sexual orientation, gender identity, gender expression, veteran status, political affiliation or political philosophy. Class rosters are provided to the instructor with the student's legal name. I will gladly honor your request to address you by an alternate name or gender pronoun. Please advise me of this preference early in the semester so that I may make appropriate changes to my records. For more information, see the policies on classroom behavior and the Student Code of Conduct.

  • Honor Code
    All students enrolled in a University of Colorado Boulder course are responsible for knowing and adhering to the Honor Code. Violations of the policy may include: plagiarism, cheating, fabrication, lying, bribery, threat, unauthorized access to academic materials, clicker fraud, submitting the same or similar work in more than one course without permission from all course instructors involved, and aiding academic dishonesty. All incidents of academic misconduct will be reported to the Honor Code (honor@colorado.edu); 303-492-5550). Students who are found responsible for violating the academic integrity policy will be subject to nonacademic sanctions from the Honor Code as well as academic sanctions from the faculty member. Additional information regarding the Honor Code academic integrity policy can be found at the Honor Code Office website.

  • Sexual Misconduct, Discrimination, Harassment and/or Related Retaliation
    The University of Colorado Boulder (CU Boulder) is committed to fostering a positive and welcoming learning, working, and living environment. CU Boulder will not tolerate acts of sexual misconduct intimate partner abuse (including dating or domestic violence), stalking, protected-class discrimination or harassment by members of our community. Individuals who believe they have been subject to misconduct or retaliatory actions for reporting a concern should contact the Office of Institutional Equity and Compliance (OIEC) at 303-492-2127 or cureport@colorado.edu. Information about the OIEC, university policies, anonymous reporting, and the campus resources can be found on the OIEC website.

    Please know that faculty and instructors have a responsibility to inform OIEC when made aware of incidents of sexual misconduct, discrimination, harassment and/or related retaliation, to ensure that individuals impacted receive information about options for reporting and support resources.

  • Religious Holidays
    Campus policy regarding religious observances requires that faculty make every effort to deal reasonably and fairly with all students who, because of religious obligations, have conflicts with scheduled exams, assignments or required attendance. In this class, you should notify your instructor of any conflict at least two weeks in advance.

    See the campus policy regarding religious observances for full details.