Foundations of Autonomous Systems (CSCI-4830 and CSCI-5854)

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.

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

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.

• 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 Honor Code may include but are not limited to: plagiarism (including use of paper writing services or technology [such as essay bots]), 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. Understanding the course's syllabus is a vital part of adhering to the Honor Code.
  
  All incidents of academic misconduct will be reported to Student Conduct & Conflict Resolution at StudentConduct@colorado.edu. Students found responsible for violating the Honor Code will be assigned resolution outcomes from Student Conduct & Conflict Resolution and will be subject to academic sanctions from the faculty member. Visit the Honor Code website for more information on the academic integrity policy.

• Accommodation for Disabilities, Temporary Medical Conditions, and Medical Isolation
  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, see Temporary Medical Conditions on the Disability Services website.
  
  If you need to miss class or request an adjustment because of a temporary illness, injury, or required medical isolation, please email me as soon as reasonably possible. You do not need to disclose the nature of your condition or provide medical documentation. We will determine an appropriate arrangement for missed work, attendance, or deadlines based on the circumstances and the requirements of the course.

• Accommodation for Religious Obligations
  Instructional faculty members must make every reasonable effort to accommodate all students who have conflicts with scheduled exams, assignment deadlines, or required attendance due to a religious observance. Whenever possible, students must notify the instructional faculty member at least two weeks in advance of the expected exam, assignment deadline, or attendance conflict to request an accommodation for religious observance. If the start date of the course is less than two weeks before the date of the requested accommodation, students must notify the instructional faculty member on the start date of the course. See the Student Academic Accommodations for Religious Observances Policy for more information.
  
  Please email me as early as possible, and whenever possible at least two weeks in advance, if a religious observance conflicts with an exam, assignment deadline, or required class attendance. We will arrange a reasonable alternative without academic penalty.

• Student Names and Pronouns
  CU Boulder recognizes that students’ legal information does not always align with how they identify. If you wish to have a name other than your legal name appear on your instructors’ class rosters and in Canvas, or if you wish to choose pronouns to appear on your instructors’ class rosters and in Canvas, visit the Registrar's website for instructions on how to change your personal information in university systems.

• Classroom Behavior
  Students and faculty are responsible for maintaining an appropriate learning environment in all instructional settings, whether in person, remote, or online. Failure 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, marital status, political affiliation, or political philosophy.
  
  Additional classroom behavior information:
  Student Classroom and Course-Related Behavior Policy.
  Student Code of Conduct.
  Office of Institutional Equity and Compliance.

• Sexual Misconduct, Discrimination, Harassment and/or Related Retaliation
  CU Boulder is committed to fostering a productive and welcoming learning, working, and living environment. University policy prohibits protected-class discrimination and harassment, sexual misconduct (harassment, exploitation, and assault), intimate partner abuse (dating or domestic violence), stalking, and related retaliation by or against members of our community on- or off-campus. Denial of an approved accommodation for disability, religious observance, or pregnancy or pregnancy-related medical conditions may be discriminatory.
  
  The Office of Institutional Equity and Compliance (OIEC) addresses these concerns, and individuals who have been subjected to misconduct can contact OIEC at 303-492-2127 or OIEC@colorado.edu. Information about university policies, OIEC reporting options, and OIEC support resources, including confidential services, can be found on the OIEC website.
  
  Faculty and graduate instructors are required to inform OIEC when someone discloses misconduct, regardless of when or where it occurred. This is to ensure that those impacted receive outreach from OIEC about resolution options and support resources. To learn more about reporting and support options for a variety of concerns, visit the Don't Ignore It page.

• Mental Health and Wellness
  The University of Colorado Boulder is committed to supporting students’ mental health and overall wellbeing. If personal, academic, or emotional challenges are affecting your wellbeing or success, Counseling and Psychiatric Services (CAPS) is here to help. CAPS offers counseling, referrals, psychiatric care, crisis support, and much more. Visit CAPS in the C4C, or call 303-492-2277, 24/7.

• Acceptable Use of AI in This Class
  Generative artificial intelligence tools may be used to support your learning—for example, to brainstorm ideas, clarify concepts, improve the wording of your writing, or help debug code—unless the instructions for a particular assignment state otherwise. These tools may not be used to generate or substantially complete work that you submit as your own.
  
  Any permitted use of generative AI that contributes to submitted work must be acknowledged. Your acknowledgment should identify the tool used and briefly explain how it was used. You remain responsible for the accuracy, originality, and completeness of all submitted work and must be able to explain and defend your solution. Undisclosed or prohibited use of generative AI may be treated as a violation of the Honor Code. Assignment-specific instructions take precedence over this general policy.