Skip to content

GitLab

Discrete Event Controller Synthesis · Changes

Page history
Update Discrete Event Controller Synthesis authored by Sebastian Uchitel's avatar Sebastian Uchitel
Hide whitespace changes
Inline Side-by-side
Showing with 23 additions and 23 deletions
enduser/Discrete-Event-Controller-Synthesis.md
View page @ 0ae32f45
......@@ -5,13 +5,17 @@ MTSA supports a synthesising behaviour models that control a given plant to sati
controller ||CONTROLLER = (PLANT)~{SPECIFICATIONS}.
```
The specification includes various items, some are optional:
# GR1
For GR1 controller synthesis specification includes various items
* Safety properties. These are process names that describe bad behaviour with error states. They may have been constructed using the property or ltl_property keyword)
* Assumptions. These are names of assertions that must be boolean formulae (i.e., no temporal operators) expressed in terms of fluents. An assertion A is interpreted by the synthesis procedure as []<>A.
* Liveness. As with assumptions, they are boolean formulae and are interpreted as being g preceded by []<>.
* Controllable alphabet. This is the set of events that are controllable by the controller to be synthesised.
The control problem solved is to build an LTS that is deterministic and that when composed with the plant, there are no deadlocks, the plant is never blocked from doing an event that is not controllable, and all traces in the composition satisfy the implication []<> A1 && .. && []<> An -> []<> G1 && .. && Gm where A1, ..., An are assumptions and G1, ..., Gn are liveness goals.
```
controllerSpec NAME = {
safety = { COMMA SEPARATED PROCESS NAMES }
......@@ -21,6 +25,8 @@ controllerSpec NAME = {
}
```
A concrete example
......@@ -48,35 +54,31 @@ controller ||C = (Plant)~{Spec}.
# Compatibility
To check if the assumptions in a controller specification are compatible (i.e., the environment can achieve the assumptions for any controller), which is diserable (see Nicolás Roque D'Ippolito, Victor Braberman, Nir Piterman, and Sebastián Uchitel. 2010. Synthesis of live behaviour models. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (FSE '10). Association for Computing Machinery, New York, NY, USA, 77–86. [pdf](https://doi.org/10.1145/1882291.1882305))
For GR1 specifications, to check if the assumptions are compatible (i.e., the environment can achieve the assumptions for any controller), which is diserable (see Nicolás Roque D'Ippolito, Victor Braberman, Nir Piterman, and Sebastián Uchitel. 2010. Synthesis of live behaviour models. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (FSE '10). Association for Computing Machinery, New York, NY, USA, 77–86. [pdf](https://doi.org/10.1145/1882291.1882305))
```
checkCompatibility ||Compatible = (Plant)~{Spec}.
```
# Supervisory Control
In supervisory control, Discrete Event Systems (DES) are expressed compactly by relying on a modular approach based on the parallel composition of multiple interacting components, referred to as the plant.
Supervisory control aims at controlling DES to achieve certain `guarantees`, this is done by deploying a so-called "supervisor" that dynamically disables `controllable` events while monitoring `uncontrollable` events.
A supervisor is a solution to compositional control problem if, by disabling only controllable events, restricts the plant to states from where marked states are always reachable, but not necessary reached (i.e., uncontrollable events may prevent actually reaching marked states, but may never lead to a deadlock). This is why we will always be using the tag `nonblocking` in `controllerSpec`.
# Non Blocking
As opposed to traditional supervisory control techniques we don't look for maximally permissive supervisors.
MTSA supports synthesis of controllers that achieve non-blocking directors for safety properties. See Daniel Ciolek, Matias Duran, Florencia Zanollo, Nicolas Pazos, Julián Braier, Victor Braberman, Nicolas D’Ippolito, Sebastian Uchitel,
On-the-fly informed search of non-blocking directed controllers, Automatica,
Volume 147, 2023, 110731, ISSN 0005-1098. [pdf](https://doi.org/10.1016/j.automatica.2022.110731).
## Marking states:
There's two ways to specify winning (i.e. marked) states in `controllerSpec`:
To do non-blocking synthesis the controller specification must include the keyword `nonblocking`
* Using the keyword `marking` followed by a set of transition labels.
>Note that we use marked transitions in the controllerGoal, but actually these are internally translated into marked states. If all transitions leading to a state `a` are marked, it all works as expected and `a` is a marked state. If `a` can be reached through marked and non marked transitions, then there will be two states internally, one marked and one not marked, and both will have the same outgoing transitions.
* Using the keyword `liveness` followed by a set of assertions, they will be used as guarantees.
>Currently, when having more than one, it will try to satisfy all at once.
```
controllerSpec ANonBlockingSpecification = {
controllable = {c45}
marking = {c45, u55}
nonblocking
}
```
## Algorithms:
As of the moment there's only one algorithmic option to use in this type of problems, *Directed Controller Synthesis*. Go to [DCS](DCS) for instructions in how to use it.
The states that the controller is expected to never block the plant from having the possibility of reaching can be marked in two ways:
## Example marking states:
* Keyword `marking` within the controller specification can be used to determine a set of transition labels. A marked state is reached if a transition is taken that has a label in the marking transition label set.
```
Example = A1,
......@@ -97,7 +99,7 @@ controllerSpec Goal = {
heuristic ||DirectedController = Plant~{Goal}.
```
## Example using guarantees (liveness keyword):
* Keyword `liveness` followed by a set of assertions can be used to define marked states. Although the syntax is as in GR(1), the interpretation differs. Each liveness goal does not need to occur infinitely often, it must be possible to occur infinitely often instead.
```
Example = A0,
......@@ -122,6 +124,4 @@ heuristic ||DirectedController = Plant~{Goal}.
```
* [Supervisory Control](enduser/supervisoryControl)
* [Reactive Synthesis](enduser/reactiveSynthesis)
* [DCS](enduser/DCS)
\ No newline at end of file