Estimation and Verification of Partially-Observed Discrete-Event Systems
Xiang Yin










X. Yin Department of Automation, Shanghai Jiao Tong University, Shanghai 200240, China.

             
              
              yinxiang@sjtu.edu.cn           







Estimation and Verification of Partially-Observed Discrete-Event Systems
    Xiang Yin
    
========================================================================







§ INTRODUCTION


State estimation is one of the most fundamental problems in the systems and control theory.
In many real-world systems, it is not always possible to  access the full information of the system due to  measurement noises/uncertainties and the existence of adversaries.
Therefore, how to estimate the state of the system is crucial when one wants to make decisions based on the  limited and incomplete information.

Given a system, one of the most important questions is to prove/disprove the correctness of the system with respect to  some desired requirement (or specification).
In particular, we would like to check the correctness of the system in a formal manner in the sense that the checking procedures are algorithmic and  results have provable correctness guarantees. Such a formal satisfaction checking problem is referred to as the verification problem.
Performing formal  property verification is very important for many complicated but safety-critical infrastructures.


This article considers  state estimation and verification problems for an important class of man-made cyber-physical systems called Discrete-Event Systems (DES).
Roughly speaking, DES are dynamic systems with discrete state-spaces and event-triggered dynamics.
DES models are widely used in the study of complex automated systems where the behavior is inherently event-driven,
as well as in the study of discrete abstractions of continuous, hybrid, and/or cyber-physical systems.
Over  the past decades, the theory of DES has been successfully applied to many real-world problems, 
e.g., the control of automated systems, fault diagnosis/prognosis and information-flow security analysis.

The main purpose of this article is to provide a tutorial and an overview of state estimation techniques and their related property verification problems for partially-observed DES.
Specifically, we focus on  the verification of observational properties, i.e.,  information-flow properties whose satisfactions are based on the observation of the system.
The outline of this article is as follows: 

  
  * In Section <ref>, we briefly introduce some necessary terminologies and the partially-observed DES model considered in this article.
  
  * In Section <ref>, we introduce three types of state estimation problems, namely, current state estimation, initial state estimation and delayed state estimation.
  Then we provide state estimation techniques  for different state estimation problems.
  
  * In Section <ref>, we introduce several important observational properties that arise in the analysis of partially-observed DES.
  In particular, we consider detectability, diagnosability, prognosability, distinguishability and opacity, which cover most of the important properties in partially-observed DES.
  One feature of this section is that we study all these properties  in a uniform manner by defining them in terms of state estimates introduced in Section <ref>.
  
  * In Section <ref>, we provide verification procedures for all properties introduced in Section <ref>.
  All verification procedures are summarized as detailed algorithms using  state estimation techniques provided in Section <ref>.
  
  * In Section <ref>, some related problems and further readings on estimation and verification of partially-observed DES are provided.

The entire article is self-contained. Related references are provided in each section.





§ PARTIALLY-OBSERVED DISCRETE-EVENT SYSTEMS

This section provides the basic   model of partially-observed DES and some related terminologies.
The reader is referred to the textbook <cit.> for more details on DES.

Let Σ be a finite set of events.
A string s=σ_1…σ_n,σ_i∈Σ is a finite sequence of events.
We denote by Σ^* the set of all strings over Σ including the empty string ϵ.
For any string s∈Σ^*, we denote by |s| its length with |ϵ|=0.
A language L⊆Σ^* is a set of strings.
For any string s∈ L in language L, we denote by L/s the post-language of s in L, i.e.,
L/s:={w∈Σ^*: sw∈ L}.
The prefix-closure of language L is defined by L={ s∈Σ^*:∃w∈Σ^*  s.t. sw∈ L };
L is said to be prefix-closed if L=L.

A DES is modeled as a non-deterministic finite-state automaton (NFA)

    G=(X, Σ,δ,X_0),

where X is a finite set of states, Σ is a finite set of events,
δ: X×Σ→ 2^X is the (partial) non-deterministic transition function,
where for any x,x'∈ X,σ∈Σ, x'∈δ(x,σ) means that there exists a transition from state x to state x' with event label σ,
and X_0⊆ X is the set of initial states.
The transition function is also extended to δ:X×Σ^*→ 2^X recursively by:
(i) δ(x,ϵ)={x}; and
(ii) for any x∈ X,s∈Σ^*,σ∈Σ, we have  δ(x,sσ)=   ∪_x'∈δ(x,s)δ(x',σ).
For the sake of simplicity, we write δ(s)=∪_x_0∈ X_0δ(x_0,s).
We define ℒ(G,x)={s∈Σ^*:δ(x,s)!} as the set of strings that can be generated by G from state x∈ X, where “!" means “is defined".
We define ℒ(G):=∪_x_0∈ X_0ℒ(G,x_0) the language generated by system G.

System G is a deterministic finite-state automaton (DFA)
 if (i) |X_0|=1; and (ii) ∀ x∈ X,σ∈Σ:|δ(x,σ)|=1.
We say that a sequence of state x_0x_1… x_n forms a cycle in G if (i) ∀ i=0,…,n-1,∃σ∈Σ: x_i+1∈δ(x_i,σ);
and (ii) x_0=x_n.

Let G_1=(X_1,Σ_1,δ_1,X_0,1) and G_2=(X_2,Σ_2,δ_2,X_0,2) be two automata.
The product of G_1 and G_2, denoted by G_1× G_2, is defined as the accessible part of a new NFA

    G_1× G_2=(X_1× X_2, Σ_1∪Σ_2, δ_1,2, X_0,1× X_0,2),

where the transition function is defined by: for any (x_1,x_2)∈ X_1× X_2, for any σ∈Σ_1∩Σ_2, we have

    δ_1,2((x_1,x_2),σ)={[ δ_1(x_1,σ) ×δ_2(x_2,σ)           if σ∈Σ_1∩Σ_2;              undefined              otherwise ].


In the partial observation setting, not all events generated by the system can be observed.
Formally, we assume that the event set is partitioned as follows

    Σ=Σ_o∪̇Σ_uo,

where Σ_o is the set of observable events and Σ_uo is the set of unobservable events.
The natural projection from Σ to Σ_o is a mapping P:Σ^*→Σ_o^* defined recursively as follows:

    P(ϵ)=ϵ and  
      P(sσ)=
      {[    P(s)σ if σ∈Σ_o;     P(s) if σ∉Σ_o ].

That is, for any string s∈Σ^*, P(s) is obtained by erasing all unobservable events in it.
We denote by P^-1:Σ_o^*→ 2^Σ^* the inverse projection, i.e.,
for any α∈Σ^*_o, we have P^-1(α)={    s∈Σ^*: P(s)=α}.
Note that the codomain of P^-1 is 2^Σ^* as the inverse projection of a string is not unique in general.
We also extend the natural projection to P:2^Σ^*→ 2^Σ_o^* by:
for any L⊆Σ^*, P(L)={P(s)∈Σ_o^*: s∈ L}.
The inverse mapping is also extended to P^-1:2^Σ_o^*→ 2^Σ^* analogously.

Hereafter, we make the following standard assumptions in the analysis of partially-observed DES:

  
  * System G is live, i.e., ∀ x∈ X,∃σ∈Σ: δ(x,σ)!; and
  
  * System G does not contain an unobservable cycle, i.e., ∀ x,x'∈ X, s∈Σ_uo^*∖{ϵ}:x'∉δ(x,s).




§ STATE ESTIMATION UNDER PARTIAL OBSERVATION




 §.§ State Estimation Problems

Since the system is partially-observed, one important question is what do we know about the system's state when a (projected) string is observed.
This is referred to as the state estimation problem in the system's theory.

One  of the most fundamental  state estimation problems is  the  current state estimation problem, 
 i.e., we want to estimate all possible states the system can be in currently based on the observation.

(Current-State-Estimate)
Let G be a DES with observable events Σ_o⊆Σ and α∈ P(ℒ(G)) be an observed string.
The current-state-estimate upon the occurrence of α, denoted by X̂_G(α), is the set of states the system could be in currently based on observation α, i.e.,

    X̂_G(α)={  x∈ X: ∃ x_0∈ X_0,s∈ℒ(G,x_0) s.t. x∈δ(x_0,s)∧ P(s)=α}.



Instead of knowing the current state of the system,  in some applications, one may also be interested in knowing which initial states the system may start from.
This  is referred to as the initial state estimation problem defined as follows.

(Initial-State-Estimate)
Let G be a DES with observable events Σ_o⊆Σ and α∈ P(ℒ(G)) be an observed string.
The initial-state-estimate upon the occurrence of α, denoted by X̂_0,G(α), is the set of initial states the system could start from initially based on observation α, i.e.,

    X̂_0,G(α)={  x_0∈ X_0: ∃  s∈ℒ(G,x_0) s.t.   P(s)=α}.



Note that, in the current-state-estimate, we use the observation up to the current instant to estimate the set of all possible states the system can be in at this instant.
If we keep observing more events in the future, our knowledge of the system's state at that instant may be further improved as 
some states in the current-state-estimate may not be consistent with the future observation.
In other words, we can use future information to further improve our knowledge about the system's state for some previous instant.
This is also referred to as the “smoothing" process; such a smoothed state estimate is also called the delayed-state-estimated defined as follows.

(Delayed-State-Estimate)
Let G be a DES with observable events Σ_o⊆Σ and αβ∈ P(ℒ(G)) be an observed string.
The delayed-state-estimate for the instant of α upon the occurrence of αβ, denoted by X̂_G(α|αβ), is the set of  states the system could be in |β| steps ago when αβ is observed, i.e.,

    X̂_G(α|αβ)=
    {  x∈ X:
    [    ∃ x_0∈ X_0,sw∈ℒ(G,x_0) s.t.; P(s)=α∧ P(sw)=αβ∧   x∈δ(x_0,s) ]}.




Let us consider system G shown in Figure <ref>, where Σ_o={a,b,c} and X_0={0,2}.
Let us consider observable string aa∈ P(ℒ(G)). 
We have P^-1(aa)∩ℒ(G)={aa,uuaa}. 
Then we know that the system may start from   states  0 or  2, i.e, X̂_0,G(aa)={0,2}. 
Also, the system may be currently  in states  4 or 6, i.e.,  X̂_G(aa)={4,6}. 
From string aa, if we further observe event c in the next instant, then we know that X̂_G(aa| aac)={6},
since event c cannot occur from state 4.





 §.§ State Estimation Techniques


In this subsection, we provide techniques for  computing different notions of state-estimates.



  §.§.§ Computation of Current-State-Estimate


The general idea for computing the current-state-estimate is to construct a structure that tracks all possible states consistent with the current observation.
This construction is well-known as the subset construction technique  that can be used to convert a NFA to a DFA.
In the DES literature, this structure is usually referred to as the observer automaton.

(Observer)
Given system G=(X,Σ,δ,X_0) with observable events Σ_o⊆Σ,
the observer is a new DFA

    Obs(G)=(X_obs,Σ_o,δ_obs,x_obs,0),

where X_obs⊆ 2^X∖∅ is the set of states,
x_obs,0={  x∈  X: ∃ x_0∈ X_0,w∈Σ_uo^*  s.t. x∈δ(x_0,w) } is the unique initial state and
δ_obs is the deterministic transition function defined by:
for any q∈ X_obs,σ∈Σ_o, we have

    δ_obs(q,σ)={ x'∈ X: ∃ x∈ q,∃ w∈Σ_uo^* s.t. x'∈δ(x,σ w)    }.

For the sake of simplicity, we will only consider the accessible part of Obs(G).


Intuitively, the observer state tracks all possible states the system can be in currently based on the observation.
Formally, we have the following result. 


For any system G with Σ_o⊆Σ, its observer Obs(G) has the following properties:

  
  * ℒ(Obs(G))=P(ℒ(G)); and
  
  * For any α∈ P(ℒ(G)), we have X̂_G(α)=δ_obs(x_obs,0,α).



Therefore, given an observation α∈ P(ℒ(G)), its current-state-estimate can simply be computed by Algorithm <ref>.
Note that the complexity of building Obs(G) is O(|Σ|2^|X|), which is exponential in the size of G. 
However, we can update the current-state-estimate recursively online and each update step only requires a polynomial complexity.






  §.§.§ Computation of Initial-State-Estimate


We provide two approaches for the computation of initial-state-estimate.

The first approach is based on the augmented automaton that augments the state-space of the original system by tracking where each state starts from.
This approach sometimes is also referred to as the trellis-based approach in the literature.

Formally, given a system G, its augmented automaton is a new NFA

    G_aug=(X_aug, Σ,δ_aug,X_0,aug  ),

where
X_aug⊆ X_0× X is the set of states,
δ_aug:X_aug×Σ→ 2^X_aug is the transition function defined by:
for any (x_0,x)∈ X_aug,σ∈Σ, we have δ_aug((x_0,x),σ)={(x_0,x')∈ X_0× X: x'∈δ(x,σ)},
and
X_0,aug={(x_0,x_0)∈ X_aug: x_0∈ X_0} is the initial state.

We can see easily that ℒ(G)=ℒ(G_aug) and for each state in G_aug,
its first component contains its initial state information and its second component contains its current state information.
Let Obs(G_aug)=(X_obs^aug,Σ_o,δ_obs^aug,x_obs,0^aug) be the observer of G_aug. 
We can easily show that 

    X̂_0,G(α)=I_0(  δ_obs^aug(x_obs,0^aug,α )    ),

where for any q∈ X_obs^aug, I_0(q) denotes the projection to its first component, i.e., I_0(q)={x_0∈ X_0:∃ x∈ X s.t. (x_0,x)∈ q}.
This observation suggests Algorithm <ref> for computing the initial-state-estimate.



The idea of the augmented-automaton-based approach is also very useful for many other purposes, e.g., control synthesis for initial state estimation,
as it only uses the dynamic of the system up to the current point.
However, the complexity of Algorithm <ref> is O(|Σ|2^|X|^2) as the size of G_aug is quadratic in the size of G.
Here we  provide the second approach for computing the initial-state-estimate with a lower complexity based on the reversed automaton of G.

For any NFA G=(X,Σ,δ,X_0), its  reversed automaton is  a new NFA

    G_R=(X,Σ,δ_R,X),

where the transition function δ_R: X×Σ→ 2^X is defined by:
∀ x,x'∈ X,σ∈Σ: x'∈δ_R(x,σ)⇔ x∈δ(x',σ).
Note that  the initial state of G_R is the entire state space.
For any string s=σ_1σ_2…σ_n ∈Σ^*, we denote by s_R its reversed string, i.e., s_R=σ_n…σ_2σ_1.
Then  the following result shows that the initial-state-estimate of a string in G can be computed based on 
the current-state-estimate of its reversed string in the reversed automaton G_R.

<cit.>
For any α∈ P(ℒ(G)), we have X̂_0,G(α)=X̂_G_R(α_R)∩ X_0.


Based on the above result,  Algorithm <ref> is proposed  to compute the initial-state-estimate
and its complexity is only  O(|Σ|2^|X|).





  §.§.§ Computation of Delayed-State-Estimate


For any αβ∈ P(ℒ(G)), the delayed-state-estimate X̂_G(α|αβ) involves two parts of information:
the current information α and the future information β.
Recall that we are interested in estimating states for the instant of α.
The following result shows that the delayed-state-estimate can simply be separated as two parts that do not depend on each other.

<cit.>
For any αβ∈ P(ℒ(G)), we have

    X̂_G(α|αβ)=  X̂_G(α)∩X̂_0,G(β)=  X̂_G(α)∩X̂_G_R(β_R).



Based on Proposition <ref>,   Algorithm <ref> can be used to compute the delayed-state-estimate and its complexity is also  O(|Σ|2^|X|).




We still consider system G shown in Figure <ref>, where Σ_o={a,b,c} and X_0={0,2}.
Its observer Obs(G) is shown in Figure <ref>.
For example, string aa reaches state {4,6} from the initial state in Obs(G).
Therefore, we have X̂_G(aa)={4,6}.
To preform   initial state estimation and delayed state estimation,
we need to build the reversed automaton G_R and  its observer Obs(G_R)  shown in Figures <ref> and <ref>, respectively.
For example, string cba reaches state {0,1,8} from the initial state in Obs(G_R).
Therefore, we have X̂_0,G(abc)=X̂_G_R((abc)_R)∩ X_0={0,1,8}∩{0,2}={0},
i.e., we know for sure that the system was initially from state 0.
To computed the delayed-state-estimate X̂_G(a | aac),
we have
X̂_G(a | aac)=X̂_G(a)∩X̂_G_R(ca)={3,4,8}∩{0,1,2,3,5}={3}.





§ PROPERTIES OF PARTIALLY-OBSERVED DES

In this section, we discuss several important properties in partially-observed DES.
As we mentioned before, we will only focus on observational properties.



 §.§ Detectability


In the previous section, we have provided algorithms for computing state estimates.
Then  the natural question arises as to can the state estimation algorithm   (eventually) provides precise state information.
This is referred to as the detectability verification problem.
Here, we consider three most fundamental types of detectability.

(Detectability  <cit.> )
Let  G be a DES with Σ_o⊆Σ. Then G is said to be

  
  * current-state detectable if (∃ n ∈ℕ)(∀α∈  P(ℒ(G)): |α| ≥  n)[|X̂_G(α)|=1];
  
  * initial-state detectable if (∃ n ∈ℕ)(∀α∈  P(ℒ(G)): |α| ≥  n)[ |X̂_0,G(α)|=1];
  
  * delayed detectable (w.r.t. parameters k_1,k_2∈ℕ)  if (∀αβ∈ P(ℒ(G)): |α|≥ k_1,|β|≥ k_2)[  |X̂_G(α|αβ)|=1].



Intuitively,  current-state detectability (respectively, initial-state detectability) requires that the current state (initial state) of the system can always be detected unambiguously within a finite delay. Note that, for initial-state-estimate, once the initial state is detected, we know it for sure forever, which is not the case for current-state-estimation.
Delayed detectability requires that, for any specific instant after k_1 steps, we can always unambiguously determine the precise state of the system at that instant 
with at most k_2 steps of information delay.
That is, one is allowed to use future information to “smooth" the state estimate of a previous instant.

The concept of detectability was initially  proposed by Shu and Lin in <cit.>, which generalizes the concept of observability studied in <cit.>.
There are also other notions of detectability proposed in the literature.
For example, weak detectability <cit.> requires that the state of the system can be detected for some path generated by the system.
Also, <cit.> proposed the notion of periodic detectability, which requires that  the state of the system can be detected periodically.
In <cit.>, the authors proposed the notion of K-detectability by replacing the detection condition |X̂_G(α)|=1 as |X̂_G(α)|≤ K,
where K∈ℕ is a positive integer specifying the detection precision.
A generalized version of detectability was proposed in <cit.>.
The reader is referred to <cit.>  for more references on detectability.



 §.§ Diagnosability and Prognosability of Fault


Another important application of partially-observed DES is the fault diagnosis/prognosis problem.
In this setting, we assume that system G may have some fault modeled as fault events  Σ_F⊆Σ.
For any string s∈Σ^*, we write Σ_F∈ s if s contains a fault event in Σ_F.
We define Ψ(Σ_F):={s e_f∈ℒ(G): e_f∈Σ_F} as the set of strings that end up with fault events.
In the fault diagnosis problem, we assume that all fault events are unobervable; otherwise, it can be diagnosed trivially.
Without loss of generality, we can further assume that the state space of G is partitioned as fault states and non-fault states

    X=X_N∪̇X_F,

such that

  
  * ∀ x_0∈ X_0,∀ s∈ℒ(G,x_0):  Σ_F∉ s⇒δ(x_0,s)⊆ X_N; and
  
  * ∀ x_0∈ X_0,∀ s∈ℒ(G,x_0):  Σ_F∈ s⇒δ(x_0,s)⊆ X_F.

This assumption can be fulfilled by taking the product   between G and a new automaton with two states capturing the occurrence of fault;
see, e.g., <cit.>.

To diagnose the occurrence of fault, the current state estimation technique can be applied.
Specifically,  for any observation  α∈ P(ℒ(G)), we know that

  
  * the fault has occurred for sure if X̂_G(α)⊆ X_F;
  
  * the fault has not occurred for sure if X̂_G(α)⊆ X_N;
  
  * the fault may have occurred but it is uncertain  if X̂_G(α)∩ X_N≠∅ and X̂_G(α)∩ X_F≠∅.

Then  the natural question arises as to can we always determine the occurrence of fault  within a finite number of delays.
This is captured by the notion of diagnosability as follows. 

(Diagnosability)
System G is said to be diagnosable w.r.t. Σ_o and Σ_F if
(∀ s∈Ψ(Σ_F))(∃ n∈ℕ) (∀ t∈ℒ(G)/s:|t|≥ n)
[ X̂_G(P(st))⊆ X_F ].



For the sake of simplicity, our definition of diagnosability is based on the current-state-estimate and the pre-specified  fault states.
Diagnosability was originally defined by <cit.> purely based on   languages as follows

    (∀ s∈Ψ(Σ_F))(∃ n∈ℕ)(∀ t∈ℒ(G)/s:|t|≥ n)
    (∀ w∈ P^-1(P(st)) ∩ℒ(G)) [Σ_F∈ w]

 One can easily check that the language-based definition and the current-state-estimate-based definition are equivalent. 
 Also, in general,   the non-fault behavior can be described as a   specification language rather than fault events; 
this formulation can also be transformed to our event-based fault setting by refining the state-space of the system; see, e.g., <cit.>.




The concept of diagnosability of DES was first introduced in <cit.>, where state-based faults are considered.
In <cit.>, the authors introduced the language-based formulation of diagnosability.
Since then  many variations of diagnosability have been studied in the literature.
For example, model reduction for diagnosability was studied in <cit.>.
Diagnosability of repeated/intermittent faults was studied in <cit.>. 
The reader is referred to the recent survey <cit.> for more references on diagnosability analysis.

In some applications,  we may want to predict the occurrence of fault before it actually occurs.
This problem is referred to as the fault prognosis problem.
Still, we assume that Σ_F⊆Σ is the set of fault events and X_N⊆ X is the set of non-fault states.
However, in the fault prognosis problem, a fault event needs not be unobservable.
To formulate the problem, we define the  following two sets of states:

  
  * boundary states, ∂(G)={x∈ X_N: ∃ e_f∈Σ_F s.t. δ(x,e_f)!}; and
  
  * indicator states,
  (G)={x∈ X_N: ∃ n∈ℕ,∀ s∈ℒ(G,x) s.t. |s|>n⇒Σ_F ∈ s}.

Intuitively, a boundary state is a non-fault state  from which a fault event may occur in the next step,
and  an indicator state is a state from which a fault event  will occur for sure within a finite number of steps.
With the help indicator states, we can also use current-state-estimation algorithm to perform online fault progsnosis.
Specifically,  for any observation  α∈ P(ℒ(G)), we know that

  
  * the fault will occur for sure in a finite number of steps if X̂_G(α)⊆(G);
  
  * the fault is not guaranteed to occur within any finite number of steps  if X̂_G(α)⊈(G).

Similarly,  the natural question arises as to can we successfully predict the occurrence of fault in the sense that:
(i) there is no missed fault; and (ii) there is no false alarm.
This is captured by the notion of prognosability as follows.


(Prognosability)
System G is said to be prognosable w.r.t. Σ_o and Σ_F if
(∀ s∈ℒ(G):  δ(s)∩∂(G) ≠∅ )
(∃ t∈{s})
[ X̂_G(P(t))⊆(G)].


Prognosability is also referred to as predictability in the literature.
Intuitively, prognosability requires that, for any string that reaches a boundary state, it has a prefix for which we can claim unambiguously that fault will occur for sure in the future,
i.e., we can issue a fault alarm.
Still, for the sake of simplicity, here we characterize prognosability using current-state-estimate, boundary states and indicator states.
Our definition is also  equivalent to the language-based definition in  <cit.>, where predictability was originally introduced.
Prognosability also has several variations in the literature.
For example, in <cit.>, two performance bounds were proposed to characterize how early a fault alarm can be issued 
and when a fault is guaranteed to occur once an alarm is issued.



 §.§ State Disambiguation and Observability


In some applications, the purpose of state estimation is to distinguish some states.
This problem is referred to as the state disambiguation problem <cit.>.
Formally, the specification of this problem is defined as a set of state pairs T_spec⊆ X× X
and we want to make sure that we can always distinguish between a pair of states in T_spec.

(Distinguishability)
System G is said to be distinguishable w.r.t. Σ_o and T_spec⊆ X× X if
(∀α∈ P(ℒ(G)))  [ (X̂_G(α)×X̂_G(α) )  ∩ T_spec= ∅].


Distinguishability is very useful as many important properties in the literature can be formulated as distinguishability.
For example,  one can check that prognosability can actually be re-written as  ditinguishability with specification T_spec=   ∂(G) ×  (X_N∖(G)).
Observability is another important property in partially-observed DES, which together with controllability provide the necessary and sufficient conditions for the existence of a supervisor achieving a desired language. The reader is referred to <cit.> for formal definition of observability.
This property is also a special case of distinguishability (possibly after state-space refinement) as it essentially requires that we can distinguish two states at which different control actions are needed; see, e.g.,  <cit.>.



 §.§ Opacity


Finally, state estimation is also useful in information-flow security analysis, which is an important topic in cyber-physical systems.
In this setting, we assume that the system is also monitored by a passive intruder (eavesdropper) that can observe the occurrences of events in Σ_o.
Furthermore, we assume that the system has a “secret" that does not want to be revealed to the intruder.
In general, what is a secret is problem dependent.
Here, we consider a simple scenario where the secret is modeled as a set of secret states X_S⊆ X.
Then we use the notion of opacity to characterize whether or not the secret can be revealed to the intruder.

(Opacity <cit.>)
Let  G be a DES with Σ_o⊆Σ and secret states X_S⊆ X. Then G is said to be

  
  * current-state opaque if, for any  α∈ P(ℒ(G)), we have  X̂_G(α) ⊈X_S;
  
  * initial-state opaque if, for any  α∈ P(ℒ(G)), we have  X̂_0,G(α) ⊈X_S;
  
  * infinite-step opaque  if, for any   αβ∈ P(ℒ(G)), we have  X̂_G(α|αβ) ⊈X_S.



Essentially, opacity is a confidentiality property  capturing the plausible deniability of the system's “secret" in the presence of an outside observer that is potentially malicious.
More specifically, current-state opacity (respectively, initial-state opacity) requires that
the intruder should never know for sure that the system is currently at (respectively, initially from) a secret state.
The system is said to be infinite-step opaque if the intruder can never determine for sure that the system was at a secret state for any specific instant even based on the future information.

Opacity was originally introduced in the computer science literature <cit.>.
Then it was introduced to the framework of DES by <cit.>.
There are also many variations of opacity studied in the literature.
For example, in <cit.>, Lin formulated  opacity using a language-based framework, where the notions of strong opacity and weak opacity are proposed.
In <cit.>, a concept called initial-and-final-state opacity was provided; the authors also studied the transformations among several notions of opacity.
When one is only allowed to used a bounded delayed information to improve the state estimate for a previous instant (or we do not care about the secret anymore after some delays),
infinite-step opacity becomes to K-step opacity <cit.>, where K is a  non-negative integer capturing the delay bound.
Opacity is also closely related to another two information-flow security properties called anonymity <cit.> and non-interference <cit.>.
The reader is referred to the survey <cit.>  for more references on opacity.





§ VERIFICATION TECHNIQUES


In this section, we provide techniques for verifying observational properties introduced in the previous section.
First, we show that most of the properties in  partially-observed DES can be verified using the observer structure
and 
some important properties can be more efficienty verified using the twin-plant technique in polynomial-time.



 §.§ Observer-Based Verification




  §.§.§ Verification of Detectability

First, we study the verification of current-state detectability.
Recall that, current-state detectability requires that  (∃ n∈ℕ)(∀α∈ P(ℒ(G)): |α|≥ n)[  |X̂_G(α)|=1].
In other words, a system is not current-state detectable if
there is an arbitrarily long observation string such that the current-state-estimate is not always a singleton starting from any instant.
Since P(ℒ(G)) is a regular language, due to the Pumping lemma, the existence of such an arbitrarily long string is equivalent to the existence of a cycle in
Obs(G) in which a state is not a singleton.
This immediately suggests Algorithm <ref> for the verification of current-state detectability.
Initial-state detectability can also be checked in the same manner using G_aug.
The only differences from  Algorithm <ref>  are
 (i) we  need to consider Obs(G_aug) rather than Obs(G) in line 1; and
(ii) in line 2, we need to check the existence of a cycle q_0q_1… q_n in Obs(G_aug) such that |I_0(q_i)|>1 for some i=1,…,n.



To check delayed detectability (for parameters k_1,k_2∈ℕ),  first we recall that
the delayed-state-estimate can be computed by X̂_G(α|αβ)=X̂_G(α)∩X̂_G_R(β_R).
Therefore, delayed detectability can be checked by the following steps:

  
  * First, we compute all possible current-state-estimate X̂_G(α) reachable via some string α whose length is greater than or equal to k_1;
  
  * Then, we compute all possible current-state-estimate of X̂_G_R(β_R) in G_R reachable via some string β_R whose length is greater than or equal to k_2;
  
  * Finally, we test whether or not there exist such X̂_G(α) and  X̂_G_R(β_R) such that |X̂_G(α)∩X̂_G_R(β_R)|>1.
  If so, then it means that some instant after k_1 steps cannot be determined within k_2 steps of delay, i.e,  the system is not delayed detectable.

This procedure is formalized by  Algorithm <ref>, where states in lines 3 and 4 can be computed by a simple depth-first search or a breath-first search. 





  §.§.§ Verification of Diagnosability


The verification of diagnosability is very similar to the case of current-state detectability.
Specifically, a system is not diagnosable if there is an arbitrarily long string after the occurrence of fault such that the current-state-estimate is not a subset of X_N
starting from any instant.
Therefore, the general idea is to replaced condition |q_i|>1 in Algorithm <ref> by q_i⊈X_F.
However, we need to do a little bit more here since we are only interested in   arbitrarily long uncertain strings after the occurrence of fault;
this is also referred to as an indeterminate cycles in the literature <cit.>.
In other words, the existence of an arbitrarily long uncertain but non-fault string does not necessarily violate diagnosability.

To this end, we need to compose Obs(G) with the dynamic of the original system G.
Specifically, let Obs(G) be the observer of G. We define

    Obs(G)=(X_obs,Σ,δ̃_obs,x_obs,0)

as the  DFA by adding self-loops of all unobservable events at each state in X_obs.
One can easily check that ℒ(G)=ℒ(G×Obs(G)). 
Then, by looking at the first component of each state in G×Obs(G), we know whether a fault event has occurred or not. 
Therefore, we can check diagnosability based on G×Obs(G) by Algorithm <ref>.






  §.§.§ Verification of Distinguishability and Opacity


The verification of distinguishability is straightforward using the observer.
Specifically, we just need to check whether or not there exists a state q∈ X_obs  in Obs(G) such that (q× q)  ∩ T_spec≠∅.
If so, the system is not distinguishable; otherwise, it is distinguishable.
Since we have discussed that prognosability is a special case of distinguishability, it can also be checked in the same manner.

Similarly, current-state opacity can be verified by  checking whether or not there exists a state q∈ X_obs in Obs(G) such that q⊆ X_S.
If so, the system is not opaque; otherwise, it is opaque.
To check initial-state opacity, we need to construct Obs(G_R) and to check  whether or not there exists a state q∈ X_obs^R in Obs(G_R) such that q∩ X_0  ⊆ X_S.

The verification of infinite-step opacity is similar to the case of delayed detectability; both involve delayed-state-estimate that can be computed according to Proposition <ref>.
The verification procedure for infinite-step opacity is provided in  Algorithm <ref> with complexity  O(|Σ|4^|X| ).





 §.§ Twin-Plant-Based Verification

In the previous section, we have shown that the observer  can be used for the verification of all properties introduced.
However, the size of the observer is exponential in the size of the system.
Then  the natural question arises as to can we find polynomial-time algorithms for verifying these properties.
Unfortunately, it has been shown in <cit.> that deciding opacity is PSPACE-complete; hence, no polynomial-time algorithm exists.
However, it is indeed possible to check diagnosability, detectability and distinguishability in polynomial-time by using the twin-plant structure.
This structure was originally proposed in <cit.> for the verification of observability;
later on it has been used for verifying diagnosability (under the name of  “verifier") by <cit.> and for verifying detectability (under the name of “detector") by <cit.>.

(Twin-Plant)
Given system G=(X,Σ,δ,X_0) with observable events Σ_o⊆Σ,
the twin-plant is a new  NFA
V(G)=(X_V,  Σ_V  ,δ_V  ,X_0,V), where

  
  * X_V⊆ X× X is the set of states;
  
  * Σ_V=(Σ_o×Σ_o)∪ (Σ_uo×{ϵ})∪ ({ϵ}×Σ_uo)  is the set of events;
  
  * X_0,V=X_0× X_0 is the set of initial states;
  
  * δ_V:X_V×Σ_V→ 2^X_V is the partial transition function defined by:
  for any state (x_1,x_2) ∈ X_V and event σ∈Σ

(a) If σ∈Σ_o, then the following transition is defined

    δ_V((x_1,x_2),(σ,σ))= δ(x_1,σ)×δ(x_2,σ)

(a) If σ∈Σ_uo, then the following transitions are defined

    δ_V((x_1,x_2),(σ,ϵ))   = δ(x_1,σ)×{x_2}
    δ_V((x_1,x_2),(ϵ,σ))   ={x_1}×δ(x_2,σ)


Hereafter, we only consider the accessible part of V(G).


Intuitively, the twin-plant V tracks all pairs of observation equivalent strings in G.
Specifically, if s_1,s_2∈ℒ(G) are two strings in G such that P(s_1)=P(s_2),
then there exists a string s∈ℒ(V(G)) in V(G) such that its first and second components are s_1 and s_2, respectively.
On the other hand, for any string s=(s_1,s_2)∈ℒ(V(G)) in V(G), we have that P(s_1)=P(s_2).

The twin-plant can be applied directly for the verification of distinguishability.
Specifically, we need to check if V(G) contains a pair of states in the specification.
This procedure is presented in Algorithm <ref>.

According to the definition of detectability, we know that the system is not detectable if and only if there exist two arbitrarily long strings having the same observation,
such that these two strings lead to two different states.
As we discussed above, all such string pairs can be captured by the twin-plant.
This suggests Algorithm <ref> for the verification of current-state detectability.

The case of diagnosability is similar.
Specifically, a system is not diagnosable  if there exist an arbitrarily long fault string and a non-fault string such that they have the same observation.
This condition can be checked by Algorithm <ref>.
Note that, we have already assumed that there is no unobservable cycle in G.
Otherwise, we need to add the following condition to the “if condition" in line 2 of Algorithm <ref> to obtain an arbitrarily long fault string:

    ∃ j=0,…,n-1,∃σ_V∉Σ_uo×{ϵ}: (x_j+1^1,x_j+1^2)∈δ_V((x_j^1,x_j^2),σ_V).

Since the size of the twin-plant is only quadratic in the size of G,
distinguishability, detectability and diagnosability can all be checked in polynomial-time,
which is better than the observer-based approach. 
















§ RELATED PROBLEMS AND FURTHER READINGS




 §.§ State Estimation under General Observation Models

Throughout this article, we assume that the observation of the system is modeled as a natural projection.
The natural projection mapping is essentially static in the sense that an event is always either observable or unobservable.
One  related topic is the  sensor selection problem for static observations <cit.>,
i.e., we want to decide which events should be observable by placing with sensors such that a given observational property is fulfilled.
Another related topic in the static observation setting is the robust state estimation problem when the observation is unreliable.
This problem has been investigated in the context of detectability analysis <cit.>,
diagnosability anlaysis <cit.>
and supervisory control <cit.> for partially-observed DES.

In many situations, due to information communications and acquisitions, the observation mapping may be dynamic,
i.e., whether or not an event is observable depends the trajectory of the system.
One example is the dynamic sensor activation problem, where we can decide to turn sensors on/off dynamically online based on the observation history.
In <cit.>, the fault diagnosis problem is studied under the dynamic observation setting.
In <cit.>, observability is studied under the dynamic observation setting.
In <cit.>, the authors investigated the verification and synthesis of detectability under dynamic observations.
Opacity under dynamic observations is also studied in <cit.>. 
A general approach for dynamic sensor activation for property enforcement is proposed by <cit.>. 
In <cit.>, it has been shown that (co)diagnosability and (co)observability can be mapped from one to the other in the general dynamic observation setting. The reader is referred to the recent survey <cit.> for more references on  state estimation problem under dynamic observations.




 §.§ State Estimation in Coordinated, Distributed and Modular Systems


In the setting of this article, we only consider the scenario where the system is monitored by a single observer,  
which is referred to as the centralized state estimation.
In many large-scale systems, sensors can be physically distributed and the system can be monitored by multiple local observers that have incomparable information.
Each local observer can perform local state estimation and send it to a coordinator.
Then the coordinator will fuses all local information according to some pre-specified protocol in order to obtain a global estimation decision.
This is referred to as the decentralized estimation and decision making problem under coordinated architecture.

In the context of DES, the decentralized estimation and decision making problem was first studied by <cit.> in the context of decentralized supervisory control, where the notion of coobservability is proposed.
In <cit.>, the problem of decentralized fault diagnosis problem was studied and a corresponding property called codiagnosability was proposed; the verification codiagnosability  has also been studied in the literature <cit.>.
The decentralized fault prognosis has also been studied in the literature; see, e.g., <cit.>.
Note that, in   decentralized decision making problems, one important issue is the underlying coordinated architecture.
For example, <cit.> and <cit.> only consider  simple binary architectures  for control and diagnosis, respectively; more complicated architectures  can be found in <cit.>.

When each local observer is allow to communicate and exchange information with each other, the state estimation problem is referred to as the distributed estimation problem.
Works on distributed state estimation and property verification can be founded in <cit.>.
Finally, state estimation and verification of partially-observed modular DES have also been considered in the literature <cit.>,
where a modular system is composed by a set of local modules in the form of G=G_1×⋯× G_n.



 §.§ Estimation and Verification of Petri Nets and Stochastic DES


In this article, we focus on DES modeled as finite state automata.
Petri nets, another important class of DES models, are widely used to model many classes of concurrent systems.
In particular, Petri nets provide a compact model without enumerating the entire state space and it is well-known that Petri net languages are more expressive than regular languages.
The problems of state estimation and property verification have also drawn many attentions in the context of Petri nets.
For example, state (marking) estimation algorithms for Petri nets  have been  proposed  in <cit.>.
Decidability and verification procedures for
diagnosability <cit.>,
detectability <cit.>,
prognosability <cit.> and
opacity <cit.>
are also studied in the literature for Petri nets.

Another important generalization of the finite state automata model is the stochastic DES (or labelled Markov chains).
Stochastic DES can not only characterize whether or not a system can reach a state, it can also capture the possibility of reaching a state.
Hence it provides a model for the quantitative analysis and verification of DES.
State estimation and  verification of many important properties  have also been extended to the stochastic DES setting;
this includes, e.g., diagnosability <cit.>, detectability <cit.>, prognosability <cit.> and
opacity <cit.>.





 §.§ Control Synthesis of Partially-Observed DES


So far, we have only discussed  property verification problems in partially-observed DES.
In many applications, when  the answer to the verification problem is negative,  it is important to synthesize a supervisor or controller that provably enforces the property by restricting the system behavior but as permissive as possible.
This control synthesis problem has been studied in the literature in the framework of the supervisory control theory initiated by Ramadge and Wonham <cit.>. 
The reader is referred to the textbooks <cit.> for more details on supervisory control of DES.
Supervisory control under partial observation  was originally investigated by <cit.>. 
Since then, many control synthesis algorithms for partial-observation supervisors have been proposed <cit.>.
In particular, <cit.> solves the synthesis problem for maximally-permissive non-blocking supervisors in the partial observation setting.

In the context of enforcement of observational properties, in <cit.>, an approach  was proposed for designing a  supervisor that enforces diagnosability.
Control synthesis algorithms have also been proposed in the literature for enforcing opacity; see, e.g. <cit.>.
In <cit.>, the authors studied the problem of synthesizing   supervisors that enforce  detectability.
A uniform approach for control synthesis for enforcing a wide class of properties was recently proposed by Yin and Lafortune in a series of papers <cit.>.



plain



