PaperlayerView exact revision on arXiv

Source-linked AI summary

CA-Observability of Discrete Event Systems under Cyber Attacks

Shengbao Zheng, Shaolong Shu, Feng Lin

arXiv:2610.08263v1eess.SYcs.SY

TL;DR

Conventional observability methods cannot be extended to CA-observability under cyber attacks, leaving a distinct checking problem. The paper constructs an augmented automaton and develops an algorithm to check the property, then characterizes its closure behavior and a method for constructing a suitable sublanguage. It shows that CA-observability is closed under neither intersection nor union.

  • Problem

    Methods for conventional observability cannot be extended to CA-observability, which is needed in studying supervisory control under cyber attacks.

    Source: §I · pp. 1–2

  • Method

    The paper builds an augmented automaton pairing the current system state with state estimates, proves an equality test for CA-observability, and develops a checking algorithm.

    Source: §I · p. 2, §III · pp. 5–6

  • Results

    CA-observability is closed under neither intersection nor union, and the paper constructs a CA-controllable and CA-observable sublanguage using a state-estimate-based supervisor.

    Source: §I · p. 2, §VI · p. 8, APPENDIX III PROOF OF THEOREM 4 · p. 10

  • Takeaways & Limitations

    Because closure under intersection and union fails, the infimal CA-observable superlanguage and supremal CA-observable sublanguage may not exist.

    Source: §I · p. 2

Abstract

from arXiv · show

In a previous paper, we investigate the control problem of discrete event systems under cyber attacks, where CA-controllability and CA-observability are proposed. We prove that a discrete event system can be controlled to generate a specification language K if and only if K is CA-controllable and CA-observable. While CA controllability can be "converted" to (conventional) controllability, CA-observability cannot be "converted" to (conventional) observability. In this paper, we further investigate CA-observability. We develop a method and an algorithm to check CA-observability. The method involves constructing an augmented automaton whose states are pairs of the current state and state estimate of the supervised system. We prove that K is CA-observable if and only if the language generated by the augmented automaton is equal to K. An algorithm is then developed to check CA-observability. We also investigate the properties of CA-observability. We show that CA-observability is not closed under (set) in tersection. Note that (conventional) observability is closed under intersection. We further show that CA-observability is not closed under union. This is similar to observability. If K is not CA-controllable and CA-observable, we pro pose a method to calculate a CA-controllable and CA observable sublanguage. We first calculate the supremal CA-controllable sublanguage for K which can be described by a sub-automaton of the automaton for K. We then propose a state-estimate-based supervisor based on the subautomaton, which ensures the supervised system stays within K.

I. INTRODUCTION

Networked control faces communication delays and losses, as well as cyber-attack risks, motivating robust supervisory control for discrete event systems. This paper develops ways to check CA-observability, characterizes its closure properties, and constructs a CA-controllable and CA-observable sublanguage with a state-estimate-based supervisor.

I. INTRODUCTION

  • Robust networked control must account for unavoidable communication delays and losses and the increased likelihood of cyber attacks on shared networks.The introduction identifies robustness to both network effects and cyber attacks as challenges.Source: §I · p. 1
  • An augmented automaton combining system states with state estimates supports a method and algorithm for checking CA-observability.The paper proves that K is CA-observable exactly when the augmented automaton generates K.Source: §I · p. 2
  • CA-observability is closed under neither intersection nor union, unlike conventional observability's closure under intersection.Consequently, the infimal CA-observable superlanguage and supremal CA-observable sublanguage may not exist.Source: §I · p. 2
  • A state-estimate-based supervisor built from the supremal CA-controllable sublanguage yields a suitable CA-controllable and CA-observable sublanguage of K.The sublanguage is represented by a sub-automaton of the automaton for K.Source: §I · p. 2
  • The paper's contributions beyond are a CA-observability checking approach, closure results, and a sublanguage calculation method with a state-estimate-based supervisor.The supervisor controls the system to generate the calculated sublanguage.Source: §I · p. 2

A. Discrete Event Systems

The paper models a discrete event system as an automaton and uses languages and event projections to describe its behavior under partial observation.

A. Discrete Event Systems

  • A discrete event system is modeled as an automaton with states Q, events Σ, a partial transition function δ, initial state q0, and marked states Qm.The paper assumes all states are marked, so Qm = Q.Source: A. Discrete Event Systems · p. 3
  • The generated language consists of strings defined from the initial state, while the marked language consists of strings that also end in a marked state.The generated language is prefix-closed.Source: A. Discrete Event Systems · p. 3
  • Events are divided into controllable and uncontrollable sets and observable and unobservable sets; projection P removes unobservable events from a string.The paper denotes the observable and unobservable transitions by δo and δuo, respectively.Source: A. Discrete Event Systems · p. 3

B. ALTER Model

The ALTER model represents sensor attacks as transition-based languages of possible replacements for observed events, accommodating multiple attacked observations.

B. ALTER Model

  • For each attackable transition, the ALTER model assigns an attack language specifying the strings an attacker may substitute for its event.The language is based on the attacker's knowledge and the corresponding sensor.Source: B. ALTER Model · p. 3
  • The model permits nondeterministic attacks and includes no change, deletion, replacement, and insertion as special cases.Each case corresponds to a possible altered string in the transition's attack language.Source: B. ALTER Model · p. 3
  • ALTER composes the attack mapping Θπ with partial-observation projection P to represent observations under sensor attacks.The resulting mapping Φπ(s) can contain multiple observed strings for a system string s.Source: B. ALTER Model · p. 3
  • The ALTER model is general enough to include deletion, insertion, and replacement, while representing attacks through specific attack languages.Those languages are specified by a model builder based on the attacker's knowledge.Source: B. ALTER Model · p. 3

C. Supervisory Control

The supervisory-control section models how attackers can alter observations and control commands, then uses state estimates and attack-aware automata to formulate safety control under cyber attacks.

C. Supervisory Control

  • After an attack-altered observation w, the supervisor selects a set of enabled events, while attackers may alter control commands by enabling or disabling attackable controllable events.Uncontrollable events must remain enabled and cannot be disabled by attackers.Source: C. Supervisory Control · p. 4
  • Attacks can make the supervised system's generated language nondeterministic, so the paper uses the large language as an upper bound on possible generated languages.The large language is defined recursively.Source: C. Supervisory Control · p. 4
  • The safety specification K is generated by a sub-automaton whose states are safe, and the control objective is to keep the supervised system's large language within K.The desired large language may be equal to or contained in K.Source: C. Supervisory Control · p. 4
  • The state estimate comprises states the attacked supervised system may occupy after an observed string, with reachable states restricted to H when enforcing K.The estimate is based on observations in Φπ(L(H)).Source: C. Supervisory Control · p. 4
  • The construction replaces attackable transitions in H with automata for their attack languages, then models unobservable transitions as ε-transitions.The resulting nondeterministic automaton marks Θπ(L(H)) before partial observation is incorporated.Source: C. Supervisory Control · p. 4
  • The CA-observer computes estimates from observed strings, and the CA-supervisor uses those estimates to prevent entry into unsafe states.The estimate after w is ξ(x0, w) ∩ QH.Source: C. Supervisory Control · p. 5

III. CHECKING CA-OBSERVABILITY

The section checks CA-observability by constructing an augmented automaton and testing whether its generated language equals the specification. It also illustrates the test on an example.

III. CHECKING CA-OBSERVABILITY

  • The analysis assumes K is CA-controllable, which can be ensured when all events are controllable and control-channel attacks are absent.This isolates the question of CA-observability.Source: §III · p. 5
  • Each augmented-automaton state pairs the plant’s current state with the set of possible state estimates.The construction starts from (q0, {x0}).Source: §III · p. 5
  • K is CA-observable if and only if the augmented automaton generates exactly K.The augmented automaton’s language equals the supervised system’s large language.Source: §III · p. 6
  • The checking algorithm builds a nondeterministic automaton, a CA-observer, and an augmented automaton, then tests enabled-event equality.It returns Yes when the equality holds for every augmented state, and No otherwise.Source: §III · p. 6
  • In Example 1, the enabled-event equality test holds, so the specification language K is CA-observable.The example constructs the attack-replaced nondeterministic automaton, CA-observer, and augmented automaton before applying the test.Source: §III · p. 6

IV. PROPERTIES OF CA-OBSERVABILITY

CA-observability is closed under neither intersection nor union, unlike conventional observability, which is closed under intersection. These failures mean certain infimal superlanguages or supremal sublanguages may not exist.

IV. PROPERTIES OF CA-OBSERVABILITY

  • K1 and K2 being CA-observable does not ensure their intersection is CA-observable, so an infimal CA-observable superlanguage may not exist.Conventional observability is closed under intersection, and its infimal observable superlanguage always exists.Source: §IV · p. 7
  • K1 and K2 being CA-observable does not ensure their union is CA-observable, so a supremal CA-observable sublanguage may not exist.This is similar to conventional observability, which is not closed under union.Source: §IV · p. 7

V. CA-CONTROLLABLE AND CA-OBSERVABLE

The paper constructs a CA-controllable and CA-observable sublanguage of K using the supremal CA-controllable sublanguage and a state-estimate-based supervisor. The resulting sublanguage may not be maximal.

V. CA-CONTROLLABLE AND CA-OBSERVABLE

  • The method starts with the supremal CA-controllable sublanguage K↑, represented by a sub-automaton of the automaton for K.CA-controllability is closed under union, so K↑ exists.Source: §V · p. 7
  • The construction removes states that can reach illegal states through uncontrollable and/or attackable events.The resulting automaton is used in the subsequent construction procedure.Source: §V · p. 7
  • The proposed state-estimate-based supervisor yields a controlled-system language that is a CA-controllable and CA-observable sublanguage of K.The paper describes this language as suitable for synthesizing a supervisor when K is not CA-controllable and CA-observable.Source: §V · p. 7
  • The resulting CA-controllable and CA-observable sublanguage may not be maximal, and finding a maximal one remains open.A supremal CA-observable sublanguage of K may not exist.Source: §V · p. 7

VI. CONCLUSION

The paper presents an augmented-automaton test for CA-observability, shows that CA-observability is not closed under intersection or union, and constructs a CA-controllable and CA-observable sublanguage with a state-estimate-based supervisor.

VI. CONCLUSION

  • The paper checks CA-observability, establishes its failure of closure under intersection and union, and constructs a CA-controllable and CA-observable sublanguage using a state-estimate-based supervisor.The supervisor is based on the supremal CA-controllable sublanguage and constrains the closed-loop system to the resulting sublanguage.Source: §VI · p. 8

APPENDIX I PROOF OF THEOREM 2

  • For strings in the augmented automaton, the proof represents the reached state as a pair (q, X) and follows its transitions event by event.The induction step considers an event σ and the resulting augmented state (q′, X′).Source: Appendix I · p. 8

APPENDIX II PROOF OF THEOREM 3

APPENDIX III PROOF OF THEOREM 4

  • The proof shows that individually CA-observable K1 and K2 can have an intersection that is not CA-observable.The augmented automaton for K1 ∩ K2 generates a language unequal to K1 ∩ K2.Source: APPENDIX III PROOF OF THEOREM 4 · pp. 9–10

APPENDIX IV PROOF OF THEOREM 5

  • The proof shows that individually CA-observable K1 and K2 can have a union that is not CA-observable.The augmented automaton for K1 ∪ K2 generates a language unequal to K1 ∪ K2.Source: APPENDIX IV PROOF OF THEOREM 5 · pp. 10–11

APPENDIX V PROOF OF THEOREM 6

The proof establishes properties of the constructed language and uses induction to relate its transitions to those of the system and subautomaton.

APPENDIX V PROOF OF THEOREM 6

  • K↑ is CA-controllable with respect to L(G), Σuc, and Σa.Source: Appendix V · p. 11
  • The proof states that the constructed language is CA-controllable and CA-observable, and is a sublanguage of K.Source: Appendix V · p. 11
  • The proof uses induction on string length and considers extensions sσ that remain in L(G) and K↑.Source: Appendix V · pp. 11–12
Loading 2610.08263v1…