Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Diagnosability and attack detection for discrete event systems under sensor attacks

  • Published:
Discrete Event Dynamic Systems Aims and scope Submit manuscript

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.

This is a preview of subscription content,log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19
Fig. 20
Fig. 21
Fig. 22

Similar content being viewed by others

Notes

  1. One could think of the acronym ALTER as capturing the keywords: Attack Language, Transition-BasEd, Replacement.

  2. The technique of modifying the system model to embed attacks has been used in other works that have considered attacks on DES, but the details often differ based on the type of attack considered.

  3. In prior work, it is usually assumed that either an attack model is known or an “all-out” attack model is used. We adopt the same viewpoint in this paper. Basically, if one is going to test the vulnerabilities of a system, then one must start with potential vulnerabilities.

References

  • Alves MRC, Pena PN, Rudie K (2022) Discrete-event systems subject to unknown sensor attacks. Discrete Event Dynamic Systems: Theory and Applications 32:143–158

    Article MathSciNet  Google Scholar 

  • Alves MV, Barcelos RJ, Carvalho LK, Basilio JC (2022) Robust decentralized diagnosability of networked discrete event systems against dos and deception attacks. Nonlinear Anal Hybrid Syst 44:101162

    Article MathSciNet  Google Scholar 

  • Basilio JC, Hadjicostis CN, Su R (2021) Analysis and control for resilience of discrete event systems: Fault diagnosis, opacity and cyber security. Foundations and Trends in Systems and Control 8(4):285–443

    Article  Google Scholar 

  • Carvalho LK, Wu YC, Kwong R, Lafortune S (2018) Detection and mitigation of classes of attacks in supervisory control systems. Automatica 97:121–133

    Article MathSciNet  Google Scholar 

  • Carvalho LK, Moreira MV, Basilio JC (2021) Comparative analysis of related notions of robust diagnosability of discrete-event systems. Annu Rev Control 51:23–36

    Article MathSciNet  Google Scholar 

  • Cassandras CG, Lafortune S (2021) Introduction to Discrete Event Systems. Springer Nature, 3rd ed

  • Dibaji SM, Pirani M, Flamholz DB, Annaswamy AM, Johansson KH, Chakrabortty A (2019) A systems and control perspective of CPS security. Annu Rev Control 47:394–411

    Article MathSciNet  Google Scholar 

  • Duo W, Zhou M, Abusorrah A (2022) A survey of cyber attacks on cyber physical systems: Recent advances and challenges. IEEE/CAA Journal of Automatica Sinica 9(5):784–800

    Article  Google Scholar 

  • Ghasaei A, Zhang ZJ, Wonham WM, Iravani R (2020) A discrete-event supervisory control for the AC microgrid. IEEE Trans Power Delivery 36(2):663–675

    Article  Google Scholar 

  • Hadjicostis CN, Lafortune S, Lin F, Su R (2022) Cybersecurity and supervisory control: A tutorial on robust state estimation, attack synthesis, and resilient control. In: 2022 IEEE 61st Conference on Decision and Control (CDC), pp. 3020–3040, IEEE

  • Hadjicostis CN (2021) Estimation and Inference in Discrete Event Systems. Springer

    Google Scholar 

  • Kharrazi A, Mishra Y, Sreeram V (2017) Discrete-event systems supervisory control for a custom power park. IEEE Transactions on Smart Grid 10(1):483–492

    Article  Google Scholar 

  • Li Y, Hadjicostis CN, Wu N (2022) Tamper-tolerant diagnosability under bounded or unbounded attacks. IFAC-PapersOnLine 55(28):52–57

    Article  Google Scholar 

  • Lin F, Wonham WM (1988) On observability of discrete-event systems. Inf Sci 44(3):173–198

    Article MathSciNet  Google Scholar 

  • Lin L, Zhu Y, Su R (2020) Synthesis of covert actuator attackers for free. Discrete Event Dynamic Systems: Theory and Applications 30:561–577

    Article MathSciNet  Google Scholar 

  • Lin F, Lafortune S, Wang C (2023) Diagnosability of discrete event systems under sensor attacks. IFAC-PapersOnLine 56(2):3572–3578

    Article  Google Scholar 

  • Matsui S, Lafortune S (2022) Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies. Discrete Event Dynamic Systems 32(4):573–610

    Article MathSciNet  Google Scholar 

  • Meira-Góes R, Kang E, Kwong RH, Lafortune S (2020) Synthesis of sensor deception attacks at the supervisory layer of cyber-physical systems. Automatica 121:109172

    Article MathSciNet  Google Scholar 

  • Porche III IR (2019) Cyberwarfare: An Introduction to Information-AgeConflict.Artech House

  • Ramadge PJ, Wonham WM (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25(1):206–230

    Article MathSciNet  Google Scholar 

  • Rashidinejad A, Wetzels B, Reniers M, Lin L, Zhu Y, Su R (2019) Supervisory control of discrete-event systems under attacks: An overview and outlook. 2019 18th European Control Conference (ECC), pp. 1732–1739, IEEE

  • Reshmila S, Devanathan R (2016) Diagnosis of power system failures using observer based discrete event system. In: 2016 IEEE First International Conference on Control, Measurement and Instrumentation (CMI), pp. 131–135, IEEE

  • Romero-Rodríguez M, Delpoux R, Piétrac L, Dai J, Benchaib A, Niel E (2019) An implementation method for the supervisory control of time-driven systems applied to high-voltage direct current transmission grids. Control Eng Pract 82:97–107

    Article  Google Scholar 

  • Saleh JH, Saltmarsh EA, Favarò FM, Brevault L (2013) Accident precursors, near misses, and warning signs: Critical review and formal definitions within the framework of discrete event systems. Reliability Engineering & System Safety 114:148–154

    Article  Google Scholar 

  • Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete-event systems. IEEE Trans Autom Control 40(9):1555–1575

    Article MathSciNet  Google Scholar 

  • Seatzu C, Silva M, Van Schuppen JH (2013) Control of discrete-event systems, vol. 433. Springer

  • Su R (2018) Supervisor synthesis to thwart cyber attack with bounded sensor reading alterations. Automatica 94:35–44

    Article MathSciNet  Google Scholar 

  • Tai R, Lin L, Su R (2023) Synthesis of optimal covert sensor-actuator attackers for discrete-event systems. Automatica 151:110910

    Article MathSciNet  Google Scholar 

  • Takai S (2021) A general framework for diagnosis of discrete event systems subject to sensor failures. Automatica 129:109669

    Article MathSciNet  Google Scholar 

  • Tong Y, Wang Y, Giua A (2022) A polynomial approach to verifying the existence of a threatening sensor attacker. IEEE Control Systems Letters 6:2930–2935

    Article MathSciNet  Google Scholar 

  • Wakaiki M, Tabuada P, Hespanha JP (2019) Supervisory control of discrete-event systems under attacks. Dynamic Games and Applications 9(4):965–983

    Article MathSciNet  Google Scholar 

  • Wonham WM, Cai K (2019) Supervisory control of discrete-event systems. Springer

    Book  Google Scholar 

  • Wonham W, Cai K, Rudie K (2018) Supervisory control of discrete-event systems: A brief history. Annu Rev Control 45:250–256

    Article MathSciNet  Google Scholar 

  • Zhang Q, Li Z, Seatzu C, Giua A (2018) Stealthy attacks for partially-observed discrete event systems. In: 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), vol. 1, pp. 1161–1164, IEEE

  • Zhang Q, Seatzu C, Li Z, Giua A (2022) Selection of a stealthy and harmful attack function in discrete event systems. Scientific Reports 12

  • Zhao B, Lin F, Wang C, Zhang X, Polis MP, Wang LY (2015) Supervisory control of networked timed discrete event systems and its applications to power distribution networks. IEEE Transactions on Control of Network Systems 4(2):146–158

    Article MathSciNet  Google Scholar 

  • Zheng S, Shu S, Lin F (2021) Modeling and control of discrete event systems under joint sensor-actuator cyber attacks. In: IEEE International Conference on Automation, Control and Robotics Engineering (CACRE 2021), pp. 1–8, IEEE

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering, Wayne State University, Detroit, MI, 48202, USA

    Feng Lin & Caisheng Wang

  2. Department of Electrical Engineering and Computer Science, University of Michigan, Ann Arbor, MI, 48109, USA

    Stéphane Lafortune

Authors
  1. Feng Lin

    You can also search for this author inPubMed Google Scholar

  2. Stéphane Lafortune

    You can also search for this author inPubMed Google Scholar

  3. Caisheng Wang

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence toFeng Lin.

Ethics declarations

Conflict of Interest

The authors have no competing interests to declare that are relevant to the content of this article.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work is supported in part by the US National Science Foundation under grants ECCS-2146615 and ECCS-2144416.

Appendix

Appendix

Proof of Theorem1

Let us take negations of the conditions in Theorem1 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, fors, 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\), whered 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\), whered 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.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Lin, F., Lafortune, S. & Wang, C. Diagnosability and attack detection for discrete event systems under sensor attacks.Discrete Event Dyn Syst34, 465–495 (2024). https://doi.org/10.1007/s10626-024-00401-6

Download citation

Keywords

Access this article

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Advertisement

[8]ページ先頭
©2009-2025 Movatter.jp