Table of Contents
Fetching ...

Active prognosis and diagnosis of modular discrete-event systems

Shaopeng Hu, Shaowen Miao, Jan Komenda, Zhiwu Li

TL;DR

The work tackles the verification and enforcement of prognosability and diagnosability in deterministic DESs, introducing a unified pre-normality framework that links these properties to language extensions. It proves the existence of supremal prognosable/diagnosable and normal sublanguages and provides algorithms to compute the supremal controllable, normal, and prognosable/diagnosable sublanguages in monolithic DESs. The results are extended to modular DESs, showing that modular local supervisors can enforce global prognosability/diagnosability under nonconflicting conditions. This off line supervisory synthesis approach offers formal guarantees and a scalable alternative to online active diagnosis/prognosis, with clear pathways to modular implementation.

Abstract

This paper addresses the verification and enforcement of prognosability and diagnosability for discreteevent systems (DESs) modeled by deterministic finite automata. We establish the equivalence between prognosability (respectively, diagnosability) and pre-normality over a subset of the non-faulty language (respectively, a suffix of the faulty language). We then demonstrate the existence of supremal prognosable (respectively, diagnosable) and normal sublanguages. Furthermore, an algorithm is then designed to compute the supremal controllable, normal, and prognosable (respectively, diagnosable) sublanguages. Since DESs are typically composed of multiple components operating in parallel, pure local supervisors are generally insufficient, as prognosability and diagnosability are global properties of a system. Given the limited work on enforcing prognosability or diagnosability in modular DESs, where these properties are enforced through local supervisors, this paper leverages a refined version of pre-normality to compute modular supervisors for local subsystems. The resulting closed-loop system is shown to be globally controllable, normal, and prognosable/ diagnosable. Examples are provided to illustrate the proposed method.

Active prognosis and diagnosis of modular discrete-event systems

TL;DR

The work tackles the verification and enforcement of prognosability and diagnosability in deterministic DESs, introducing a unified pre-normality framework that links these properties to language extensions. It proves the existence of supremal prognosable/diagnosable and normal sublanguages and provides algorithms to compute the supremal controllable, normal, and prognosable/diagnosable sublanguages in monolithic DESs. The results are extended to modular DESs, showing that modular local supervisors can enforce global prognosability/diagnosability under nonconflicting conditions. This off line supervisory synthesis approach offers formal guarantees and a scalable alternative to online active diagnosis/prognosis, with clear pathways to modular implementation.

Abstract

This paper addresses the verification and enforcement of prognosability and diagnosability for discreteevent systems (DESs) modeled by deterministic finite automata. We establish the equivalence between prognosability (respectively, diagnosability) and pre-normality over a subset of the non-faulty language (respectively, a suffix of the faulty language). We then demonstrate the existence of supremal prognosable (respectively, diagnosable) and normal sublanguages. Furthermore, an algorithm is then designed to compute the supremal controllable, normal, and prognosable (respectively, diagnosable) sublanguages. Since DESs are typically composed of multiple components operating in parallel, pure local supervisors are generally insufficient, as prognosability and diagnosability are global properties of a system. Given the limited work on enforcing prognosability or diagnosability in modular DESs, where these properties are enforced through local supervisors, this paper leverages a refined version of pre-normality to compute modular supervisors for local subsystems. The resulting closed-loop system is shown to be globally controllable, normal, and prognosable/ diagnosable. Examples are provided to illustrate the proposed method.

Paper Structure

This paper contains 17 sections, 13 equations, 5 figures, 1 algorithm.

Figures (5)

  • Figure 1: Projection notations in this paper.
  • Figure 2: (a) A DFA $G_1$ and (b) its observer $Obs(G_1)$.
  • Figure 3: (a) A DFA $G_2$, (b) its observer $Obs(G_2)$, and (c) its verifier $G_2|||G_2$.
  • Figure 4: $\mathrm{supCNP}^2(L(G_1), \Psi_f^{-2}, \Sigma_{uc},P)$.
  • Figure 5: (a) A DFA $H_1$ with $H_1 \sqsubset G_1$, $L(H_1)=L(G_1)$ and $\delta_1(6,b)=7$, (b) the observer $Obs(H_1)$, (c) $\mathrm{supCNP}^0(L_1, \Psi_{1,f}^{-0}, \Sigma_{1,uc},P_{1,o}^{1})$, and (d) $\mathrm{supCNP}^0(L_2, \Psi_{2,f}^{-0}, \Sigma_{2,uc},P_{2,o}^{2})$.

Theorems & Definitions (23)

  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 13 more