Fault-Hiding Control Reconfiguration

Nominal Control

Our nominal control problem effectively is a standard control problem under partial observation. Formally, the nominal control problem is a tuple (Sigma_n,Ln,En) with the nominal plant Ln and the nominal specification En. We aim for a prefix-closed controller Hn such that the closed-loop system Ln || Hn

(NC1) is complete
(NC2) is non-conflicting, i. e. (Closure(Ln)) || Hn = Closure(Ln||Hn)
(NC3) is controllable w.r.t (Ln,Sigma_ucon  Sigma_lo)
(NC4) satisfies the specification, i. e. Ln||Hn  En.

We provide a convenience function for the computation of nominal controllers.

Control Reconfiguration

Virtualisation

In order to create the necessary degrees of freedom, the nominal controller needs to be decoupled from the faulty plant. Formally we relabel the controllable uncontrollable events, a process that we call virtualisation.

Given is a bijective function \rho and we define Sigma_vcon := \rho Sigma_con and Sigma_vucon := \rho Sigma_vucon. We define the function h:SIGn*SIGv* recursively according to h(epsilon) = epsilon and h(s o) = h(s) rho(o) if o\notinSigma_hi or h(s o) = h(s) o otherwise. Given a nominal controller Hn the corresponding virtual controller Hv is given by Hv := h Hn.

Self-Reconfiguring Closed-Loop System

We seek for a prefix closed reconfigurator  Sigma_R* such that for all virtualised controllers Hv the self-reconfiguring closed-loop system Lf||R||Hv

(R1) is complete
(R2) is non-conflicting, i. e. ( Closure(Lf)||R||Hv = Closure(Lf||R||Hv)
(R3) is controllable w. r. t. ( Lf||Hv, Sigma_ucon  Sigma_vcon  Sigma_lo  Sigma_hi
(R4) satisfies the specification E = Ef||Er

holds.

Reconfigurator Design

Given a language  Sigma* such that

(K1) K is controllable w.r.t. (Lf||Hv,Sigma_uconSigma_vconSigma_loSigma_hi
(K2) K is relatively closed w.r.t. Lf||Hv
(K3) K is prefix-normal w.r.t. (Lf||Hv,Sigma_R)
(K4) K is (Sigma-Sigma_hi)-Complete
(K5) K is weakly sensor-consistent w.r.t Lv, Lv = h(Ln)
(K6)  PinvVP Lv, Lv = h(Ln)
(K7)  E, E = Ef||E_R

holds, then the reconfigurator R = PR (K) ensures the properties (R2)-(R4) in the self-reconfiguring closed-loop system Lf||R||Hv.

The properties (K1)-(K7) are preserved under arbitrary union, thus for a given specification E there exists the supremal sublanguage of E w.r.t. the properties (K1)-(K7). Algorithms for the computation of the supremal complete sublanguage and the supremal weakly sensor-consistent sublanguage are provided in this LuaExtension. Each of the properties (K1)-(K7) satisfies the prerequisites in [FTC3], hence, the respective supremal sublanguage can be computed using a simple iterative scheme. The whole design process is prototypically shown in a tuorial

Verifikation of Non-Conflictingness

Let  Closure(K) denote a target language and define the operators

Omega1a = {s  Closure(K)|( o  Sigma_uconSigma_vcon)[s o  M]}
Omega1b = {s  Closure(K)|( o  Sigma_loSigma_hi)[s o  M]}
Omega1c = {s  Closure(K)|( o  Sigma)[s o  M]}

and let

\Omega = \Omega1a o \Omega1b o \Omega1c

denote their concatenation. Consider the iteration

M0 = K
M_i+1 = Omega Mi.

Whenever K satisfies (K1)-(K7) and Closure(K) is fix-point of \Omega , then R = P_R(Closure(K)) ensures for any virtualised solution Hv to the nominal control problem (Sigma_n,Ln,En) the properties (R1)-(R4).

FtcIsComplete

Test completeness.

Signature:

FtcIsComplete(+In+ Generator gK, +Out+ Boolean bIsCmp)

FtcIsComplete(+In+ Generator gK, +In+ Alphabet aSIGo, +Out+ Boolean bIsCmp)

FtcIsComplete(+In+ Generator gK, +In+ Alphabet aSIGo, +Out+ StateSet sBadStates, +Out+ Boolean bIsCmp)

Detailed description:

This function is equivalent to IsComplete.

Optionally, the set of states q_Bad that conflicts with completeness can be returned.

FtcSupComplete

Computate the supremal complete sublanguage.

Signature:

FtcSupComplete(+In+ Generator gK, +In+ Alphabet aSIGo, +Out+ Generator gRes)

Detailed description:

This function is equivalent to Complete.

Parameter Conditions:

K needs to be closed

FtcIsWeakSensorConsistent

Test weak sensor-consistency.

Signature:

FtcIsWeakSensorConsistent(+In+ Generator gK, +In+ Generator gLv, +In+ Alphabet aVUCON, +In+ Alphabet aCV, +Out+ StateSet qBad, +Out+ StateSet qLsns, +Out+ StateSet qKsns, +Out+ Boolean bIsWsc)

FtcIsWeakSensorConsistent(+In+ Generator gK, +In+ Generator gLv, +In+ Alphabet aVUCON, +In+ Alphabet aCV, +Out+ Boolean bIsWsc)

Detailed description:

Given is a reconfiguration problem (Ln,En,Lf,Ef,E_R). With Lv = h(Ln) the virtualised plant, Sigma_vucon the virtual uncontrollable events and Sigma_vc the virtual controller events. A language  Sigma* is called weakly sensor-consistent w.r.t. Lv, if

( s  Closure(K))[(PV s)Sigma_vucon  (Closure(Lv)) ≠ 0  
                   s(Sigma-Sigma_vc)*Sigma_vucon  ( Closure(K) ) ≠ 0].

holds.

Given generators gK, with L(gK) = K, gLv, with L(gLv) = Lv and containers which hold Sigma_vcon and Sigma_vc this functions tests if K is weakly sensor-consistent w.r.t. Lv and returns the result as a boolean value. Optionally, the state-set that conflicts with weak sensor-consistency qBad, and good states in gLv and gK can be returned.

Parameter Conditions:

Trim realisations

FtcSupWeakSensorConsistent

Computation of the supremal weak sensor-consistent sublanguage

Signature:

FtcSupWeakSensorConsistent(+In+ Generator gK, +In+ Generator gLv, +In+ Alphabet aVUCON, +In+ Alphabet aCV, +Out+ Generator gRes)

Detailed description:

Given is a reconfiguration problem (Ln,En,Lf,Ef,Er) and let Lv = h(Ln) denote the virtualised plant model and let

K = sup{M  K|M is weakly sensor-consistent w.r.t. Lv}

denote the supremal weakly sensor-consistent sublanguage of K.

Based on a generator gK with Lm(gK) = K and containers that hold Sigma_vucon and Sigma_vc this function returns a generator gRes with Lm(gRes) = K

Parameter Conditions:

K needs to be closed

Trim realisations

FtcIsNonconflicting

Check for a non-conflicting self-reconfiguring closed-loop system.

Signature:

FtcIsNonconflicting(+In+ Generator gK, +In+ Alphabet aLO, +In+ Alphabet aHI, +In+ Alphabet aUCON, +In+ Alphabet aCON, +Out+ Boolean bRes)

Detailed description:

Given is a candidat K = Lf||R||Hv for the self-reconfiguring closed-loop system togther with the set of low-level events Sigma_lo, the set of high-level events Sigma_hi, the set of uncontrollable events Sigma_ucon and the set of virtual controllable events Sigma_vcon. Consider a target language  Closure(K), define the operators

Omega1a = {s  Closure(K)|( o  Sigma_uconSigma_vcon)[s o  M]}
Omega1b = {s  Closure(K)|( o  Sigma_loSigma_hi)[s o  M]}
Omega1c = {s  Closure(K)|( o  Sigma)[s o  M]}

and let

Omega = Omega1a o Omega1b o Omega1c

denote their concatenation. Consider the iteration

M0 = K
M_i+1 = Omega(Mi)

Based on a generator gK with Lm(gK) = K and containers alpLO, alpHI, alpUCON and alpVCON that hold the alphabets Sigma_lo, Sigma_hi, Sigma_ucon and Sigma_vcon, this function computes the largest fix-point of the operator \Omega and returns TRUE if Closure(K) = \Omega K and FALSE otherwise.

FtcInactivityConditions

Construct inactivity conditions.

Signature:

FtcInactivityConditions(+In+ Alphabet aCON, +In+ Alphabet aUCON, +Out+ Generator gE)

FtcInactivityConditions(+In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ String sF, +Out+ Generator gE)

Detailed description:

Given containers aCON, aUCON, aVCON and aVUCON that hold the controllable events Sigma_con and an empty generator genEr, this functions constructs gEr such that Lm(gEr) = Er, with E_R = Closure(gEr)

Closure({rho(x)x|x  SIGcon}{x rho(x)|x  SIGcon}Sigma_hiSigma_lo)*)F Sigma*

holds.

By default, the controllable and uncontrollable events are relabled by appending the postfix "_v" and the fault-event is named "F". Alternatively, the name of the fault-event can be given as a parameter.

Parameter Conditions:

Trim realisations

FtcVirtualise

Virtualise a generator or an alphabet

Signature:

FtcVirtualise(+In+ Generator gOrg, +In+ Alphabet aUntouched, +Out+ Generator gRes)

FtcVirtualise(+In+ Alphabet aOrg, +In+ Alphabet aUntouched, +Out+ Alphabet aRes)

FtcVirtualise(+In+ Generator gOrg, +In+ Alphabet aUntouched, +In+ String aPostfix, +Out+ Generator gRes)

FtcVirtualise(+In+ Alphabet aOrg, +In+ Alphabet aUntouched, +In+ String aPostfix, +Out+ Alphabet aRes)

Detailed description:

Given an event-set Sigma, this function returns an alphabet Sigma' such that there exists a bijective function rho such that \Sigma'=roh(\Sigma). Technically, all events are relabelled by adding the postfix sPostfix.

Given a generator gOrg, with, L(gOrg) = L this function returns a generator gRes with L(gRes) = h(L).

By default, all events exept alpUntouched are relabled by appending the postfix "_v". Alternatively, the postix can be given as a parameter.

Example:

FtcNomController

Compute nominal controller.

Signature:

FtcNomController(+In+ Generator gLn, +In+ Generator gEn, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +Out+ Generator gC)

Detailed description:

Given are generators gLn and gEn, with Lm(gLn) = Ln and Lm(gEn) = En together with containers alpCON, alpUCON and alpHI that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon and the high-level events Sigma_hi. This function return constructs a generator gC with Lm(gC) = Hn such that the controller Hn ensures (NC1)-(NC4) for the closed loop system Ln||Hn.

FtcReconfigurator

Compute universal reconfigurator.

Signature:

FtcReconfigurator(+In+ Generator gLn, +In+ Generator gLf, +In+ Generator gEr, +In+ Generator gEf, +In+ Generator gHn, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +In+ Alphabet aLO, +Out+ Generator gR)

Detailed description:

Given are generators gLn, gLf, gEr, gEf and gHn with Lm(gLn) = Ln, Lm(gLf) = Lf, Lm(gEr) = Er, Lm(gEf) = Ef and Lm(gHn) = Hn together with containers alpCON, alpUCON, alpHI and alpLO that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon, the high-level events Sigma_hi and the low-level events Sigma_lo. This function return constructs a generator gR with Lm(gR) = R such that the reconfigurator R ensures (R1)-(R4) for the self-reconfiguring closed loop system Lf||R||Hv, for all virtualised controllers Hv.

FtcReconfiguratorTimed

Compute universal reconfigurator. Use controllabity for timed DES.

Signature:

FtcReconfiguratorTimed(+In+ Generator gLn, +In+ Generator gLf, +In+ Generator gEr, +In+ Generator gEf, +In+ Generator gHn, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +In+ Alphabet aLO, +Out+ Generator gR)

Detailed description:

Given are generators gLn, gLf, gEr, gEf and gHn with Lm(gLn) = Ln, Lm(gLf) = Lf, Lm(gEr) = Er, Lm(gEf) = Ef and Lm(gHn) = Hn together with containers alpCON, alpUCON, alpHI and alpLO that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon, the high-level events Sigma_hi and the low-level events Sigma_lo. This function return constructs a generator gR with Lm(gR) = R such that the reconfigurator R ensures (R1)-(R4) for the self-reconfiguring closed loop system Lf||R||Hv, for all virtualised controllers Hv.

Note that the controllability property (R3) was replaced by a controllablity developed for timed discrete event systems. This function is experimental.

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