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, 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 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 }
    assumption = { COMMA SEPARATED ASSERTION NAMES }
    liveness = { COMMA SEPARATED ASSERTION NAMES }
    controllable = { NAME OF SET OF LABELS }
}

A concrete example:

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

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 = (System)~{Spec}.
||ControlledSystem = (System || C).

Compatibility

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)

checkCompatibility ||Compatible = (Plant)~{Spec}.

plant keyword

This keyword may be useful for debugging a non-realizable specification (i.e., one that does not have a controller). It returns an LTS that is the composition of the system to be controlled with the safety properties that must be guaranteed. Following example above:

plant ||Plant = (System)~{Spec}.

permissive keyword

This feature has known bugs. Do not use for now.

By default GR1 synthesis commits to a single strategy, keeping only the controllable moves that make progress towards the goal. Adding permissive to the controllerSpec instead produces the maximally permissive controller: it keeps every controllable move that still guarantees the goal, not just the progress-making ones. The result is the largest sub-behaviour of the plant that satisfies the specification — useful when you want to preserve all valid behaviours for later refinement or analysis — at the cost of a larger, non-deterministic controller.

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

controller ||C = (System)~{Spec}.

Reachability

The reachability keyword is used within controllerSpec. When used instead of a GR(1) control problem a reachability one is solved. In other words, the liveness goal must be reached only once.

set ContAlphabet = {c1, c2, c3}

System = (c1 -> System | c2 -> u1 -> AUX | c3 -> u2 -> System), 
AUX = (c2 -> AUX).

fluent Fu1 = <u1, c1>
assert Au1 = Fu1

controllerSpec Spec = {
	liveness = {Au1}
	controllable = ContAlphabet
	reachability

}

controller ||C = (System)~{Spec}.
minimal ||ControlledSystem = (System || C).
checkCompatibility ||Compatible =  (System)~{Spec}.

Non-Blocking

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.

To do non-blocking synthesis the controller specification must include the keyword nonblocking.

In addition, MTSA only supports non-blocking directors (i.e., non maximal) built using directed controller synthesis (DCS) which means that the keyword heuristic must be used.

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.

Example = A1,
A1 = (u1 -> A2 | u3 ->A4),
A2 = (u2 -> A1),
A4 = (c ->A5),
A5 = (u4 -> A5 | c -> A6),
A6 = (u2 -> A6).

||Plant = Example.

controllerSpec Goal = {
    controllable = {c}
    marking = {u4}
    nonblocking
}

heuristic ||DirectedController = Plant~{Goal}.

||ControlledPlant = (DirectedController || Plant).

• 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. Instead of requiring that every infinite trace of the composite plant, sees the liveness goals infinitely often, it requires that every finite trace can be extended (not necessarily controllably) in the controlled plant to see the liveness goals infinitely often.

Example = A0,
A0 = (u1 -> A1),
A1 = (c1 -> Up | c2 -> Down | c3-> Up2),
Up = (up -> Up),
Down = (down -> Down), 
Up2 = (down->up-> Up2).

fluent GoingUp = <up, u1>
fluent GoingDown = <down, u1>

assert NeverGonnaGiveYouUp = (!GoingUp && GoingDown)

||Plant = Example.

controllerSpec Goal = {
    liveness = {NeverGonnaGiveYouUp}
    controllable = {c1, c2, c3}
}

heuristic ||DirectedController = Plant~{Goal}.
||ControlledPlant = (DirectedController || Plant).

Unsupported

The following are unsupported or not yet documented properly

Fluent Activity / Concurrency

These are soft-goal clauses used inside a controllerSpec / controller goal block, telling the heuristic controller synthesiser what to optimise. This functionality is experimental and may not be fully functional.

• concurrencyFluents={...} — names fluents whose simultaneous truth the synthesiser tries to maximise; a non-empty set routes synthesis to a dedicated concurrency-control problem.
• activityFluents={...} — names "activity" fluents the synthesiser tries to keep active; drives the "best controller" heuristic.

To be checked

• controlled_det — controlled determinism
• lazyness — controller laziness parameter
• non_transient — non-transient constraint
• reachability — reachability analysis

DCS / Non-blocking

• heuristic — triggers Directed Controller Synthesis
• marking — marks states for non-blocking synthesis
• disturbances — disturbance specification
• partialOrderReduction — enables partial order reduction
• compositional — compositional synthesis approach
• monolithicDirector — monolithic director synthesis

RTC Controllers

• rtc — Reactive Test Case controller
• rtcAnalysis — RTC analysis controller
• failure — fault/failure specification
• test_latency — test latency specification
• exceptionHandling — exception handling

Updating Controller

• updatingController — updating controller problem
• oldController — reference to the old controller
• oldGoal — old goal specification
• newGoal — new goal specification
• mapping — state mapping
• transition — transition specification
• graphUpdate — graph update specification
• initialState — initial state in the update graph
• transitions — transitions in the update graph

Control Stack

• controlstack — control stack specification
• tier — control tier definition

Exploration

• exploration — exploration specification
• environment — exploration environment
• model — exploration model
• goal — exploration goal
• environment_actions — environment action set

---

← End User