Misc Synthesis Related Functions

Functions in this section are either still experimental or simply did not fit into another section.


Computes the supremal controllable sublanguage w.r.t. forcible/preemptyble events.


SupTconNB(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GSupervisor)

SupTconNB(+In+ Generator GPlant, +In+ EventSet AContr, +In+ EventSet AForcib, +In+ EventSet APreemp, +In+ Generator GSpec, +Out+ Generator GSupervisor)

Detailed description:

The temporal concepts of forcibility and preemptability are most conveniently studied in the context of timed discrete-event systems (TDES). However, the current version of libFAUDES does not provide conversion routines from timed activity graphs to timed discrete-event systems. For the time being, there is only a pragmatic implementation for the synthesis of the following notion of controllability.

Consider two languages L and K over a common alphabet Sigma, a set of uncontrollable events Sigma_uc  Sigma. a set of forcible events Sigma_f  Sigma, and a set of preemptable events Sigma_p  Sigma_uc with Sigma_fSigma_p = 0.

Then K is said to be controllable w.r.t. (L,Sigma_uc,Sigma_f,Sigma_p) iff for all  Closure(K)

sSigma_f  Closure(K) = 0        sSigma_uc  Closure(L)    Closure(K)
sSigma_f  Closure(K) ≠ 0        s(Sigma_uc-Sigma_p)  Closure(L)    Closure(K) .

For Sigma_p = {tick}  Sigma_uc, the above notion of controllability should match the common setting of controllability for TDES.

The function SupTconNB seeks to compute the supremal controllable subset of KL with K = Lm(GCand) and L = Lm(GPlant), referring to the above deefinition. The current implementation inspects the transitions in the product composition GPlant x GCand and removes those which conflict with the definition until a trim generator is obtained.

Parameter Conditions:

This implementation requires the alphabets of plant and specification to match. Furthermore, both generators must be deterministic. Effectively, the specification is intersected with the plant language.

[Experimental!] The implemenation needs more testing -- please report back on unexpected behaiour.

[Note] We should introduce a preemptable flag in the System data-type for more a convenient user interface.


Test consistency of an abstraction w.r.t. standard controller synthesis.


IsStdSynthesisConsistent(+In+ System GPlant, +In+ Generator GPlant0, +Out+ Boolean BRes)

IsStdSynthesisConsistent(+In+ Generator GPlant, +In+ EventSet AContr, +In+ Generator GPlant0, +Out+ Boolean BRes)

Detailed description:

Given a plant and an abstraction thereof, we ask the question whether any controller designed for the abstraction leads to a well-posed closed loop when applied to the actual plant. Answers to this question not only depend on the abstractions under consideration, but also on the detailed set of requirements imposed on the closed loop: on the abstraction level, closed-loop propeties are satisfied by design, while for the actual closed loop they need to be implied by the abstraction at hand.

For the natural projection as an abstraction, the corresponding inverse projection for controller implementation, and the common closed-loop requirements of controllability and non-conflictingness, the above question has been discussed in [S10]. In particular, it is demonstrated by example that the well-studied natural observer property is a sufficient but restrictive condition for an affirmative answer. The below test implements (a variation of) the sufficient and necessary criterion developed in [S10].

Given a plant behaviour L = Lm(GPlant), consider an abstraction Lo = Lm(GPlant0) obtained by natural projection, i.e., Lo = Po(L). Then, the function IsStdSynthesisConsistent returns true if and only if for any controllable and relatively closed sublanguage Ko  Lo, the language Pinvo(Ko)L is a controllable and relatively closed sublanguage of the actual plant L.

Acknowledgement: the initial version of this functions was implemented by Matthias Leinfelder in course of his bachelor thesis.


The below example is taken from [S10] and refers to the alphabets Sigma_o = {r, p, a} and Sigma_c = {a, p}.

Plant GPlant
Abstraction GPlant0

The function IsStdSynthesisConsistent returns true, to indicate that the abstraction is suitable for the common synthesis approach. Note, though, the projection fails to be a natural observer.

Parameter Conditions:

Both generators must be deterministic. The abstraction GPlant0 must have been obtained from the plant GPlant by natural projection; this prerequisit is not tested (!). The set of controllable events must be a subset of the abstraction alphabet specified by GPlant0.


Compute a reduced supervisor.


SupReduce(+In+ System GPlant, +In+ System GSup, +Out+ System GReducedSup)

Detailed description:

Given a plant and a supervisor, this function seeks to compute an alternative supervisor with a reduced state count, while maintaining the closed-loop behaviour. SupReduce returns "true" to indicate success.

The problem of supervisor reduction was first discussed in [S6]. When plant and supervisor are given as gerenators G and S over a common alphabet Sigma, one seeks for a state minimal supervisor S_red and an alphabet Sigma_red such that

G || S   =   G || S_red .

It is shown in [S6] that the above supervisor reduction problem is NP-hard. However, [S6] also provides a polynomial-time algorithm to find a supervisor with a potentially reduced state size. This algorithm is implemented by the function SupReduce


The below example is taken from [S6]. We have

Plant GPlant
Initial Supervisor GSup
Reduced Supervisor GReducedSup

The reduced supervisor has only three states and a reduced alphabet Sigma = {alpha,beta}. In this example, it turns out that the supervisor GSup does not need to take any action in states 1 and 4. Hence, these two states can be merged to state 1 in the reduced supervisor GSupRed. It also has to be noted that the supervisor does not need to take any action if the events gamma or delta occur. Hence, these events do not appear in the alphabet of GSupRed.

Parameter Conditions:

This implementation requires the alphabets of the given plant and supervisor to match. Furthermore, both generators must be deterministic.

libFAUDES 2.32b --- 2024.03.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings"