Omega-Controllable Sublanguages

Functions related to controllability and controller synthesis on the infinite time axis.

Definition of Omega-Controllability

Addressing the control of discrete event systems on the infinite time axis, [S3] develops a notion of omega-controllability.

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 omega-controllable w.r.t (L,Sigma_uc) if the following conditions are satisfied:

(i)  Prefix(K) is controllable w.r.t (Prefix(L),Sigma_uc), i.e., Prefix(K)Sigma_uc ∩ Prefix(L)  ⊆  Prefix(K) ; and
(ii)  K is relatively topological closed w.r.t. L, i.e., K  =  Closure(K) ∩ L .

Note 1: for omega-languages, 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 omega-controllability conforms to [S3] and [S4]. It must not be confused with the more general approach taken in [S5].

Note 3: all omega-languages 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 omega-language and obtain Bm(G) = B(Lm(G)) by determinism of G; see also Generator.

Controller Synthesis for Omega-Languages

Consider 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 non-blocking, i.e., Prefix(L ∩ H) = Prefix(L) ∩ Prefix(H) ;
(2)     the controller H exhibits a prefix which is controllable w.r.t. (Prefix(L),Sigma_uc) ; and,
(3)     the closed-loop behaviour satisfies the specification, i.e., L ∩ H ⊆ E.

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,
(b)     Prefix(K) is controllable w.r.t. (Prefix(L),Sigma_uc); and,
(c)     K ⊆ E.

Note that (a) and (b) amount to omega-controllability. Moreover, if a language K satisfies (a)-(c), the controller H = Closure(K) solves the synthesis problem.

In contrast to the situation of star-languages, 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

K↑ := sup{ K ⊆ E | K is omega-controllable w.r.t (L,Sigma_uc) }

is itself relatively topological closed and, thus, is omega-controllable. For this case, [S4] discusses the computaion of a realisation, see also SupConCmplClosed and SupConCmplNB.

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 closed-loop trajectories fulfill the acceptance condition of K↑. Alternatively, one can extract a non-minimal restrictive supervisor that can be implemented by a closed behaviour. A generator that realises K↑ can be computed by OmegaSupConNB.

Example

For illustration of omega-controllability, 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 omega-languages are topologically closed.

A-B-machine, std. variant
A-B-machine, B exhausts the machine
A-B-machine, B breaks the machine

In our discussion, we consider three alternative specifications, that require the closed loop to

  • persistenly alternate successful operation of processes A and B, or to

  • persistently run some operation successfully, or to

  • start with process A, eventually switch to B, and, on success turn back to A.

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.

A-B-machine, std. variant A-B-machine, B exhausts the machine A-B-machine, B breaks the machine
alternate eventual success in running A and B eventual success is guaranteed by the plant; relative closedness is satisfied the specification requires immediatly to process A after success in B; hence, the closed-loop will not suffer from an exhausted machine; relative closedness is satisfied the specification requires the machine to eventually process B, and, hence, the closed-loop will block with a broken machine; however, the intersection of plant and specification is empty; so, technically, relative closedness is satisfied
persistently run any process with eventual success the specification is a superset of the plant; relative closedness is satisfied a minimal restrictive supervisor cannot exist, since such a supervisor would need to eventually decide to process A once the machine is exhausted; relative closedness is not satisfied since B breaks the machine, persistent success implies not to run process B; relative closedness is satisfied
eventually switch to B plant does not imply the eventuality property to process B; relative closedness is not satisfied. plant does not imply the eventuality property to process B; relative closedness is not satisfied. plant does not imply the eventuality property to process B; relative closedness is not satisfied.

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 closed-loop behaviour has been computed using SupConCmplNB.

A-B-machine, std. variant, with alternate-A-and-B-success specification
A-B-machine, std. variant, with persistently-any-success specification
A-B-machine, B exhausts the machine, with alternate-A-and-B-success specification
A-B-machine, B breaks the machine, with persistenly-any-success specification

IsOmegaControllable

Test 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 omega-controllability 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 omega-trim.

SupConCmplClosed

Computes 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

K↑ = sup{ K ⊆ E∩L | K is controllable w.r.t (L,Sigma_uc)  and complete } .

It can be observed that K↑ is prefix closed.

The set of uncontrollable events Sigma_uc is either taken from the plant generator's event attributes or specified as the complement of the parameter ACntrl. The result GSupervisor is returned to generate K↑; see e.g. [S4] for the base algorithm used in the implementation of this function.

Relevance to omega-languages:

It is shown in [S4] that the omega-language B(GSupervisor) is the supremal omega-controllable sublanguage of B(GSpec):

B(GSupervisor) = 
  sup{ K ⊆ B(GSpec)∩B(GPlant) | K is omega-controllable w.r.t (B(GPlant),Sigma_uc) } .

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.

SupConCmplNB

Computes 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

K↑ = sup{ K ⊆ E∩L | K is controllable w.r.t (L,Sigma_uc)  and complete } .

The set of uncontrollable events Sigma_uc is either taken from the plant generator's event attributes or specified as the complement of the parameter ACntrl. The result GSupervisor is returned to mark K↑. The algorithm used in this implementation is similar to the one presented in [S4].

Relevance to omega-languages:

Assume that the omega-language 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 omega-controllable sublanguage of Bm(GSpec):

Bm(GSupervisor') = 
         sup{ K ⊆ Bm(GSpec)∩Bm(GPlant) | K is omega-controllable w.r.t (Bm(GPlant),Sigma_uc) } .

Parameter Conditions:

This implementation requires the alphabets of plant and specification to match. Furthermore, both generators must be deterministic and omega-trim. The result will be deterministic and omega-trim.

SupConNormCmplNB

Computes 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):

K↑  =  sup{ K ⊆ E |
          K is controllable w.r.t. (L,Sigma_uc) and Closure(K) is normal w.r.t. (L,Sigma_o) and K is complete }.

The set of controllable events Sigma_c and the set of observable events Sigma_o may be given explicitely or are extracted from the argument GPlant. The implemention performs the iteration proposed in [S7]:

1.   K_0 = L ∩ E, 0→i
2.   K_i+1 = sup{ K ⊆ Closure(K_i) |
         K is controllable w.r.t. (L,Sigma_uc) and
         Closure(K) is normal w.r.t. (Closure(L),Sigma_o) }
3.   K_i+2 = sup{ K ⊆ Closure(K_i+1) | K is complete  }
4.   K_i+3 = K_0 ∩ K_i+2
5.   if K_i+3 = K_i, terminate the iteration and return the fixpoint as result K; else continue at step 2. i→i+3

In step 2., controllability w.r.t. L can be equivalenty replaced by controllability w.r.t. Closure(L). Thus, computation of the supremal sublanguage can be performed by SupConNormClosed. In step 3., the supremal complete sublanguage is obtained by subsequently removing states that have no successor state; see also Complete. By [S7], the above iteration terminates after a finite number of steps and the fixpoint K equals the supremum K↑. Furthermore, if E is relatively marked w.r.t. L, then the result K is relatively closed w.r.t. the plant L.

Relevance to omega-languages:

SupConNormCmplNB can be used to solve a particular problem of controller synthesis under partial observation. Consider the omega-languages 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 non-blocking, i.e., Prefix( B(L) ∩ Pinv0(Ho) ) = Prefix(B(L)) ∩ Prefix(Pinv0(Ho))} ;
(2)     the closed-loop behaviour B(L) ∩ Pinv0(Ho) exhibits a prefix which is controllable w.r.t. (Prefix(B(L)),Sigma_uc) ; and,
(3)     the closed-loop behaviour satisfies the specification, i.e., B(L) ∩ Pinv0(Ho) ⊆ E.

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 prefix-closed 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 closed-loop behaviour is supremal in the sense that

Bm(GRes)  =  L ∩ Pinv0(Ho↑) = 
         sup{ L ∩ Pinv0(Ho) | Ho is topoligically closed and satisfies conditions (1)-(3) } .

Parameter Conditions:

Parameters have to be deterministic, result is deterministic.

OmegaSupConNB

Synthesis for omega-languages.

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 closed-loop 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

L ∩ K  =  K  ⊆  L ∩ Closure(K).

We require the closed-loop to be nonblocking and the supervisor not to disable uncontrollable events, i.e. for all s ∈ Prefix(L) ∩ Prefix(K) we must have

(a)   s ∈ Prefix(L∩K) and
(b)   o ∈ Sigma_uc, so ∈ Prefix(L)    ⇒    so ∈ Prefix(K) .

The nonblockng condition (a) is trivially fulfilled, while (b) amounts to controllabiliy for the prefix of K w.r.t. the prefix of L. Neither for the plant nor for the supervisor we ask how a technical realization actually manages to satisfy their respective acceptance condition. However, while K ⊆ L ensures that the supervisor will support the plant in this regard, the plant could permanently prevent the supervisor from running into a marked state. Thus, we introcude as condition (c) that while the closed-loop evolves, the supervisor must allways have the chance to apply a control strategy such that the acceptance condition of the plant implies that the trajectory eventually passes a maked state. Technically, we require for all s ∈ Prefix(L) ∩ Prefix(K)

(c)    ∃ V ⊆ K: s ∈ Prefix(V), and V is omega-controllable w.r.t. L.

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 closed-loop behaviour K ⊆ E that satisfies conditions (a), (b) and (c). Moreover, supremal closed-loop behaviour equals the union over all omega-controllable sublanguages of E.

Note. A more general approach to the control of omega-languages 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 omega-controllability 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 A-B-machine and the eventually-switch-to-B specification.

A-B-machine, std. variant, with eventually-switch-to-B specification
A-B-machine, B exhausts the machine, with eventually-switch-to-B specification
A-B-machine, B breaks the machine, eventually-switch-to-B 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 omega-trim.

IsRelativelyOmegaClosed

Test for relative omega-closedness.

Signature:

IsRelativelyOmegaClosed(+In+ Generator GPlant, +In+ Generator GCand, +Out+ Boolean BRes)

Detailed description:

An omega-language K is relatively closed w.r.t. the omega-language L, if K can be recovered from its closure and L. Formally:

K = Closure(K) ∩ L .

Note that, the closure operator refers to the so called topological closure; see also OmegaClosure.

This function tests, whether

Bm(GCand) = B(GCand) ∩ Bm(GPlant)

by performing the product composition of the two generators in order to verify the following three conditions:

  • L(GCand) ⊆ L(GPlant);

  • no SCC of GPlant x GCand without GCand-marking contains a state with GPlant-marking; and

  • no SCC of GPlant x GCand without GPlant-marking contains a state with GCond-marking.

The function returns "true" if all conditions are satisfied.

Example:

Consider the A-B-machine 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 omega-limit 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 specification-marked 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 omega-trim.

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

>>