Coordination Control PlugIn

This plug-in implements functions for coordination control synthesis of prefix-closed languages (this means that for most of the functions, input generators are required to have all states marked), see the literature. The case of non-prefix-closed languages is still under investigation and will be added as soon as the algorithms are developed.

The following functions are implemented (see details below): Given a plant L = || L(Gi), i=1,...,n, and a specification language K, the goal is to construct the supremal conditionally controllable sublanguage of K.

    Functions for prefix-closed synthesis:
  • SupConditionalControllable - the main function, computes the supremal conditionally controllable sublanguage of K with respect to the given set of subsystems.
  • ConDecExtension - this function computes/extends the alphabet ek so that the language K becomes conditionally decomposable with respect to the given set of alphabets and ek.
  • IsConditionalControllable - check that a language is conditionally controllable.
  • IsConditionalDecomposable - check that a language is conditionally decomposable.
    Functions for NON-prefix-closed synthesis (under development):
  • IsConditionalClosed - this function works with non-prefix-closed languages and will be used later (this part is still under investigation).
    Additional function:
  • ccTrim - a graph based implemenatation of Trim() function.

Copyright (c) 2011 - 2015, Tomas Masopust

IsConditionalClosed

Tests for conditional closedness.

Signature:

IsConditionalClosed(+In+ GeneratorVector specVect, +In+ Generator pk, +In+ GeneratorVector genVect, +In+ Generator gk, +Out+ Boolean BRes)

Detailed description:

The function checks conditional closedness of a given conditionally decomposable language K = P1+k(K) || P2+k(K) || ... || Pn+k(K) with respect to generators Gi, i=1,2,...,n.

A language K is conditionally closed with respect to generators Gk and (Gi,i=1,2,...,n) if

  • Pk(K) is Lm(Gk)-closed
  • Pi+k(K) is Lm(Gi)||Lm(Pk(K))-closed

Note: L-closed is also referred to as L-relatively prefix-closed.

It is required that the subparts Pi+k and Gi are at the same position in the vectors, i.e., specVector.At(i) = Pi+k(K) and genVect.At(i) = Gi, for all i.

The representation of K as the parallel composition of the components is chosen for the reason that the computation of a projection can be of exponential complexity. Therefore, it is rather left for the user to compute the decomposation of K. Usually, it is required that the projection is a natural observer, which ensures the lower complexity of the operation projection.

Parameter Conditions:
  • specVector is a vector of deterministic generators for the languages Pi+k, i=1,2,...,n.

  • pk is a deterministic generator for the language Pk(K).

  • genVector is a vector of deterministic generators Gi, i=1,2,...,n.

  • gk is a deterministic generator for the coordinator Gk such that its event set ek contains all shared events.

  • BRes is true if K is conditionally closed

IsConditionalControllable

Tests for conditional controllability.

Signature:

IsConditionalControllable(+In+ GeneratorVector specVect, +In+ Generator pk, +In+ GeneratorVector genVect, +In+ Generator gk, +In+ EventSet ACntrl, +Out+ Boolean BRes)

Detailed description:

The function checks conditional controllability of a given conditionally decomposable language K = P1+k(K) || P2+k(K) || ... || Pn+k(K) with respect to generators Gi, i=1,2,...,n, and the corresponding sets of uncontrollable events Ei+k,u, i=1,2,...,n. It returns true if K is conditionally controllable.

A language K is conditionally controllable with respect to generators Gk and (Gi,i=1,2,...,n) and the set of uncontrollable events Ek,u and (Ei,u,i=1,2,...,n) if

  • Pk(K) is controllable w.r.t. L(Gk) and Ek,u
  • Pi+k(K) is controllable w.r.t. L(Gi)||L(Pk(K)) and Ei+k,u, where Ei+k,u is the set of all uncontrollable events of the event sets Ei and Ek

It is required that the subparts Pi+k and Gi are at the same position in the vectors, i.e., specVector.At(i) = Pi+k(K) and genVect.At(i) = Gi, for all i.

The representation of K as the parallel composition of the components is chosen for the reason that the computation of a projection can be of exponential complexity. Therefore, it is rather left for the user to compute the decomposation of K. Usually, it is required that the projection is a natural observer, which ensures the lower complexity of the operation projection.

Parameter Conditions:
  • specVector is a vector of deterministic nonblocking generators for the languages Pi+k, i=1,2,...,n.

  • pk is a deterministic nonblocking generator for the language Pk(K).

  • genVector is a vector of deterministic nonblocking generators Gi, i=1,2,...,n.

  • gk is a deterministic nonblocking generator for the coordinator Gk such that its event set ek contains all shared events.

  • ACntrl is a set of controllable events. The local controllable events are computed by intersection of the alphabets of the generators Gi with the set ACntrl.

IsConditionalDecomposable

Tests for conditional decomposability.

Signature:

IsConditionalDecomposable(+In+ System gen, +In+ EventSetVector alphVector, +In+ EventSet ek, +InOut+ System proof, +Out+ Boolean BRes)

Detailed description:

The function checks conditional decomposability of a given language K=Lm(gen) with respect to a vector of alphabets alphVector and an additional alphabet ek. It returns true if K is conditionally decomposable.

A languge K is conditionally decomposable w.r.t. the event sets Ek and (Ei, i=1,2,...,n) if K = P1+k(K) || P2+k(K) || ... || Pn+k(K), where Pi+k is a natural projection from the global event set to the event set Ei union Ek.

Parameter Conditions:
  • gen is a deterministic generator

  • alphVector is a vector of at least two alphabets; the union of these alphabets must include the alphabet of the generator gen

  • ek is a specific alphabet such that all shared events of at least two alphabets from alphVector are included in ek, and ek is included in the union of all the alphabets from alphVector

  • proof is a generator that gives a proof that the language K is not conditionally decomposable. The language Lm(proof) represents all the strings that violate the condition.

ConDecExtension

Extension of Ek for K to become conditionally decomposable.

Signature:

ConDecExtension(+In+ System gen, +In+ EventSetVector alphVector, +InOut+ EventSet ek)

Detailed description:

The function extends ek so that K=Lm(gen) becomes conditionally decomposable with respect to a vector of alphabets alphVector and the extended alphabet ek. It returns the extended alphabet ek.

A languge K is conditionally decomposable w.r.t. the event sets Ek and (Ei, i=1,2,...,n) if K = P1+k(K) || P2+k(K) || ... || Pn+k(K), where Pi+k is a natural projection from the global event set to the event set Ei union Ek.

Parameter Conditions:
  • gen is a deterministic generator

  • alphVector is a vector of at least two alphabets; the union of these alphabets must include the alphabet of the generator gen

  • ek is a specific alphabet such that all shared events of at least two alphabets from alphVector are included in ek, and ek is included in the union of all the alphabets from alphVector

SupConditionalControllable

Computation of the supremal conditionally controllable sublanguage of the specification K

Signature:

SupConditionalControllable(+In+ System SpecGen, +In+ GeneratorVector genVector, +In+ EventSet ACntrl, +In+ EventSet InitEk, +Out+ GeneratorVector supVector, +Out+ Generator Coord)

Detailed description:

The function computes supremal conditionally controllable sublanguage of a given conditionally decomposable language K = P1+k(K) || P2+k(K) || ... || Pn+k(K) with respect to generators Gi, i=1,2,...,n, and the corresponding sets of uncontrollable events Ei+k,u, i=1,2,...,n. It returns the supervised coordinator and a vector of corresponding supervisors such that the language of their parallel composition is the supremal conditionally controllable sublanguage of K. It proceeds in the following steps:

  1. Compute the alphabet Ek (based on the initialization InitEk) so that it contains all shared events of the generators and makes the language K = L(SpecGen) conditionally decomposable with respect to the alphabets of the generators and Ek
  2. Extend Ek so that projections Pk : E* -> Ek* are L(Gi)-observers for Gi given at genVect.At(i)
  3. Compute the coordinator Gk = || Pk(Gi)
  4. Compute supCk = SupCon(Pk(K),Gk,Ek,u) and supCi+k = SupCon(Pi+k(K),Gi||Pk(K),Ei+k,u), i=1,...,n, so that || supCi+k is the supremal conditionally controllable sublanguage of K

A language K is conditionally controllable with respect to generators Gk and (Gi,i=1,2,...,n) and the set of uncontrollable events Ek,u and (Ei,u,i=1,2,...,n) if

  • Pk(K) is controllable w.r.t. L(Gk) and Ek,u
  • Pi+k(K) is controllable w.r.t. L(Gi)||L(Pk(K)) and Ei+k,u, where Ei+k,u is the set of all uncontrollable events of the event sets Ei and Ek

Parameter Conditions:
  • SpecGen is a deterministic nonblocking generators for the specification languages K.

  • genVector is a vector of deterministic nonblocking generators Gi, i=1,2,...,n.

  • ACntrl is the global set of controllable events.

  • InitEk is the initial set Ek which will be extended if necessary.

  • supVector is a vector of supervisors supCi+k, i=1,2,...,n, such that their parallel composition is the supremal conditionally controllable sublanguage of K returned by the procedure.

  • Coord contains the computed supervised coordinator.

ccTrim

A bit more efficient trim operation based on graph algorithms.

Signature:

ccTrim(+In+ Generator gen, +Out+ Generator trimGen, +Out+ Boolean BRes)

Detailed description:

The generator is transformed to a graph representation and the graph algorithms are used. The graph representation uses the adjacency list. (Only for experimental reasons. Optimization in progress.) It returns true if the generator gen is trimmed.

Parameter Conditions:
  • gen is a deterministic generator

  • trimGen is the trimmed gen generator

Literature

[CC_AUT2012] J. Komenda, T. Masopust, J.H. van Schuppen: Supervisory Control Synthesis of Discrete-Event Systems using a Coordination Scheme, Automatica 48(2), 247-254, 2012.

[CC_SCL2011] J. Komenda, T. Masopust, J.H. van Schuppen: Synthesis of controllable and normal sublanguages for discrete-event systems using a coordinator, Systems & Control Letters, 60(7), 492-502, 2011.

[CC_2012PP] J. Komenda, T. Masopust, J.H. van Schuppen: On Conditional Decomposability, Preprint, http://arxiv.org/abs/1201.1733.

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

>>