▲

CSCI 7000: Automata for Verification, Synthesis, and Learning

Logistics

Relevant Textbooks

Assignments

Grading

The overall grade will be based on a cumulative score computed by adding together the grades from:

Topics Covered

  1. Regular Languages on Finite Words
  2. Omega-Regular Languages and Büchi Automata
  3. Different Acceptance Conditions for Omega-Automata
  4. Linear Temporal Logic
  5. McNaughton’s Theorem
  6. Parity Automata of Minimum Index
  7. The Topology of $\Sigma^\omega$
  8. Games
  9. Simulation Relations
  10. Alternation
  11. Synthesis of Reactive Games
  12. Tree Automata
  13. Probabilistic Model Checking
  14. Reinforcement Learning with Omega-Rewards

Schedule and Lecture Notes

The schedule of lectures shown below is subject to change. We will post lecture notes or provide pointers to the texbook. We will strive to post all material well in advance. Please take a look through them, and come prepared for class.
# Date Description Chapter
1 Week 1 — August 27 Introduction to the course. Automata on finite words and Regular Expressions. AVS: Chapter 1

Part One: Verification

2 Week 1 — August 29 Automata on finite words: Closure Properties and Pumping Lemma. AVS Chapter 1
3 Week 2 — September 3 Omega Regular Expressions and Büchi Automata AVS Chapter 2
4 Week 2 — September 5 Deterministic an Generalized Büchi Automata, and Closure Properties. AVS Chapter 2
5 Week 3 — September 10 Monadic second-order theory of one successor (S1S) and Büchi Automata. AVS Chapter 2.6
6 Week 3 — September 12< /td> Omega Automata and Various Acceptance Conditions AVS Chapter 3
7 Week 4 — September 17 Linear Temporal Logic AVS Chapter 4
8 Week 4 — September 19 Linear Temporal Logic and Nondeterminsitic Büchi Automata. AVS Chapter 4
9 Week 5 — September 24 McNaughton’s Theorem AVS Chapter 5
10 Week 5 — September 26 McNaughton’s Theorem (Contd.) AVS Chapter 5
11 Week 6 — October 1 Parity Automata of Minimum Index AVS Chapter 6
12 Week 6 — October 3 Topology of $\Sigma^\omega$ AVS Chapter 7
13 Week 7 — October 8 Wrap-up (Automata for Verification).
14 Week 7 — October 10 In-class Quiz

Part Two: Synthesis

15 Week 8 — October 15 Graph Games AVS Chapter 8.1 to 8.6
16 Week 8 — October 17 Algorithms for Parity Games AVS Chapter 8.7
17 Week 9 — October 22 Alternation AVS Chapter 11
18 Week 9 — October 24 Alternation AVS Chapter 11
19 Week 10 — October 29 Reactive Synthesis AVS Chapter 12
20 Week 10 — October 31 Reactive Synthesis (Contd.) AVS Chapter 12
21 Week 11 — November 5 Tree Automata AVS Chapter 13

Part Three: Learning

22 Week 12 — November 7 Markov Decision Processes and Optimal Control
23 Week 13 — November 12 Probabilistic Model Checking
24 Week 13 — November 14 Probabilistic Model Checking (Limit Deterministic Büchi Automata)
25 Week 14 — November 19 Reinforcement Learning
26 Week 14 — November 21 In-Class Quiz II
Week 10 — November 25—November29 No Class — Fall Break
27 Week 11 — December 3 Reinforcement Learning and Omega-Regular Rewards
28 Week 12 — December 5 Learning Automata from Examples
29 Week 13 — December 10 Generative Adversarial Network Games
30 Week 13 — December 12 Wrap-up / Project Presentations.

Notes

  1. Accommodation Statement. If you qualify for accommodations because of a disability, please submit to me a letter from Disability Services in a timely manner (for exam accommodations provide your letter at least one week prior to the exam) so that your needs can be addressed. Disability Services determines accommodations based on documented disabilities. Contact Disability Services at 303-492-8671 or by e-mail at dsinfo [AT] colorado.edu. If you have a temporary medical condition or injury, see Temporary Injuries under Quick Links at the Disability Services website and discuss your needs with me.
  2. Religious Observances. 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 full details here .
  3. 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 differences of race, color, culture, religion, creed, politics, veteran's status, sexual orientation, gender, gender identity and gender expression, age, disability, and nationalities. 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.
  4. Discrimination and Harassment. The University of Colorado Boulder (CU Boulder) is committed to maintaining a positive learning, working, and living environment. CU Boulder will not tolerate acts of sexual misconduct, discrimination, harassment or related retaliation against or by any employee or student. CU's Sexual Misconduct Policy prohibits sexual assault, sexual exploitation, sexual harassment, intimate partner abuse (dating or domestic violence), stalking or related retaliation. CU Boulder's Discrimination and Harassment Policy prohibits discrimination, harassment or related retaliation based on race, color, national origin, sex, pregnancy, age, disability, creed, religion, sexual orientation, gender identity, gender expression, veteran status, political affiliation or political philosophy. Individuals who believe they have been subject to misconduct under either policy should contact the Office of Institutional Equity and Compliance (OIEC) at 303-492-2127. Information about the OIEC, the above referenced policies, and the campus resources available to assist individuals regarding sexual misconduct, discrimination, harassment or related retaliation can be found at the OIEC website.
  5. Honor Code. All students enrolled in a University of Colorado Boulder course are responsible for knowing and adhering to the academic integrity policy of the institution. Violations of the policy may include: plagiarism, cheating, fabrication, lying, bribery, threat, unauthorized access, clicker fraud, resubmission, and aiding academic dishonesty. All incidents of academic misconduct will be reported to the Honor Code Council (honor@colorado.edu; 303-735-2273). Students who are found responsible for violating the academic integrity policy will be subject to nonacademic sanctions from the Honor Code Council as well as academic sanctions from the faculty member. Additional information regarding the academic integrity policy can be found at honorcode.colorado.edu.