




Controllable SublanguagesFunctions related to the notion of controllability and (basic) supervisory control. Definition of ControllabilityThe notion of controllability was originally introduced by P.J. Ramadge and W.M. Wonham, e.g. [S1]:
Consider two languages L and K over a common alphabet Sigma,
and a set of uncontrollable events Sigma_uc ⊆ Sigma.
Then K is said to be controllable w.r.t. (L,Sigma_uc) iff
The definition addresses the situation where K is the closedloop behaviour that has been achieved by supervision of a plant L. Whenever, after some past string s ∈ Closure(K), the uncontrollable event o ∈ Sigma_uc is accepted by the plant Closure(L), it must also be accepted by the controller and, hence, cannot be rejected in the closed loop Closure(K). Controller SynthesisFor the purpose of controller synthesis, consider a plant L ⊆ Sigma*, a specification E ⊆ Sigma*, and, uncontrollable events Sigma_uc ⊆ Sigma. The task then is to find a prefix closed controller H ⊆ Sigma*, such that
(1)
L and H are nonblocking, i.e.,
Closure(L ∩ H) = Closure(L) ∩ H ;
For any prefix closed controller H which satisfies the above conditions, the closed loop K = L ∩ H exhibits the following properties:
(a)
K is relatively closed w.r.t. L, i.e., K = L ∩ Closure(K);
Moreover, if a language K satisfies (a)(c), the controller H = Closure(K) solves the synthesis problem.
A fundamental result presented in [S1] is that
all of the conditions (a)(c) are retained under
arbitrary union. Thus, the set of all achievable closedloop behaviours
forms a complete upper semilattice. In particular,
the supremum
An example is given at the main page of the Synthesis plugin. Note 1: In the literature the supervisor is commonly represented by a map V that maps past observations s ∈ Closure(L) to control patterns V(s) = \gamma, Sigma_uc ⊆ \gamma ⊆ Sigma. The closedloop behaviour of L under supervison V is then defined by the condition, that at each instance of time an event can only occur if it complies with the plant behaviour and the current control pattern. However, for the scope of this documentation, we feel that a simplified presentation purely in terms of languages is preferable. Note 2: For the above problem of controller synthesis the plant is represented as a single language L. For the situation, where the plant is more adequatly modelled by a generator that fails to be nonblocking, i.e. L(G) ≠ Closure(Lm(G)), one may proceed with L = L(G) and employ a specification E ⊆ Lm(G) to design a marking controller that avoids blocking; see also SupConNB. IsControllableTests controllablity condition. Signature:IsControllable(+In+ Generator GPlant, +In+ EventSet ACntrl, +In+ Generator GCand, +Out+ Boolean BRes) IsControllable(+In+ System GPlant, +In+ Generator GCand, +Out+ Boolean BRes) Detailed description:This function tests controllability of L(GCand) w.r.t. (L(GPlant),Sigma_uc). The set of uncontrollable events Sigma_uc is either taken from the plant event attributes or specified as the complement of the parameter ACntrl. Since the definition of controllability exclusively refers to the closure of the relevant languages, this function can be also used to test controllability of Lm(GCand) w.r.t. (Lm(GPlant),Sigma_uc), provided that the specified generators are nonblocking. This can be achieved by applying Trim before calling IsControllable. The current implementation performs the test by inspecting the transitions in the product composition GPlant x GCand. If GCand disables a transition in GPlant that is labled with an uncontrollable event, the function returns "false". Else, it returns "true". Example:Consider the very simple machine scenario. We have
In the product composition, the state BBF disables the uncontrollable event beta_1 since the buffer is full and cannot take any workpiece. However, in the corresponding plant state BB, the event beta_1 is enabled, since machine M1 is busy and may on completion pass on the workpiece. Thus, the specification is not controllable w.r.t. the plant and the function IsControllable returns "false" when applied to GPlant and GSpec. 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. SupConClosedComputes the supremal controllable sublanguage. Signature:SupConClosed(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GSupervisor) SupConClosed(+In+ Generator GPlant, +In+ EventSet AContr, +In+ Generator GSpec, +Out+ Generator GSupervisor) Detailed description:
Given a plant L = L(GPlant) and a specification E = L(GSpec),
this function computes the supremal controllable and closed sublanguage K ⊆ E∩L:
Clearly, K↑ satisfies the closedloop conditions (a)(c). In particular, H = K↑ solves the synthesis problem. Example:For verysimple machine example, it happens that SupConClosed returns the same generator as SupConNB does. However, for SupConClosed the result is interpreted as the generated language. 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. SupConNBComputes the supremal controllable sublanguage. Signature:SupConNB(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GSupervisor) SupConNB(+In+ Generator GPlant, +In+ EventSet AContr, +In+ Generator GSpec, +Out+ Generator GSupervisor) Detailed description:
Given a plant realisation G (argument GPlant) and a
specification E = Lm(GSpec), this function
computes the supremal controllable sublanguage K↑ ⊆ E∩Lm(G):
For the synthesis problem in this documentation, we assume that G is nonblocking. Here, K↑ satisfies the closedloop conditions (b) and (c). In addition, K↑ can be observed to be relatively prefixclosed w.r.t. E. If the specification E is relatively marked w.r.t. the plant Lm(G) (see also IsRelativelyMarked), this implies that K↑ is relatively prefixclosed w.r.t. Lm(G), i.e., K↑ also fulfills the closedloop condition (a) and the controller H = Closure(K↑) solves the synthesis problem.
If the specification E fails to be relatively marked w.r.t. the plant L,
one may replace E with the supremal sublanguage that is relatively closed
(see also SupRelativelyPrefixClosed) before invoking SupConNB,
to obtain
Alternatively, one may resort to a so called marking supervisor H = K↑ that only satisfies conditions (b) and (c). From H ⊆ L, the marking of the supervisor implies the marking of the plant and we can implement the closed loop as the intersection Closure(L)∩H, hence the notion of a marking supervisor. The nonblocking condition then becomes formally Closure(Closure(L)∩H) = Closure(L)∩Closure(H), which, by H ⊆ L, is trivially satisfied. Example:The supervisor given for the verysimple machine example has been obtained by SupConNB. It failes to be relativelyclosed and thus is interpreted as a marking supervisor. 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. IsRelativelyPrefixClosedTest for relative prefixclosedness. Signature:IsRelativelyPrefixClosed(+In+ Generator GPlant, +In+ Generator GCand, +Out+ Boolean BRes) Detailed description:
A language K is relatively closed w.r.t. a language
L, if K can be recovered from its closure and L.
Formally:
Here, QPlant_m and QCand_m refer to the marked states of GPlant and GCand, respectively. The function returns "true" if both conditions are fulfilled. Example:Consider the very simple machine scenario.
The string alpha_1 beta_1 is within the languages generated by the supervisor and the plant respectively. It is not within the language marked by the supervisor, since that language is a subset of the language marked by the specification and thus requires the buffer to be empty. In particular, the string alpha_1 beta_1 witnesses a violation of relative closedness condition and the function IsRelativelyPrefixClosed returns "false" when applied to GPlant and GSupervisor. Parameter Conditions:This implementation requires the alphabets of both generators to match. Furthermore, both specified generators must be deterministic and nonblocking. IsRelativelyMarkedTest for relative marking. Detailed description:
A language K is relatively marked w.r.t. a language
L, if its marking is implied by L.
Formally:
Here, QPlant_m and QCand_m refer to the marked states of GPlant and GCand, respectively. The function returns "true" if the condition is fulfilled. Example:Consider the very simple machine scenario; see also IsControllable. In the product composition of plant and specification the state IIF is not marked, since the specification required the buffer to be empty. However, the corresponding II plant state is marked. The string alpha_1 beta_1 therefore is in Lm(GPlant)∩L(GSpec) but not in Lm(GSpec). Thus, the condition is violated and the function IsRelativelyMarked returns "false" when applied to GPlant and GSpec. Parameter Conditions:This implementation requires the alphabets of both generators to match. Furthermore, both specified generators must be deterministic and nonblocking. SupRelativelyPrefixClosedComputes the supremal relatively prefixclosed sublanguage. Signature:SupRelativelyPrefixClosed(+In+ Generator GPlant, +In+ Generator GSpec, +Out+ Generator GRes) Detailed description:
Given a plant L = Lm(GPlant) and a
specification E = Lm(GSpec), this function
computes the supremal sublanguage K↑ ⊆ E that
is relatively prefixclosed w.r.t. L:
For a formal discussion on relativeclosedness in the context of supervisory control, including a formula for the supremal relatively closed sublanguage, see [S9]. Example:
Parameter Conditions:This implementation requires the alphabets of both generators to match. Furthermore, both specified generators must be deterministic. libFAUDES 2.31f  2023.02.02  with "synthesisobserverobservabilitydiagnosishiosysiosystemmultitaskingcoordinationcontroltimedsimulatoriodeviceluabindingspybindings" 