1

Supervisory Control of Discrete-event Systems
under Attacks

arXiv:1701.00881v1 [] 4 Jan 2017

Masashi Wakaiki, Paulo Tabuada, and João P. Hespanha

Abstract
We consider a supervisory control problem for discrete-event systems, in which an attacker corrupts
the symbols that are observed by the supervisor. We show that existence of a supervisor enforcing a
specification language, in the presence of attacks, is completely characterized by controllability (in the
usual sense) and observability of the specification (in a new appropriately defined sense). The new
notion of observability takes into account the attacker’s ability to alter the symbols received by the
attacker. For attacks that correspond to arbitrary insertions/removals of symbols, the new notion of
observability can be tested by checking the usual notion of observability for a set of discrete-event
systems with appropriately redefined observation maps. Focusing on attacks that replace and/or remove
symbols from the output strings, we construct observers that are robust against attacks and lead to
an automaton representation of the supervisor. We also develop a test for observability under such
replacement-removal attacks by using the so-called product automata.

Index Terms
Discrete-event systems, supervisory control, security

M. Wakaiki is with the Department of Electrical and Electronic Engineering, Chiba University, Chiba, 263-8522, Japan (e-mail:
wakaiki@chiba-u.jp).
P. Tabuada is with the Department of Electrical Engineering, University of California, Los Angeles, CA 90095, USA (e-mail:
tabuada@ee.ucla.edu).
J. P. Hespanha is with the Center for Control, Dynamical-systems and Computation (CCDC), University of California, Santa
Barbara, CA 93106, USA (e-mail: hespanha@ece.ucsb.edu).

This material is based upon work supported by the NSF under Grant No. CNS-1329650. The first author acknowledges Murata
Overseas Scholarship Foundation and The Telecommunications Advancement Foundation for their support of this work. The
work of the second author was partially supported by the NSF award 1136174.

January 5, 2017

DRAFT

2

I. I NTRODUCTION
Recent developments in computer and network technology make cyber-physical systems prevalent in modern societies. The integration between cyber and physical components introduces
serious risks of cyber attacks to physical processes. For example, it has been recently reported
that attackers can adversarially control cars [1] and UAVs [2]. Moreover, the Moroochy water
breach in March 2000 [3] and the StuxNet virus attack in June 2010 [4] highlight potential threats
to infrastructure systems. An annual report [5] published in 2014 by the German government
stated that an attacker tampered with the controls of a blast furnace in a German steel factory.
We study supervisory control for Discrete-event systems (DESs) under adversarial attacks.
DESs are dynamic systems equipped with a discrete state space and an event-driven transition
structure. Such models are widely used to describe cyber-physical systems such as chemical
batch plants [6], power grids [7], and manufacturing systems [8]. The objective of this paper is
to answer the question: How do we control DESs if an attacker can manipulate the information
provided by sensing and communication devices? This question encourages system designers to
reconsider the supervisory control problem from the viewpoint of security.
Fig. 1 shows the closed-loop system we consider, in which an observation string generated by
the plant is substituted by a string corrupted by an adversarial attack. The attack changes the original string by inserting, removing, and replacing symbols, and is allowed to non-deterministically
change the same original string to distinct strings. Furthermore, since we cannot foretell what
an attacker will do as we design supervisors, we consider a set of possible attacks. The problem
we study is how to determine if there exists a supervisor that can enforce the specification
notwithstanding the attacks. Whenever such supervisor exists, we also study the problem of how
to construct it. This work is inspired by the research on state estimation under sensor attacks
for linear time-invariant systems developed in [9]–[11].

Plant
Enabled events
in the next step

Observation string
Attack

Supervisor

Corrupted string
(may be an empty string)

Fig. 1: Closed-loop system under attacks.

January 5, 2017

DRAFT

3

Related works: Supervisory control theory has developed frameworks to handle plant uncertainties and faults; see, e.g., [12]–[14] for robust control and [15]–[17] for fault tolerant
control. These studies can be used as countermeasures against attacks, but there are conceptual
differences between uncertainties/faults and attacks. In fact, uncertainties/faults do not coordinate
with harmful intent, whereas attackers can choose their action in order to achieve malicious
purposes. For example, the stealthy deception attacks in [18], [19] aim to inject false information
without being detected by the controller. Therefore we present a new framework for supervisory
control under adversarial attacks.
Several aspects of security have also been explored in the DES literature. One particular line
of research aims at studying the opacity of DESs, whose goal is to keep a system’s secret
behavior uncertain to outsiders; see, e.g., [20]–[23] and reference therein. Intrusion detection in
the DES framework has been investigated in [24]–[27]. These security methods guarantee the
confidentiality and integrity of DESs, but relatively little work has been done towards studying
supervisory control robustness against attacks.
An attacked plant can be modeled by a single DES with nondeterministic observations.
Supervisory control for such a DES has been studied in [28], [29]. The major difference from
the problem setting in these previous works is that in our work, the attacked output, i.e., the nondeterministic observation function, is uncertain. In other words, if GAi denotes the DES obtained
by modeling the plant under an attack Ai , then the problem we consider can be regarded as robust
supervision for an uncertain DES in a set of possible models {GA1 , . . . , GAn }, each representing
a potential type of attack.
Contributions and organization of this paper: In Section II, after defining attacks formally, we
introduce a new notion of observability under attacks, which is a natural extension of conventional
observability introduced in [30], [31]. We show that there exists a partial observation supervisor
that achieves a given language under attack if and only if the language is controllable in the
usual sense and observable according to the new notion of observability introduced in this
paper. Moreover, the desired supervisor is obtained explicitly. For attacks that correspond to
arbitrary insertions/removals of symbols, the new notion of observability can be reduced to the
conventional observability of a set of DESs with appropriately redefined observation maps, and
the number of elements in this DES set is the square of the number of possible attacks.
In Section III, we construct an automaton representation of the supervisor derived in Section II.
The results in this section are specific to attacks that replace and/or remove specific symbols from

January 5, 2017

DRAFT

4

the output string. First, we provide the mathematical formulation of replacement-removal attacks.
Then we construct an observer automaton that is resilient against such an attack, extending the
result in [30]. Finally, using the observer for each possible attack, we obtain an automaton
representation of the desired supervisor.
Section IV is devoted to developing a test for observability under attacks. Attacks are restricted
to the replacement and/or removal of symbols in this section as well. Constructing a product
automaton in [32], we show how to test observability under replacement-removal attacks in a
computationally efficient way. The computational complexity of this observability test is (Number
of possible attacks)2 × (Complexity of the conventional observability test without attacks), which
is the same as in the insertion-removal attack case of Section II.
Notation and definitions
The following notation and definitions are standard in the DES literature (see, e.g., [33], [34]).
For a finite set Σ of event labels, we denote by |Σ| the number of elements in Σ, and by
Σ∗ the set of all finite strings of elements of Σ, including the empty string . For a language
L ⊂ Σ∗ , the prefix closure of L is the language

L̄ := u ∈ Σ∗ : ∃v ∈ Σ∗ , uv ∈ L ,
where uv denotes the concatenation of two strings in Σ∗ , and L is said to be prefix closed if
L = L̄. We define the concatenation of languages L1 , L2 ⊂ Σ∗ by
L1 L2 := {w1 w2 ∈ Σ∗ : w1 ∈ L1 , w2 ∈ L2 }.
Let the set of events Σ be partitioned in two sets as Σ = Σc ∪ Σu with Σc ∩ Σu = ∅, where
Σc is called the set of controlled events and Σu the set of uncontrolled events. For a language
L defined on Σ, a prefix-closed set K ⊂ L is said to be controllable if KΣu ∩ L ⊂ K.
Consider an observation map P : Σ → (∆ ∪ {}) that maps a set of events Σ into a set
of observation symbols ∆ (augmented by the empty event ). This observation map P can be
extended to map strings of events in Σ∗ to strings of observation symbols in ∆∗ , using the rules
P () =  and
P (wσ) = P (w)P (σ),

∀w ∈ Σ∗ , σ ∈ Σ.

A prefix-closed language K ⊂ L is P -observable with respect to L if
ker P ⊂ actK⊂L

January 5, 2017

DRAFT

5

where ker P denotes the equivalence relation on Σ∗ defined by

ker P := (w, w0 ) ∈ Σ∗ × Σ∗ : P (w) = P (w0 ) ,
and actK⊂L is a binary relation on Σ∗ defined as follows: The pair (w, w0 ) ∈ actK⊂L if (and
only if) w, w0 ∈ K implies that there does not exist σ ∈ Σ such that neither
[wσ ∈ K, w0 σ ∈ L \ K] nor [wσ ∈ L \ K, w0 σ ∈ K].
We will omit the underling language L when it is clear from the context.
Consider an automaton G = (X, Σ, ξ, x0 ), where X is the set of states, Σ is the nonempty
event set, ξ : X × Σ → X is the transition mapping (a partial function), and x0 ∈ X is the
initial state. We write ξ(x, σ)! to mean that ξ(x, σ) is defined. The transition function ξ can be
extended to a function X × Σ∗ → X according to the following rule:
•
•

For all x ∈ X, ξ(x, ) := x
For all x ∈ X, w ∈ Σ∗ , and σ ∈ Σ,


ξ(ξ(q, w), σ)
ξ(x, wσ) :=

undefined

if ξ(q, w)! and ξ(ξ(q, w), σ)!
otherwise.

The language generated by G is given by
L(G) := {w ∈ Σ∗ : f (x0 , w)!}.
II. S UPERVISED D ISCRETE - EVENT S YSTEMS UNDER ATTACKS
In Section II A, we first introduce attacks on observation symbols and a new notion of
observability under attacks. In Section II B, we present the main result of this section, which
shows that there exists a supervisor achieving a given language in the presence of attacks if and
only if the language is controllable in the usual sense and observable under attacks. Next, in
Section II C, we focus our attention on attacks that insert and remove symbols, and show that the
new notion of observability under such attacks can be reduced to the conventional observability
notion of a set of DESs.
A. Observability under attacks
By an attack, we mean the substitution of an observation string w ∈ ∆∗ generated by the plant
by a corrupted string y ∈ ∆∗ that is exposed to the supervisor (see Fig. 1). The corrupted string

January 5, 2017

DRAFT

6

y may differ from the original string w by the insertion, removal, or replacement of symbols.
The simplest form of attack could be modeled by a function y = A(w) that maps ∆∗ to ∆∗ .
However, we are interested in more general forms of attacks where the attacker is allowed to
non-deterministically map the same original string w ∈ ∆∗ to distinct strings y ∈ ∆∗ , in order to
make the task of the supervisor more difficult. We thus model attacks by a set-valued function
∗

A : ∆∗ → 2∆ that maps each original string w ∈ ∆∗ to the set A(w) ⊂ ∆∗ of all possible
corrupted strings y. Note that the supervisor receives one of the strings in the set A(w), not
∗

A(w) itself. The attack map Aid : ∆∗ → 2∆ that assigns to each string w ∈ ∆∗ the set {w}
containing only the original string w can be viewed as the absence of an attack.
When we design supervisors, attack maps may be uncertain due to lack of knowledge of
which sensors are attacked. In this paper, we therefore consider a set of possible attacks A =
{A1 , . . . , An }, and we are interested in the following scenario: We know the attack set A in
advance, and that only one attack in the set A is conducted. In other words, the attacker is not
allowed to switch between the attacks in the set A. However, when we construct a supervisor,
we do not know which attack actually occurs, and hence the aim is to design a robust supervisor
with respect to all attacks in A.
Example 1: Consider the language L(G) generated by the automaton G shown in Fig. 2a.
We investigate the observability under attacks of the specification language K generated by the
automaton GK in Fig. 2b. The difference between G and GK is an event c from x1 to x3 .
The purpose of supervisory control here would be to avoid this “shortcut”. We consider the
observation map P defined by
P (σ) =



σ

if σ ∈ ∆ := {a, b, d}




otherwise,

and three attacks A1 , A2 , A3 defined by A1 (σ) = ∆ for all σ ∈ ∆,
A2 (a) = {a, b},

A2 (b) = {b},

A2 (d) = {a, d}

A3 (a) = {a},

A3 (b) = {b},

A3 (d) = {}.

The attack A1 replaces each output symbol arbitrarily, so the supervisor knows from the output
only whether an observable event occurs. The attack A2 can replace the symbol a by b and the
symbol d by a, respectively, whereas the attack A3 always erases the symbol d. The goal is then
to design a supervisor that enforces the specification GK , without knowing which of the three
attacks is taking place. We shall return to this example later in the paper.

January 5, 2017


DRAFT

7

x0

a
c

d

c

x3

r0

x1

b

r1

d

x2

(a) System automaton G.

a

b

r3

c

r2

(b) Specification automaton GK .

Fig. 2: Automata in Example 1.

∗

For simplicity of notation, we denote by AP : Σ∗ → 2∆ the attacked observation map
obtained from the composition AP := A ◦ P . We introduce a new notion of observability under
a set of attacks, which can be seen as a direct extension of the conventional observability notion
introduced in [30], [31].
Definition 2 (Observability under attacks): Given an attack set A, we say that a prefix-closed
language K ⊂ L is P -observable under the attack set A if
RA,A0 ⊂ actK⊂L ,

∀A, A0 ∈ A,

(1)

where the relation RA,A0 contains all pairs of strings that may result in attacked observation
maps AP and A0 P with a common string of output symbols, i.e.,

RA,A0 := (w, w0 ) ∈ Σ∗ × Σ∗ : AP (w) ∩ A0 P (w0 ) 6= ∅ .

(2)

In view of the definition (2), the P -observability condition (1) can be restated as requiring that,
for every w, w0 ∈ K,
∃A, A0 ∈ A s.t. AP (w) ∩ A0 P (w0 ) 6= ∅
⇒ @σ ∈ Σ s.t. [wσ ∈ K, w0 σ ∈ L \ K] or [wσ ∈ L \ K, w0 σ ∈ K],

(3)

or equivalently, for every w, w0 ∈ K,
∃A, A0 s.t. AP (w) ∩ A0 P (w0 ) 6= ∅
⇒ ∀σ ∈ Σ, wσ ∈
/ L or w0 σ ∈
/ L or [wσ, w0 σ ∈ K] or [wσ, w0 σ ∈ L \ K].

(4)

In words, observability means that we cannot find two attacks A, A0 ∈ A that would result in
the same observation for two strings w, w0 ∈ K such that (w, w0 ) 6∈ actK⊂L , i.e., two strings

January 5, 2017

DRAFT

8

w, w0 ∈ K such that one will transition to an element of K and the other to an element outside
K, by the concatenation of the same symbol σ ∈ Σ.
First we obtain a condition equivalent to observability under attacks for controllable languages.
In the non-attacked case, this condition is used as the definition of conventional observability in
the book [34, Sec. 3.7].
Proposition 3: Suppose that the prefix-closed language K ⊂ L is controllable. Then K is P observable under the set of attacks A if and only if for every w, w0 ∈ K, σ ∈ Σc , and A, A0 ∈ A,
the following statement holds:
[AP (w) ∩ A0 P (w0 ) 6= ∅, wσ ∈ K, w0 σ ∈ L] ⇒ w0 σ ∈ K.

(5)

Proof: We use the necessary and sufficient condition (3) for the specification language K to
be observable under attacks.
(⇒) Suppose that K is P -observable under A, and suppose that w, w0 ∈ K, σ ∈ Σc , and
A, A0 ∈ A satisfy
AP (w) ∩ A0 P (w0 ) 6= ∅,

wσ ∈ K,

w0 σ ∈ L.

Then (3) directly leads to w0 σ ∈ K.
(⇐) Suppose that (5) holds for all w, w0 ∈ K, σ ∈ Σc , and A, A0 ∈ A. From (3), it is enough
to show that if w, w0 ∈ K satisfy AP (w) ∩ A0 P (w0 ) 6= ∅ for some A, A0 ∈ A, then there does
not exist σ ∈ Σ such that
[wσ ∈ K, w0 σ ∈ L \ K] or [wσ ∈ L \ K, w0 σ ∈ K].
Since K is controllable, if σ ∈ Σu and wσ, w0 σ ∈ L, then wσ, w0 σ ∈ K from (5). Moreover,
for all σ ∈ Σc , if wσ ∈ K and w0 σ ∈ L, then w0 σ ∈ K. Exchanging w and w0 , we also have if
w0 σ ∈ K and wσ ∈ L, then wσ ∈ K. This completes the proof.



Example 1 (cont.): Consider the language L(G), the specification language K = L(GK ), and
the attack sets A1 , A2 , A3 in Example 1. Let the controllable event set be Σc = {a, c}, and the
uncontrollable event be Σu = {b, d}. It is straightforward to show that K is controllable, and we
can use Proposition 3 to verify that K is observable under the attack set A = {A1 }. Additionally,
K is observable under the attack sets A = {A2 } and A = {A3 }, but is not observable under
A = {A2 , A3 }. In fact, if we define w := abcda and w0 := wb, then
A2 P (w) = {abaa, abab, abda, abdb, bbaa, bbab, bbda, bbdb}
A3 P (w0 ) = {abab},

January 5, 2017

DRAFT

9

and hence A2 P (w) ∩ A3 P (w0 ) 6= ∅, but c ∈ Σc satisfies wc ∈ L \ K and w0 c ∈ K. Thus K
is robust with respect to symbol replacements but vulnerable to a combination of replacements


and removals.
B. Existence of supervisors

Our objective in this subsection is to provide a necessary and sufficient condition for the existence of a supervisor that achieves a specification language in the presence of output corruption.
To this end, we first introduce supervisors for an attack set and define controlled languages under
attacks.
A P -supervisor for a language L ⊂ Σ∗ and an attack set A is a function f :

S

A∈A

AP (L) →

2Σ , where AP (L) is the set of all possible output strings under the attack A, that is,

AP (L) := y ∈ ∆∗ : ∃w ∈ L s.t. y ∈ AP (w) .
We will say that a supervisor f is valid if f (w) ⊃ Σu for all w ∈

S

A∈A

AP (L).

Given a P -supervisor f for a language L and an attack set A, the maximal language Lmax
f,A
controlled by f under the attack A ∈ A is defined inductively by  ∈ Lmax
f,A and
wσ ∈ Lmax
f,A

⇔

w ∈ Lmax
f,A ,

wσ ∈ L,

∃y ∈ AP (w) s.t. σ ∈ f (y),

max
whereas the minimal language Lmin
f,A (⊂ Lf,A ) controlled by f under the attack A ∈ A is defined

inductively by  ∈ Lmin
f,A and
wσ ∈ Lmin
f,A

⇔

w ∈ Lmin
f,A ,

wσ ∈ L,

∀y ∈ AP (w), σ ∈ f (y).

max
In general, Lmin
f,A ⊂ Lf,A , but in the absence of an attack, i.e., A = Aid , both languages coincide.
min
By construction, Lmax
f,A and Lf,A are prefix closed.

By definition, Lmax
f,A is the largest language that the attack A could enforce by exposing to the
supervisor f an appropriate corrupted output string in AP (w). On the other hand, Lmin
f,A is the
smallest language that the attack A could enforce. In other words, A could not reject any string
in this set by the choice of corrupted output strings in AP (w).
The following result provides a necessary and sufficient condition on a language K ⊂ L for
the existence of a P -supervisor f for an attack set A whose minimal and maximal controlled
max
languages Lmin
f,A , Lf,A are both equal to K.

Theorem 4: For every nonempty prefix-closed set K ⊂ L and every attack set A:

January 5, 2017

DRAFT

10

max
1) There exists a valid P -supervisor f for A such that Lmin
f,A = Lf,A = K for all A ∈ A if

and only if K is controllable and P -observable under A;
2) If K is controllable and P -observable under A, then the following map f :

S

A∈A

AP (L) →

max
2Σ defines a valid P -supervisor for which Lmin
f,A = Lf,A = K for all A ∈ A:

[

f (y) := Σu ∪ σ ∈ Σc : ∃w ∈ K, A ∈ A s.t. [y ∈ AP (w), wσ ∈ K] , ∀y ∈
AP (L).
A∈A

(6)
When the set of attacks A contains only Aid , Theorem 4 specializes to the case without attacks.
Remark 5: As the proof below shows, in order to obtain controllability in item 1), it is enough
min
that Lmax
f,A = K or Lf,A = K for some A ∈ A.



Proof of Theorem 4: We first prove that Lmax
f,A = K for some A ∈ A implies the controllability
of K. Pick some word w̄ ∈ KΣu ∩ L. Such a word must be of the form w̄ = wσ ∈ L such
that w ∈ K and σ ∈ Σu . The supervisor f is defined for all the strings y that are produced
by an attacker. Therefore, if w ∈ K ⊂ L, then f (y) is defined for every y ∈ AP (w). Since f
is a valid supervisor, any uncontrollable event belongs to f (y), in particular, σ ∈ f (y). Since
max
max
w ∈ K = Lmax
f,A , it now follows by the definition of Lf,A that wσ ∈ Lf,A = K, which shows
max
that KΣu ∩ L ⊂ K, and therefore K is controllable. From Lmin
f,A = K instead of Lf,A = K,

controllability can be obtained in the same way.
Next we prove that K is P -observable under an attack set A by using the fact that K =
max
Lmin
f,A = Lf,A for all A ∈ A. To do so, we employ the statement (4), which is equivalent to

observability under attacks. Pick a pair of words w, w0 ∈ K such that
∃A, A0 s.t. AP (w) ∩ A0 P (w0 ) 6= ∅,
and an arbitrary symbol σ ∈ Σ such that wσ, w0 σ ∈ L. If such a symbol σ does not exist, then
all σ satisfy wσ 6∈ L or w0 σ 6∈ L, and we immediately conclude that K is observable under A
min
from (4). If such σ exists and wσ ∈ K = Lmin
f,A , then by the definition of Lf,A , we must have

w ∈ Lmin
f,A = K,

wσ ∈ L,

∀y ∈ AP (w), σ ∈ f (y).

Since AP (w) ∩ A0 P (w0 ) 6= ∅, we must then have
0
0
0
w0 ∈ Lmax
f,A0 = K, w σ ∈ L, ∃y ∈ A P (w ) s.t. σ ∈ f (y).

January 5, 2017

DRAFT

11

Consequently, w0 σ ∈ Lmax
/ K = Lmax
f,A and we
f,A0 = K. Alternatively, if wσ ∈ L \ K, then wσ ∈
must have
w ∈ Lmax
/ f (y).
f,A = K, wσ ∈ L, ∀y ∈ AP (w), σ ∈
Since AP (w) ∩ A0 P (w0 ) 6= ∅, we must then have
0
0
0
w0 ∈ Lmin
/ f (y),
f,A0 = K, w σ ∈ L, ∃y ∈ A P (w ) s.t. σ ∈

and hence w0 σ ∈
/ Lmin
f,A0 = K. This shows that (4) holds, and therefore K is P -observable under
A.
To prove the existence of the supervisor in item 1 (and also the statement in item 2), pick
the supervisor f according to (6). We prove by induction on the word length that the supervisor
min
f so defined satisfies K = Lmax
f,A = Lf,A for all A ∈ A. The basis of induction is the empty
min
string  that belongs to Lmax
f,A and Lf,A because of the definition of these sets and belongs to K

because this set is prefix-closed.
min
Suppose now that K, Lmax
f,A , and Lf,A have exactly the same words of length n ≥ 0, and pick
0
a word w0 σ ∈ Lmax
f,A of length n + 1 with σ 6= . We show that w σ ∈ K as follows. Since
0
w0 ∈ Lmax
f,A has length n, we know by the induction hypothesis that w ∈ K. On the other hand,

since w0 σ ∈ Lmax
f,A , we must have
w0 ∈ Lmax
f,A ,

w0 σ ∈ L,

∃y ∈ AP (w0 ) s.t. σ ∈ f (y).

If σ ∈ Σu , then we see from controllability that w0 σ ∈ K. Let us next consider the case σ ∈ Σc .
By the definition (6) of f , σ ∈ f (y) must mean that
∃w ∈ K, Ā ∈ A

s.t.

[y ∈ ĀP (w), wσ ∈ K].

(7)

We therefore have
w, w0 ∈ K, AP (w0 ) ∩ ĀP (w) 6= ∅, wσ ∈ K, w0 σ ∈ L.
Since K is controllable and observable under A, Proposition 3 shows that w0 σ ∈ K. This shows
min
max
that any word of length n + 1 in Lmax
f,A also belongs to K. Since Lf,A ⊂ Lf,A , it follows that

any word of length n + 1 in Lmin
f,A also belongs to K.
Conversely, for a word w0 σ ∈ K ⊂ L of length n + 1 with σ 6= , we prove w0 σ ∈ Lmin
f,A
as follows. Since K is prefix closed, we have w0 ∈ K. The induction hypothesis shows that
0
min
w0 ∈ Lmin
f,A . To obtain w σ ∈ Lf,A , we need to show that

w0 ∈ Lmin
f,A ,

January 5, 2017

w0 σ ∈ L,

∀y ∈ AP (w0 ), σ ∈ f (y).

DRAFT

12

The first statement is a consequence of the induction hypothesis (as discussed above). The second
statement is a consequence of the fact that w0 σ ∈ K ⊂ L. As regards the third statement, if
σ ∈ Σu , then σ ∈ f (y) for all y ∈ AP (w0 ) by definition. It is therefore enough to show that
σ ∈ Σc leads to σ ∈ f (y), that is, the statement (7), for every y ∈ AP (w0 ). We obtain (7) for
the particular case Ā = A, w = w0 ∈ K. Thus any word of length n + 1 in K also belongs to
max
min
Lmin
f,A and hence also to Lf,A ⊃ Lf,A , which completes the induction step.



C. Observability under insertion-removal attacks
In this subsection, we consider attacks that insert and remove certain symbols from output
strings, and reduce observability under such attacks to the conventional observability in the
non-attacked case.
Given a set of symbols α ⊂ ∆ in the observation alphabet, we define the insertion-removal
∗

attack Aα : ∆∗ → 2∆ that maps each string u ∈ ∆∗ to the set of all strings v ∈ ∆∗ that can be
obtained from u by an arbitrary number of insertions or removals of symbols in α. We say that
Aα corresponds to an attack on the output symbols in α. In this context, it is convenient to also
define the corresponding α-removal observation map R¬α : ∆ → (∆ ∪ {}) by


 t ∈ α
R¬α (t) =

t t 6∈ α.

(8)

The α-removal observation map can be extended to strings of events in the same way as the
observation map P . This α-removal observation map allows us to define the attack Aα : ∆∗ →
∗

2∆ on the output symbol in α as follows:

Aα (u) = v ∈ ∆∗ : R¬α (u) = R¬α (v) .

(9)

Example 6: Let α = {t1 } ⊂ {t1 , t2 }. Then R¬α (t1 t2 ) = t2 , and

∗
Aα (t1 t2 ) = {tn1 t2 tm
1 : n, m ≥ 0} = v ∈ ∆ : R¬α (t1 t2 ) = R¬α (v) .



The next result shows that the observability in Definition 2 under insertion-removal attacks
is equivalent to the usual observability (without attacks) for an appropriate set of output maps.
Note that the composition R¬α ◦ P : ∆ → (∆ ∪ {}) can be regarded as an observation map (in
the usual sense, i.e., without attacks).

January 5, 2017

DRAFT

13

Theorem 7: For every nonempty prefix-closed language K ⊂ L and insertion-removal attack
set A = {Aα1 , Aα2 , . . . , AαM } consisting of M ≥ 1 observation attacks, K is P -observable
under the set of attacks A if and only if K is (R¬α ◦ P )-observable for every set α := αi ∪ αj ,
∀i, j ∈ {1, 2, . . . , M }.
Theorem 7 implies that one can use the standard test for DES observability (without attacks)
in [32] to determine observability under insertion-removal attacks (Definition 2).
Remark 8 (Computational complexity of observability test for insertion-removal attacks):
Consider a language L = L(G) generated by a finite automaton G = (X, Σ, ξ, x0 ) and a
specification language K = L(GK ) ⊂ L generated by a finite automaton GK = (R, Σ, η, r0 ).
According to Thereom 7, in order to test observability under an insertion-removal attack set A,
it is enough to construct |A|2 test automatons, each of which verifies the usual observability.
Since the computational complexity of verifying the usual observability with the test automaton
is O(|X| · |R|2 · |Σc |) (see, e.g., [34, Sec. 3.7]), the total complexity for this observability test
under attacks is O(|X| · |R|2 · |Σc | · |A|2 ).



The following result is the key step in proving Theorem 7.
Lemma 9: Given any two sets α1 , α2 ⊂ ∆ and α := α1 ∪ α2 , we have that
(v, v 0 ) ∈ ker R¬α

⇒

Aα1 (v) ∩ Aα2 (v 0 ) 6= ∅,

(10)

where ker R¬α is defined by

ker R¬α := (v, v 0 ) ∈ ∆∗ × ∆∗ : R¬α (v) = R¬α (v 0 ) .

(11)

Proof: To prove this result, we must show that given two strings v, v 0 ∈ ∆∗ such that
R¬α (v) = R¬α (v 0 ), there exists a third string y ∈ ∆∗ that belongs both to Aα1 (v) and Aα2 (v 0 ).
In view of (9), this means that y ∈ ∆∗ must satisfy
R¬α1 (v) = R¬α1 (y),

R¬α2 (v 0 ) = R¬α2 (y).

(12)

The desired string y can be constructed through the following steps:
1) Start with the string y1 := R¬α1 (v), which is obtained by removing from v all symbols in
α1 . Since α := α1 ∪ α2 , we have R¬α = R¬α2 ◦ R¬α1 . Hence
R¬α2 (y1 ) = R¬α2 (R¬α1 (v)) = R¬α (v) = R¬α (v 0 ),
and the strings y1 and v 0 still only differ by symbols in α1 and α2 .

January 5, 2017

DRAFT

14

2) Construct y2 by adding to y1 suitable symbols in α1 so that R¬α2 (y2 ) = R¬α2 (v 0 ). This is
possible because y1 and v 0 only differ by symbols in α1 and α2 and y1 has no symbols in α1
by definition. To get R¬α2 (y2 ) = R¬α2 (v 0 ), we do not care about the symbols in α2 , so we just
have to insert into y1 the symbols in α1 that appear in v 0 (at the appropriate locations).
3) By construction,
R¬α1 (y2 ) = y1 = R¬α1 (v),
and hence the original v and y2 only differ by symbols in α1 . Moreover, R¬α2 (y2 ) = R¬α2 (v 0 ),
that is, v 0 and y2 only differ by symbols in α2 . We therefore conclude that y := y2 satisfies (12)
and hence belongs to both Aα1 (v) and Aα2 (v 0 ).



Proof of Theorem 7: By definition, K is P -observable under the set of attacks A if and only
if
RAαi ,Aαj ⊂ actK⊂L ,

∀i, j ∈ {1, 2, . . . , M }.

Also, by definition, K is (R¬α ◦ P )-observable for the set α := αi ∪ αj if and only if
ker(R¬α ◦ P ) ⊂ actK⊂L .
To prove the result, it therefore suffices to show that, for all i, j ∈ {1, 2, . . . , M }, we have that
RAαi ,Aαj = ker(R¬α ◦ P ),

α := αi ∪ αj .

To show that this equality holds, first pick a pair (w, w0 ) ∈ RAαi ,Aαj , which means by the
definition (2) of RAαi ,Aαj that there exists a string y ∈ ∆∗ that belongs both to Aαi P (w) and
Aαj P (w0 ), and therefore
y ∈ Aαi P (w)


R¬αi P (w) = R¬αi (y)

⇔ R¬αj P (w0 ) = R¬αj (y)

⇔

y ∈ Aαj P (w0 )

Since α := αi ∪ αj , we have that R¬α = R¬αj ◦ R¬αi = R¬αi ◦ R¬αj , and consequently



R¬α P (w) = R¬αj R¬αi P (w) = R¬αj R¬αi (y)



= R¬αi R¬αj (y) = R¬αi R¬αj P (w0 ) = R¬α P (w0 ) .
Hence (w, w0 ) ∈ ker(R¬α ◦ P ). We have thus shown that RAαi ,Aαj ⊂ ker(R¬α ◦ P ).

January 5, 2017

DRAFT

15

To prove the reverse inclusion, pick a pair (w, w0 ) ∈ ker(R¬α ◦ P ), which means that



R¬α P (w) = R¬α P (w0 ) , and therefore P (w), P (w0 ) ∈ ker R¬α by the definition (11)
of ker R¬α . In conjunction with Lemma 9, this leads to


Aαi P (w) ∩ Aαj P (w0 ) 6= ∅.
Therefore we have (w, w0 ) ∈ RAαi ,Aαj . This shows that ker(R¬α ◦ P ) ⊂ RAαi ,Aαj , which


concludes the proof.
III. R EALIZATION OF S UPERVISORS UNDER ATTACKS

The objective of this section is to describe the supervisor f in (6) through an automaton for
replacement-removal attacks, which will be introduced in Section III A and are a special class of
the attacks considered in Section II. In Section III B, we provide a construction for an automaton
that describes a supervisor for replacement-removal attacks and then formally prove in Section
III C that the proposed automaton represents the supervisor f in (6).
A. Replacement-removal attack
The results in this section are specific to attacks that consist of replacement and/or removal of
specific symbols from the output strings. For a given replacement-removal map φ : ∆ → 2∆∪{}
that maps each output symbol to a (possibly empty) set of symbols, the corresponding attack
∗

map A : ∆∗ → 2∆ is defined by A() = {} and

A(yt) := wy wt : wy ∈ A(y), wt ∈ φ(t)

(13)

for all y ∈ ∆∗ and t ∈ ∆. Sets of attacks of this form are called replacement-removal attack
sets. Recalling that AP := A ◦ P , we conclude from (13) that
AP (sσ) = AP (s)AP (σ),

∀s ∈ Σ∗ , σ ∈ Σ.

(14)

In what follows, it will be convenient to define the inverse map AP −1 by

AP −1 (y) := w ∈ Σ∗ : y ∈ AP (w) ,
∀y ∈ ∆∗ ,
and extend it to languages L∆ ⊂ ∆∗ :

AP −1 (L∆ ) := w ∈ Σ∗ : ∃y ∈ L∆ s.t. y ∈ AP (w) .
The following lemma provides basic properties of AP and AP −1 for a replacement-removal
attack A:

January 5, 2017

DRAFT

16

Lemma 10: Consider a replacement-removal attack A.
1) For all w, s ∈ Σ∗ , we have
AP (ws) = AP (w)AP (s).

(15)

2) Let y1 , . . . , ym ∈ ∆ and w1 , . . . , wn ∈ Σ. If y1 · · · ym ∈ AP (w1 · · · wn ), then there exist
i1 , . . . , im such that 1 ≤ i1 < i2 < · · · < im ≤ n and
 ∈ AP (w1 · · · wi1 −1 ),
 ∈ AP (wi1 +1 · · · wi2 −1 ),

y1 ∈ AP (wi1 )
y2 ∈ AP (wi2 )

..
.
 ∈ AP (wim +1 · · · wn ),
where, for example, if i2 − i1 = 1, then the condition  ∈ AP (wi1 · · · wi2 −1 ) is omitted.
3) For all y, v ∈ ∆∗ , we have
AP −1 (yv) = AP −1 (y)AP −1 (v).

(16)

Proof: 1) If s = , then (15) holds for all w ∈ Σ∗ because AP () = {}. For s = s1 · · · sk
with si ∈ Σ, we obtain (15), by using (14) iteratively. Thus we have (15) holds for all w, s ∈ Σ∗ .
2) We prove the item 2 by induction on the word length of y1 · · · ym . In the case m = 1,
suppose that
y1 ∈ AP (w1 · · · wn ) = AP (w1 ) · · · AP (wn ).
If y1 6∈ AP (wi ) for every i = 1, . . . , n, then y1 6∈ AP (w1 · · · wn ). Hence y1 ∈ AP (wi ) for at
least one i. Let y1 ∈ AP (wi ) hold for i = j1 , . . . , jk . It follows that there exists l ∈ {j1 , . . . , jk }
such that
 ∈ AP (w1 · · · wl−1 ), y1 ∈ AP (wl ),  ∈ AP (wl+1 · · · wn ).
The desired i1 is such an index l.
Suppose now that the item 2 holds with y1 · · · yk of length k ≥ 1 and that
y1 · · · yk yk+1 ∈ AP (w1 · · · wn ) = AP (w1 ) · · · AP (wn ).
Similarly to the case m = 1, we see that there exists ik+1 such that
y1 · · · yk ∈ AP (w1 · · · wik+1 −1 ),

January 5, 2017

yk+1 ∈ AP (wik+1 ),

 ∈ AP (wik+1 +1 · · · wn ).

DRAFT

17

Applying the induction hypothesis to y1 · · · yk ∈ AP (w1 · · · wik+1 −1 ), we have the desired
conclusion with y1 · · · yk+1 of length k + 1.
3) If (16) holds for all y ∈ ∆∗ and v ∈ ∆ ∪ {}, then an iterative calculation shows that (16)
holds for all y ∈ ∆∗ and all v ∈ ∆∗ . Hence it is enough to prove that (16) holds for all y ∈ ∆∗
and t ∈ ∆ ∪ {}.
Suppose that w ∈ AP −1 (y)AP −1 (t) for y ∈ ∆∗ and t ∈ ∆ ∪ {}. Then
∃w1 ∈ AP −1 (y), w2 ∈ AP −1 (t) s.t. w = w1 w2 .
Since y ∈ AP (w1 ) and t ∈ AP (w2 ), it follows that
yt ∈ AP (w1 )AP (w2 ) = AP (w),
which implies w ∈ AP −1 (yt). We therefore have AP −1 (y)AP −1 (t) ⊂ AP −1 (yt).
Next we prove the converse inclusion. If t = , then we have from AP () = {} that
AP −1 (y)AP −1 (t) ⊃ AP −1 (yt).
Let us next consider the case t 6= . Suppose that w ∈ AP −1 (yt) for y ∈ ∆∗ and t ∈ ∆. Since
yt ∈ AP (w) and yt 6= , it follows that w 6= . Let w = w1 · · · wn with wi ∈ Σ. From the item
2, there exists i ∈ {1, . . . , n} such that y ∈ AP (w1 · · · wi ) and t ∈ AP (wi+1 · · · wn ). Hence if
we define w1 := w1 · · · wi and w2 := wi+1 · · · wn , then
w = w1 w2 , w1 ∈ AP −1 (y), w2 ∈ AP −1 (t).
Hence w ∈ AP −1 (y)AP −1 (t). Thus AP −1 (y)AP −1 (t) ⊃ AP −1 (yt), which completes the proof.

B. Supervisors described by observers
Inspired by the non-attacked results in [30], we first construct an observer that is resilient
against replacement-removal attacks, which plays an important role in the representation of the
supervisor f in (6).
Consider a specification automaton GK = (R, Σ, η, r0 ) with a set ∆ of output symbols and
an output map P : Σ → (∆ ∪ {}). We define the unobservable reach URA (r) of each state
r ∈ R under a replacement and removal attack A ∈ A by

URA (r) := z ∈ R : ∃u ∈ AP −1 () s.t. z = η(r, u) ,

January 5, 2017

DRAFT

18

Observer
fobs,A (x0,obs,A , t)
x0,obs,A

t2

u 2 AP

1

u 2 AP

(✏) e 2 AP

x0

1

1

(✏)

(t) \ ⌃

f (xe , e)

xe

Unobservable reach

Fig. 3: Observer ObsA (GK ) for an attack A.

which can be extended to a set of states B ⊂ R by
[
URA (B) :=
URA (r).
r∈B

To estimate the current state r of the specification automaton GK in the presence of a
replacement-removal attack A ∈ A, the observer ObsA (GK ) = (Robs,A , ∆, ηobs,A , r0,obs,A ) is
constructed in the following iterative procedure:
1) Define r0,obs,A := URA (r0 ) ⊂ R and set Robs,A = {r0,obs,A }.
2) For each set of states B ∈ Robs,A and t ∈ ∆, if η(re , e) is defined for some re ∈ B and
e ∈ AP −1 (t) ∩ Σ, then define
ηobs,A (B, t) := URA {r ∈ R : ∃re ∈ B, e ∈ AP (t)−1 ∩ Σ s.t. r = η(re , e)}



(17)

and add this set to Robs,A ; otherwise ηobs,A (B, t) is not defined.
3) Go back to step 2) until no more sets can be added to Robs,A .
Fig. 3 illustrates the observer ObsA (GK ).
Example 1 (cont.): Consider the specification language K = L(GK ) and the attack A1 as in
Example 1. Fig. 4 shows the observers obtained through the procedure described above for the
attacks Aid (absence of attack) and A1 . The structure of the observer ObsA1 (GK ) is similar to
that of ObsAid (GK ), but ObsA1 (GK ) transitions by using only the length of the observed strings,
which guarantees the robustness of K against replacement attacks.



The next result provides the realization of the P -supervisor f in (6) for the language L and
the specification K. This realization is base on a specification automaton GK := (R, Σ, η, r0 )
with L(GK ) = K and a family of observer automata ObsA (GK ) designed using the procedure
S
outlined above. Without loss of generality, we can restrict the domain of f to A∈A AP (K).
January 5, 2017

DRAFT

19

{r0 }

a

d

{r1 }

{r0 }

b

a, b, d

a, b, d

{r2 , r3 }

{r1 }

a, b, d

{r2 , r3 }

(a) Observer ObsAid (GK ) for the attack Aid (non-

(b) Observer ObsA1 (GK ) for the attack A1 .

attacked case).

Fig. 4: Observers in Example 1.

Theorem 11: Consider a nonempty prefix-closed set K ⊂ L and a replacement-removal attack
set A. Build a specification automaton GK := (R, Σ, η, r0 ) with L(GK ) = K and an observer
S
ObsA (GK ) := (Robs,A , ∆, ηobs,A , r0,obs,A ) for every A ∈ A. Define functions Ψ : A∈A Robs,A →
S
2Σ and ΦA : A∈A AP (K) → 2Σ by

Ψ(robs,A ) := Σu ∪ σ ∈ Σc : ∃r ∈ robs,A s.t. η(r, σ)!



Ψ ηobs,A (r0,obs,A , y) y ∈ AP (K)
ΦA (y) :=

Σu
y 6∈ AP (K).
Then the supervisor f in (6) can be obtained using
[
[
f (y) =
ΦA (y)
∀y ∈
AP (K).
A∈A

(18)
(19)

(20)

A∈A

We can precompute the function Ψ(robs,A ) for each observer state robs,A and then can obtain
the desired control action by looking at the current state robs,A and the corresponding event set
Ψ(robs,A ) for all observers ObsA (GK ) (A ∈ A).
Remark 12: The branch ΦA (y) = Σu for y 6∈ AP (K) in (19) implies that once an attack A
and a corrupted output string y satisfy y 6∈ AP (K), the corresponding observer ObsA (GK ) is not
under operation because the actual attack must be different from the attack A that the observer
assumes. Analogous to the case for linear time-invariant systems in [9]–[11], once y ∈
/ AP (K)
is detected, the supervisor can exclude that attack from further consideration and stop updating
the corresponding observer.

January 5, 2017



DRAFT

20

C. Proof of Theorem 11
The following lemma shows that the state of ObsA (GK ) is the set containing all the the states
of GK that could be reached from the initial state under the attack A.
Lemma 13: Consider a replacement-removal attack A. For all y ∈ L(ObsA (GK )), we have
r ∈ ηobs,A (r0,obs,A , y)

⇔

∃w ∈ AP −1 (y) s.t. r = η(r0 , w).

(21)

Moreover, L(ObsA (GK )) = AP (L(GK )).
The proof of Lemma 13 relies on a key technical result that provides a more direct representation
of ηobs,A in (17) without unobservable reaches URA .
Lemma 14: Consider a replacement-removal attack A. Let B ∈ Robs,A and t ∈ ∆. If η(re , e)
is defined for some re ∈ B and e ∈ AP −1 (t), then we define

η̄obs,A (B, t) := r ∈ R : ∃re ∈ B, e ∈ AP −1 (t) s.t. r = η(re , e) .
Then
ηobs,A (B, t)!

⇔

η̄obs,A (B, t)!

(22)

and
ηobs,A (B, t) = η̄obs,A (B, t).

(23)

Proof: First we prove (22). To prove this, it suffices to show that for all B ∈ Robs,A and
t ∈ ∆,
η(re , e)! for some re ∈ B and e ∈ AP −1 (t) ∩ Σ
⇔

η(re , e)! for some re ∈ B and e ∈ AP −1 (t)

(24)

By construction, (⇒) holds. We prove (⇐) as follows. Assume that there exist r̄e ∈ B and
ē ∈ AP −1 (t) such that η(r̄e , ē) is defined. Since t ∈ AP (ē), Lemma 10 shows that there exist
e1 ∈ Σ∗ , e2 ∈ Σ, and e3 ∈ Σ∗ such that
ē = e1 e2 e3 ,  ∈ AP (e1 ), t ∈ AP (e2 ),  ∈ AP (e3 ).

(25)

Since η(r̄e , ē)!, we also obtain η(η(r̄e , e1 ), e2 )!. Therefore if we prove that
r̄e ∈ B,

 ∈ AP (e1 )

⇒

η(r̄e , e1 ) ∈ B,

(26)

then (⇐) of (24) holds with re = η(r̄e , e1 ) and e = e2 .

January 5, 2017

DRAFT

21

Let us show (26). Since B ∈ Robs,A , it follows that B = URA (B̄) for some B̄ ⊂ R. From
r̄e ∈ B, we have r̄e = η(r, u) for some r ∈ B̄ and u ∈ AP −1 (). Since  ∈ AP (e1 ), it follows
that ue1 ∈ AP −1 (). Thus
η(r̄e , e1 ) = η(r, ue1 ) ∈ URA (B̄) = B,
which completes the proof of (22).
Next we prove (23). To show ηobs,A (B, t) ⊂ η̄obs,A (B, t), suppose that z ∈ ηobs,A (B, t). Then
there exist

r ∈ r0 ∈ R : ∃re ∈ B, e ∈ AP (t)−1 ∩Σ s.t. r0 = η(re , e) =: M
and u ∈ AP −1 () such that z = η(r, u). This implies that
∃re ∈ B, e ∈ AP −1 (t) ∩ Σ, u ∈ AP −1 () s.t. z = η(re , eu).
Since eu ∈ AP −1 (t), it follows that z ∈ η̄obs,A (B, t). Thus ηobs,A (B, t) ⊂ η̄obs,A (B, t)
To prove the reverse inclusion, pick z ∈ η̄obs,A (B, t). Then
∃r̄e ∈ B, ē ∈ AP −1 (t) s.t. z = η(r̄e , ē).
Since t ∈ AP (ē), it follows from Lemma 10 that there exist e1 ∈ Σ∗ , e2 ∈ Σ, and e3 ∈ Σ∗ such
that (25) holds. Furthermore, as discussed above, r̄e ∈ B and  ∈ AP (e1 ) lead to η(r̄e , e1 ) ∈ B.
Since e2 ∈ AP −1 (t) ∩ Σ, we have

η(r̄e , e1 e2 ) = η η(r̄e , e1 ), e2 ∈ M.
Finally, since  ∈ AP (e3 ), it follows that
z = η(re , e1 e2 e3 ) ∈ URA (M ) = ηobs,A (B, t).
Thus ηobs,A (B, t) ⊃ η̄obs,A (B, t). This completes the proof.



We are now ready to prove Lemma 13.
Proof of Lemma 13: We prove (21) by induction on the word length. Since

r0,obs,A = z ∈ R : ∃u ∈ AP −1 () s.t. z = η(r0 , u) ,
we have that if y = , then
r ∈ ηobs,A (r0,obs,A , y) ⇔ ∃u ∈ AP −1 () s.t. r = η(r0 , u),
which means that (21) holds for y = .

January 5, 2017

DRAFT

22


Suppose now that (21) holds for all words y ∈ L ObsA (GK ) of length n ≥ 0. Pick a word


y 0 t ∈ L ObsA (GK ) of length n + 1, where y 0 ∈ L ObsA (GK ) has length n. By Lemma 14,

ηobs,A (r0,obs,A , y 0 t) = ηobs,A ηobs,A (r0,obs,A , y 0 ), t

= η̄obs,A ηobs,A (r0,obs,A , y 0 ), t
We therefore have
r ∈ ηobs,A (r0,obs,A , y 0 t)

∃re ∈ ηobs,A (r0,obs,A , y 0 ), e ∈ AP −1 (t) s.t. r = η(re , e). (27)

⇔

Since y 0 has length n, we know by the induction hypothesis that re ∈ ηobs,A (r0,obs,A , y 0 ) if and
only if
∃w0 ∈ AP −1 (y 0 ) s.t. re = η(r0 , w0 ).
Combining this with (27), we obtain
r ∈ ηobs,A (r0,obs,A , y 0 t)

⇔

∃w0 ∈ AP −1 (y 0 ), e ∈ AP −1 (t) s.t. r = η(r0 , w0 e).

(28)

To prove (⇒) in (21), suppose that r ∈ ηobs,A (r0,obs,A , y 0 t). Then from (28) and Lemma 10,
w := w0 e satisfies
w ∈ AP −1 (y 0 )AP −1 (t) = AP −1 (y 0 t)
and r = η(r0 , w), which implies that (⇒) in (21) holds.
Let us next show that (⇐) in (21) holds. Conversely, suppose that
∃w ∈ AP −1 (y 0 t) s.t. r = η(r0 , w).
Since AP −1 (y 0 t) = AP −1 (y 0 )AP −1 (t) from Lemma 10, it follows that
∃w0 ∈ AP −1 (y 0 ), e ∈ AP −1 (t) s.t. w = w0 e.
Since r = η(r0 , w0 e), (28) shows that r ∈ ηobs,A (r0,obs , y 0 t), and hence we have (⇐) in (21).


Next we prove L ObsA (GK ) = AP L(GK ) by induction on the word length. The basis

of induction is the empty string  that belongs to L ObsA (GK ) by definition, and belongs to

AP L(GK ) because AP () = {}.

January 5, 2017

DRAFT

23



Suppose now that L ObsA (GK ) and AP L(GK ) have exactly the same words of length
n ≥ 0, and pick a word y 0 t ∈ ∆∗ of length n+1, where y 0 and t have length n and 1, respectively.
Lemma 14 shows

y 0 t ∈ L ObsA (GK )
⇔

ηobs,A (r0,obs,A , y 0 t)!

⇔



ηobs,A (r0,obs,A , y 0 )! ∧ ∃re ∈ ηobs,A (r0,obs,A , y 0 ), e ∈ AP −1 (t) s.t. η(re , e)! .

(29)

Suppose that y 0 t ∈ L(ObsA (GK )). We do not use the induction hypothesis to prove that
y 0 t ∈ AP (L(GK )) holds. Since y 0 ∈ L(ObsA (GK )) as well, it follows from (21) that
re ∈ ηobs,A (r0,obs,A , y 0 )

⇔

∃w0 ∈ AP −1 (y 0 ) s.t. re = η(r0 , w0 ).

(30)

Combining this with (29), we have
∃w0 ∈ AP −1 (y 0 ), e ∈ AP −1 (t) s.t. η(r0 , w0 e)!.

(31)

Hence w := w0 e satisfies AP (w) = AP (w0 )AP (e) 3 y 0 t and w ∈ L(GK ), which implies



y 0 t ∈ AP L(GK ) . Thus we have L ObsA (GK ) ⊂ AP L(GK ) .

Conversely, suppose that y 0 t ∈ AP L(GK ) . Then there exists w ∈ L(GK ) such that y 0 t ∈
AP (w). Lemma 10 shows that
w = w1 w2 , y 0 ∈ AP (w1 ), t ∈ AP (w2 ).

(32)


for some w1 , w2 ∈ Σ∗ . Since w ∈ L(GK ) leads to w1 ∈ L(GK ), it follows that y 0 ∈ AP L(GK ) .

Since y 0 has length n, the induction hypothesis gives y 0 ∈ L ObsA (GK ) . Hence we have

ηobs,A (r0,obs,A , y 0 )! and (30). To prove y 0 t ∈ L ObsA (GK ) , it suffices from (29) and (30) to show
that (31) holds. Define w0 := w1 and e := w2 . Then we have w0 ∈ AP −1 (y 0 ) and e ∈ AP −1 (t)
from (32). Moreover,
w0 e = w1 w2 = w ∈ L(GK )


leads to η(r0 , w0 e)!. We therefore obtain (31). Thus L ObsA (GK ) ⊃ AP L(GK ) , which
completes the proof.



Using Lemma 13, we finally provide the proof of Theorem 11.
S
Proof of Theorem 11: Define fA : A∈A AP (K) → 2Σ by
fA (y) := Σu ∪ {σ ∈ Σc : ∃w ∈ K s.t. y ∈ AP (w), wσ ∈ K}

January 5, 2017

DRAFT

24

for all y ∈

S

A∈A

AP (K). Then the supervisor f in (6) satisfies
[
[
f (y) =
fA (y)
∀y ∈
AP (K),
A∈A

A∈A

Hence, in order to obtain (20), we need to prove that fA = ΦA for each A ∈ A.
By definition, fA (y) = Σu = ΦA (y) for all y 6∈ AP (K). Suppose that y ∈ AP (K). Since
L(GK ) = K, it follows from Lemma 13 that


AP (K) = AP L(GK ) = L ObsA (GK ) .

Since y ∈ AP (K) = L ObsA (GK ) , we conclude from (21) that
∃r ∈ ηobs,A (r0,obs,A , y) s.t. η(r, σ)!

⇔

∃w ∈ AP −1 (y) s.t. η(r0 , wσ)!.

Since η(r0 , wσ)! means that w, wσ ∈ K, it follows that


σ ∈ Σc : ∃r ∈ ηobs,A (r0,obs,A , y) s.t. η(r, σ)!
= {σ ∈ Σc : ∃w ∈ AP −1 (y) s.t. wσ ∈ K}
= {σ ∈ Σc : ∃w ∈ K s.t. y ∈ AP (w), wσ ∈ K}

which implies that fA (y) = ΦA (y) also for every y ∈ AP (K). This completes the proof.



IV. T EST FOR O BSERVABILITY UNDER R EPLACEMENT-R EMOVAL ATTACKS
In this section, we propose an observability test under replacement-removal attacks in Section III A, inspired by product automata [32].
A. Product automata
Consider a language L = L(G) generated by a finite automaton G = (X, Σ, ξ, x0 ). We want
to test the observability under an attack set A of a specification language K = L(GK ) ⊂ L
generated by a finite automaton GK = (R, Σ, η, r0 ).
For each A, A0 ∈ A, we construct a product automaton TA,A0 = (Q, ΣT,A,A0 , δA,A0 , q0 ) for the
observability test, where Q := R × X × R, q0 := (r0 , x0 , r0 ), and

ΣT,A,A0 := (σ, σ 0 ) ∈ (Σ ∪ {}) × (Σ ∪ {}) \ {(, )} : AP (σ) ∩ A0 P (σ 0 ) 6= ∅ .
The events in ΣTA,A0 are the pairs of events of the original automaton G that may not be
distinguished under attacks A and A0 by a supervisor.

January 5, 2017

DRAFT

25

The transition function δA,A0 : Q × ΣT,A,A0 → Q is defined in the following way: For every
q = (r, x0 , r0 ) ∈ Q and every σT = (σ, σ 0 ) ∈ ΣT,A,A0 , δA,A0 (q, σT ) is defined if (and only if)
η(r, σ), ξ(x0 , σ 0 ), and η(r0 , σ 0 ) are all defined. If δA,A0 (q, σT ) is defined, then

δA,A0 (q, σT ) = η(r, σ), ξ(x0 , σ 0 ), η(r0 , σ 0 ) .
B. Observability test
For each A, A0 ∈ A, let us denote by AcA,A0 (Q) the set of accessible states from the initial
state q0 by some string in L(TA,A0 ), that is,

AcA,A0 (Q) := q ∈ Q : ∃(w, w0 ) ∈ L(TA,A0 ) s.t. q = δA,A0 (q0 , (w, w0 )) .
The following theorem provides a necessary and sufficient condition for observability under
replacement-removal attacks, which can be checked using a set of test automatons {TA,A0 }A,A0 ∈A .
Theorem 15: Consider a replacement-removal attack set A and the test automaton TA,A0
defined above. Assume that a prefix-closed language K ⊂ L(G) is controllable. Then K is not
P -observable under A if and only if there exist A, A0 ∈ A, (r, x0 , r0 ) ∈ AcA,A0 (Q), and σ ∈ Σc
such that
η(r, σ)! ∧ ξ(x0 , σ)! ∧ ¬η(r0 , σ)!.

(33)

The proof of Theorem 15 is provided in the next subsection.
Remark 16 (Computational complexity of observability test for replacement-removal attacks):
The number of the elements in AcA,A0 (Q) is at most |X| · |R|2 . Since we only have to check the
state transition of the elements in AcA,A0 (Q) driven by a controllable event, the total computational complexity to test observability is O(|X| · |R|2 · |Σc | · |A|2 ) for the replacement-removal
attack case. This complexity is the same as the one we derived in Remark 8 for insertion-removal


attacks.

Example 1 (cont.): Consider again the language L(G), the specification language K = L(GK ),
and the attack set A = {A2 , A3 } in Example 1. To check observability under A by Theorem 15,
we need to construct four test automatons TA2 ,A2 , TA3 ,A3 , TA3 ,A2 , and TA2 ,A3 . We see from TA3 ,A2
in Fig. 5 that K is not observable under A. In fact, for the state (r2 , x01 , r10 ) and the controllable
event c ∈ Σc , we have
η(r2 , c)!, ξ(x01 , c)!, and ¬η(r10 , c)!.
Thus K is not observable under A, which is consistent with the discussion in Example 1.

January 5, 2017



DRAFT

26

(r0 , x00 , r00 )

(r1 , x01 , r10 )

(a, a)
0

0

(d, d) (r2 , x3 , r3 ) (b, b)
(r2 , x01 , r10 )

(r3 , x03 , r30 )

(c, ✏) (✏, c)
(c, c)

(✏, c)
(d, ✏)
(d, c)

(b, a)
(a, d)
(r1 , x00 , r00 )

(r2 , x02 , r20 )

(c, ✏)
(r3 , x02 , r20 )

(d, ✏)

(✏, c)

(r0 , x03 , r30 )

(r0 , x02 , r20 )

Fig. 5: Test automaton TA3 ,A2 .

C. The proof of Theorem 15
For all (w, w0 ) ∈ Σ∗ × Σ∗ and all (σ, σ 0 ) ∈ (Σ ∪ {}) × (Σ ∪ {}), we define
(w, w0 )(σ, σ 0 ) := (wσ, w0 σ 0 ).
Using this notation, we define


Σ∗T,A,A0 := (, ) ∩ (σ1 , σ10 ) · · · (σn , σn0 ) : (σi , σi0 ) ∈ ΣT,A,A0 , ∀i = 1, . . . , n, n ∈ N .
Also, we define Σ0T,A,A0 := {(, )} and for each n ≥ 1,

ΣnT,A,A0 := (σ1 , σ10 ) · · · (σn , σn0 ) : (σi , σi0 ) ∈ ΣT,A,A0 , ∀i = 1, . . . , n .
ΣnT,A,A0 is a subset of Σ∗T,A,A0 whose elements have length n ≥ 0.
The following proposition provides another representation of δA,A0 (q0 , (w, w0 )) with initial
states r0 and x0 .
Lemma 17: Consider replacement-removal attacks A, A0 and the test automaton TA,A0 defined
above. For every (w, w0 ) ∈ Σ∗T,A,A0 , if δA,A0 (q0 , (w, w0 )) is defined, then

δA,A0

η(r0 , w)!, ξ(x0 , w0 )!, η(r0 , w0 )!


q0 , (w, w0 ) = η(r0 , w), ξ(x0 , w0 ), η(r0 , w0 ) .

(34)
(35)

Proof: We prove (34) and (35) by induction on the word length of (w, w0 ). The basis of
induction is the empty string (, ). Since δA,A0 (q0 , (, )) = q0 = (r0 , x0 , r0 ) and η(r0 , ) = r0 ,
ξ(x0 , ) = x0 , η(r0 , ) = r0 , it follows that (34) and (35) hold.

January 5, 2017

DRAFT

27


Suppose now that for all (w, w0 ) ∈ ΣnT,A,A0 with n ≥ 0, if δA,A0 q0 , (w, w0 ) is defined, then

0
0 q0 , (w̄, w̄ )
(34) and (35) hold. Let (w̄, w̄0 ) ∈ Σn+1
satisfies
δ
is defined. Then there exist
0
A,A
T,A,A
(w, w0 ) ∈ ΣnT,A,A0 and (σ, σ 0 ) ∈ ΣT,A,A0 such that (w̄, w̄0 ) = (w, w0 )(σ, σ 0 ) and


δA,A0 q0 , (w, w0 ) !, δA,A0 δA,A0 (q0 , (w, w0 )), (σ, σ 0 ) !.

(36)

We know by the induction hypothesis that η(r0 , w), ξ(x0 , w0 ), and η(r0 , w0 ) are defined and that


δA,A0 q0 , (w, w0 ) = η(r0 , w), ξ(x0 , w0 ), η(r0 , w0 ) . Hence we see from the second statement of

(36) that η(r0 , w̄) = η η(r0 , w), σ is defined. Similarly, ξ(x0 , w̄0 ) and η(r0 , w̄0 ) are defined.
Furthermore, we have


δA,A0 q0 , (w̄, w̄0 ) = δA,A0 δA,A0 (q0 , (w, w0 )), (σ, σ 0 )

= η(r0 , w̄), ξ(x0 , w̄0 ), η(r0 , w̄0 ) .
Thus the desired statements (34) and (35) hold for all (w̄, w̄0 ) ∈ Σn+1
T,A,A0 , which completes the


induction step.

The next lemma shows that the product automaton TA,A0 tests state transitions by two events
in K whose observation alphabets may not be distinguished under attacks A and A0 by the
supervisor:
Lemma 18: Consider replacement-removal attacks A, A0 . For the test automaton TA,A0 defined
as in Section IV A, we have

L(TA,A0 ) := (w, w0 ) ∈ Σ∗T,A,A0 : δA,A0 (q0 , (w, w0 ))!

= (w, w0 ) ∈ Σ∗ × Σ∗ : w, w0 ∈ K, AP (w) ∩ A0 P (w0 ) 6= ∅ =: L̂A,A0 .

(37)

In the proof of Lemma 18, we use the lemma below that provides the property of Σ∗T,A,A0 and
a set equivalent to L̂A,A0 .
Lemma 19: Consider two replacement-removal attacks A, A0 and the test automaton TA,A0
defined as in Section IV A. For all (w, w0 ) ∈ Σ∗ × Σ∗ , we have
(w, w0 ) ∈ Σ∗T,A,A0

⇔

AP (w) ∩ A0 P (w0 ) 6= ∅.

(38)

Moreover, the language L̂A,A0 in (37) satisfies

L̂A,A0 = (w, w0 ) ∈ Σ∗T,A,A0 : w, w0 ∈ K .

(39)

Proof: (⇒ of (38)) We show the proof by induction on the word length (w, w0 ) ∈ Σ∗T,A,A0 . The
basis of the induction, (, ), satisfies  ∈ AP ()∩A0 P (). We therefore have AP ()∩A0 P () 6= ∅.

January 5, 2017

DRAFT

28

Suppose that all words (w, w0 ) ∈ ΣnT,A,A0 satisfies AP (w)∩A0 P (w) 6= ∅. Let (w̄, w̄0 ) ∈ Σn+1
T,A,A0 .
Then there exists (w, w0 ) ∈ ΣnT,A,A0 and (σ, σ 0 ) ∈ ΣT,A,A0 such that w̄ = wσ and w̄0 = w0 σ 0 .
The induction hypothesis shows that AP (w) ∩ A0 P (w0 ) 6= ∅, and by construction, we have
AP (σ) ∩ A0 P (σ 0 ) 6= ∅. Thus AP (w̄) ∩ A0 P (w̄0 ) 6= ∅.
(⇐ of (38)) We split the proof into two cases:
[w =  or w0 = ] and [w 6=  and w0 6= ].
First we consider the case [w =  or w0 = ]. Let w = . Since AP () ∩ A0 P (w0 ) 6= ∅ and
since AP () = {}, it follows that  ∈ A0 P (w0 ). If w0 = , then (w, w0 ) = (, ) ∈ Σ∗T,A,A0 .
Suppose that w0 6= . Let w0 = w10 · · · wk0 with w10 , . . . , wk0 ∈ Σ. Then
 ∈ AP (w0 ) = AP (w10 ) · · · AP (wk0 ),
and hence  ∈ AP () ∩ AP (wi0 ) for all i = 1, . . . , k. Thus (w, w0 ) ∈ Σ∗T,A,A0 .
Next we study the case [w 6=  and w0 6= ]. Let w = w1 · · · wl with w1 , . . . , wl ∈ Σ and
w0 = w10 · · · wk0 with w10 , . . . , wk0 ∈ Σ. Suppose that AP (w) ∩ A0 P (w0 ) = {}. Then
 ∈ AP (w) = AP (w1 ) · · · AP (wl )
 ∈ AP (w0 ) = AP (w10 ) · · · AP (wk0 ).
Hence  ∈ AP (wj ) for all j = 1, . . . , l and  ∈ AP (wi0 ) for all i = 1, . . . , k. Thus (w, w0 ) ∈
Σ∗T,A,A0 .
Suppose that AP (w) ∩ A0 P (w0 ) 6= {}, then there exists y ∈ ∆∗ \ {} such that y ∈ AP (w) ∩
A0 P (w0 ). Let y = y1 · · · ym with y1 , . . . , ym ∈ ∆. From Lemma 10, there exist i1 , . . . , im such
that y1 ∈ AP (wi1 ), . . . , ym ∈ AP (wim ) and
 ∈ AP (w1 · · · wi1 −1 ) = AP (w1 ) · · · AP (wi1 −1 )
 ∈ AP (wi1 +1 · · · wi2 −1 ) = AP (wi1 +1 ) · · · AP (wi2 −1 )
..
.
 ∈ AP (wim +1 · · · wl ) = AP (wim +1 ) · · · AP (wl ),
which implies that  ∈ AP (wi ) for all i 6= i1 , . . . , im . We also have similar indices for w0 . Thus
(w, w0 ) ∈ Σ∗T,A,A0 .
The second statement (39) directly follows from (38).



Using Lemmas 17 and 19, we prove Lemma 18.

January 5, 2017

DRAFT

29

Proof of Lemma 18: From Lemmas 17 and 19, we obtain L(TA,A0 ) ⊂ L̂A,A0 .
Let us prove L(TA,A0 ) ⊃ L̂A,A0 . From Lemma 19, it is enough to show this inclusion by
induction on the word length (w, w0 ) ∈ Σ∗T,A,A0 . Since AP () ∩ A0 P () = {}, the basis of the
induction, (, ), belongs to both sets L(TA,A0 ) and L̂A,A0 .
Suppose that all words in L̂A,A0 whose length is n ≥ 0 belong to L(TA,A0 ). Let (w̄, w̄0 ) ∈ L̂A,A0
0
have length n + 1, that is, (w̄, w̄0 ) satisfy Σn+1
T,A,A0 and w̄, w̄ ∈ K. Then

(w̄, w̄0 ) = (w, w0 )(σ, σ 0 )
for some (w, w0 ) ∈ ΣnT,A,A0 and some (σ, σ 0 ) ∈ ΣT,A,A0 . Since w, w0 ∈ K, the induction hypothesis
shows that η(r0 , w), ξ(x0 , w0 ), and η(r00 , w0 ) are defined. Hence

δA,A0 q0 , (w̄, w̄0 ) !




η η(r0 , w), σ ! ∧ ξ ξ(x0 , w0 ), σ 0 ! ∧ η η(r00 , w0 ), σ 0 !

⇐

The right statement is equivalent to w̄, w̄0 ∈ K. Thus all the words in L̂A,A0 whose length is
n + 1 belong to L(TA,A0 ). This completes the proof.



We are now ready to provide a proof of Theorem 15, where the property of L(TA,A0 ) in
Lemma 18 plays an important role.
Proof of Theorem 15: (⇒) Suppose that K is not observable under the attack set A. From
Proposition 3, there exist w, w0 ∈ K, σ ∈ Σc , and A, A0 ∈ A such that
AP (w) ∩ A0 P (w0 ) 6= ∅, wσ ∈ K, and w0 σ ∈ L \ K.

Then Lemma 18 shows that (w, w0 ) ∈ L(TA,A0 ). Hence δA,A0 q0 , (w, w0 ) is defined, and (34) in
Lemma 17 holds. Define r, x0 , r0 by
r := η(r0 , w),

x0 := ξ(x0 , w0 ),

r0 := η(r0 , w0 ).

Then we see from (35) in Lemma 17 that

(r, x0 , r0 ) = δA,A0 q0 , (w, w0 ) ,
and hence (r, x0 , r0 ) ∈ AcA,A0 (Q). Furthermore, since wσ ∈ K and w0 σ ∈ L \ K, we have (33).
(⇐) Conversely, suppose that A, A0 ∈ A, (r, x0 , r0 ) ∈ AcA,A0 (Q), and σ ∈ Σc satisfy (33). Since

(r, x0 , r0 ) ∈ AcA,A0 (Q), it follows that (r, x0 , r0 ) = δA,A0 q0 , (w, w0 ) for some (w, w0 ) ∈ L(TA,A0 ),
and hence Lemma 17 shows that
r = η(r0 , w),

January 5, 2017

x0 = ξ(x0 , w0 ),

r0 = η(r0 , w0 ).

DRAFT

30

In conjunction with (33), this leads to wσ ∈ K and w0 σ ∈ L \ K. On the other hand, since
(w, w0 ) ∈ L(TA,A0 ), it follows from Lemma 18 that w, w0 ∈ K and AP (w) ∩ A0 P (w0 ) 6= ∅. Thus
Proposition 3 shows that K is not observable under the attack pair {A, A0 }. This completes the


proof.
V. C ONCLUSION

We studied supervisory control for DESs in the presence of attacks. We defined a new notion of
observability under attacks and proved that this notion combined with conventional controllability
is necessary and sufficient for the existence of a supervisor enforcing the specification language
despite the attacks. Furthermore, we showed that the usual notion of observability can be used
to test the new notion of observability in the case of insertion-removal attacks. The automaton
representation and the observability test were extended for replacement-removal attacks. In [35],
we also define normality under attacks and discuss the existence of a maximally permissive
supervisor. An important direction for future work is to combine robustness against attack with
confidentiality and integrity in supervisory control for DESs.
R EFERENCES
[1] S. Checkoway, D. McCoy, B. Kantor, D. Anderson, Shacham, S. H. Savage, K. Kocher, A. Czeskis, F. Roesner, and
T. Kohno, “Comprehensive experimental analyses of automotive attack surfaces,” in Proc. USENIX Security Symposium,
2011.
[2] A. J. Kerns, D. P. Shepard, J. A. Bhatti, and T. E. Humphreys, “Unmanned aircraft capture and control via GPS spoofing,”
J. Field Robot., vol. 31, pp. 617–636, 2014.
[3] J. Slay and M. Miller, “Lessons learned from the Maroochy water breach,” in Proc. Critical Infrastructure Protection, vol.
253, 2007, pp. 73–82.
[4] J. P. Farwell and R. Rohozinski, “Stuxnet and the future of cyber war,” Survival, vol. 53, pp. 23–40, 2011.
[5] T. De Maiziére, “Die Lage der IT-Sicherheit in Deutschland 2014,” Tech. Report, Federal Office for Information Security,
2014. [Online]. Available: http://www.wired.com/wp-content/uploads/2015/01/Lagebericht2014.pdf
[6] P. Falkman, B. Lennartson, and M. Tittus, “Specification of a batch plant using process algebra and petri nets,” Control
Eng. Practice, vol. 17, pp. 1004–1015, 2009.
[7] X. Zhao, P. Shi, and L. Zhang, “Asynchronously switched control of a class of slowly switched linear systems,” Systems
Control Lett., vol. 61, pp. 1151–1156, 2012.
[8] M. Uzam and G. Gelen, “The real-time supervisory control of an experimental manufacturing system based on a hybrid
method,” Control Eng. Practice, vol. 17, pp. 1174–1189, 2009.
[9] H. Fawzi, P. Tabuada, and S. Diggavi, “Secure estimation and control for cyber-physical systems under adversarial attacks,”
IEEE Trans. Automat. Control, vol. 59, pp. 1454–1467, 2014.
[10] Y. Shoukry and P. Tabuada, “Event-triggered state observers for sparse noise/attacks,” IEEE Trans. Automat. Control,
vol. 61, pp. 2079–2091, 2016.

January 5, 2017

DRAFT

31

[11] M. S. Chong, M. Wakaiki, and J. P. Hespanha, “Observability of linear systems under adversarial attacks,” in Proc. ACC’15,
2015.
[12] F. Lin, “Robust and adaptive supervisory control of discrete event systems,” IEEE Trans. Automat. Control, vol. 38, pp.
1848–1852, 1993.
[13] S. Takai, “Robust supervisory control of a class of timed discrete event systems under partial observation,” Systems Control
Lett., vol. 39, pp. 267–273, 2000.
[14] A. Saboori and S. H. Zad, “Robust nonblocking supervisory control of discrete-event systems under partial observation,”
Systems Control Lett., vol. 55, pp. 839–848, 2006.
[15] A. M. Sánchez and F. J. Montoya, “Safe supervisory control under observability failure,” Discrete Event Dyn. System:
Theory Appl., vol. 16, pp. 493–525, 2006.
[16] A. Paoli, M. Sartini, and S. Lafortune, “Active fault tolerant control of discrete event systems using online diagnostics,”
Automatica, vol. 47, pp. 639–649, 2011.
[17] S. Shu and F. Lin, “Fault-tolerant control for safety of discrete-event systems,” IEEE Trans. Autom. Sci. Eng., vol. 11, pp.
78–89, 2014.
[18] S. Amin, X. Litrico, S. Sastry, and A. M. Bayen, “Cyber security of water SCADA systems–Part I: Analysis and
experimentation of stealthy deception attacks,” IEEE Trans. Control Systems Tech., vol. 21, pp. 1963–1970, 2013.
[19] A. Teixeira, H. Shames, I. Sandberg, and K. H. Johansson, “A secure control framework for resource-limited adversaries,”
Automatica, vol. 51, pp. 135–148, 2015.
[20] S. Takai and Y. Oka, “A formula for the supremal controllable and opaque sublanguage arising in supervisory control,”
SICE J Control Meas. System Integr., vol. 1, pp. 307–311, 2008.
[21] J. Dubreil, P. Darondeau, and H. Marchand, “Supervisory control for opacity,” IEEE Trans. Automat. Control, vol. 55, pp.
1089–1100, 2010.
[22] A. Saboori and C. N. Hadjicostis, “Opacity-enforcing supervisory strategies via state estimator constructions,” IEEE Trans.
Automat. Control, vol. 57, pp. 1155–1165, 2012.
[23] Y.-C. Wu and S. Lafortune, “Synthsis of insertion functions for enforcement of opacity security properties,” Automatica,
vol. 50, pp. 1336–1348, 2014.
[24] D. Thorsley and D. Teneketzis, “Intrusion detection in controlled discrete event systems,” in Proc. 45th IEEE CDC, 2006.
[25] S.-J. Whittaker, M. Zulkernine, and K. Rudie, “Toward incorporating discrete-event systems in secure software development,” in Proc. ARES’08, 2008.
[26] N. Hubballi, S. Biswas, S. Roopa, R. Ratti, and S. Nandi, “LAN attack detection using discrete event systems,” ISA Trans.,
vol. 50, pp. 119–130, 2011.
[27] L. K. Carvalho, Y.-C. Wu, R. Kwong, and S. Lafortune, “Detection and prevention of actuator enablement attacks in
supervisory control systems,” in Proc. WODES’16, 2016.
[28] S. Xu and R. Kumar, “Discrete event control under nondeterministic partial observation,” in Proc. IEEE CASE’09, 2009.
[29] T. Ushio and S. Takai, “Nonblocking supervisory control of discrete event systems modeled by Mealy automata with
nondeterministic output functions,” IEEE Trans. Automat. Control, vol. 61, pp. 799–804, 2016.
[30] R. Cieslak, C. Desclaux, A. S. Fawaz, and P. Varaiya, “Supervisory control of discrete event processes with partial
observations,” IEEE Trans. Automat. Control, vol. 33, pp. 249–260, 1988.
[31] F. Lin and W. M. Wonham, “On observability of discrete-event systems,” Inform. Sci., vol. 44, pp. 173–198, 1988.
[32] J. N. Tsitsiklis, “On the control of discrete-event dynamical systems,” Math. Control Signals Systems, pp. 95–107, 1989.
[33] P. J. Ramadge and W. M. Wonham, “The control of discrete event systems,” Proc. IEEE, vol. 77, pp. 81–98, 1989.
[34] C. Cassandras and S. Lafortune, Introduction to Discrete Event Systems.

January 5, 2017

Boston, MA: Kluwer, 1999.

DRAFT

32

[35] M. Wakaiki, P. Tabuada, and J. P. Hespanha, “Supervisory control of discrete-event systems under attacks,” Tech. Report,
University of California, Santa Barbara, 2016. [Online]. Available: http://www.ece.ucsb.edu/∼hespanha/published/DES
under attack ver8 19 Tech note.pdf

January 5, 2017

DRAFT

