Privacy Preserving Controller Synthesis via Belief Abstraction
Bo Wu Hai Lin



Detuning the Honeycomb of α-RuCl_3:

Pressure-Dependent Optical Studies Reveal Broken Symmetry
    Martin Dressel
    December 30, 2023
==============================================================================================


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.



§ INTRODUCTION

Privacy is becoming one of the most critical concerns in many practical systems <cit.>. 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 <cit.> 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 <cit.>. And to enforcing the opacity, the proposed approaches  include  synthesizing the supervisor <cit.>, insertion functions <cit.> or edit functions <cit.> to control or manipulate the observed behavior .

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 <cit.>, 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 <cit.>, 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 <cit.> 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 over-approximation of the underlying continuous dynamic <cit.>, which has been successfully applied on the traffic network control with temporal logic specifications <cit.>. The belief abstraction idea has also been proposed in <cit.>, 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) <cit.>. 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 <cit.> 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 <ref> provides the necessary preliminaries to define and solve our problem. Section <ref> introduces our opacity notion. Section <ref> deals with the efficient abstraction of the belief space based on the mixed monotone property. Section <ref> propose two approaches to obtain the controller that preserves the opacity and satisfies the task specification. Section <ref> concludes the paper.





§ PRELIMINARIES
 



 §.§ Nondeterministic Finite Automaton (NFA)

NFA is a popular model to describe the non-probabilistic behavior of the system. 
<cit.>
	An NFA is a tuple 𝒯=(Q,Σ,δ,I) where 
	
	    
  * Q is a finite set of states; 
	    
  * Σ is a finite set of actions; 
	    
  * δ:Q×Σ→ 2^Q 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 𝒯 is defined by ℒ(𝒯)={ω∈Σ^*|∃ q∈ I,δ(q,ω) is defined}. 



 §.§ Markov Decision Process


<cit.>
	An MDP  is a tuple ℳ=(S,π_0,A,P) where
	
	    
  * S is a finite set of states;
	    
  * π_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'):=Pr(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 𝒯_ℳ=(S,A,δ,I), where s∈ I if π_0(s)>0 and s'∈δ(s,a), if P(s,a,s')>0.

A path of an MDP is a sequence  of the form ω=s_0s_1s_2...s_is_i+1...s_n with the length n+1≤ 1, where P(s_j,a_j,s_j+1)>0 for j∈[0,n-1]. We denote Path^fin_s as the collection of finite length paths that start in a state s. To reason about an MDP,  the nondeterminism of the action selection has to be resolved by a scheduler (also known as adversary or policy).

	A scheduler μ:Path_ŝ^fin→ A  of an MDP ℳ is a function mapping every finite path ω_fin∈ Path_ŝ^fin onto an action a∈ A(last(ω_fin)) where last(ω_fin) denotes the last state of ω_fin.


By definition, the scheduler specifies the next action to take at the current state for each finite path w that is possible to encounter. The behavior of an MDP ℳ under a given scheduler μ is then purely probabilistic and thus reduces to a discrete time Markov chain (DTMC) with a set of recurrent classes. 
We denote Sch_ℳ as the set of all possible schedulers for ℳ. A policy μ is called memoryless if μ(ω_fin)=μ(last(ω_fin), that is, the action to take only depends on the current state. A policy is said to have memory otherwise. 







 §.§ Linear Temporal Logic

LTL  is a popular specification language to describe a wide range of temporal properties of sequences of states such as safety (bad things never happen), liveness (good things eventually happen), persistence (good things happen infinitely often), response (if A then B) and so on. 

An LTL formula is generated recursively from a set of atomic propositions (AP), true,false, the Boolean operators  (negation), ∨ (disjunction), ∧ (conjunction) and temporal operators  □ (always), X (next), ∪ (until),  (eventually). Please see <cit.> for detailed semantics and syntax. 








§ CURRENT STATE OPACITY IN BELIEF SPACE

Given a system modeled as an MDP ℳ=(S,π_0,A,P), we assume that there is an intruder that has the knowledge of ℳ 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, the intruder may  maintain a belief b_t:S→ [0,1],∑_s∈ Sb_t(s)=1 over S at time t. At time t+1, when action a∈ A is observed, the belief update is as follows.

    b_t+1(s') = ∑_s∈ SP(s,a,s')b_t(s)

Equivalently in matrix form, we could have

    b_t+1=H_ab_t

where H_a is a N× N matrix with H_a(i,j)=P(s_j,a,s_i), b_0=π_0, N=|S|. Therefore, the dynamics of the belief b_t 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 S_s⊂ S representing the secret states that the system tries to hide from the intruder. S_s is a strict subset of S, since if S_s=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,

    ∑_s∈ S_sb_t(s)≤λ, ∀ t

Any belief state that violates (<ref>) is a bad state that should  be avoided. The switched linear system in (<ref>) is analogous to the observers for a partially observed automaton <cit.> whose states, instead of being a distribution over S, belong to 2^S, the power set of S. The following motivating example will be used through out the paper to illustrate our framework.


Suppose the MDP ℳ models the evolution of inventory levels of a company, which has three states, where s_1 and s_2 represents low and high inventory level and s_3 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 s_1,s_2∈ S_s and x_1=b(s_1),x_2=b(s_2), s_3 is a non-secret state. A = {σ_1,σ_2} represents two different purchase quantities. The initial condition is that b(s_1)=0.3,b(s_2)=0.1. The transition probabilities are as shown in the following matrices, because of random demand levels. 

    H_σ_1=[ 0.2,  0 ,  0.1; 0.4, 0.3,  0.2; 0.4, 0.7,  0.7 ],
    H_σ_2=[  0.4, 0.65,   0.3;  0.2,    0,   0.2;  0.4, 0.35,   0.5 ]





§ BELIEF ABSTRACTION

Checking whether the belief state will enter an undesired region by violating (<ref>) is a reachability problem of (<ref>). 
In this paper, we explore the intrinsic structure of the system (<ref>) by  showing that it is in fact mixed monotone where efficient abstraction method is available <cit.>. 

A system 

    x = F(x)

is mixed monotone, where x∈ X⊂ℝ^n 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) x_1≤ x_2⇒ f(x_1,y)≤ f(x_2,y),∀ x_1,x_2,y∈ X, 3) y_1≥ y_2⇒ f(x,y_1)≤ f(x,y_2),∀ x,y_1,y_2∈ X, where ≤ denotes the element-wise inequality. A switched system is mixed monotone if it is mixed monotone for each mode (action) a∈ A. 

Since ∑_s∈ Sb_t(s)=1, (<ref>) can be equivalently written as an N-1-dimension dynamical system

    b^[1,N-1]_t+1 = F_a(b^[1,N-1]_t)

where b^[1,N-1]_t = [b_t,1,...,b_t,N-1]^T and the function mapping F_a will be shown in the following lemma which proves that (<ref>) is indeed mixed monotone. 

The switched system (<ref>) is mixed monotone. 

From (<ref>), for at a∈ A and t we have 

    b_t+1=H_ab_t =   [ p_1,1     … p_1,N; p_2,1     … p_2,N;     ⋮     …     ⋮; p_N,1     … p_N,N ][ b_t,1; b_t,2;     ⋮; b_t,N ]

Since the probabilities have to sum to one, we have ∑_i=1^Np_i,j=1,∀ j∈{1,...,N} and ∑_i=1^Nb_t,i=1. Therefore, (<ref>) can be rewritten as

    [ b_t+1,1; b_t+1,2;       ⋮; b_t+1,N ]=
       [            p_1,1                …            p_1,N;            p_2,1                …            p_2,N;                ⋮                …                ⋮; 1-∑_i=1^N-1p_i,1                … 1-∑_i=1^N-1p_i,N ]
       [            b_t,1;            b_t,2;                ⋮; 1-∑_i=1^N-1b_t,i ]

Since b_t+1,N = 1-∑_i=1^N-1b_t+1,i, from (<ref>) we have the following equation on the N-1-dimensional system


    [   b_t+1,1;   b_t+1,2;         ⋮; b_t+1,N-1 ]=[     p_1,1         …   p_1,N-1;     p_2,1         …   p_2,N-1;         ⋮         …         ⋮;   p_N-1,1         … p_N-1,N-1 ][   b_t,1;   b_t,2;       ⋮; b_t,N-1;         ]
       -[   p_1,N       …   p_1,N;   p_2,N       …   p_2,N;       ⋮       …       ⋮; p_N-1,N       … p_N-1,N ][   b_t,1;   b_t,2;       ⋮; b_t,N-1;         ]
    +
    [   p_1,N;   p_2,N;       ⋮; p_N-1,N;         ]

Equivalently, we have

    b^[1,N-1]_t+1 = F(b^[1,N-1]_t) = A_1b^[1,N-1]_t-A_2b^[1,N-1]_t+B
  
where A_k(i,j)≥ 0, ∀ i,j∈{1,...,N-1},k∈{1,2}, B(i)≥ 0, ∀ i∈{1,...,N-1}. If we define f(x,y)= A_1x-A_2y+B, from Definition <ref>, 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 (<ref>) is mixed monotone.


Mixed monotone systems  admit efficient over-approximation of the reachable set by evaluating the function f at two points as proven in Theorem <ref>.
<cit.>
Given a mixed monotone system as defined in (<ref>) with decomposition function f(x,y), given x_1,x_2∈ X with x_1≤ x_2, we have 

    f(x_1,x_2)≤ F(x) ≤ f(x_2,x_1), ∀ x∈[x_1,x_2]


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. 

    F([x_1,x_2])⊆ [f(x_1,x_2),f(x_2,x_1)]

where F(X')={F(x)|x∈ X'} and X'∈ X is called the one-step reachable set from X' <cit.>. x∈ [x_1,x_2] if and only if x_1≤ x≤ x_2. It can be observed from (<ref>) that it is sufficient to evaluate the decomposition function f at two points x_1 and x_2 to compute an over-approximation of the one-step reachable set where the bounding has been shown to be tight <cit.>. 

Given the MDP model ℳ=(S,π_0,A,P), now we are ready to construct a finite state abstraction of the  belief space dynamic as defined in (<ref>), which is similar to <cit.>. The major difference is that, the domain X in <cit.> is a box  where the interval in each dimension is independent of others, while in this paper, from (<ref>) 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 {I_q},q∈ Q, where I_q=[x^q_1,x^q_2],x_1^q≤ x_2^q, ⋃_q∈ QI_q= X, int(I_q)∩ int(I_q')=∅, ∀ q,q'∈ Q,q≠ q', int(I_q) denotes the interior of I_q.


The probabilistic simplex x_1+x_2≤ 1, x_1≥ 0, x_2≥ 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 (<ref>), which basically defines a bad set ⊥ = {b|∑_s∈ S_sb(s)>λ} that the belief should never enter. The following lemma then shows that there exists a simple algorithm to determine whether a partition I_q has an overlap with ⊥.


Given an interval I_q=[x_1,x_2],x_1≤ x_2 and the set ⊥, then I_q⋂⊥≠∅ if  ∑_s∈ S_sx_2(s)>λ.


Any I_q that overlaps with ⊥ is categorized as a bad region that should be avoided. Figure <ref> illustrates the partition of Example <ref> where the opacity requirement is that b(s_1)+b(s_2)≤ 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 re-partition this grid into two smaller grids such that the initial belief state is no longer in a bad region.



The second step is to construct the NFA 𝒯=(Q⋃ bad,Σ,δ,I) given the MDP model ℳ=(S,π_0,A,P) and the partition {I_q},q∈ Q, where Σ=A. To determine the transition relation in 𝒯, q'∈δ(q,σ), if and only if [f_σ(x_1,x_2),f_σ(x_2,x_1)]⋂ I_q'≠∅. That is,if our over-approximated one-step reachable set for I_q has a non-empty interception with the partitioned region I_q' given the action σ, there will be a transition relation q'∈δ(q,σ) in the abstraction system 𝒯. We still take Figure <ref> as the example to illustrates how to determine the transition relation. All the shaded grids are bad regions and there are 6 states (correspondingly 6 regions) of interest in 𝒯. Let's look at q_2. By mixed monotone property, we only have to evaluate two points, namely p_1=(0,0.4) and p_2=(0.2,0.6). With action σ_1∈Σ, from Figure <ref> it can be seen that the over-approximation reachable set overlaps with q_0 and q_1. Therefore, we have q_0∈δ(q_2,σ_1) and q_1∈δ(q_2,σ_1). 
Similarly, we have 
q_3∈δ(q_2,σ_2), q_4∈δ(q_2,σ_2) and bad∈δ(q_2,σ_2). 

Here, bad denotes a bad region. 





It should be noted that such abstraction could produce spurious trajectories that do not actually exist in (<ref>). 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 (<ref>) 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 <ref>, since we have (q_3,σ_2,bad)∈→, action σ_2 will be disabled in q_3. 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 𝒯 or the initial state of 𝒯 is pruned. If the latter situation happens, it implies that the current partition may be too coarse so that the over-approximation 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 (<ref>) will eventually drive the belief state to ⊥ under arbitrary switching. If this is the case, there is no hope to find a non-empty 𝒯 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 <ref> is shown in Figure <ref>. 

	



§ CONTROLLER SYNTHESIS

Once we obtain the abstracted belief model 𝒯, together with the MDP model ℳ, 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.



 §.§ Direct Synthesis

For Example <ref>, 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 ℳ' based on the original model ℳ to constrain the available actions at each state considering the opacity constraint. Recall that we assume that in ℳ, A(s)=A,∀ s∈ S. However, with the privacy constraints represented as 𝒯, some of the actions may cause privacy violation (even though not necessarily, since 𝒯 is an over-approximation of the concrete dynamics). The new MDP is  ℳ'=(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 𝒯_ℳ obtained from ℳ and 𝒯. The synchronous product is defined in a standard way as follows <cit.>.
 
	Given two NFAs 𝒯_i=(Q_i,Σ,δ_i,I_i) with i=1,2, the product automaton 𝒯 as the result of synchronous product of 𝒯_1 and 𝒯_2 is the NFA 𝒯=𝒯_1⊗𝒯_2= (Q,Σ,δ,I), where Q= Q_1× Q_2,I = I_1× I_2 and (q_1',q_2')∈δ((q_1,q_2),σ) if and only if q_1'∈δ_1(q_1,σ) and q_2'∈δ_2(q_2,σ).	
	

Once we get 𝒯'=𝒯_ℳ⊗𝒯={Q',Σ,δ',I'}, we obtain A'(s) as follows.

    A'(s) = ⋂_(q,s)∈ Q'Σ((q,s))

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 (<ref>), we obtain A'(s)={σ_1},∀ s∈ S in Figure <ref>. Then the second step is the controller synthesis performed on the MDP ℳ' to obtain the policy such that the task specification ϕ in LTL or PCTL can be satisfied with the optimal probability p on ℳ'. For this step, the synthesis algorithm can be found in <cit.>.

The optimal policy obtained on ℳ' satisfies the opacity specifications and incurs the same probability to satisfy the  specification as in ℳ.


Since ℳ' only differs from ℳ 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 (<ref>), 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 ℳ' 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.  



 §.§ Edit function

If the intruder is the competitor in Example <ref>,  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 <cit.> 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 ℳ=(S,π_0,A,P) and its corresponding NFA 𝒯_ℳ=(Q,Σ,δ,I) where Q=S,Σ=A, we are looking for an edit function f_e:Σ^*→Σ^*, such that the followings are satisfied.

    
  * ∀ω∈ℒ(𝒯_ℳ),f_e(ω)  is defined
    
  * ∀ω∈ℒ(𝒯_ℳ),∃ s∈ I, δ(s,f_e(ω))  is defined
    
  * ∀ω∈ℒ(𝒯_ℳ), after executing f_e(ω), the switched system defined as in (<ref>) satisfies (<ref>).

Intuitively, the first item requires that the edit function f_e 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, f_e may not be unique. 





Given a system modeled as an MDP ℳ=(S,π_0,A,P), f_e can be implemented as a (potentially) infinite-state edit automaton 𝒯_f=(Q_f,Σ,δ_f,I_f), where Σ=A, δ_f⊆ Q_f×Σ×Σ^*× Q_f. Therefore, each transition (q,σ,o,q') in 𝒯_f 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⊆ Q_f×Σ×Σ× Q_f, that is, it must output one and only one event σ∈Σ after an event has actually happened in the system.

In this paper,  f_e is easier to synthesize, since all actions are defined at every state, and the second requirement of f_e is automatically satisfied.  To guarantee the third requirement, the output behavior of f_e can be the language generated by the abstraction 𝒯=(Q,Σ,δ,I). That is, the edit automaton 𝒯_f=(Q,Σ,δ_f,I), where given the transition (q,o,q'),o∈Σ in 𝒯 and given the actual event σ∈Σ, there is a transition (q,σ,o,q'). Therefore, the intruder observes a subset of the generated language of 𝒯, 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 𝒯 in Figure <ref>. Regardless of the real system action  that is executed, starting from q_0, 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 (<ref>). 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 q_0 in Figure <ref>, 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 q_1, from Figure <ref>, 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 𝒯 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 (<ref>).



§ CONCLUSION

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. 




IEEEtran

