Complete and Controllable Sublanguages

SupConCmplClosed

Computes the supremal controllable and complete sublanguage.

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. [W3] for the base algorithm used in the implementation of this function.

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.

SupConCmpl

Computes the supremal controllable and complete sublanguage.

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 [W3].

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.

SupConNormCmpl

Computes the supremal controllable normal and complete sublanguage.

Detailed description:

The function SupConNormCmpl 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:

SupConNormCmpl 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.