GitLab

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 -> 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}>
assert E = FE
assert D = FD

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

controller ||C = (Plant)~{G}.

To check if the assumptions are compatible use:

check compatibility ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.

• Supervisory Control
• Reactive Synthesis
• DCS