Course syllabus
Logic, Learning, and Decision
SSY165, 7.5 hp, Study Period 1, HT23
The course is offered by the Department of Electrical Engineering
Contact details
Examiner and lecturer
Bengt Lennartson, phone: 031-772 3722, bengt.lennartson@chalmers.se
Teaching assistants
Ludvig Svedlund, ludvige@chalmers.se
Alvin Combrink, combrink@chalmers.se
Office Hours: Tuesdays and Fridays, 12:30 - 13:15, online on request (see Zoom Links)
Tuesdays: Room 5434 Edith Building
Fridays: Room 5324 Edith Building
Exam Office
Room EDIT 3342, studadm.e2@chalmers.se
Course purpose
The course aims to give fundamental knowledge and skills in the area of logic, learning, and decision, especially on modeling and specification formalisms, simulation, synthesis, optimization, and control function implementation. Typical applications are control functions for embedded systems, control of automated production systems, and communication systems.
Schedule
Course literature
Logic, Learning, and Decision, Bengt Lennartson. Lecture Notes 2023, to be downloaded from Files.
Logic, Learning, and Decision - Exercises, 2023, to be downloaded from Files.
Lecture Program
| Lecture nr/ Book chapter | Date, Room | Contents |
|
L1, Ch. 1 |
Monday, Aug 28 |
Introduction. Discrete states, automata, typical models from different application areas, and closed-loop systems. Synchronous composition, specification, verification, controller synthesis, implementation. |
|
|
Thursday, Aug 31 |
No lecture. |
|
L2, Ch. 2 |
Monday, Sept 4 |
Discrete mathematics. Propositional logic, truth tables, tautological equivalences, and implications. Formal proofs. Sets, operations on sets, set algebra. |
|
L3, Ch. 3 |
Thursday, Sept 7 |
Formal models. Automata, sets of states and events, transition relations, partial transition functions, traces, formal languages. |
|
L4, Ch. 3 |
Monday, Sept 11 |
Formal models. Synchronous composition and language intersection, Petri nets. |
|
L5, Ch. 4, 6 |
Thursday, Sept 14 |
Modeling & Specification. Verification. Specification of desired and non-desired behaviors, marked, forbidden, and reachable states. Controllable and uncontrollable events, verification of controllability. |
|
L6, Ch. 7 |
Monday, Sept 18 |
Controller synthesis. Plant, specification, supervisor synthesis. |
|
L7, Ch. 7 |
Thursday, Sept 21 |
Controller synthesis. Supervisor synthesis algorithm. |
|
L8. Ch. 8 |
Monday, Sept 25 |
Extended models. Extended finite automata, timed automata, hybrid automata. |
|
L9, Ch. 9 |
Thursday, Sept 28 |
Temporal logic. |
|
L10, Ch. 9 |
Monday, Oct 2 |
Temporal logic. mu-calculus. |
|
L11, Ch. 10 |
Thursday, Oct 5 |
Reinforcement learning. |
|
L12, Ch. 8 |
Monday, Oct 9 |
Extended models. Markov chains. Queuing theory, Markov decision processes. |
|
L13, Ch 11 |
Thursday, Oct 12 |
Model reduction. Abstraction by Bisimulation. |
|
L14 |
Monday, Oct 16 |
Summary. Comments on the written examination. |
Exercises
The student is expected to spend a significant amount of time besides these classes to solve all the problems. Solutions to the exercises are distributed to give additional support.
| Date, Room | Exercises | |
|
pw 1 |
Thursday, Aug 31 |
Introduction 1.1 - 1.8 |
|
pw 2 |
Thursday, Sept 7 |
Discrete mathematics 2.1 - 2.6 |
|
pw 3 |
Thursday, Sept 14 |
Modeling and specification 4.1 - 4.9 |
|
pw 4 |
Thursday, Sept 21 |
Verification 6.1 - 6.6 |
|
pw 5 |
Thursday, Sept 28 |
Controller synthesis 7.1 - 7.7 |
|
pw 6 |
Thursday, Oct 5 |
Temporal Logic |
|
pw 7 |
Thursday, Oct 12 |
Markov processes, Reinforcement Learning |
|
pw 8 |
Thursday, Oct 19 |
Questions and preparations for the exam |
Exercise self-activity and support for home assignments
From period week two, a self-activity and support session for exercises and home assignments is offered on Wednesday, 8-10, SB-M022, except 20 Sept, 8-10, SB-M300.
Home assignments
Three mandatory home assignments, and one optional introductory assignment, are included in the course. These activities are performed in two-member groups. We strongly recommend completing the introductory assignment as preparation for the mandatory ones.
Changes made since the last occasion
Course name changed from Discrete Event Systems to Logic, Learning, and Decision. The topic on Reinforcement Learning is extended to also include continuous state space models.
Learning objectives and syllabus
After completion of this course, the student should be able to:
- Use basic discrete mathematics in order to be able to analyze discrete event systems.
- Give an account of different formalisms for modeling discrete event systems, especially finite state automata, formal languages, Petri nets, extended finite state automata, timed and hybrid automata, and demonstrate skills to choose between them.
- Present different kinds of specifications, such as progress and safety specifications, defining what a system should and should not do.
- Compute and analyze different properties of discrete event systems such as reachability, coreachability, and controllability.
- Explain the meaning of supervisor synthesis, verification, and simulation.
- Use computer tools in order to perform synthesis and optimization of control functions based on given system models and specifications of desired behavior for the total closed-loop system.
- Formulate and analyze hybrid systems including discrete and continuous dynamics.
- Specify temporal logic properties and verify them by mu-calculus.
- Explain and apply basic Markov processes and queuing theory for performance analysis of systems including uncertainties.
- Apply reinforcement learning based on the dynamic programming principle.
Link to the syllabus on Studieportalen: Study plan
Examination form
Final grade requires an approved written examination and three approved home assignments (assignments 1, 2, and 3).
Regular examination date is October 23, am, and first re-sit examination date is January 3, pm. Allowed aids at the examination: Standard mathematical tables such as Beta.
Course representatives
The following students have been elected by the student administration to be course representatives in the course evaluation:
Junzhao Cheng 492618333@qq.com
Anish Janardhan janardhananish@gmail.com
Elisa Lafont elisa.lafont@insa-lyon.fr
Ajay Nayak ajaynayak1998@gmail.com
Niclas Persson niclaspe@student.chalmers.se
Yinsong Wang wangyinsong01@gmail.com
To be a study representative means that you will be involved in the course evaluation process. See more details at https://www.chalmers.se/en/education/your-studies/plan-and-conduct-your-studies/course-evaluation/
Course summary:
| Date | Details | Due |
|---|---|---|