182.764 Logical Foundations of Cyber-Physical Systems
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2019S, VU, 4.0h, 6.0EC

Properties

  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise

Aim of course

The technological developments of the past two decades have nurtured a fascinating convergence of computer science and electrical, mechanical and biological engineering. Nowadays, computer scientists work hand in hand with engineers to model, analyze and control complex systems, that exhibit discrete as well as continuous behavior. Examples of such systems include automated highway systems, air traffic management, automotive controllers, robotics and real-time circuits. They also include biological systems, such as immune response, bio-molecular networks, gene- regulatory networks, protein-signaling pathways and metabolic processes.

The more pervasive and more complex these systems become, the more is the infrastructure of our modern society relying on their dependability. Traditionally however, the modeling, analysis and control theory of discrete systems is quite different from the one of continuous systems. The first is based on automata theory, a branch of discrete mathematics, where time is typically abstracted away. The second is based on linear systems theory, of differential (or difference) equations, a branch of continuous mathematics where time is of essence. This course is focused on the principles underlying their combination. By the end of this course the students will be provided with detailed knowledge and substantial experience in the mathematical modeling, analysis and control of hybrid systems.

Subject of course

Hybrid automata as discrete-continuous models of hybrid systems. Executions and traces of hybrid automata. Infinite transition systems as a time-abstract semantics of hybrid automata.  Finite abstractions of infinite transition systems. Language inclusion and language equivalence. Simulation and bisimulation. Quotient structures. Approximate notions of inclusion and simulation. State logics, and model checking. Partition-refinement and model checking within mu-calculus. Classes of hybrid automata for which the model-checking problem is decidable. Modern overapproximation techniques for reachability analysis. Simulation-based verification techniques. Controller synthesis problem for exact and approximate quotient structures. Stability, Lyapunov functions and differential invariants. Modern analysis and controller synthesis tools.

Didactic concept: The theoretical knowledge obtained in the lecture will be practiced in several exercises solved in groups.

Additional information

ECTS-Breakdown 3 ECTS = 150 hours:

  • 0.5h  lecture introduction
  • 54h (18 lectures, 2h per lecture + 1h pre/postprocessing)
  • 75h exercises
  • 20h exam preparation
  • 0.5h  oral exam
    ------
    150h

Literature

  • Lygeros, Tomlin, Sastry. Hybrid Systems: Modeling analysis and control
  • Tabuada. Verification and control of hybrid systems: A symbolic approach
  • Lee and Varaiya. Structure and interpretation of signals and systems
  • Alur. Principles of Embedded Computation
  • Lee and Seshia. Introduction to Embedded Systems: A CPS Approach
  • Clarke, Grumberg and Peled. Model checking
  • Hefferon, Linear Algebra
  • Linear Algebra Video Lecture by Gilbert Strang

Verification Tools

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Tue10:00 - 12:0005.03.2019 - 25.06.2019 Treitlstrasse 3/3, LibraryLecture Dates
Thu10:00 - 12:0007.03.2019 - 27.06.2019 Treitlstrasse 3/3, LibraryLecture Dates
Logical Foundations of Cyber-Physical Systems - Single appointments
DayDateTimeLocationDescription
Tue05.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu07.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue12.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu14.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue19.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu21.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue26.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu28.03.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue02.04.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu04.04.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue09.04.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu11.04.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue30.04.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu02.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue07.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu09.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue14.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu16.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Tue21.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates
Thu23.05.201910:00 - 12:00 Treitlstrasse 3/3, LibraryLecture Dates

Examination modalities

  • Oral exam
  • Submitted exercises

Course registration

Begin End Deregistration end
19.02.2019 08:00 11.03.2019 23:59

Registration modalities:

Registration to the course via TISS. You will be added to the TUWEL course, where the rest of the course will be organized.

Curricula

Study CodeSemesterPrecon.Info
066 938 Computer Engineering

Literature

No lecture notes are available.

Previous knowledge

Familiarity with elementary discrete and continuous mathematics, signals and systems and the control theory. Fluency in devising and writing simple mathematical proofs.

In particular, knowledge about the following topics is highly recommended:

  • mathematics: (simulation of) difference/differential equations, approximation, linear algebra, discrete mathematics
  • computer science: finite automata theory, logics and boolean algebra, first order logic, temporal logics, abstractions, model checking, formal verification
  • control theory: signals and systems, observability, controllability, stability

Courses that cover these topics (additional to computer engineering undergraduate courses like Signals and Systems 1 and 2): Discrete Mathematics, Formal Methods of Computer Science

Language

English