Version:
[release notes]

Module 2: Working with automata

In Module 1, you learned that:

  • Supervisory controllers play an important role in cyber-physical systems, as they ensure that the system operates correctly and safely.
  • Synthesis-based engineering of supervisory controllers combines model-based engineering with computer-aided design, allowing engineers to focus on what the controller should do (the requirements) rather than on how it should do it (the design and implementation).
  • Synthesis-based engineering can help to reduce the effort required to develop and evolve supervisory controllers, and improve the quality of the resulting controllers.
  • Supervisory controller synthesis can automatically generate correct-by-construction supervisory controller models, from models of the uncontrolled system (the plant) and the requirements.
  • For synthesis, the system should be seen as a discrete event system, and the plants and requirements should be modeled using discrete event models.
  • Important concepts of discrete event systems are components, states, state spaces, events, alphabets, transitions and languages.
  • Discrete event systems can be modeled using automata, which primarily consist of locations that model states, and edges that model transitions.
  • Besides using locations to model states, using discrete variables to model states can be convenient to reduce the size of the model.
  • The state of a discrete event system modeled using automata with variables consists of the current locations of the automata, and the current values of the discrete variables.
  • The value of a variable can only be updated using assignments on edges within the same automaton as where the variable is declared.
  • An edge can have a guard that limits when a transition can be performed for the edge, while the updates and target location of the edge then determine the effect on the automaton's state once a transition is performed.
  • The initial state of a system is defined by the initial locations of its automata and the initial values of its variables.
  • Marked locations and variable values indicate states where the system is stable, and are safe havens that the system should be able to return back to.
  • The CIF simulator can be used to simulate CIF models, and analyze their behavior.
  • A water lock allows water vessels to bridge height differences in rivers and canals, consists of various components, and if not controlled properly is prone to various dangerous situations.

In this module, you dive deeper into the concepts related to automata, and you will learn more about using multiple automata that interact. You learn about terms like reachability, deadlock, non-determinism and synchronization. You extend your knowledge of modeling automata with CIF, and learn new ways of using variables. And you will work with more CIF tools.

This module is divided into the following sub-modules: