Skip to content

GitLab

Discrete Event Controller Synthesis · Changes

Page history
suchitel updated page: Discrete Event Controller Synthesis authored by Sebastian Uchitel's avatar Sebastian Uchitel
Hide whitespace changes
Inline Side-by-side
Showing with 15 additions and 18 deletions
enduser/Discrete-Event-Controller-Synthesis.md
View page @ b8d24337
MTSA supports a synthesising behaviour models that control a given plant to satisfy a given property. The plant is defined using an FSP composite process. The property is defined using the controllerSpec keyword.
MTSA supports synthesising behaviour models that control a given plant to satisfy a given property. The plant is defined using an FSP composite process. The property is defined using the `controllerSpec` keyword.
# GR1
For GR1 controller synthesis specification includes various items
For GR1 controller synthesis, the 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.
* 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 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.
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 = {
......@@ -21,10 +21,7 @@ controllerSpec NAME = {
}
```
A concrete example
A concrete example:
```
Plant = (a -> b -> d -> Plant | c -> d -> Plant | e -> AUX),
......@@ -50,7 +47,7 @@ controller ||C = (Plant)~{Spec}.
# Compatibility
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))
For GR1 specifications, to check if the assumptions are compatible (i.e., the environment can achieve the assumptions for any controller), which is desirable (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}.
......@@ -58,11 +55,11 @@ checkCompatibility ||Compatible = (Plant)~{Spec}.
# Non Blocking
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,
MTSA supports synthesis of controllers that achieve non-blocking control 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).
To do non-blocking synthesis the controller specification must include the keyword `nonblocking`
To do non-blocking synthesis the controller specification must include the keyword `nonblocking`.
```
controllerSpec ANonBlockingSpecification = {
......@@ -72,9 +69,9 @@ controllerSpec ANonBlockingSpecification = {
}
```
The states that the controller is expected to never block the plant from having the possibility of reaching can be marked in two ways:
The states that the controller is expected to never block the plant from having the possibility of reaching can be marked in two ways:
* 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.
* 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,
......@@ -95,7 +92,7 @@ controllerSpec Goal = {
heuristic ||DirectedController = Plant~{Goal}.
```
* 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.
* 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,
......@@ -120,4 +117,4 @@ heuristic ||DirectedController = Plant~{Goal}.
```
---
[← End User](End-User)
\ No newline at end of file
[← End User](End-User)