Normal Sublanguages

IsNormal

Tests normality condition.

Detailed description:

Tests whether the language K (marked by argument K or GCand) is normal w.r.t. the language L (marked by argument L or GPlant) and the set of observable events. The latter may be given explicitely or is extracted from GPlant.

The implementation tests for K ⊇ L ∩ Pinv0(P0(K)), which is necessary for normality. Under the assumption K ⊆ L, the test is also sufficient.

Parameter Conditions:

Arguments are required to be deterministic. For a necessary and sufficient test, K must mark a subset of the language marked by L.

SupNorm

Computes the supremal normal sublanguage.

Detailed description:

The function SupNorm computes a realisation of the supremal sublanguage N↑ of K (generated by argument K or GCand) that is normal w.r.t. L (generated by argument L or GPlant):

N↑  =  sup{N  ⊆  K | N is normal w.r.t. (L,Sigma_o) }.

The set of observable events Sigma_o may be given explicitely or is extracted from GPlant. The implemention evaluates the Lin-Brandt formula for prefix closed languages L and K, as proposed in [S2]:

N↑  =  K - Pinv0(P0(L-K))

Note that, even though K and L are generated languages and, thus, are prefix closed, the supremal normal sublanguage in general fails to be prefix closed. In particular, the generator GRes marks the result. See also SupNormClosed.

Parameter Conditions:

Parameters have to be deterministic, the result will be deterministic. K must be a subset of L; While arguments are interpreted as generated languages, the result is given as marked language.

SupNormClosed

Computes the supremal normal and closed sublanguage.

Detailed description:

The function SupNormClosed computes a realisation of the supremal sublanguage N↑ of K (generated by argument K or GCand) that is normal w.r.t. L (generated by argument L or GPlant) and closed:

N↑  =  sup{N  ⊆  K | N is normal w.r.t. (L,Sigma_o) and prefix closed } .

Note that, since K and L are prefix closed, the above supremum is equivalently characterised by

N↑  =  sup{N  ⊆  K | Closure(N) is normal w.r.t. (L,Sigma_o) }.

The set of observable events Sigma_o may be given explicitely or is extracted from GPlant. The implemention evaluates the Lin-Brandt formula for prefix closed languages, as proposed in [S2]:

N↑  =  K - Pinv0(P0(L-K))Sigma*.

In contrast to SupNorm, the above formula evaluates to a closed language. The generator GRes is set up to both mark and generate the result.

Parameter Conditions:

Parameters have to be deterministic, result is deterministic. K must be a subset of L. While arguments are interpreted as generated languages, the result is given as marked and generated language.

SupConNormClosed

Computes the supremal controllable, normal and closed sublanguage.

Detailed description:

The function SupConNormClosed computes a realisation of the supremal controllable, normal and closed sublanguage K↑ of the specification E (generated by argument E or GSpec) w.r.t.\ the plant L (generated by argument L or GPlant):

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

Note that, since L and E are prefix closed, the above supremum is equivalently characterised by

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

The set of controllable events Sigma_c and the set of observable events Sigma_o may be given explicitely or are extracted from GPlant. The implemention evaluates the following expressions

1.   N↑ = sup{ N ⊆ E | Closure(N) is normal w.r.t. (L,Sigma_o) }
2.   No↑ = P0(N↑) , Lo = P0(L)
3.   Ko↑ = sup{ Ko ⊆ No↑ | Ko is controllable w.r.t. (Lo,Sigma_uc) }
4.   K  =  L ∩ Pinv0(Ko↑)

and returns a generator GRes that marks and generates K. It is readily verified, that K satisfies the closed-loop conditions (a)-(d); see also [C1]. Supremality is established in [S2], i.e., we have indeed K = K↑

Example:

Consider the very-simple machine example and assume that all events except of beta_1 are observabe, i.e. Sigma_o={alpha_1, alpha_2, beta_2}. The specification requires the supervisor to disable alpha_1 unless the buffer it not known to be empty, and, to disable alpha_2 unless the buffer it not known to be full. Thus, a supervisor may initially enable alpha_1 and disable alpha_2. The plant will then start M1, i.e., it executes alpha_1, to eventually complete the process, indicated by the unobservable event beta_1. However, the only way for the supervisor to figure that the process was completed and that alpha_2 could be enabled would be a subsequent alpha_1. However, the supervisor will not enable alpha_1 unless the buffer is known to be empty, and this will never happen, as long as alpha_2 is disabled. Consequently, the process stops after the sequence alpha_1 beta_1 and SupConNormClosed consistently returns the following

supremal controllable and normal sublanguage for prefix closed plant and specificaton.

Parameter Conditions:

Parameters have to be deterministic, result is deterministic. While arguments are interpreted as generated languages, the result is given as marked and generated language.

SupConNormNB

Computes the supremal controllable and normal sublanguage.

Detailed description:

The function SupConNormNB computes a realisation of the supremal controllable and normal 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 contr. w.r.t. (L,Sigma_uc) and 
            Closure(K) is normal w.r.t. (Closure(L),Sigma_o) }.

In contrast to SupConNormClosed, this function addresses marked languages and the resulting supremal sublanguage is not expected to be prefix closed.

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 = K_0 ∩ K_i+1
4.   if K_i+2 = K_i, terminate the iteration and return the fixpoint as result K;
         else continue at step 2. i→i+2

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. Under the hypothesis, that E is relatively marked, the results presented in [S7] imply that (i) the above iteration terminates, and that (ii) the fixpoint K indeed equals the supremum K↑, and that (iii) the latter is relatively closed w.r.t. the plant L. Thus, K↑ satisfies the closed-loop conditions (a)-(d) and H0↑ = P0(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 SupConNormNB, to obtain

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

This will result in the supremal language K⇧ that satisfies all four closed-loop conditions (a)-(d).

Remark. The implementation follows the above pseudo code and in addition introduces a Trim operation on the iterate Ki, as proposed in [S7]. In particular, GPlant is technically required to be non-blocking in order for SupConNormClosed to compute the above supremum. If, on the other hand, GPlant is blocking, normality and controllability are achieved w.r.t. the generated language, and one can use the result to obtain a non-blocking supervisor.

Example:

Consider the very-simple machine example and assume that all events except of beta_1 are observabe, i.e. Sigma_o={alpha_1, alpha_2, beta_2}. As discussed above, the supremal controllable and normal sublanguage (evaluated for the closure of plant and specifications) consists of the string alpha_1 beta_1 and its prefixes. Due to monotonicity of the relevant operators, the supremal controllable and normal sublanguage when evaluated for the marked plant and specification languages must be a subset, and the only such subset within plant and specification consists of the empty string.

To obtain a non-trivial result, one may relax the specification by taking its closure and thus don't insist in eventually ending up with an empty buffer. SupConNormNB then returns the below

supremal controllable and normal sublanguage for prefix closed specificaton.

One way to operate both machines with an unobservable event beta_1, is to extend the buffer to have a capacity of two work pieces and to not insist in the buffer to become eventually empty.

Buffer with capacity two

and the resulting supremal controllabel and normal sublanguage

Parameter Conditions:

Parameters have to be deterministic; result is deterministic.