Course syllabus
7.5 hp, Study Period 1, HT25
The course is offered by the Department of Electrical Engineering
Contact details
Examiner and lecturer
Bengt Lennartson, phone: 0730-79 42 26, bengt.lennartson@chalmers.se
Teaching assistants
Lasse Kötz, kotz@chalmers.se (Please message me on email directly instead of canvas messages.)
Alvin Combrink, combrink@chalmers.se
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-making, especially 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 Period week |
Date, Room | Contents |
|
L1, Ch. 1 |
Monday, Sept 1 |
Introduction. Discrete states, automata, typical models from different application areas, and closed-loop systems. Synchronous composition, specification, verification, controller synthesis, implementation. |
|
L2, Ch. 2 |
Thursday, Sept 4 |
Discrete mathematics. Propositional logic, truth tables, tautological equivalences, and implications. Formal proofs. |
|
L3, Ch. 2 |
Monday, Sept 8 |
Discrete mathematics. Sets, operations on sets, set algebra. Relations and fixed points. Satisfiability solvers. |
|
L4, Ch. 3 |
Thursday, Sept 11 |
Formal models. Automata, sets of states and events, transition relations, partial transition functions, traces, and formal languages. |
|
L5, Ch. 3 |
Monday, Sept 15 |
Formal models. Synchronous composition and language intersection, Petri nets. |
|
L6, Ch. 4, 6 |
Thursday, Sept 18 |
Modeling & Specification. Verification. Specification of desired and non-desired behaviors, marked, forbidden, and reachable states. Controllable and uncontrollable events, verification of controllability. |
|
L7, Ch. 7 |
Monday, Sept 22 |
Controller synthesis. Plant, specification, supervisor synthesis. |
|
L8, Ch. 7 |
Thursday, Sept 25 |
Controller synthesis. Supervisor synthesis algorithm. |
|
L9. Ch. 9 |
Monday, Sept 29 |
Temporal logic and mu-calculus. |
|
L10, Ch. 9 |
Thursday, Oct 2 |
Temporal logic and automata. |
|
L11 |
Monday, Oct 6 |
Reinforcement learning. |
|
L12, Ch. 8 |
Thursday, Oct 9 |
Extended models. Extended finite automata (EFAs), timed, and hybrid automata. |
|
L13, Ch. 8 |
Monday, Oct 13 |
Extended models. Markov chains. Queuing theory, Markov decision processes. |
|
L14 |
Thursday, Oct 16 |
Model reduction. Abstraction by Bisimulation. |
|
L15 |
Monday, Oct 20 |
Summary. Comments on the written examination. |
Exercises
The student is expected to spend a significant amount of time outside of these classes to solve all the problems. Solutions to the exercises are distributed to give additional support.
| Period week | Date, Room | Exercises |
|
Pw 1 |
Thursday, Sept 4 |
Introduction 1.1 - 1.8 Discrete mathematics 2.1 - 2.3 |
|
Pw 2 |
Thursday, Sept 11 |
Discrete mathematics 2.4 - 2.6 |
|
Pw 3 |
Thursday, Sept 18 |
Verification 6.1 - 6.6 |
|
Pw 4 |
Thursday, Sept 25 |
Controller synthesis 7.1 - 7.7 |
|
Pw 5 |
Thursday, Oct 2 |
Temporal Logic 17.5, 20.5, 21.4, 22.4b, 23.3, 24.5 |
|
Pw 6 |
Thursday, Oct 9 |
EFAs 8.1, 17.3, 20.3 Reinforcement Learning 20.6, 21.5, 22.5, 23.4, 24.6 |
|
Pw 7 |
Thursday, Oct 16 |
Markov processes 8.3, 17.6, 23.5 Model reduction 21.6, 22.6, 23.6 |
|
Pw 8 |
Thursday, Oct 23 |
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.
Home assignments
Two 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 in the last years
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. The two first home assignments have been merged into one, meaning that the course now only includes 2 home assignments.
Learning objectives and syllabus
After completion of this course, the student should be able to:
- Use basic discrete mathematics 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 machines, and timed and hybrid automata, and demonstrate skills to choose between them.
- Present different types 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 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 two approved home assignments (Assignments 1 and 2).
The regular examination date is October 31, am, and the first re-sit examination date is January 7, am. 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:
cx4856@gmail.com Xi Cheng
st194087@stud.uni-stuttgart.de Torben Müller
patrik.niens@hotmail.se Patrik Niens
mary.sargolzehi@gmail.com Maryam Sargolzehi
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 |
|---|---|---|