Non-Deterministic Liveness-Enforcing Supervisor Tolerant to Sensor-Reading Modification Attacks

Dan You ,,, and Shouguang Wang , Senior,

Abstract—In this paper, we study the supervisory control problem of discrete event systems assuming that cyber-attacks might occur.In particular, we focus on the problem of liveness enforcement and consider a sensor-reading modification attack(SM-attack) that may disguise the occurrence of an event as that of another event by intruding sensor communication channels.To solve the problem, we introduce non-deterministic supervisors in the paper, which associate to every observed sequence a set of possible control actions offline and choose a control action from the set randomly online to control the system.Specifically, given a bounded Petri net (PN) as the reference formalism and an SMattack, an algorithm that synthesizes a liveness-enforcing nondeterministic supervisor tolerant to the SM-attack is proposed for the first time.

I.INTRODUCTION

Acyber-physical system (CPS) integrates computing and communication to monitor and control physical processes [1].The use of communication networks not only endows the physical components of CPS with information processing and communication capabilities, but also increases the vulnerability of CPS to cyber-attacks [2].The supervisory control of CPS under cyber-attacks has been receiving more and more attentions, especially in the area of discrete event systems (DESs).By modeling a CPS as a DES, the existing studies dealing with attack issues can be classified into three categories, namely, attack strategy design [3]-[5], attack detection and defense [6]-[10], and robust/tolerant supervisor design [3], [11]-[19].In this work, we investigate the design of robust/tolerant supervisors in the sense that a given control specification can be satisfied by such a supervisor despite the existence of attacks.

Much attention has been paid to the robust/tolerant supervisor design in the literature.Wakaikiet al.[11] design a supervisor robust against the so-called replacement-removal attacks in the sensor channels.In more detail, the attacker may erase an event produced by the plant or replace it with another one by tampering with sensor-readings in related sensor channels.Essentially, their work is similar to the work dealing with the supervisory control of DES with nondeterministic observations [13]-[15].The conditions under which a supervisor exists exactly enforcing a given control specification are provided in [13], [14], while a supervisor synthesis method is given in [15] using a model transformation technique.Su [3]considers sensor deception attacks as well but requires attacks to be stealthy, which means that the supervisor cannot be aware of the existence of attacks.Specifically, the attacker may replace an observable event generated by the plant with a bounded sequence of observable events.From the viewpoint of an attacker, the supremal stealthy attack strategy is computed first and then a supervisor robust against the attack is synthesized from the viewpoint of a system defender.Meira-Góeset al.[12] investigate the synthesis of supervisors robust to parameterized sensor deception attacks.In addition to sensor deception attacks, actuator deception attacks are taken into account in [16]-[18].

The above studies basically consider language or state specifications.In contrast, the liveness-enforcing control specification has received little attention in the presence of attacks.Liveness is a property characterizing a specific dynamic behavior of a system.How to enforce liveness has been widely studied in different problem settings [20]-[23].Nevertheless, to our best knowledge, [19] is the only work dealing with the liveness-enforcing problem under attacks.In [19], the problem is investigated based on bounded Petri net (PN) systems [24], [25] and sensor-reading modification attacks (SMattacks) are considered, which are a particular class of the replacement-removal attacks in [11].In the scenario of SMattacks, an intruder has the ability to disguise the occurrence of some transitions as that of other transitions by modifying sensor-readings in vulnerable sensor channels.An algorithm that synthesizes a liveness-enforcing supervisor tolerant to SM-attacks is provided in [19].Unfortunately, the supervisor is not guaranteed to be maximally permissive.How to get a maximally permissive liveness-enforcing supervisor tolerant to an SM-attack remains an open issue.

We note that the supervisor in [19] refers to a deterministic supervisor, which means that the supervisor associates every observed sequence with a unique control action.In contrast to deterministic supervisors, there are non-deterministic supervisors.In simple words, a non-deterministic supervisor associates every observed sequence with a set of possible control actions.Which one is chosen to control the system is determined randomly online.Non-deterministic supervisors are first proposed to tackle the standard supervisory control problem under partial observation [26], [27].Compared with using deterministic supervisors, the main advantages of using them include that 1) The complexity of synthesizing a supervisor is reduced from being exponential to polynomial; and 2) More control specifications can be realized such as temporal logic CTL* [28] andμ-calculus [29].Moreover, in the setting of the non-deterministic plant and non-deterministic control specification, non-deterministic supervisors are capable of solving a(bi)similarity control problem [29]-[33].Recently, they are also used to solve an opacity enforcing problem [34].

In this paper, we design non-deterministic supervisors to enforce the property of liveness on DES under SM-attacks.As far as we know, the liveness-enforcing problem under attacks has never been solved by using non-deterministic supervisors.Indeed, in the scenario of SM-attacks, it could happen that an observation does not explicitly reflect real information.For example, in the case that an SM-attack may disguise the firing of transitiont1as the firing of transitiont2, when we observet2, we are not sure which transition fires producing the observationt2ift1andt2are both enabled.It is the vague information that makes the liveness-enforcing problem under SM-attacks very complex.The use of a non-deterministic supervisor can exactly eliminate the vague situation and keep more possible behavior of the controlled system.In the above example, a non-deterministic supervisor may give two possible control actions, namely, disablingt1ort2.No matter which one is chosen online to control the system, we know with certainty which transition fires producing the observationt2.Following this basic idea, we develop an algorithm in the paper,which synthesizes a liveness-enforcing non-deterministic supervisor tolerant to an SM-attack.We may see that, compared with the current methods that synthesize a deterministic supervisor, the proposed method enjoys lower computational complexity in synthesizing a non-deterministic one.Note that as in [19] PNs are used as a modeling tool to solve the problem in this paper and only bounded PN systems are considered.

The remainder of the paper is organized as follows.Section II reviews the basic notions involved in the paper.Section III formulates the problem to be addressed in the paper.How to synthesize a non-deterministic liveness-enforcing supervisor tolerant to SM-attacks is answered in Section IV.Discussion on the proposed method is provided in Section V.Section VI concludes this paper and indicates future work.

II.PRELIMINARIES

A. Petri Nets

A reachability graph (RG) of a PN system (N,m0) is a directed graph describing the system evolution.Specifically,each node of the RG corresponds to a reachable markingm∈R(N,m0) and each arc is labelled by a transitiont∈T.Specifically, there exists an arc labelled by transitiontfrom a node representing markingm1to a node representing markingm2in the RG if and only if it holds thatm1[t〉m2.

B. Deterministic and Non-Deterministic Supervisors

Given a PN system (N,m0), we useLo(N,m0) to denote the set of all possible observed sequences of the system and use Δ =2Tto denote the set of all control actions, each of which refers to a set of transitions to be disabled, or equivalently, whose firing should be forbidden.

A deterministic supervisor of a PN system (N,m0) isμ:Lo(N,m0)→Δ, associating to every observed sequence a control action.A non-deterministic supervisor of a PN system (N,m0) isμ:Lo(N,m0)→2Δ, associating to every observed sequence a set of control actions.It is worth noting that only one control action is chosen among the set to control the PN system during its evolution and it is chosen online non-deterministically.

Given a PN system (N,m0) and a supervisorμ, we denote the system under the control ofμas (N,m0)|μand the set of reachable markings of (N,m0)|μasR(N,m0)|μ.

A supervisorμis said to beliveness-enforcingfor a PN system (N,m0) if the controlled system (N,m0)|μis live, i.e.,∀t∈T, ∀m∈R(N,m0)|μ, ∃m'∈R(N,m)|μ, s.t.m'[μt〉, wherem'[μt〉 denotes thattcan fire at markingm'under the control ofμ.

C. SM-Attacks

We define an SM-attack as a mappingO:T→2T.

The setO(t) enumerates all the possible observations whentoccurs due to the existence of the SM-attack.

Example 1: Consider a bounded PN (N,m0) with the set of transitionsT= {t1,t2,t3} and an SM-attackOsuch thatO=[O(t1),O(t2),O(t3)]T= [{t1}, {t2,t3}, {t3}]T.We can see that,due to the existence of the SM-attack, the occurrence oft2might produce the observationt2ort3.In other words, the occurrence oft2is possibly disguised as the occurrence oft3.As fort1andt3, their observations can never be changed.

We may generalize the notationO(·) to a sequence of transitionsσ=t1t2…tk∈T*such thatO(σ) =O(t1)O(t2)…O(tk).Note that given two setsAandB, it is defined thatAB= {ab|a∈A,b∈B}.Then, given a PN system (N,m0) and an SM-attackO, we have

III.PROBLEM STATEMENT

The problem that we plan to address in the paper is formulated as follows.

Problem 1: Given a bounded PN system (N,m0) and an SMattackO, design a liveness-enforcing supervisor tolerant toO.

“Tolerant” means that the supervisor is liveness-enforcing even in the presence of an SM-attack.The problem has been investigated in [19], where the solution is a deterministic supervisor that is not guaranteed to be maximally permissive.In this work, we intend to solve the problem by designing a supervisor that is allowed to be non-deterministic.

IV.NON-DETERMINISTIC CONTROL

In this section, we first introduce a so-called supervisor graph that represents a supervisor in this paper and then provide an algorithm that synthesizes a non-deterministic supervisor for solving Problem 1.

A. Supervisor Graph

A structure called a supervisor graph is formally defined in[19] to describe a deterministic supervisor intuitively.We still use it in this paper but with some modification such that it can describe a non-deterministic supervisor as well.In simple words, a supervisor graph is now a directed graph where a node is assigned to be an initial node, each arc is labelled by a transition and each node is associated with a set of control actions.Note that we simply writeμ(x) to represent the set of control actions associated with a nodex.Indeed, for all observed sequences leading from the initial node to nodexin a supervisor graph, they are associated with the same set of control actions, i.e.,μ(x).

Example 2: Fig.1 shows a supervisor graph with an initial nodex0.It tells that 1) for any observed sequence leading from initial nodex0to nodex1, the set of control actions is{{t2}, {t3}}, which means that it is chosen non-deterministically online to disablet2ort3; 2) for any observed sequence leading fromx0tox3,t1should be disabled; and 3) for any observed sequence leading fromx0to nodex0orx2, no transition should be disabled.To be intuitive, nodes with a nonempty set of control actions are colored in grey.

In the remainder of the paper, we omit writingμ(x) = ∅ for every nodexin a supervisor graph to save space.Besides, a node in a supervisor graph basically corresponds to a set of markings.Thus, for the sake of simplicity, we may name a node by its corresponding marking set if there is no ambiguity.

Fig.1.Supervisor graph.

Example 3: Consider a PN system (N,m0) in Fig.2(a).Its RGGrshown in Fig.2(b) can be viewed as a supervisor graph of (N,m0).It tells that whatever we observe, we do not disable any transition.Also, graphGlin Fig.3 is a supervisor graph of (N,m0).It indicates that 1) When we observe a sequence (e.g.,t2) leading to node {m1}, we should disablet2;2) When we observe a sequence (e.g.,t2t3) leading to node{m3}, we should disablet4; and 3) When we observe a sequence (e.g.,t3) leading to other nodes, we do not disable any transition.Trivially,Glrepresents a deterministic supervisor since no node is associated with a set containing two or more control actions.

Fig.2.Case study.(a) PN system (N, m0) modelled for chemical reactions;(b) Its RG Gr.

Fig.3.Maximally permissive liveness-enforcing deterministic supervisor Gl of the PN system (N, m0) in Fig.2(a) under no attack.

G'inG, we say thatG'is accessible fromx(or equivalently,xcan accessG') if there exists a nodex'inG'accessible fromx.Note thatxandx'can be the same node and we can see that if a node can access an SCC, the node can access every node in this SCC.Moreover, given a nodexin a supervisor graph, we may use•xto denote the set of input nodes ofxandx•to denote the set of output nodes ofx.A nodexis said to be a sink node if it has no output node, i.e.,x•= ∅.An SCCG'is said to be a sink SCC if no node outsideG'is accessible from a node inG'.

B. Proposed Algorithm

In this subsection, we propose an algorithm to solve Problem 1.To this end, we introduce the following concepts.

Definition 1: Given a setT'⊆Tof transitions and an SMattackO, we say that Π ⊆ 2T'is a feasible partition onT'w.r.t.Oif

1) ∪π∈Ππ =T';

2) ∀π ∈ Π, |π| ≥ 1; and

3) ∀π ∈ Π, (|π| = 1)∨(∀t1,t2∈ π,O(t1)∩O(t2) = ∅).

In Definition 1, condition 1) means that the union of all sets in Π is equal to the setT'; condition 2) requires that every set in Π contains at least one transition; and condition 3) indicates that for every set in Π, either it contains only one transition or no two transitions in it have the same observation.

Definition 2: Given a setT'⊆Tof transitions and an SMattackO, a feasible partition Π ⊆ 2T'is said to be optimal if for any other feasible partition Π' ⊆ 2T', it holds that ∀π ∈ Π,∀π' ∈ Π', π ⊄ π'.

In simple words, when we compute a feasible partition on a set of transitions, we actually divide the set of transitions into several groups such that any two transitions in a group do not have the same observation.The optimality of a feasible partition indicates that no more transition can be added to any group such that the partition remains to be feasible.

We next present a function namedOptimalFeasiblePartition(i.e., Function 1), by which the optimal feasible partition is derived.Note that, given a transitiont∈Tand an SM-attackO, we denoteTe(t) = {t'∈T{t}|O(t)∩O(t') ≠ ∅}, namely,T(t)consists of all transitions who possibly produce the same observation astdue to the SM-attackO.

Function 1 Π := OptimalFeasiblePartition (T', O)Input: A set T' ⊆ T of transitions and an SM-attack O;Output: Π ⊆ 2T'.1) Π := {T'};2) for t ∈ T' do 3) for π ∈ Π do images/BZ_246_510_2766_532_2799.pngT(t)4) if t ∈ π ∧ ∩π ≠ ∅ then images/BZ_246_503_2817_525_2850.pngT(t)5) π1 := π and π2: = π{t};6) Π := Π{π}∪{π1, π2};7) end if 8) end for 9) end for 10) output: Π.

Result 1: Given a set of transitionsT'⊆Tand an SM-attackO, Π :=OptimalFeasiblePartition(T',O) is the optimal feasible partition onT'w.r.t.O.

Proof: By contradiction, suppose that Π is not the optimal feasible partition.It means that there exists a feasible partition Π' such that ∃π ∈ Π, ∃π' ∈ Π', π ⊂ π'.Lett∈ π'π.By functionOptimalFeasiblePartition, ∃t'∈ π, s.t.t∈Te(t′) since otherwisetis a transition in π.Hence, we can see that ∃t,t'∈π', s.t.,t∈Te(t′), which contradicts that Π' is a feasible partition.As a result, Π is the optimal feasible partition onT'w.r.t.O.■

Algorithm 1 Supervisor Synthesizer Input: A bounded PN system (N, m0) and an SM-attack O.Output: A supervisor graph G#.1) Gl := MaxLiveEnforceSupervisor (N, m0); /*See Function 2.MaxLiveEnforceSupervisor returns a maximally permissive liveness-enforcing deterministic supervisor of (N, m0) under no attack [19] */2) for each node x in Gl do 3) if x is a confusing node w.r.t.O then TGl out(x)4) Π := OptimalFeasiblePartition ( , O);µ(x):=∪π∈Π{(TGlout(x)π)∪µ(x)}5) ;6) end if TGl 7) for each t ∈ do 8) for t' ∈ O(t){t} do 9) add an arc labelled by t'|t from x to x', where x' is a node reached from node x via an arc labelled by t;10) end for 11) end for 12) end for 13) denote the final graph as G#;14) output: G#.out(x)

Function 2 Gl = MaxLiveEnforceSupervisor (N, m0)Input: A bounded PN system (N, m0) with N = (P, T, F);Output: A maximally permissive liveness-enforcing deterministic supervisor Gl.

1) compute the RG Gr of (N, m0);2) Φ := Tarjan(Gr); /*Tarjan [35] here returns the set of SCCs excluding those that are exactly a single node in Gr */⊄3) Φ# := {α ∈ Φ| T La(α)};4) Gl := Gr;5) while there exists a sink node x or a sink SCC α ∈ Φ# in Gl do 6) if there exists a sink node x in Gl then 7) for each x' ∈ •x do 8) μ(x') := μ(x')∪T', where T' denotes the set of transitions labeling the arcs from x' to x;9) end for 10) update Gl by deleting x and its related arcs;11) end if 12) if there exists a sink SCC α ∈ Φ# in Gl then 13) for each x' ∈ •xα, where xα is a node in α and x' is a node outside α do 14) μ(x'): = μ(x')∪T', where T' denotes the set of transitions labeling the arcs from x' to xα;15) end for 16) update Gl by deleting α and its related arcs;17) end if 18) end while 19) output: Gl.

t

Example 5: Continue to consider Example 4.Suppose that the maximally permissive liveness-enforcing deterministic supervisorGlof the PN system (N,m0) under no attack is computed and there is a nodexinGlsuch that(x) =T'={t1-t5} andμ(x) = {{t6}}.To be intuitive, we consider a case as depicted in Fig.4(a) where only the subgraph ofGlthat consists of nodextogether with its output arcs and nodes is shown.Clearly,xis a confusing node.Let us see how Algorithm 1 works regardingx.First, we compute the optimal feasible partition Π on(x) w.r.t.O, which has been derived in Example 4.Next, it is computed thatμ(x) ={{t2,t3,t6}, {t1,t4,t6}, {t1,t3,t6}}.Finally, we add output arcs to nodex, which results in the subgraph in Fig.4(b).This subgraph tells that a control action at nodexis chosen non-deterministically among{t2,t3,t6}, {t1,t4,t6} and {t1,t3,t6}.Consider as an example that {t2,t3,t6} is chosen as the control action and thent6is observed.By Procedure 1, we should select the arc with labelt6|t1, which means that it is the firing oft1that produces the observationt6, and thus we reach nodex1to determine the next control action.

Given a bounded PN system (N,m0), an SM-attackO, and a supervisorG#computed by Algorithm 1, we have the following result.

Fig.4.Illustrative example: (a) A subgraph of Gl-; (b) A subgraph of G#computed by Algorithm 1.

Lemma 1: Letxandx'be two nodes inG#corresponding to markingsmandm', respectively.It holds thatm'∈R(N,m)|G#if there exists a path from nodexto nodex'inG#.

Proof: Without loss of generality, we assume that the path from nodexto nodex'inG#is

Theorem 1: Given a bounded PN system (N,m0) and an SM-attackO,G#computed by Algorithm 1 is a livenessenforcing supervisor tolerant toOifG#≠ ∅.

Proof: The proof consists of two parts, namely, 1)G#is a feasible supervisor under attackOin the sense thatG#associates every observed sequence a set of control actions; and 2)G#is liveness-enforcing.

1) Algorithm 1 first computes a liveness-enforcing deterministic supervisorGlunder no attack.It means thatGlassociates to every observed sequence, which is also the really occurred sequence, a control action.Structurally,G#is a resultant graph by adding more arcs toGl.Since arcs are added in detail as Steps 7-11 of Algorithm 1 for every node inGl, all the possible observations and their corresponding really fired transitions in the presence of attackOare provided inG#.Moreover, at every confusing nodexinGl(i.e., ∃t1,t2∈(x), s.t.O(t1)∩O(t2) ≠ ∅), we updateμ(x), the set of control actions.Sinceμ(x) is computed based on the optimal feasible partition on(x) w.r.t.O, whatever control action is chosen fromμ(x), we know with certainty which transition actually fires when getting an observation.In other words,when we observe a transition atx, we can find one and only one arc that leads from the node to the next node by Procedure 1.Thus, for every observed sequence, it corresponds to one and only one set of control actions inG#.As a result,G#is a feasible supervisor under attackO.

2) For the sake of simplicity, we say that an SCCG'in a supervisor graph is complete if its arc labels cover all transitions of the considered PN, i.e.,T⊆La(G').Now, we start the proof as follows.

SinceGlis a liveness-enforcing deterministic supervisor under no attack, we have ∀t∈T, ∀m∈R(N,m0)|Gl, ∃m'∈R(N,m)|Gl, s.t.m'[Glt〉.Moreover, every node inGlcan access a complete SCC since (N,m0) is a bounded system.Structurally, every node inG#can also access a complete SCC sinceG#is a resultant graph by adding more arcs toGl.

Letxbe a node inG#corresponding to a markingm.Clearly, there exists a path inG#from the initial nodex0tox.Thus, we havem∈R(N,m0)|G#due to Lemma 1.Also,xcan access a complete SCC.Hence, for eacht∈T, there exists a nodex'with a markingm'in the complete SCC such thatm'∈R(N,m)|G#and ∃Tdis∈μ(x'), s.t.t∉Tdis, i.e.,tcan fire atm'.Trivially, all the markings inG#constitute the setR(N,m0)|G#.As a result, we can see that

Therefore,G#is liveness-enforcing.■

C. Case Study

In this subsection, we provide a case study where the proposed method is applied.This case study is originally presented in [19].

An automatic control system is designed for playing a game on chemical reactions, where chemical (1)-(5) are involved.

Suppose that NaOH, HCl, HNO3and H2O are sufficiently provided and the chemical transformation among Na2CO3,CO2, and NaHCO3is the focus of the game.Consequently, the chemical reactions can be modelled by the PN system in Fig.2(a), wherep1-p3represent NaHCO3, Na2CO3and CO2,respectively, andt1-t5represent the chemical reactions(1)-(5), respectively.To be intuitive, the meanings of places and the needed substances triggering chemical transformation are annotated.Placep1contains two tokens in the initial marking, which models the initial condition that two copies of NaHCO3are provided.The control specification on the system requires that any of the five chemical (1)-(5) can always be performed after finite times of other chemical reactions.This corresponds to the liveness specification on the PN system in Fig.2(a).

The supervisor in the closed-loop control system observes the occurrence of chemical reactions by receiving signals from sensors and gives control actions based on observations.The supervisor communicates with sensors/actuators via communication networks, which makes the system possibly suffer from the intrusion of malicious agents.Suppose that we have the prior knowledge that the sensor signals produced by the chemical (2) are prone to be disguised as the sensor signals produced by the chemical (3) in related sensor communication channels by an intruder.Then, we can see that the system is vulnerable to the SM-attackO= [O(t1),O(t2),O(t3),O(t4),O(t5)]T= [{t1},{t2,t3},{t3}, {t4}, {t5}]T.In other words, the SM-attack may disguise the occurrence oft2as the occurrence oft3.

Now, we compute a liveness-enforcing supervisor tolerant to the SM-attack for the PN system in Fig.2(a) by Algorithm 1.First, we compute a maximally permissive liveness-enforcing deterministic supervisorGlof (N,m0) under no attack, which is shown in Fig.3.Next, we update the set of control actions at every confusing node inGland add more arcs toGl.There are two confusing nodes, i.e., {m0} and {m2}.Consider node{m0}.The optimal feasible partition on({m0}) w.r.t.Ois Π= {{t2,t5},{t3,t5}} and thus we haveμ({m0}) = {{t3}, {t2}}.Then, we add an arc labelled byt3|t2from node {m0} to node{m1}.Similarly, for node {m2}, we haveμ({m2}) = {{t3},{t2}} and add an arc labelled byt3|t2from node {m2} to node{m3}.Since no more arcs should be added, we obtain the final supervisorG#as shown in Fig.5.It is a liveness-enforcing non-deterministic supervisor for the PN system in Fig.2(a) tolerant toO.

Fig.5.Supervisor G# computed by Algorithm 1 in the case study.

V.DISCUSSION

We can see that a non-deterministic supervisor, if associating to every observed sequence a set with only one control action, is essentially a deterministic supervisor; while in other cases, a non-deterministic supervisor can be viewed as the combination of multiple or even countless deterministic supervisors.The online execution of a non-deterministic supervisor is indeed also a procedure of determining a deterministic supervisor that is used to control the system since a control action is fixed online every time a sequence is observed.

Consider the non-deterministic supervisor in Fig.5.It can be viewed as the combination of countless deterministic supervisors.In particular, there are two choices at node {m0}and {m2}, namely, disablingt2ort3.In the case that we always disablet2at node {m0} and disablet3at node {m2}, we may extract a deterministic supervisor, as shown in Fig.6,from the non-deterministic supervisor.The supervisor in Fig.6 is indeed a maximally permissive liveness-enforcing deterministic supervisor tolerant to the SM-attackOin the case study.Note that a liveness-enforcing deterministic supervisor is also computed by the method in [19] for the case study,which is shown in Fig.7.We can see that the supervisor in Fig.7 is more restrictive than the one in Fig.6, i.e., it is not maximally permissive.For example, sequencet3t5is allowed to fire by the supervisor in Fig.6, while it is not allowed to fire by the supervisor in Fig.7.On the contrary, sequences that are allowed to fire by the supervisor in Fig.7 are all allowed to fire by the supervisor in Fig.6.

Fig.6.Maximally permissive liveness-enforcing deterministic supervisor tolerant to the SM-attack O in the case study.

Fig.7.Liveness-enforcing deterministic supervisor tolerant to the SMattack O in the case study computed by the method in [19].

We finally compare the computational complexity of the proposed method and the one in [19] in finding a solution to Problem 1.We observe that both methods start from constructing a maximally permissive liveness-enforcing deterministic supervisorGlunder no attack.This step determines the exponential complexity of both methods with respect to the size of the considered PN system since the RG has to be computed.We then focus on their remaining steps for comparison in what follows.Consider the proposed method.In the worst case, it updates once the set of control actions at every node ofGland handles every arc ofGlonce.Suppose thatGlcontainsanodes and arcs in total.Then, the complexity of the proposed method isO(a) in getting a solution.In other words, the proposed method is of polynomial complexity with respect to the net size ofGl.Consider the method in [19].It has to repeatedly compute a so-called basic supervisor, which is of exponential complexity with respect to the net size ofGl[19].Consequently, we may conclude that the proposed method has lower computational complexity than the method in [19] in synthesizing a supervisor.In particular, when a maximally permissive liveness-enforcing deterministic supervisorGlunder no attack is given, the complexity of getting a solution is reduced from the exponential one to the polynomial one by using the proposed method.We note that the only additional cost of using non-deterministic supervisors lies in choosing a control action randomly online.Fortunately, such computation is actually negligible.

VI.CONCLUSIONS AND FUTURE WORK

In this paper, we consider the use of non-deterministic control mechanisms to solve the liveness-enforcing problem in the presence of cyber-attacks.Specifically, for a bounded Petri net system vulnerable to a sensor-reading modification attack(SM-attack), an algorithm is proposed that synthesizes an SMattack-tolerant liveness-enforcing supervisor that is allowed to be non-deterministic.Compared with the method in [19] synthesizing a liveness-enforcing deterministic supervisor tolerant to an SM-attack, the proposed method is simpler in computational complexity.In our future work, we may consider the improvement of the proposed method so that the resulting supervisor is more permissive.Its extension to unbounded Petri nets [36]-[38] remains open.