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.

controller ||CONTROLLER = (PLANT)~{SPECIFICATIONS}.

The specification includes various items, some are optional:

• 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.

controllerSpec NAME = {
    safety = { COMMA SEPARATED PROCESS NAMES }
    assumption = { COMMA SEPARATED ASSERTION NAMES }
    liveness = { COMMA SEPARATED ASSERTION NAMES }
    controllable = { NAME OF SET OF LABELS }
}

A concrete example

Plant = (a -> b -> d -> Plant | c -> d -> Plant | e -> AUX), 
AUX = (f -> AUX | g -> Plant).

ltl_property NoB = []!b
fluent FE = <e, {a, b, c, d, f, g}>
fluent FD = <d, {a, b, c, e, f, g}>
fluent FG = <g, {a, b, c, d, e, f}>
assert E = FE
assert D = FD
assert G = FG

controllerSpec Spec = {
	safety = {NoB}
	assumption = {G}
	liveness = {E, D}
	controllable = {a, c, e}
}

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)

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.

As opposed to traditional supervisory control techniques we don't look for maximally permissive supervisors.

Marking states:

There's two ways to specify winning (i.e. marked) states in controllerSpec:

• 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.

Algorithms:

As of the moment there's only one algorithmic option to use in this type of problems, Directed Controller Synthesis. Go to DCS for instructions in how to use it.

Example marking states:

Example = A1,
A1 = (u12 -> A2 |
u14 ->A4),
A2 = (u21 -> A1),
A4 = (c45 ->A5),
A5 = (u55 -> A5).

||Plant = Example.

controllerSpec Goal = {
    controllable = {c45}
    marking = {c45, u55}
    nonblocking
}

heuristic ||DirectedController = Plant~{Goal}.

Example using guarantees (liveness keyword):

Example = A0,
A0 = (a -> A1),
A1 = (c_1 -> Up | u_1 -> Down),
Up = (u_2 -> Up),
Down = (u_3 -> Down).

fluent GoingUp = <u_2, a>
fluent GoingDown = <u_3, a>

assert NeverGonnaGiveYouUp = (!GoingUp && GoingDown)

||Plant = Example.

controllerSpec Goal = {
    liveness = {NeverGonnaGiveYouUp}
    controllable = {c_1}
}

heuristic ||DirectedController = Plant~{Goal}.

• Supervisory Control
• Reactive Synthesis
• DCS