




OmegaControllable SublanguagesFunctions related to controllability and controller synthesis on the infinite time axis. Definition of OmegaControllabilityAddressing the control of discrete event systems on the infinite time axis, [S3] develops a notion of omegacontrollability.
Consider two omega languages L and K
over a common alphabet Sigma,
and a set of uncontrollable events Sigma_uc ⊆ Sigma.
Then K is said to be omegacontrollable w.r.t (L,Sigma_uc)
if the following conditions are satisfied:
Note 1: for omegalanguages, the closure operator Closure(.) refers to the so called topological closure; see also OmegaClosure. The prefix operator Prefix(.) gives the set of all finite length prefixes. Note 2: The above definition of omegacontrollability conforms to [S3] and [S4]. It must not be confused with the more general approach taken in [S5]. Note 3: all omegalanguages in the following discussion are assumed to be representable by finite deterministic automata with Buechi acceptance condition. Given a finite deterministic generator G, we write Bm(G) for the associated omegalanguage and obtain Bm(G) = B(Lm(G)) by determinism of G; see also Generator. Controller Synthesis for OmegaLanguagesConsider two omega languages L and E over a common alphabet Sigma to represent the plant and the specification, respectively. Let Sigma_uc ⊆ Sigma denote the set of uncontrollable events. The task then is to find a topologically closed controller H ⊆ Sigma^w, such that
(1)
L and H are nonblocking, i.e.,
Prefix(L ∩ H) = Prefix(L) ∩ Prefix(H) ;
For any topologically closed controller H which satisfies the above conditions, the closed loop K = L ∩ H exhibits the following properties:
(a)
K is relatively topological closed w.r.t. L; and,
Note that (a) and (b) amount to omegacontrollability. Moreover, if a language K satisfies (a)(c), the controller H = Closure(K) solves the synthesis problem.
In contrast to the situation of starlanguages, property (a) is not retained under arbitrary union.
Under the additional requirement, that E is relatively topological closed w.r.t. L,
[S3] establishes that the supremum
A more general approach, that drops the requirement of the specification E to be relatively closed, is presented in [S5]. In this situation, K↑ will fail to be relatively closed, and a controller H↑ = Closure(K↑) would fail to enforce the specification. However, one could then use K↑ itself as a supervisor, provided that a technical realisation implements a mechanism that ensures that closedloop trajectories fulfill the acceptance condition of K↑. Alternatively, one can extract a nonminimal restrictive supervisor that can be implemented by a closed behaviour. A generator that realises K↑ can be computed by OmegaSupConNB. ExampleFor illustration of omegacontrollability, consider the below veriants of a machine that may run one of two processes A and B. The processes are initiated by the controllable events a and b, respectively. Once started, a process may terminate with success c or failure d. In the first variant, each process is guaranteed to eventually succeed. In the second variant, process B exhausts the machine and can subsequently only succeed after running process A. In the third variant, process B breaks the machine. Each variant exhibits an eventuality property and, hence, neither of the induced omegalanguages are topologically closed.
In our discussion, we consider three alternative specifications, that require the closed loop to
Note that, technically, a specification language is required to be a subset of the plant language. The above realisations are "lazy" in the sense that they do not fulfil this requirement. For the following diccussion, we think of the above specifications to be intersected with the respective plant language; see also OmegaParallel. For a minimal restrictive supervisor to exist, the specification is required to be relatively closed w.r.t. the plant. Intuitively, this is true whenever any eventuality property required by the specification is implied by the plant. The following table comments on relative closedness of indivual combinations of plant and specification.
The third row of the above table points out that there are relevant applications that do not fulfil the requirement of a relatively closed specification. This has been addressed in [S5]; see also OmegaSupConNB. For the cases where relative closedness is satisfied, the minimal restrictive closedloop behaviour has been computed using SupConCmplNB. IsOmegaControllableTest controllablity condition. Signature:IsOmegaControllable(+In+ Generator GPlant, +In+ EventSet ACntrl, +In+ Generator GCand, +Out+ Boolean BRes) IsOmegaControllable(+In+ System GPlant, +In+ Generator GCand, +Out+ Boolean BRes) Detailed description:This function tests omegacontrollability of Bm(GCand) w.r.t. (Bm(GPlant),Sigma_uc), where the set of controllable events Sigma_uc is specified as the complement of the parameter ACntrl. The current implementation performs the test by invoking IsControllable and IsRelativelyOmegaClosed. It returns true, if both conditions are satisfied. Parameter Conditions:This implementation requires the alphabets of plant and specification to match. Furthermore, both generators must be deterministic and omegatrim. SupConCmplClosedComputes the supremal controllable and complete sublanguage. Signature:SupConCmplClosed(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GSupervisor) SupConCmplClosed(+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 a realisation of the supremal controllable and complete sublanguage
Relevance to omegalanguages:
It is shown in [S4] that
the omegalanguage B(GSupervisor)
is the supremal omegacontrollable sublanguage of B(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. The result will be deterministic and accessible. SupConCmplNBComputes the supremal controllable and complete sublanguage. Signature:SupConCmplNB(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GSupervisor) SupConCmplNB(+In+ Generator GPlant, +In+ EventSet AContr, +In+ Generator GSpec, +Out+ Generator GSupervisor) Detailed description:
Given a plant L = Lm(GPlant) and a
specification E = Lm(GSpec), this function
computes the supremal controllable and complete sublanguage
Relevance to omegalanguages:
Assume that the omegalanguage B(E) is relatively
closed w.r.t. B(L),
consider a realization GSpec' of Closure(E), i.e., Lm(GSpec') = Closure(E),
and denote GSupervisor' the result of SupConCmplNB when
applied to Gplant and GSpec'. Then GSupervisor' realizes
the supremal omegacontrollable sublanguage of
Bm(GSpec):
Parameter Conditions:This implementation requires the alphabets of plant and specification to match. Furthermore, both generators must be deterministic and omegatrim. The result will be deterministic and omegatrim. SupConNormCmplNBComputes the supremal controllable normal and complete sublanguage. Signature:SupConNormCmplNB(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GRes) SupConNormCmplNB(+In+ Generator GPlant, +In+ EventSet AContr, +In+ EventSet AObs, +In+ Generator GSpec, +Out+ Generator GRes) Detailed description:
The function SupConNormCmplNB computes a realisation GRes of the supremal controllable, normal
and complete sublanguage K↑ of the specification E
(marked by argument E or GSpec) w.r.t.
the plant L (marked by argument L or GPlant):
Relevance to omegalanguages:SupConNormCmplNB can be used to solve a particular problem of controller synthesis under partial observation. Consider the omegalanguages B(L) and B(E) as plant and specification, respectively, where B(E) is assumed to be relatively closed w.r.t. B(E). We require a controller Ho ⊆ Sigma_o^w, Sigma_o ⊆ Sigma, to satisfy the following conditions:
(1)
B(L) and Ho are nonblocking, i.e.,
Prefix( B(L) ∩ Pinv0(Ho) ) = Prefix(B(L)) ∩ Prefix(Pinv0(Ho))} ;
When B(E) is assumed to be relatively closed w.r.t. B(L),
we may also assume without further loss of generality that L is complete
and that E is relatively prefixclosed w.r.t. L.
If, in addition, in every infinite string w ∈ B(L) there are infinitely many occurences
of observable events, then the topologically closed controller Ho↑ = B(P0(L(GRes)))
satisfies the above conditions.
Moreover, the resulting closedloop behaviour is supremal in the sense that
Parameter Conditions:Parameters have to be deterministic, result is deterministic. OmegaSupConNBSynthesis for omegalanguages. Signature:OmegaSupConNB(+In+ System GPlant, +In+ Generator GSpec, +Out+ Generator GSupervisor) OmegaSupConNB(+In+ Generator GPlant, +In+ EventSet AContr, +In+ Generator GSpec, +Out+ Generator GSupervisor) Detailed description:
The function OmegaSupConNB addresss the
situation where the specification fails to be relatively closed w.r.t. the plant.
We formaly model the closedloop interconnection
of a plant L ⊆ Sigma^w
and supervisor K ⊆ L by the intersection
L∩K. Since we dropped the requirement of relative closedness,
we obtain
It is readily verified that condition (c) implies condition (b). Furthermore, all three conditions are preserved under arbitrary union. Thus, given a specification E ⊆ L, there exists a supremal closedloop behaviour K ⊆ E that satisfies conditions (a), (b) and (c). Moreover, supremal closedloop behaviour equals the union over all omegacontrollable sublanguages of E. Note. A more general approach to the control of omegalanguages has been developed in [S5]. When applied to the specific case of determinitsic Buchi automata addressed here  and despite some minor differences in the perspective we take  the above condition (c) is equivalent to the notion of omegacontrollability proposed in [S5]. There, it has been shown that the supremal controllable sublanguage can be represented in terms of the so called controllability prefix and the marking of the specification. The current of implementation OmegaSupConNB is derived as an adaption of the methods proposed in [S5] (and companion papers) to the specific case at hand. Example:The following results have been obtained for the three variants of ABmachine and the eventuallyswitchtoB specification. 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. The result will be deterministic and omegatrim. IsRelativelyOmegaClosedTest for relative omegaclosedness. Detailed description:
An omegalanguage K is relatively closed w.r.t. the omegalanguage
L, if K can be recovered from its closure and L.
Formally:
This function tests, whether
The function returns "true" if all conditions are satisfied. Example:Consider the ABmachine in the variant in which B exhausts the machine and the specification that persistently requires any sucessful operation. Then the product will generate strings b c (b d)^*. Consider the omegalimit w of this set of strings. The states attained when generating w eventually correspond to the plant states XB and FB and to the specification state B. In the product generator, the states must be part of an SCC. Furthermore, since B is not marked there must exists an SCC with no specificationmarked state. However, this SCC also contains a state that coresponds to XB, which is marked by the plant. Thus, the procedure return "false". Parameter Conditions:This implementation requires the alphabets of both generators to match. Furthermore, both specified generators must be deterministic and omegatrim. libFAUDES 2.28b  2019.12.01  with "synthesisobserverdiagnosisiosystemhiosysmultitaskingcoordinationcontroltimediodevicesimulatorluabindings" 