Diagnosability and attack detection for discrete event systems under sensor attacks

Abstract

This paper extends the theory of diagnosability by investigating fault diagnosis in discrete event systems under sensor attacks using finite-state automata as models. It assumes that an attacker has compromised the communication channel between the system’s sensors and the diagnostic engine. While the general attack model utilized by the attacker has been previously studied in the context of supervisory control, its application to fault diagnosis remains unexplored. The attacker possesses the capability to substitute each compromised observable event with a string from an attack language. The attack model incorporates event insertion and deletion, as well as static and dynamic attacks. To formally capture the diagnostic engine’s ability to identify faults in the presence of the attacker, a novel concept called CA-diagnosability is introduced. This extends the existing notions of CA-controllability and CA-observability. A testing procedure for CA-diagnosability is developed, and its correctness is proven. Some sufficient conditions for CA-diagnosability that can be easily checked are also proposed and proved. The paper then investigates conditions under which the role of an attacker can be reverted from malicious to benevolent, that is, to help the diagnoser to diagnose faults. The paper further applies diagnosability theory to investigate conditions under which the presence of the attacker can be detected.

Appendix

Proof of Theorem 1

Let us take negations of the conditions in Theorem 1 as follows.

$$\begin{aligned}&\lnot (\exists n \in \mathcal{{N}})(\forall s\in \Psi (L(G)))(\forall u \in L(G)/s) \\&|u| \ge n \Rightarrow (\forall v \in (\Phi ^a)^{-1}(\Phi ^a(s u)) \cap L(G)) \Sigma _f \in v \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&\lnot (|u| \ge n \Rightarrow (\forall v \in (\Phi ^a)^{-1} (\Phi ^a(s u)) \cap L(G)) \Sigma _f \in v) \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge \lnot (\forall v \in (\Phi ^a)^{-1}(\Phi ^a(s u)) \cap L(G)) \Sigma _f \in v \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in (\Phi ^a)^{-1}(\Phi ^a(s u)) \cap L(G)) \Sigma _f \not \in v \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in L(G)) v \in (\Phi ^a)^{-1}(\Phi ^a(s u)) \wedge \Sigma _f \not \in v \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in L(G)) (\exists w \in \Phi ^a(s u)) \\&v \in (\Phi ^a)^{-1}(w) \wedge \Sigma _f \not \in v \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in L(G)) (\exists w \in \Phi ^a(s u)) \\&w \in \Phi ^a (v) \wedge \Sigma _f \not \in v \\ \Leftrightarrow&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v \end{aligned}$$

Similarly,

$$\begin{aligned}&\lnot (\exists n' \in \mathcal{{N}})(\forall s'\in \Psi (L(G^e)))(\forall u' \in L(G^e)/s')\\&|u'| \ge n' \Rightarrow (\forall v' \in P^{-1}(P(s' u')) \cap L(G^e) ) \Sigma _f \in v' \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&\lnot (|u'| \ge n' \Rightarrow (\forall v' \in P^{-1}(P(s' u')) \cap L(G^e) ) \Sigma _f \in v') \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&|u'| \ge n' \wedge \lnot (\forall v' \in P^{-1}(P(s' u')) \cap L(G^e) ) \Sigma _f \in v' \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in P^{-1}(P(s' u')) \cap L(G^e) ) \Sigma _f \not \in v' \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in L(G^e) ) v' \in P^{-1}(P(s' u')) \wedge \Sigma _f \not \in v' \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in L(G^e) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{aligned}$$

Hence, equivalently, we need to prove

$$\begin{aligned}&(\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v \end{aligned}$$

if and only if

$$\begin{aligned}&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in L(G^e) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' \\ \end{aligned}$$

It is natural to define that a (non-prefix-closed) language is diagnosable if and only if its prefix closure is diagnosable. Hence, we replace $L(G^e)$ by $L_m(G^e)$ as

$$\begin{aligned}&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L(G^e)))(\exists u' \in L(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in L(G^e) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L_m(G^e)))(\exists u' \in L_m(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in L_m(G^e) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{aligned}$$

By Eq. (5), $L_m(G^e) = \Theta ^a (L(G))$. Thus,

$$\begin{aligned}&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (L_m(G^e)))(\exists u' \in L_m(G^e)/s') \\&|u'| \ge n' \wedge (\exists v' \in L_m(G^e) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' \\ \Leftrightarrow&(\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (\Theta ^a (L(G))))(\exists u' \in \Theta ^a (L(G))/s') \\&|u'| \ge n' \wedge (\exists v' \in \Theta ^a (L(G)) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{aligned}$$

Therefore, equivalently, we need to prove

$$\begin{aligned} {\begin{matrix} &{} (\forall n \in \mathcal{{N}})(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\ &{} |u| \ge n \wedge (\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v \end{matrix}} \end{aligned}$$

(18)

if and only if

$$\begin{aligned} {\begin{matrix} &{} (\forall n' \in \mathcal{{N}})(\exists s'\in \Psi (\Theta ^a (L(G))))(\exists u' \in \Theta ^a (L(G))/s') \\ &{} |u'| \ge n' \wedge (\exists v' \in \Theta ^a (L(G)) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{matrix}} \end{aligned}$$

(19)

Let us first prove

$$\begin{aligned} {\begin{matrix} &{} (\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\ &{} (\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v \end{matrix}} \end{aligned}$$

(20)

if and only if

$$\begin{aligned} {\begin{matrix} &{} (\exists s'\in \Psi (\Theta ^a (L(G))))(\exists u' \in \Theta ^a (L(G))/s') \\ &{} (\exists v' \in \Theta ^a (L(G)) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{matrix}} \end{aligned}$$

(21)

Proof of (21) $\Rightarrow$ (20): Suppose (21) is true. Then, for $s', u', v'$ in (21), we have

$$\begin{aligned}&s' u' \in \Theta ^a (L(G)) \wedge v' \in \Theta ^a (L(G)) \\ \Rightarrow&(\exists s u \in L(G)) s' u' \in \Theta ^a (s u) \\&\wedge (\exists v \in L(G)) v' \in \Theta ^a (v) . \end{aligned}$$

Since $s'\in \Psi (\Theta ^a (L(G))) \Rightarrow \Sigma _f \in s'u'$. By Assumption A3, $\Sigma _f \in s u$. Let $s u \in L(G)$ be such that $s\in \Psi (L(G)) \wedge s' \in \Theta ^a (s)$. Then,

$$\begin{aligned}&su \in L(G) \Rightarrow u \in L(G)/s \\&\Sigma _f \not \in v' \Rightarrow \Sigma _f \not \in v \ \ \ (\text{ by } \text{ Assumption } \text{ A3}) \\&P(v') = P(s' u') \Rightarrow (\exists w) w = P(v') = P(s' u') \\&\Rightarrow (\exists w) w \in P(\Theta ^a (v)) \wedge w \in P(\Theta ^a (s u)) \\&\Rightarrow (\exists w) w \in \Phi ^a (v) \wedge w \in \Phi ^a (s u) \\&\Rightarrow \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset . \end{aligned}$$

Therefore,

$$\begin{aligned}&(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&(\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v , \end{aligned}$$

that is, (20) is true.

Proof of (20) $\Rightarrow$ (21): Suppose (20) is true. Then, for s, u, v in (20), we have

$$\begin{aligned}&\Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \\ \Rightarrow&P(\Theta ^a(v)) \cap P(\Theta ^a(s u)) \not = \emptyset \\ \Rightarrow&(\exists w) w \in P(\Theta ^a(v)) \wedge w \in P(\Theta ^a(s u)) \\ \Rightarrow&(\exists w, v', s' u') v' \in \Theta ^a(v) \wedge s' u' \in \Theta ^a(s u) \\&\wedge w=P(v')=P(s' u') \\ \Rightarrow&(\exists v', s' u') v' \in \Theta ^a(v) \wedge s' u' \in \Theta ^a(s u) \\&\wedge P(v')=P(s' u') . \end{aligned}$$

Since $s\in \Psi (L(G)) \Rightarrow \Sigma _f \in su$. By Assumption A3, $\Sigma _f \in s' u'$. Let $s'u' \in \Theta ^a (s u)$ be such that $s'\in \Psi (\Theta ^a (L(G))) \wedge s' \in \Theta ^a (s)$. Then,

$$\begin{aligned}&su \in L(G) \Rightarrow s' u' \in \Theta ^a (L(G)) \Rightarrow u' \in \Theta ^a (L(G))/s' \\&v \in L(G) \Rightarrow v' \in \Theta ^a (L(G)) \\&\Sigma _f \not \in v \Rightarrow \Sigma _f \not \in v' ( \text{ by } \text{ Assumption } \text{ A3}) . \end{aligned}$$

Therefore,

$$\begin{aligned}&(\exists s'\in \Psi (\Theta ^a (L(G))))(\exists u' \in \Theta ^a (L(G))/s') \\&(\exists v' \in \Theta ^a (L(G)) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{aligned}$$

that is, (20) is true.

Let us now prove (18) if and only if (19).

Proof of (19) $\Rightarrow$ (18): Suppose (19) is true. Then, for any $n \in \mathcal{{N}}$, let $n' = n + d$, where d is given in Assumption A4.

Because (21) $\Rightarrow$ (20), we have

$$\begin{aligned}&(\exists s'\in \Psi (\Theta ^a (L(G))))(\exists u' \in \Theta ^a (L(G))/s') \\&|u'| \ge n' \wedge (\exists v' \in \Theta ^a (L(G)) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' \\ \Rightarrow&(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&(\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v \end{aligned}$$

Furthermore, by the proof of (21) $\Rightarrow$ (20),

$$\begin{aligned}&s \in L(G) \wedge u \in L(G)/s \wedge s' \in \Theta ^a (s) \\&\wedge u' \in \Theta ^a(L(G))/s' \wedge s' u' \in \Theta ^a (s u) \end{aligned}$$

By Assumption A4, we have $|(|u|-|u'|)| \le d$. Hence,

$$\begin{aligned}&|u'| \ge n' \wedge |(|u|-|u'|)| \le d \\ \Rightarrow&|u'| \ge n' \wedge |u'|-|u| \le d \\ \Rightarrow&|u'| \ge n' \wedge |u| \ge |u'|-d \\ \Rightarrow&|u| \ge n'-d =n . \end{aligned}$$

Therefore, (18) is true.

Proof of (18) $\Rightarrow$ (19): Suppose (18) is true. Then, for any $n' \in \mathcal{{N}}$, let $n = n' + d$, where d is given in Assumption A4.

Because (20) $\Rightarrow$ (21), we have

$$\begin{aligned}&(\exists s\in \Psi (L(G)))(\exists u \in L(G)/s) \\&|u| \ge n \wedge (\exists v \in L(G)) \Phi ^a(v) \cap \Phi ^a(s u) \not = \emptyset \wedge \Sigma _f \not \in v \\ \Rightarrow&(\exists s'\in \Psi (\Theta ^a (L(G))))(\exists u' \in \Theta ^a (L(G))/s') \\&(\exists v' \in \Theta ^a (L(G)) ) P(v') = P(s' u') \wedge \Sigma _f \not \in v' . \end{aligned}$$

Furthermore, by the proof of (20) $\Rightarrow$ (21),

$$\begin{aligned}&s \in L(G) \wedge u \in L(G)/s \wedge s' \in \Theta ^a (s) \\&\wedge u' \in \Theta ^a(L(G))/s' \wedge s' u' \in \Theta ^a (s u) \end{aligned}$$

By Assumption A4, we have $|(|u|-|u'|)| \le d$. Hence,

$$\begin{aligned}&|u| \ge n \wedge |(|u|-|u'|)| \le d \\ \Rightarrow&|u| \ge n \wedge |u|-|u'| \le d \\ \Rightarrow&|u| \ge n \wedge |u'| \ge |u|-d \\ \Rightarrow&|u'| \ge n-d =n' . \end{aligned}$$

Therefore, (19) is true.