Privacy Preserving Controller Synthesis via Belief Abstraction

arXiv:1802.10051v2 [cs.CR] 5 Mar 2018

Bo Wu and Hai Lin
Abstract— Privacy is a crucial concern in many systems
in addition to their given tasks. We consider a new notion
of privacy based on beliefs of the system states, which
is closely related to opacity in discrete event systems.
To guarantee the privacy requirement, we propose to
abstract the belief space whose dynamics is shown to
be mixed monotone where efficient abstraction algorithm
exists. Based on the abstraction, we propose two different
approaches to synthesize controllers of the system to
preserve privacy with an illustrative example.

I. I NTRODUCTION
Privacy is becoming one of the most critical concerns
in many practical systems [1]–[4]. The vulnerabilities to
information leaking pose significant challenges in systems that may have a huge social or economic impact if
their privacy is compromised. Examples of such systems
include automobiles, transportation systems, healthcare
systems, robotic systems, power grid and so on.
In the recent years, a notion called “opacity” is
receiving an increasing interest in privacy analysis and
enforcement. Opacity is a confidentiality property that
characterizes a system’s capability to hide its “secret”
information from being inferred by outside passive observers with possibly malicious intentions (termed as
intruders in the sequel). The intruder is assumed to know
the system’s structure and has (partial) access to the
system’s outputs but cannot observe the system states.
The system is opaque if the intruder never decides that
the secret happens with absolute certainty.
Various notions of opacity have been proposed in both
deterministic and stochastic models. Interested readers
are referred to [5] for a comprehensive review. In this
paper, we are interested in the current-state opacity
(CSO), where the secret information is whether or
not the current state of the system is a secret state.
There are essentially two main directions in the opacity
research — verification and enforcement. Algorithms
are designed to verify if the system is opaque from
the intruders [6]. And to enforcing the opacity, the
proposed approaches include synthesizing the supervisor
[7], insertion functions [8]–[10] or edit functions [11] to
control or manipulate the observed behavior .
The partial support of the National Science Foundation (Grant
No. CNS-1446288, ECCS-1253488, IIS-1724070) and of the Army
Research Laboratory (Grant No. W911NF- 17-1-0072) is gratefully
acknowledged.
Bo Wu and Hai Lin are with the Department of Electrical Engineering, University of Notre Dame, Notre Dame, IN, 46556 USA.

bwu3@nd.edu, hlin1@nd.edu

The current definition of the current-state opacity
relies on the absolute certainty that the current state belongs to the secret states. However, with a probabilistic
model, in some cases the intruder may just be able to
maintain a belief distribution over the system states. In
other words, the intruder may only infer that the current
state is a secret state with certain probability based
on the observation history. As mentioned in [12], such
scenario may not be characterized as a CSO violation
by its definition, but still may potentially pose security
threat if the intruder deems the current state being a
secret state with a high confidence.
Thus, we are motivated to introduce, to the best of
our knowledge, a new opacity notion where the system
is considered opaque if the intruder’s confidence that
the current state is a secret state never exceeds a given
threshold. Similar privacy problems have been considered in the computer science community. Protecting
users’ anonymity on the world-wide-web by clustering
the users in large groups that collectively issue requests
for the group members is studied in [13], where the
developed anonymity protocol hides the user identity
which originates certain actions, such that the probability
of the sender being the originator based on the observed
outputs satisfies certain property. Program synthesis to
protect data privacy defined in intruder’s belief is studied
in [14] where the intruder can interact with the program.
The enforcement modifies the program by conflating the
outputs if the privacy requirement is to be violated.
Typically, the intruder updates its belief by computing
its posterior belief distribution based on its a prior belief.
Such update depends on the action executed by the
system since it determines the transition probability. The
opacity requirement defines a convex region that the
belief state should avoid. But to analyze whether the
belief will always stay in the “safe” zone and satisfies
privacy requirement could be a challenging task. In this
paper, we propose to abstract the continuous belief space
into a finite set of grids. By proving that the belief
dynamics is mixed monotone, we could efficiently obtain
the abstracted finite state system that serves as an overapproximation of the underlying continuous dynamic
[15], which has been successfully applied on the traffic
network control with temporal logic specifications [16].
The belief abstraction idea has also been proposed in
[17], but their belief space is the power set of the state
space, which is discrete and finite.

With the abstracted finite belief transition system,
we propose two different approaches to synthesize
controllers to guarantee the privacy and optimize the
given task specification, for example, in linear temporal logic (LTL) or probabilistic computation tree logic
(PCTL) [18]. The first approach identifies the actions
in each state that are guaranteed to preserve privacy
and then synthesize the controller. The second approach
is inspired by the edit function idea [11] and directly
manipulates the observations to the intruder, such that
the intruder may never be confident that the system is
currently in a secret state with the probability more than
some threshold.
The rest of the paper is organized as follows. Section
II provides the necessary preliminaries to define and
solve our problem. Section III introduces our opacity
notion. Section IV deals with the efficient abstraction of
the belief space based on the mixed monotone property.
Section V propose two approaches to obtain the controller that preserves the opacity and satisfies the task
specification. Section VI concludes the paper.
II. P RELIMINARIES
A. Nondeterministic Finite Automaton (NFA)
NFA is a popular model to describe the nonprobabilistic behavior of the system.
Definition 1. [18] An NFA is a tuple T = (Q, Σ, δ, I)
where
• Q is a finite set of states;
• Σ is a finite set of actions;
Q
• δ : Q × Σ → 2 is the transition function;
• I ⊆ Q is a set of initial states.
Note that we didn’t define the accepting states, which
is a subset of Q, since they are not of interest in this
paper. The transition function δ can be extended to Q ×
Σ∗ in a natural way. Given the initial set I ⊆ Q of states,
the language generated by T is defined by L(T ) = {ω ∈
Σ∗ |∃q ∈ I, δ(q, ω) is defined}.
B. Markov Decision Process
Definition 2. [19] An MDP is a tuple M =
(S, π0 , A, P ) where
• S is a finite set of states;
P
• π0 : S → [0, 1],
s∈S π0 (s) = 1, is the initial state
distribution;
• A is a finite set of actions;
′
′
• P (s, a, s ) := P r(s |s, a). That is, the probability
of transiting from s to s′ with action a.
A(s) denotes the set of available actions at the state s.
In this paper, we assume that A(s) = A, ∀s ∈ S. If we
ignore the transition probabilities, the MDP will become
an NFA which we denote as TM = (S, A, δ, I), where
s ∈ I if π0 (s) > 0 and s′ ∈ δ(s, a), if P (s, a, s′ ) > 0.

III. C URRENT S TATE O PACITY

IN

B ELIEF S PACE

Given a system modeled as an MDP M =
(S, π0 , A, P ), we assume that there is an intruder that
has the knowledge of M and is capable of observing all
the actions but not the actual states. Note that the state
is fully observable for the policy of the system to make
decisions. Such scenario could happen in web-based
service or robotic applications where the internal states
are hidden but the service request or robot executions
can be eavesdropped. In this case,
P the intruder may
maintain a belief bt : S → [0, 1], s∈S bt (s) = 1 over S
at time t. At time t + 1, when action a ∈ A is observed,
the belief update is as follows.
X
bt+1 (s′ ) =
P (s, a, s′ )bt (s)
(1)
s∈S

Equivalently in matrix form, we could have
bt+1 = Ha bt

(2)

where Ha is a N × N matrix with Ha (i, j) =
P (sj , a, si ), b0 = π0 , N = |S|. Therefore, the dynamics
of the belief bt is governed by a switched linear system
with |A| modes. At any time t, it may choose to switch
to some mode (action) a ∈ A. Suppose there are a subset
of states Ss ⊂ S representing the secret states that the
system tries to hide from the intruder. Ss is a strict
subset of S, since if Ss = S the problem will become
trivial. It is desirable that at any time, the intruder may
never be sure that the system is in some secret state with
probability over a threshold λ ∈ [0, 1]. In other words,
X
bt (s) ≤ λ, ∀t
(3)
s∈Ss

Any belief state that violates (3) is a bad state that
should be avoided. The switched linear system in (2)
is analogous to the observers for a partially observed
automaton [20] whose states, instead of being a distribution over S, belong to 2S , the power set of S. The
following motivating example will be used through out
the paper to illustrate our framework.
Example 1. Suppose the MDP M models the evolution
of inventory levels of a company, which has three states,
where s1 and s2 represents low and high inventory level
and s3 represents the medium inventory level. The company would like to keep the current inventory level being
too high or too low as secret, because the intruders,
suppliers or competitors, may leverage such information
to adjust the price of the goods for their own benefits.
Therefore s1 , s2 ∈ Ss and x1 = b(s1 ), x2 = b(s2 ),
s3 is a non-secret state. A = {σ1 , σ2 } represents two
different purchase quantities. The initial condition is that
b(s1 ) = 0.3, b(s2 ) = 0.1. The transition probabilities
are as shown in the following matrices, because of

random demand levels.




0.2, 0, 0.1
0.4, 0.65, 0.3
Hσ1 = 0.4, 0.3, 0.2 , Hσ2 = 0.2,
0,
0.2
0.4, 0.7, 0.7
0.4, 0.35, 0.5
(4)
IV. B ELIEF A BSTRACTION
Checking whether the belief state will enter an undesired region by violating (3) is a reachability problem of
(2). In this paper, we explore the intrinsic structure of the
system (2) by showing that it is in fact mixed monotone
where efficient abstraction method is available [15].
Definition 3. A system
x = F (x)

(5)

is mixed monotone, where x ∈ X ⊂ Rn and F :
X → X is a continuous map, if there exists a decomposition function f : X × X → X such that 1)
F (x) = f (x, x), ∀x ∈ X, 2) x1 ≤ x2 ⇒ f (x1 , y) ≤
f (x2 , y), ∀x1 , x2 , y ∈ X, 3) y1 ≥ y2 ⇒ f (x, y1 ) ≤
f (x, y2 ), ∀x, y1 , y2 ∈ X, where ≤ denotes the elementwise inequality. A switched system is mixed monotone if
it is mixed monotone for each mode (action) a ∈ A.
P
Since s∈S bt (s) = 1, (2) can be equivalently written
as an N − 1-dimension dynamical system
[1,N −1]

bt+1

[1,N −1]

= Fa (bt

)

(6)

[1,N −1]

where bt
= [bt,1 , ..., bt,N −1 ]T and the function
mapping Fa will be shown in the following lemma
which proves that (6) is indeed mixed monotone.
Lemma 1. The switched system (6) is mixed monotone.
Proof. From (2), for at a ∈ A and t we have



bt,1
p1,1 . . . p1,N
 p2,1 . . . p2,N   bt,2 



bt+1 = Ha bt =  .
..   .. 
 ..
.  . 
...
pN,1

...

pN,N

PN −1
Since bt+1,N = 1 − i=1 bt+1,i , from (8) we have the
following equation on the N − 1-dimensional system


bt+1,1
bt+1,2
..
.





p1,1
p2,1
..
.

...
...

p1,N −1
p2,N −1
..
.



bt,1
bt,2
..
.




 



 



=



 



...
bt+1,N −1
pN −1,1 . . . pN −1,N −1
bt,N −1

 


p1,N
bt,1
p1,N
...
p1,N

 

 p2,N
...
p2,N 
  bt,2   p2,N 

+ . 
− .



.
.
..   ..   .. 
 ..
...
pN −1,N
bt,N −1
pN −1,N . . . pN −1,N
(9)
Equivalently, we have
[1,N −1]

[1,N −1]

= F (bt

[1,N −1]

) = A1 bt

[1,N −1]

− A2 bt

+B
(10)
where Ak (i, j) ≥ 0, ∀i, j ∈ {1, ..., N − 1}, k ∈ {1, 2},
B(i) ≥ 0, ∀i ∈ {1, ..., N − 1}. If we define f (x, y) =
A1 x − A2 y + B, from Definition 3, it is not hard to find
that all the three conditions are satisfied. Since it holds
for arbitrary a ∈ A, by definition, the switched system
(6) is mixed monotone.
bt+1

Mixed monotone systems admit efficient overapproximation of the reachable set by evaluating the
function f at two points as proven in Theorem 1.
Theorem 1. [15] Given a mixed monotone system as
defined in (5) with decomposition function f (x, y), given
x1 , x2 ∈ X with x1 ≤ x2 , we have
f (x1 , x2 ) ≤ F (x) ≤ f (x2 , x1 ), ∀x ∈ [x1 , x2 ]

(11)

This theorem is a direct result of the mixed monotone
property and is the key to the efficient abstraction, which
can be seen more clearly from the following formula.
(7)

bt,N

Since
we have
PN the probabilities have to sum toPone,
N
i=1 pi,j = 1, ∀j ∈ {1, ..., N } and
i=1 bt,i = 1.
Therefore, (7) can be rewritten as

 

p1,1
...
p1,N
bt+1,1
 bt+1,2  

p2,1
...
p2,N

 

 ..  = 
..
..

 .  

.
...
.
PN −1
PN −1
bt+1,N
1 − i=1 pi,1 . . . 1 − i=1 pi,N


bt,1


bt,2



..



.
PN −1
1 − i=1 bt,i
(8)

F ([x1 , x2 ]) ⊆ [f (x1 , x2 ), f (x2 , x1 )]

(12)

where F (X ′ ) = {F (x)|x ∈ X ′ }andX ′ ∈ X is called
the one-step reachable set from X ′ [15]. x ∈ [x1 , x2 ]
if and only if x1 ≤ x ≤ x2 . It can be observed from
(12) that it is sufficient to evaluate the decomposition
function f at two points x1 and x2 to compute an overapproximation of the one-step reachable set where the
bounding has been shown to be tight [15].
Given the MDP model M = (S, π0 , A, P ), now we
are ready to construct a finite state abstraction of the
belief space dynamic as defined in (6), which is similar
to [15]. The major difference is that, the domain X in
[15] is a box where the interval in each dimension is
independent of others, while in this paper, from (6) it
can be seen that X has the constraint |b[1,N −1] | ≤ 1.
The first step is to partition the domain X into a finite
set of intervals {Iq }, q ∈ Q, where Iq = [xq1 , xq2 ], xq1 ≤

S
xq2 , q∈Q Iq = X, int(Iq ) ∩ int(Iq′ ) = ∅, ∀q, q ′ ∈
Q, q 6= q ′ , int(Iq ) denotes the interior of Iq .
The probabilistic simplex x1 + x2 ≤ 1, x1 ≥ 0, x2 ≥
0 is gridded by squares with width 0.2. Note that the
partitioned grids can have arbitrary sizes and need not to
be equal. This example uses the equal size grids just for
demonstration. Recall the opacity requirement
(3), which
P
basically defines a bad set ⊥= {b| s∈Ss b(s) > λ} that
the belief should never enter. The following lemma then
shows that there exists a simple algorithm to determine
whether a partition Iq has an overlap with ⊥.
Lemma 2. Given an T
interval Iq P
= [x1 , x2 ], x1 ≤ x2
and the set ⊥, then Iq ⊥6= ∅ if s∈Ss x2 (s) > λ.

Any Iq that overlaps with ⊥ is categorized as a bad
region that should be avoided. Figure 1 illustrates the
partition of Example 1 where the opacity requirement is
that b(s1 ) + b(s2 ) ≤ 0.8 all the time. The blue shaded
area denotes ⊥ and all the grey shaded grids are bad
regions. Therefore, we are only concerned with the 6
non-shaded grids. We assume that the initial belief state
is always outside of ⊥. If the grid that contains the initial
belief state is bad due to the overlapping, we may repartition this grid into two smaller grids such that the
initial belief state is no longer in a bad region.
x2
1

0.8

0.6

q2

σ1

σ2

0.4

q1

q5
0.2

q0
x1
0

0.2

q3

0.4

q4

0.6

0.8

1

Fig. 1: A gridded partition, the opacity requirement is
x1 + x2 ≤ 0.8. The big dot denotes the initial condition.
The
S second step is to construct the NFA T =
(Q bad, Σ, δ, I) given the MDP model M =
(S, π0 , A, P ) and the partition {Iq }, q ∈ Q, where
′
Σ = A. To determine the transition relation in
TT, q ∈
′
δ(q, σ), if and only if [fσ (x1 , x2 ), fσ (x2 , x1 )] Iq 6= ∅.
That is,if our over-approximated one-step reachable set
for Iq has a non-empty interception with the partitioned
region Iq′ given the action σ, there will be a transition
relation q ′ ∈ δ(q, σ) in the abstraction system T . We
still take Figure 1 as the example to illustrates how to

start

q2

q1

q4

q3

q0

q5

Fig. 2: T after pruning, the solid lines denote the
transitions induced by σ1 and dashed lines for σ2
determine the transition relation. All the shaded grids
are bad regions and there are 6 states (correspondingly
6 regions) of interest in T . Let’s look at q2 . By mixed
monotone property, we only have to evaluate two points,
namely p1 = (0, 0.4) and p2 = (0.2, 0.6). With action
σ1 ∈ Σ, from Figure 1 it can be seen that the overapproximation reachable set overlaps with q0 and q1 .
Therefore, we have q0 ∈ δ(q2 , σ1 ) and q1 ∈ δ(q2 , σ1 ).
Similarly, we have q3 ∈ δ(q2 , σ2 ), q4 ∈ δ(q2 , σ2 ) and
bad ∈ δ(q2 , σ2 ). Here, bad denotes a bad region.
It should be noted that such abstraction could produce
spurious trajectories that do not actually exist in (6).
This is generally unavoidable in the partition based
approaches. However, since we are only interested in the
safety property in the belief space (if bad belief state is
reachable), such spuriousness may make the results more
conservative, but does not affect its correctness, as all
the transitions that are possible to happen in the concrete
system (6) are included in the abstraction system.
Any outgoing transition (q, σ, bad) should be deleted
from q. To do this, we directly disable the action σ from
q, as the transitions are nondeterministic. For example, in
Figure 1, since we have (q3 , σ2 , bad) ∈→, action σ2 will
be disabled in q3 . If such pruning results in any state q ′
blocking, that is, all its outing transitions for all actions
are pruned, then q ′ and all its incoming and outgoing
transitions are deleted. Such process continues until no
more states are pruned from T or the initial state of T
is pruned. If the latter situation happens, it implies that
the current partition may be too coarse so that the overapproximation is too conservative, which we may need
to find a finer partition scheme, for example, by having
smaller grids. It could also be the case that the belief
dynamics (6) will eventually drive the belief state to ⊥
under arbitrary switching. If this is the case, there is no
hope to find a non-empty T after pruning, regardless
of how the belief space is partitioned. Determining
whether it is true relies on the reachability analysis of
the underlying switched linear systems and is out of the
scope of this paper. The resulting NFA from the griding

in Figure 1 is shown in Figure 2.
V. C ONTROLLER S YNTHESIS
Once we obtain the abstracted belief model T , together with the MDP model M, it is then possible to
synthesize a policy that simultaneously satisfies the task
and privacy specification, regardless of how the nondeterminisim in the abstracted belief model is resolved.
We propose two different solutions based on different
capabilities of the intruders.
A. Direct Synthesis
For Example 1, if the intruder is the supplier which
can observe the purchasing actions since the purchase
has to go through it, we need a purchasing strategy such
that the supplier may never be sure with high confidence
that the company’s inventory is running too low or too
high. We take two steps to obtain synthesize the policy.
The first step is to obtain a new MDP M′ based on
the original model M to constrain the available actions
at each state considering the opacity constraint. Recall
that we assume that in M, A(s) = A, ∀s ∈ S. However,
with the privacy constraints represented as T , some of
the actions may cause privacy violation (even though not
necessarily, since T is an over-approximation of the concrete dynamics). The new MDP is M′ = (S ′ , π0′ , A′ , P ′ )
where S ′ = S, π0′ = π0 , A′ = A, P ′ = P , the only
difference is A′ (s) ⊆ A(s), ∀s ∈ S. To obtain A′ (s),
we propose to product the NFA TM obtained from M
and T . The synchronous product is defined in a standard
way as follows [18].
Definition 4 (Synchronous Product of NFAs). Given two
NFAs Ti = (Qi , Σ, δi , Ii ) with i = 1, 2, the product
automaton T as the result of synchronous product of T1
and T2 is the NFA T = T1 ⊗ T2 = (Q, Σ, δ, I), where
Q = Q1 × Q2 , I = I1 × I2 and (q1′ , q2′ ) ∈ δ((q1 , q2 ), σ)
if and only if q1′ ∈ δ1 (q1 , σ) and q2′ ∈ δ2 (q2 , σ).
Once we get T ′ = TM ⊗ T = {Q′ , Σ, δ ′ , I ′ }, we
obtain A′ (s) as follows.
\
Σ((q, s))
(13)
A′ (s) =
(q,s)∈Q′

where Σ((q, s) ⊆ Σ denotes the set of actions available
at the state (q, s). Intuitively, A′ (s) denotes all the
actions at s that are guaranteed to preserve privacy at
any time. With (13), we obtain A′ (s) = {σ1 }, ∀s ∈ S in
Figure 2. Then the second step is the controller synthesis
performed on the MDP M′ to obtain the policy such that
the task specification φ in LTL or PCTL can be satisfied
with the optimal probability p on M′ . For this step, the
synthesis algorithm can be found in [18].
Theorem 2. The optimal policy obtained on M′ satisfies the opacity specifications and incurs the same

probability to satisfy the specification as in M.
Proof. Since M′ only differs from M in the available
actions at each state, it is straightforward to see that
the same policy induces the same probability on both
of the MDP models. As for opacity specification, from
(13), we are guaranteed to stay in the “safe” belief space
since the action being enabled belongs to A′ (s) and
any action selected from A′ (s) is safe regardless of the
current abstracted belief partition the system is in.
Note that it could be the case that some states in
M′ do not have any action available, in such a case,
an iterative pruning process is applied to delete such
blocking states until either there is no more state to
prune or one of the initial state is pruned. If it is the
latter case, we may need a finer partition to make the
abstraction less conservative.
B. Edit function
If the intruder is the competitor in Example 1, it is
then possible to manipulate the purchase activity report
observable to it, such that the competitor may never
infer with high confidence of the company’s inventory
level being too low or too high. Unlike suppliers, the
competitor cannot distinguish between the real or the
reported purchase. This approach is inspired by the edit
function synthesis in [11] where the system has the
capability to modify the observations of the intruder
based on the real system action, such that the observed
behavior is consistent with the model’s behavior and at
the same time, the intruder may never determine with
certainty that the current state is a secret state. Formally,
given an MDP M = (S, π0 , A, P ) and its corresponding
NFA TM = (Q, Σ, δ, I) where Q = S, Σ = A, we are
looking for an edit function fe : Σ∗ → Σ∗ , such that
the followings are satisfied.
1) ∀ω ∈ L(TM ), fe (ω) is defined
2) ∀ω ∈ L(TM ), ∃s ∈ I, δ(s, fe (ω)) is defined
3) ∀ω ∈ L(TM ), after executing fe (ω), the switched
system defined as in (2) satisfies (3).
Intuitively, the first item requires that the edit function
fe should be defined for all the possible behaviors of the
system. The second item requires that the output of the
edit function, which is observed by the intruder, should
also be a valid behavior of the system. The third item
requires that the output behavior of the edit function
should satisfy the opacity specification. Note that from
this definition, fe may not be unique.
Given a system modeled as an MDP M =
(S, π0 , A, P ), fe can be implemented as a (potentially) infinite-state edit automaton Tf = (Qf , Σ, δf , If ),
where Σ = A, δf ⊆ Qf × Σ × Σ∗ × Qf . Therefore,
each transition (q, σ, o, q ′ ) in Tf denotes that from state
q, when σ ∈ Σ actually happens in the system, it is

modified to become o ∈ Σ∗ which is observed by the
intruder, and then the edit automaton transits to some q ′ .
Intuitively, if we edit every possible executions to be the
empty string ǫ, the intruder will observe nothing and the
system will always be opaque if it is opaque initially.
However, such case may become trivial. Therefore, we
restrict the transitions of the edit automaton to be of the
form δf ⊆ Qf × Σ × Σ × Qf , that is, it must output one
and only one event σ ∈ Σ after an event has actually
happened in the system.
In this paper, fe is easier to synthesize, since all
actions are defined at every state, and the second requirement of fe is automatically satisfied. To guarantee the
third requirement, the output behavior of fe can be the
language generated by the abstraction T = (Q, Σ, δ, I).
That is, the edit automaton Tf = (Q, Σ, δf , I), where
given the transition (q, o, q ′ ), o ∈ Σ in T and given the
actual event σ ∈ Σ, there is a transition (q, σ, o, q ′ ).
Therefore, the intruder observes a subset of the generated language of T , which is guaranteed to preserve
opacity. Furthermore, since we don’t have any restriction
on the actual event σ, the requirement 1 of the edit
function is also satisfied.
In our example, the observation function is essentially
the abstracted model T in Figure 2. Regardless of the
real system action that is executed, starting from q0 , the
edit function may select any action σ that is defined
at the current belief region q to be the observation to
the intruder. Then the next abstracted belief state q ′ is
determined by the belief dynamic (6). Note that such
update is based on the “fake” action σ, not the real
system action, which is hidden by the edit function. For
example, starting from q0 in Figure 2, the edit function
may output σ1 , regardless of actually event σ1 or σ2
happened. If the belief state update based on the output
behavior σ1 results in q1 , from Figure 2, next time it
could either output σ1 or σ2 irrespective of actual event.
In this approach, it can be observed that the privacy
enforcement and the controller synthesis are decoupled.
We could separately obtain the edit function from T and
synthesize the optimal policy for a given specification.
Therefore, the advantage of this approach comparing to
the direct synthesis is that the optimal performance can
always be obtained, regardless of the privacy constraint,
while in direct synthesis, the available actions at each
state are limited by (13).
VI. C ONCLUSION
In this paper we proposed, to the best our knowledge,
a new notion of opacity defined on the belief space.
We then proposed two approaches to synthesis privacy
preserving controllers that regulates the MDP model, so
that the privacy can be preserved. Both approaches rely
on the abstracted model on the belief space, where we

proved that the belief dynamic is mixed monotone and
thus efficient abstraction algorithm exists. Our future
work will be focusing on exploring less conservative
approaches to guarantee the privacy and task accomplishment.
R EFERENCES
[1] P. McDaniel and S. McLaughlin, “Security and privacy challenges in the smart grid,” IEEE Security & Privacy, vol. 7, no. 3,
2009.
[2] H. Chan and A. Perrig, “Security and privacy in sensor networks,” computer, vol. 36, no. 10, pp. 103–105, 2003.
[3] R. H. Weber, “Internet of things–new security and privacy
challenges,” Computer law & security review, vol. 26, no. 1,
pp. 23–30, 2010.
[4] J.-P. Hubaux, S. Capkun, and J. Luo, “The security and privacy
of smart vehicles,” IEEE Security & Privacy, vol. 2, no. 3, pp.
49–55, 2004.
[5] R. Jacob, J.-J. Lesage, and J.-M. Faure, “Overview of discrete
event systems opacity: Models, validation, and quantification,”
Annual Reviews in Control, vol. 41, pp. 135–146, 2016.
[6] F. Lin, “Opacity of discrete event systems and its applications,”
Automatica, vol. 47, no. 3, pp. 496–503, 2011.
[7] A. Saboori and C. N. Hadjicostis, “Opacity-enforcing supervisory strategies via state estimator constructions,” IEEE Transactions on Automatic Control, vol. 57, no. 5, pp. 1155–1165,
2012.
[8] Y.-C. Wu and S. Lafortune, “Synthesis of insertion functions for
enforcement of opacity security properties,” Automatica, vol. 50,
no. 5, pp. 1336–1348, 2014.
[9] B. Wu, Z. Liu, and H. Lin, “Parameter and insertion
function co-synthesis for opacity enhancement in parametric
stochastic discrete event systems,” in American Control
Conference (ACC). IEEE, 2018, to appear. [Online]. Available:
http://arxiv.org/abs/1802.04836
[10] B. Wu, J. Dai, and H. Lin, “Synthesis of insertion functions
to enforce decentralized and joint opacity properties of
discrete-event systems,” in American Control Conference
(ACC).
IEEE, 2018, to appear. [Online]. Available:
https://arxiv.org/abs/1802.05728
[11] Y.-C. Wu, V. Raman, B. C. Rawlings, S. Lafortune, and S. A.
Seshia, “Synthesis of obfuscation policies to ensure privacy and
utility,” Journal of Automated Reasoning, pp. 1–25, 2017.
[12] A. Saboori and C. N. Hadjicostis, “Current-state opacity formulations in probabilistic finite automata,” IEEE Transactions on
Automatic Control, vol. 59, no. 1, pp. 120–133, 2014.
[13] M. K. Reiter and A. D. Rubin, “Crowds: Anonymity for web
transactions,” ACM transactions on information and system security (TISSEC), vol. 1, no. 1, pp. 66–92, 1998.
[14] M. Kučera, P. Tsankov, T. Gehr, M. Guarnieri, and M. Vechev,
“Synthesis of probabilistic privacy enforcement,” in Proceedings
of the 2017 ACM SIGSAC Conference on Computer and Communications Security. ACM, 2017, pp. 391–408.
[15] S. Coogan and M. Arcak, “Efficient finite abstraction of mixed
monotone systems,” in Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control.
ACM, 2015, pp. 58–67.
[16] S. Coogan, M. Arcak, and C. Belta, “Formal methods for control
of traffic flow: Automated control synthesis from finite-state
transition models,” IEEE Control Systems, vol. 37, no. 2, pp.
109–128, 2017.
[17] S. Bharadwaj, R. Dimitrova, and U. Topcu, “Synthesis of
surveillance strategies via belief abstraction,” arXiv preprint
arXiv:1709.05363, 2017.
[18] C. Baier, J.-P. Katoen, and K. G. Larsen, Principles of model
checking. MIT press, 2008.
[19] M. L. Puterman, Markov decision processes: discrete stochastic
dynamic programming. John Wiley & Sons, 2014.
[20] C. G. Cassandras and S. Lafortune, Introduction to discrete event
systems. Springer Science & Business Media, 2009.

