On-Line Synthesis of Permissive Supervisors for Partially Observed Discrete Event Systems under scLTL Constraints
Ami Sakakibara Toshimitsu Ushio
eess.SY cs.FL cs.SY



 


[footnoteinfo]
	This work was supported by JST ERATO Grant Number JPMJER1603, Japan, and JSPS KAKENHI Grant Number JP19J13487, Japan. 


OU,DC]Ami Sakakibara 
OU]Toshimitsu Ushio 


[OU]
	Graduate School of Engineering Science, Osaka University, 
	1-3 Machikaneyama, Toyonaka, Osaka, 560-8531, Japan 
	(e-mail: sakakibara@hopf.sys.es.osaka-u.ac.jp; ushio@sys.es.osaka-u.ac.jp)

[DC]JSPS Research Fellow



                
We consider a supervisory control problem of a discrete event system (DES) under partial observation, where a control specification is given by a fragment of linear temporal logic. 
We design an on-line supervisor that dynamically computes its control action with the complete information of the product automaton of the DES and an acceptor for the specification. 
The concepts of controllability and observability are defined by means of a ranking function defined on the product automaton, which decreases its value if an accepting state of the product automaton is being approached.
The proposed on-line control scheme leverages the ranking function and a permissiveness function, which represents a time-varying permissiveness level. 
As a result, the on-line supervisor achieves the specification, being aware of the tradeoff between its permissiveness and acceptance of the specification, if the product automaton is controllable and observable. 




	On-line supervisory control, discrete event systems, partial observation, linear temporal logic, ranking function, automata.








§ INTRODUCTION




The supervisory control theory for discrete event systems (DESs) has been widely studied since its initiation in <cit.>. 
Synthesis of supervisors turns out to be computationally hard when the controlled system is large or has much complex aspects.
Researchers have overcome the difficulty by designing supervisors on-line. 

<cit.> proposed a method to generate limited lookahead trees on-the-fly instead of constructing a complete supervisor and their methods are extended to the settings of partial observation <cit.> or time-varying DESs <cit.>.



Another way is taken to design on-line supervisors for partially observed DESs, where the supervisor modifies appropriate control actions precomputed in the case of full observation <cit.>. 







In the supervisory control framework, control requirements are typically given by formal languages, i.e., subsets of event sequences generated by the system.  
Practically, we need to translate desired behavior of the system into formal languages, which is a hard task.
For this reason, linear temporal logic (LTL) is paid much attention to as a formal specification language for control problems, thanks to its rich expressiveness <cit.>. 



It is practically acceptable to restrict the specification language to a fragment of LTL like syntactically co-safe LTL (scLTL), for which synthesis problems can be solved in much less complexity than for the case of the general LTL <cit.>.

In <cit.>, we consider a supervisory control problem of a DES under an scLTL constraint.
We propose an on-line control scheme, where we leverage a ranking function that enables us to find desirable behavior with respect to the scLTL specification. 
The concept of ranking functions is like that of Lyapunov functions, which play a great role in determining control strategies.
The key idea is that, if the rank decreases along a trajectory, we regard it as good.
Ranking functions are useful in solving games played on a graph and reachability analysis of automata, which sometimes give solutions to LTL-related problems. 



We define a ranking function on the product automaton of the DES and the specification automaton so that its value decreases 

if an accepting state of the product automaton is being approached. 



To take the tradeoff between permissiveness of the supervisor and acceptance of the specification, 
we additionally introduce a permissiveness function that indicates a time-varying permissiveness level. 
If we have a higher permissive level, the supervisor may enable events that do not necessarily lead to  achievement of the specification. 
By referring to the permissiveness level together with the ranking function at each step of the on-line control process, the supervisor computes more permissive control patterns. 


This paper extends the on-line supervisory control scheme proposed in <cit.> to the setting of partial observation. 
After each observation, the supervisor dynamically computes its control action with the information of the fully observed product automaton, on which the ranking function is defined. 
Furthermore, we characterize the concepts of controllability and observability by means of the ranking function.
The supervisor forces the DES to satisfy the scLTL specification if the product automaton is controllable and observable.  



The rest of this paper is organized as follows. 
Section <ref> gives fundamental definitions and notations. 
Then, Section <ref> formulates a supervisory control problem for scLTL specifications. 
Section <ref> briefly explains the ranking function with its related properties.  
Section <ref> proposes our on-line control scheme, which is demonstrated in Section <ref> with a simple example.

Finally, Section <ref> concludes the paper. 




§ PRELIMINARIES





For a set T, we denote by |T| its cardinality. 
T^* (resp., T^ω) represents a set of finite (resp., infinite) sequences over T. 
For a finite or infinite sequence τ over T, 

let τ[j] be the (j+1)-st element of τ.

For any j,k ∈ℕ with j ≤ k, we denote by τ[j … k] the sequence τ[j]τ[j+1]…τ[k]. 

We write τ' ≼τ if τ' is a prefix of τ. 
For a finite sequence τ∈ T^*, τ stands for the length of τ. 




 §.§ Discrete Event Systems





























A discrete event system (DES) is a tuple 


    G=((X,Σ,δ,x_0), AP, L),
 
where 
X is the set of states, 
Σ is the set of events, 
a partial function δ: X ×Σ→ X is the transition function, 
x_0 ∈ X is the initial state, 

AP is the set of atomic propositions, and 
L: X → 2^AP is the labeling function.
G is said to be finite if X, Σ, and AP are all finite. 
We write δ(x,σ)! if a transition from x with σ is defined. 
For each x ∈ X, let Σ(x)={σ∈Σ: δ(x, σ)! }.

We denote by a triple (x,σ,x') a transition from x ∈ X to x' = δ(x,σ) for some σ∈Σ(x). 
Moreover, the transition function is extended to a sequence of inputs: for σ∈Σ and s ∈Σ^*, 
δ(x,ε) = x and δ(x,sσ)= δ( δ(x,s),σ).

Let ℒ(G) = { s ∈Σ^*: δ(x_0,s)! } be the set of all finite event sequences generated by G. 
An infinite sequence ρ∈ X(Σ X)^ω is called a run if, for any j ∈ℕ, ρ[2(j+1)] ∈δ(ρ[2j], ρ[2j+1]).
A finite sequence h ∈ X(Σ X)^* is called a history if h ∈ X or, for h with h≥ 3, h[2(j+1)] ∈δ (h[2j], h[2j+1]) for any j ∈{ 0, 1, …, h-3/2}. 

The set of runs (resp., histories) starting from the initial state x_0 is defined as 𝖱𝗎𝗇𝗌(G) (resp., 𝖧𝗂𝗌(G)).

DES G is said to be deadlock-free if, for any s ∈ℒ(G), there exists σ∈Σ such that δ(x_0,sσ)!. 

The event set is partitioned into disjoint subsets Σ = Σ_c ∪Σ_uc, where Σ_c (resp., Σ_uc) is the set of controllable (resp., uncontrollable) events.
We define Σ_c(x) = Σ(x) ∩Σ_c and Σ_uc(x) = Σ(x) ∩Σ_uc for each x ∈ X. 



We have another partition of the event set Σ = Σ_o ∪Σ_uo with the set Σ_o (resp., Σ_uo) of observable (resp., unobservable) events.
Let 𝒫: Σ^* →Σ_o^* be a natural projection defined inductively as follows:

    𝒫(ε) = ε, 
       ∀ s ∈Σ^*, ∀σ∈Σ,  𝒫(sσ ) = 
    𝒫(s) σ    if σ∈Σ_o, 
    𝒫(s)      if σ∈Σ_uo.

We also define the inverse 𝒫^-1: 2^Σ_o^*→ 2^Σ^* as 𝒫^-1 (T) = { s ∈Σ^*: t ∈ T, 𝒫(s) = t }. 
The observable behavior of the DES G is given by 𝒫(ℒ(G)) = { s = 𝒫(t) ∈Σ_o^*: t ∈ℒ(G) }.










For the set AP, a letter ν∈ 2^AP stands for a subset of atomic propositions.
A word is a finite or infinite string of letters. 

Each run in 𝖱𝗎𝗇𝗌(G) generates a sequence of letters, namely a word over 2^AP, obtained by the labeling function.
We extend the labeling function to express such words: for run ρ,
L(ρ)= L(ρ[0]) L(ρ[2]) ….
The extension for histories is defined similarly. 




 §.§ Syntactically Co-Safe Linear Temporal Logic


Linear temporal logic (LTL) is useful to describe qualitative control specifications. 
In this paper, we focus on syntactically co-safe LTL (scLTL), a subclass of LTL.

Formally, an scLTL formula φ over the set AP of atomic propositions is defined as

    φ ::= true |   a  |  a  | φ_1 φ_2  |  φ_1 φ_2  |  ◯φ |  φ_1 𝐔φ_2,
 
where a ∈ AP, φ, φ_1, φ_2 are scLTL formulas. 
In addition, we usually use a temporal operator , which is defined by 
φ := true𝐔φ.

The semantics of scLTL is defined over an infinite word <cit.>.
For an scLTL formula φ over AP and an infinite word w ∈ (2^AP)^ω, we write w φ if w satisfies φ. 
For a DES G and an scLTL formula φ, we say G satisfies φ, denoted by G φ, if L(ρ) φ for all ρ∈𝖱𝗎𝗇𝗌(G). 

Although scLTL formulas are evaluated over infinite words, it is known that we only need to check whether an input word has a good prefix of the formula. 
Any scLTL formula can be translated into a corresponding deterministic finite automaton (DFA), which is an acceptor for the good prefixes <cit.>.
For an scLTL formula φ, let A_φ = ((X_A, Σ_A, δ_A, x_A,0), F_A) be its corresponding DFA, where 
X_A is the set of states, 
Σ_A = 2^AP is the input alphabet, 
a total function δ_A: X_A ×Σ_A → X_A is the transition function, 
x_A,0∈ X_A is the initial state, and 

F_A ⊆ X_A is the set of accepting states. 
For any w ∈ (2^AP)^ω, we have 

    w φ∃ w' ∈ (2^AP)^*, w' ≼ w δ_A(x_A,0,w') ∈ F_A.





§ FORMULATION


In this paper, we formulate a supervisory control problem with scLTL specifications. 
A controller, called a supervisor, enables some controllable events at each state <cit.>. 

For each state x ∈ X, we define Γ(x) = {γ⊆Σ(x): Σ_uc (x) ⊆γ}, 



where 
γ∈Γ (x) is called a control pattern at x. 
Let Γ=⋃_x ∈ XΓ(x) be the set of all control patterns. 

The supervisor determines a control pattern after each observation. 
Formally, we define a supervisor under partial observation 𝒫 as a mapping 𝒮: 𝒫 (ℒ(G)) →Γ.




	Let 𝒮 be a supervisor under partial observation 𝒫 for a DES G = ((X, Σ, δ, x_0), AP, L). 
	The closed-loop behavior of the DES G under the control by 𝒮, denoted by 𝒮/G, is given by 
	
    ε∈ℒ(𝒮/G),  and 
       ∀ s ∈ℒ(𝒮/G), sσ∈ℒ(𝒮/G)
                        s σ∈ℒ(G)  σ∈𝒮(𝒫(s)).  
       𝖱𝗎𝗇𝗌(𝒮/G) = { x_0 σ_1 x_1 …∈𝖱𝗎𝗇𝗌(G): σ_1 ∈𝒮(ε) 
                       ∀ j ≥ 1, σ_j+1∈𝒮(𝒫(σ_1 σ_2 …σ_j)) }.























	
	Given a finite deadlock-free DES G=((X,Σ,δ, x_0), AP, L) and an scLTL formula φ over AP, 
	synthesize a supervisor 𝒮 under partial observation 𝒫 such that 𝒮/G φ.



To solve Problem <ref>, we design an on-line supervisor, which dynamically computes a control pattern after observing an event occurrence. 
Our control scheme is divided into two stages; we first execute the preprocessing off-line, and then move on to the on-line control stage, where it stops controlling the DES after detecting a history corresponding to a good prefix of the scLTL specification.





§ RANKING FUNCTION







The specification given by an scLTL formula φ is translated into the equivalent DFA A_φ. 
Then, we obtain the product automaton P of the DES G and the DFA A_φ, which is computed as follows. 

    P = G ⊗ A_φ = ((X_P,Σ_P,δ_P,x_P,0),F_P),

where 

X_P = X × X_A is the set of states, 
Σ_P = Σ is the set of events, 
δ_P:X_P ×Σ_P → X_P is the transition function, 
x_P,0 = (x_0,δ_A(x_A,0,L(x_0))) is the initial state, and 
F_P = X × F_A is the set of accepting states. 
For each x = (x_G,x_A) ∈ X_P and σ∈Σ_P, 
δ_P(x,σ) = (δ(x_G,σ), δ_A(x_A, L(δ(x_G,σ)))) and we define J_G(x) = x_G and J_A(x) = x_A.

The two kinds of event partitions are inherited from the DES: Σ_P,c=Σ_c, Σ_P,uc = Σ_uc, Σ_P,o = Σ_o, and Σ_P,uo = Σ_uo.
Note that ℒ(P) = ℒ(G) and 𝒫(ℒ(P)) = 𝒫(ℒ(G)). 

Since the product automaton captures the behavior of the DES and the DFA at the same time, our goal turns out to reach an accepting state of the product automaton. 
For that purpose, we introduce a ranking function with the existence of uncontrollable transitions <cit.>, which decreases its value if an accepting state is being approached.


	
	Let P=((X_P,Σ_P,δ_P,x_P,0),F_P) be a product automaton. 
	A function ξ: X_P →ℕ is a ranking function for P if 
	
    ∀ x ∈ X_P,   ∀σ∈Σ_P,uc(x),
       ξ(x) ≥min{ξ(δ_P(x,σ)) + I̅_F_P(x), α},

	where α > |X_P|-|F_P| and I̅_F_P: X_P →{0,1} is an indicator function such that I̅_F_P(x) = 1 if and only if x ∉ F_P.  


































In <cit.>, 
we propose an algorithm to compute a ranking function for the product automaton.

Here, we show important results related to the ranking function ξ with the upper bound α = |X_P| - |F_P| + 1.




	For any x ∈ X_P, x ∈ F_P if and only if ξ(x) = 0. 















	
	For any x ∈ X_P, 
	
    ξ(x) < α∃ s ∈Σ_P^*, δ_P(x,s) ∈ F_P.







	
	For any x ∈ X_P, 
	
    0 < ξ(x)     <α
       {σ∈Σ_P(x): ξ(x) > ξ(δ_P(x,σ)) }≠∅.






















	
	For any x ∈ X_P ∖ F_P, 
	
    Σ_P,uc(x) ⊆{σ∈Σ_P(x): ξ(x) > ξ(δ_P(x,σ)) }.


Proposition <ref> ensures that a lower-ranked successor always exists. 
Moreover, as mentioned in Proposition <ref>, each successor associated with an uncontrollable event has a lower rank than that of the current state. 





In general, the existence of supervisors under partial observation depends on the controllability and observability of the specification language. 
Although these properties are defined by means of languages in the conventional supervisory control theory <cit.>, here we characterize them with the ranking function.

	The product automaton P is said to be controllable (with respect to ξ) if ξ(x_P,0) < α. 
	


	The product automaton P is said to be observable (with respect to ξ and 𝒫) if 
	
    ∀ s, s' ∈ℒ(P),  ∀   σ∈Σ_P, 
    𝒫(s) = 𝒫(s')    ξ(δ_P(x_P,0, s)) > ξ(δ_P(x_P,0,sσ)) 
        s'σ∈ℒ(P) 
       ξ(δ_P(x_P,0, s')) > ξ(δ_P(x_P,0,s'σ)).



If the context is clear, we just say P is controllable or observable without referring to ξ and 𝒫.
The observability condition requires that, if an event is defined after different sequences with the same observation, then all of the transitions triggered by the event agree with each other in a sense of whether the product automaton gets closer to accepting states or not. 






We characterize transitions of the product automaton with respect to the ranking function. 
Let (x,σ,x') ∈ X_P ×Σ_P × X_P be a transition defined in the product automaton.

	
  * (x,σ,x') is legal (with respect to ξ) if ξ(x) > ξ(x'). 
	
  * (x,σ,x') is neutral (with respect to ξ) if ξ(x) ≤ξ(x') < α. 
	
  * (x,σ,x') is illegal (with respect to ξ) if ξ(x') = α. 


It is possible to lead the product automaton to reach an accepting state 
if we always choose legal transitions. 
On the other hand, however, 


we are likely to obtain more permissive supervisors if we allow not only legal transitions but also neutral ones to be enabled. 
Permissiveness is one of the most important concepts in the supervisory control theory, where 
we often aim to design a supervisor that enables as many events as possible. 




§ ON-LINE SUPERVISORY CONTROL UNDER PARTIAL OBSERVATION


In this section, we explain the on-line supervisory control scheme for Problem <ref>, given the product automaton P and the ranking function ξ. 
Notice that we have a tradeoff between permissiveness of the supervisor and achievement of the specification. 
The supervisor becomes more permissive if it enables events triggering neutral transitions. 
However, infinitely many occurrences of neutral transitions results in livelock, i.e., the product automaton may stay within states x with 0 < ξ(x) < α while it always holds the possibility of reaching an accepting state but actually suspends going there.  







To take the tradeoff into consideration, we introduce a criterion for how many neutral transitions we allow to be enabled.
More precisely, the supervisor we design determines its control action on-line, being aware of 

a time-varying permissiveness level, 

which is referred to together with the ranking function to improve permissiveness of supervisors. 
Here, we introduce a function that quantifies a permissiveness level. 



	
	A permissiveness function is a function η:ℕ→ℝ that satisfies the following three conditions. 
	
		
  * η(0) ≤α;
		
  * η(k) ≥η(k+1) for any k ∈ℕ;
		
  * η(k̅) = 0 for some k̅∈ℕ. 
	

That is, the permissiveness level decreases as time goes by and will eventually be exhausted. 



With partially observed information, 
the supervisor cannot know which state the product automaton is currently in. 
We define the unobservable reach <cit.> from a state x ∈ X_P under an event subset Σ' ⊆Σ_P as follows. 

    𝖴𝖱_Σ'(x) =   { x' ∈ X_P: u ∈ (Σ_uo∩Σ')^*, x' = δ_P(x,u) }.

For a subset X' ⊆ X_P, let 𝖴𝖱_Σ'(X') = ⋃_x ∈ X'𝖴𝖱_Σ'(x). 

The set of next states after each observation is defined recursively as follows: for s_o ∈𝒫(ℒ(P)) and σ_o ∈Σ_o,

    𝖭𝖲(ε)    = { x_P,0}, 
    𝖭𝖲(s_o σ_o)    = { x' = δ_P(x,σ_o) ∈ X_P: x ∈𝖴𝖱_Σ_P(𝖭𝖲(s_o)) }.



The key idea of our on-line control scheme is made up of the following two rules.
First, we always enable events that trigger legal transitions no matter which state the DES is in or how much the permissiveness level currently is. 
Second, it is possible to allow neutral transitions if we have enough permissiveness level. 
These concepts are realized by two different control actions given by, for each x ∈ X_P and k ∈ℕ, 

    γ̂_leg(x)
    =   {σ∈Σ_P: ∃ s ∈Σ_uo^*, δ_P(x,s)! δ_P(x,sσ)! 
                     ξ(δ_P(x,s)) > ξ(δ_P(x,sσ)) }, 
    γ̂_per(x,k) =   {σ∈Σ_P: ∀ s ∈Σ_uo^*, 
               δ_P(x,sσ)! ξ (δ_P(x,sσ)) < η(k) }.

Applying γ̂_leg(x) results in occurrences of only legal transitions within 𝖴𝖱_Σ_P (x)  

while the supervisor enables events in γ̂_per(x), 

which may trigger neutral transitions, if the permissiveness level is high. 
The supervisor refers to the permissiveness function to see whether such additional events are acceptable currently or not.

From Proposition <ref>, we have the following proposition. 


	
	If the product automaton is controllable, then for any x ∈ X_P ∖ F_P, we have γ̂_leg(x) ≠∅. 



	Assume that the product automaton is controllable and observable. 
	Then, for any x ∈ X_P ∖ F_P, we have 
	
    ∀σ∈γ̂_leg(x), ∀ s ∈Σ_uo^*, 
        δ_P(x,s)! δ_P(x,sσ)! ξ(δ_P(x,s)) > ξ(δ_P(x,sσ)).




	Let x ∈ X_P ∖ F_P.
	From Proposition <ref>, then, γ̂_leg(x) ≠∅. 
	Suppose that, for some σ∈γ̂_leg(x), we have 
	
    ∃ s ∈Σ_uo^*,    δ_P(x,s)! δ_P(x,sσ)! 
       ξ(δ_P(x,s)) ≤ξ(δ_P(x,sσ)).

	From the definition of γ̂_leg(x), the event σ satisfies 
	
    ∃ s' ∈Σ_uo^*,    δ_P(x,s')! δ_P(x,s'σ)! 
       ξ(δ_P(x,s)) > ξ(δ_P(x,sσ)).

	Let t_x ∈ℒ(P) such that δ_P(x_P,0,t_x). 
	Then, we have 𝒫(ℒ(t_xs)) = 𝒫(ℒ(t_xs')) but for the event σ both Eqs. (<ref>) and (<ref>) hold, which contradicts the assumption that the product automaton is observable. 



In the on-line control scheme, the supervisor keeps the set 𝖭𝖲(s_o) of states where the product automaton is estimated to be from the observation s_o ∈𝒫(ℒ(P)). 
After observing an observable event σ_o ∈Σ_o, the supervisor updates the set to 𝖭𝖲(s_o σ_o) and computes a control pattern to be applied for the control of 𝖴𝖱_Σ(𝖭𝖲(s_oσ_o)). 



Then, based on the idea mentioned above, the supervisor 𝒮̂ computes a control pattern satisfying, for each s_o ∈𝒫(ℒ(P)), 

    𝒮̂(s_o) = γ̂_leg(𝖭𝖲(s_o)) ∪γ̂_per(𝖭𝖲(s_o),s_o),

where 

    γ̂_leg(𝖭𝖲(s_o)) = ⋃_x ∈𝖭𝖲(s_o)γ̂_leg(x),  
    γ̂_per(𝖭𝖲(s_o)) = ⋂_x ∈𝖭𝖲(s_o)γ̂_per(x).



















 













































	



From Proposition <ref>, we have the following proposition. 

	
	If the product automaton is controllable, then for any s_o ∈𝒫(ℒ(P)), γ̂_leg(𝖭𝖲(s_o)) ≠∅. 




	
	Assume that the product automaton is controllable and observable. 
	Then, for any s_o ∈𝒫(ℒ(P)) and any x ∈𝖭𝖲(s_o), 
	
    ∀ x' ∈𝖴𝖱_Σ_P (x), 
    	∀σ∈γ̂_leg(𝖭𝖲(s_o)) ∖γ̂_leg(x), 
    	δ_P(x',σ)!.




	We prove the proposition by contradiction. 
	Let s_o ∈𝒫(ℒ(P)). 
	By the controllability of P and Proposition <ref>, we have γ̂_leg(𝖭𝖲(s_o)) ≠∅. 
	Suppose that, for some x' ∈𝖴𝖱_Σ_P(x), there exists σ∈γ̂_leg(𝖭𝖲(s_o)) ∖γ̂_leg(x) with δ_P(x',σ)!.
	This means that for some y ∈𝖭𝖲(s_o) with y ≠ x, we have σ∈γ̂_leg(y) and δ_P(x', σ)!. 
	Equivalently, both of the following conditions hold for some σ:
	
    1)    ∃ t_x ∈𝒫^-1(s_o), x = δ_P(x_P,0,t_x) ∃ u ∈Σ_uo^*, δ_P(x,uσ)!.
    
    	2)     ∃ t_y ∈𝒫^-1(s_o), y = δ_P(x_P,0,t_y) ∃ s_y ∈Σ_uo^*, δ_P(y,s_y)! 
       δ_P(y,s_yσ)! ξ(δ_P(y,s_y)) > ξ (δ_P(y,s_y σ)).

	In the above conditions, we have 𝒫(t_xu) = 𝒫(t_x) ε = s_o and 𝒫(t_yy_s) = 𝒫(t_y) ε = s_o.
	To sum up, we have 
	
    ∃ t_x', t_y'    ∈ℒ(P), 𝒫 (t_x') = 𝒫(t_y')  t_y'σ∈ℒ(P)  
       ξ (δ_P(y,t_y')) > ξ(δ_P(y,t_y'σ))  t_x' σ∈ℒ(P).

	On the other hand, however, it holds that ξ(δ_P(x,t_x')) ≤ξ(δ_P(x,t_x'σ)) because σ∉γ̂_leg(x).
	We now have the contradiction to the observability condition of the product automaton.
	
	
	

From Proposition <ref>, we have the following lemma.

	If the product automaton is controllable and observable, we have, 
	for any s_o ∈𝒫(ℒ(P)),  
	
    ∀ x ∈𝖭𝖲(s_o),  𝖴𝖱_γ̂_leg(𝖭𝖲(s_o))(x) = 𝖴𝖱_γ̂_leg(x)(x).





































	If the product automaton is observable, 
	then for any s_o ∈𝒫(ℒ(P)),  
	
    ∀ x ∈𝖭𝖲(s_o),  max_ x' ∈𝖴𝖱_γ̂_leg(𝖭𝖲(s_o))(x)ξ(x') < ξ(x).








 §.§ On-line Control Algorithm




  §.§.§ Main part.

The on-line supervisory control scheme is described in Algorithm <ref>.
The supervisor keeps the sets NS of next states after the observation so far, which is initialized with { x_P,0}. 
At each step k, the on-line supervisor computes a control pattern γ_k that will be applied to NS, the corresponding unobservable reach UR, and the set NS' of new next states after potential occurrences of observable events. 

The functions LegExpand and ReExpand compute γ̂_leg(NS) and γ̂_per(NS), respectively (but for now we skip the detailed explanations).
After computed, the control pattern γ_k is issued to the DES G, which executes one of the enabled events.


The new observation is represented by the function 𝗈𝖻𝗌𝖾𝗋𝗏𝖾(G, γ_k), according to which  


the supervisor updates information related to the memory NS and time step k and goes on to determine the next control action. 









  §.§.§ Subfunctions.

In the main part of Algorithm <ref>, we first compute γ̂_leg(NS) by the function LegExpand. 
Then, by the function ReExpand, we additionally examine if other controllable events can be added to the next control pattern. 
The functions LegExpand and ReExpand expands states in NS in a depth-first-search mannar until an observable event is detected.

The function LegExpand expands an input state x ∈ X_P and updates γ, γ̅, UR, and NS' if necessary.
When a legal transition with an event σ is detected during the search, the event is added to γ.
After the call of LegExpand in Algorithm <ref>, we have γ̂_leg(NS) and the unobservable reach of NS under the control pattern γ̂_leg(NS). 
We move on to the other function ReExpand, 

which examines each controllable event σ_c that has not been in γ̂_leg(NS).
Unlike LegExpand, we have a global boolean variable 𝚜𝚝, initialized with false. 

It is necessary to examine all states that may be visited if σ_c, the currently examined controllable event, is added to γ_k.
If we find the event σ_c cannot be in γ̂_per(NS), then the variable 𝚜𝚝 turns to be true.







































	













































 §.§ Correctness of Algorithm <ref>

The on-line supervisor refers to the current rank ξ(x) and the current permissiveness level η(k) to take into consideration the tradeoff between permissiveness and acceptance of the specification. 
More precisely, the more permissiveness level we have, the more neutral transitions we allow to be enabled. 
Since the permissiveness level decreases with the elapse of time, the supervisor enables less events as time goes by. 
In the following, we show the correctness of Algorithm <ref>.



	If the product automaton is controllable, then 
	for any s_o ∈𝒫(ℒ(P)), 
	𝒮̂(s_o) ≠∅. 




	By Eq. (<ref>), for any s_o ∈𝒫(ℒ(P)), we have 𝒮̂(s_o) ⊇γ̂_leg(𝖭𝖲(s_o)), which is always nonempty as mentioned in Proposition <ref>.
	
	
	
	
	
	
	




	For any s_o ∈𝒫(ℒ(P)) and any x ∈𝖴𝖱_Σ(𝖭𝖲(s_o)),  
	we have 𝒮̂(s_o) ∈Γ(J_G(x)).



	From Proposition <ref>, for any x ∈ X_P, γ̂_leg(x) ∈Γ(J_G(x)).
	Then, by Eq. (<ref>) and the definition of γ̂_leg(𝖭𝖲(s_o)), the lemma holds.


















	
	Assume that the product automaton P is observable. 
	For any x ∈ X_P with 0 < ξ(x) < α, there exists k ∈ℕ such that, for any l ≥ k,  
	γ̂_per(x,l) = ∅.





	Note that, for each x ∈ X_P and k ∈ℕ,
	
    γ̂_per(x,k) = ⋂_x' ∈𝖴𝖱_Σ(x){σ∈Σ_P(x'): ξ(δ_P(x',σ)) < η(k) }.

	By the second and third conditions of Definition <ref>, on the other hand, there exists k̅∈ℕ such that, for all l̅≥k̅, η(l̅)=0.	
	
	
	
	Since the ranking function ξ returns nonnegative values, {σ∈Σ_P: ξ(δ_P(x,σ)) < 0 } = ∅ for any x ∈ X_P.
	That is, we have γ̂_per(x,l̅) = ⋂_x' ∈𝖴𝖱_Σ(x)∅ = ∅ for all l̅≥k̅.





	
	Assume that the product automaton P is observable. 
	In the while loop of Algorithm <ref>, 
	
	neutral transitions of the product automaton occur only finitely often.




	We prove the lemma by contradiction. 
	Suppose that neutral transitions occur infinitely often.
	That is, there exists s ∈Σ^ω such that 
	
    [                                    ∀ k ∈ℕ, ∃ l ≥ k,; ξ(δ_P(x_P,0, s[0… l])) ≤ξ( δ_P(x_P,0, s[0… l+1]) ). ]

	Let σ_l+1:=s[l+1] for some l∈ℕ that satisfies the above inequality, x_l+1:= δ_P(x_P,0,s[0… l]), and t_l := 𝒫(s[0… l]). 
	Then, we have 
	
    σ_l+1∈𝒮̂(t_l) = γ̂_leg(𝖭𝖲(t_l)) ∪γ̂_per(𝖭𝖲(t_l),t_l).

	Since transition (x_l, σ_l+1, x_l+1) is neutral, it holds that 
	
    σ_l+1∈γ̂_per(𝖭𝖲(t_l),t_l).



	By Eq. (<ref>), therefore, there exist infinitely many l ∈ℕ satisfying Eq. (<ref>), which contradicts Proposition <ref>.





	
	Assume that P is controllable and observable. 
	In Algorithm <ref>, 
	an accepting state of the product automaton is eventually reached 
	under the control by the on-line supervisor 𝒮̂.
	
	
	
	
	




	Recall that η(0) ≤α and that e is nonincreasing, as mentioned in Definition <ref>.
	By the controllability of P, we have ξ(x_P,0) < α. 
	Since the on-line supervisor 𝒮̂ never allows illegal transitions, 
	we have, for any s ∈ℒ(𝒮̂/G), ξ(δ_P(x_P,0,s)) < α. 
	By Proposition <ref>, then, it is always possible to lead the product automaton to an accepting state by some appropriate event sequence.
	From Lemma <ref>, while the on-line computation is running, the supervisor 𝒮̂ observes neutral transitions only finitely often. 
	Let k̅∈ℕ be the step index such that η(k̅) = 0. 
	Then, for any observation s_o ∈𝒫(ℒ(P)) with s_o>k̅, we have 

	𝒮̂(s_o) = γ̂_leg(𝖭𝖲(s_o)).
	In other words, the supervisor 𝒮̂ chooses only legal transitions after time step k̅. 
	Since the rank always decreases during each legal transition, eventually a state ranked as 0, namely, an accepting state is reached. 





	𝒮̂/G φ if P is controllable and observable. 




	From Lemma <ref>, the on-line supervisor forces the plant DES G to generate event sequences with which the product automaton eventually reaches an accepting state. 
	Note that, when an accepting state of the product automaton is reached, then the corresponding word is accepted by the DFA A_φ. 
	By Eq. (<ref>), any run that has the corresponding history as a prefix satisfies the scLTL formula φ.





















































§ ILLUSTRATIVE EXAMPLE


In this section, we demonstrate the proposed method with a simple example. 
Consider a DES G_ex depicted in the left of Fig. <ref>, where X = {x_0, x_1, x_2, x_3, x_4 }; Σ_o = {o_1,o_2,o_3} and Σ_uo={u_1,u_2,u_3,u_4}; AP = {a,b,c}; L(x_0)=L(x_4)=∅, L(x_1)={a}, L(x_2)={b}, and L(x_3) = {c}. 
We assume that all events are controllable and the initial state is x_0.
For the DES G_ex, we impose an scLTL formula 
φ_ex =  a  a 𝐔 b  a 𝐔 c 
as a control specification. 
φ_ex requires to eventually go to a state labeled with a after visiting both b-states and c-states.
We use a tool Spot[https://spot.lrde.epita.fr/] to translate φ_ex into a DFA, which is shown in the right of Fig. <ref>. 

Let η(k) = max{ -k+5, 0 }. 
Then, at the initial step of the on-line control scheme, the unobservable reach from NS = {x_P,0 = (x_0,y_0)} is computed as shown in Fig. <ref>.
After the call of LegExpand, we have UR ={ (x_0,y_0), (x_2,y_3) }, NS' = { (x_3,y_2) }, and γ_0 = γ̂_leg((x_0,y_0)) = {u_2,o_2}. 
Since the current permissiveness level is η(0) = 5, the function ReExpand adds u_3, o_1, o_3 to γ_0. 
The sets UR and NS' are also updated with the related states. 
We do not expand the state (x_1,y_5) any more because its rank hits the upper bound.

Assume that 𝗈𝖻𝗌𝖾𝗋𝗏𝖾(G_ex,γ_0) = o_1, according to which the supervisor updates NS to {(x_0,y_0), (x_4,y_0)} and ends up obtaining γ_1 = γ_0 after the computation at the next step.
Then, assume that the event o_1 is observed again, i.e., 𝗈𝖻𝗌𝖾𝗋𝗏𝖾(G_ex,γ_1) = o_1.
Although we start from the same set NS = {(x_0,y_0), (x_4,y_0)} as the previous step, we have a different result.
Since η(2) = 3, the function ReExpand does not add to the current control pattern γ_2 events triggering neutral transitions to states ranked as 3. 
At the end of the computation for k=2, we have γ_2 = {u_2,o_2} and NS' = {(x_3,y_2)}. 



Similarly, after observing o_2 = 𝗈𝖻𝗌𝖾𝗋𝗏𝖾(G_ex,γ_2), only legal transitions are enabled because all states reachable from (x_3,y_2) have a rank lower than η(3) = 2. 
At the end of the computation at step 3, we have NS' ⊆ F_P.
No matter which event is observed, then, the supervisor stops the control. 
 









§ CONCLUSION


We propose a novel on-line supervisory control scheme of partially observed DESs to achieve a control specification given by scLTL formulas. 
We introduce the controllability and observability based on the ranking function, which derives a sufficient condition for the existence of the on-line supervisor. 
In the on-line computation, the supervisor computes the unobservable reach after each observation and refers to the ranking function together with the permissiveness function.  
Depending on the permissiveness level at each step, the supervisor improves its permissiveness if possible. 
It is future work to extend the proposed scheme to cases of general or quantitative LTL and to establish a verification method of the observability.





             
                                                     
                                                   


































§ COMPUTATION OF RANKING FUNCTION
    

Here, we briefly explain the results in <cit.>, where we propose an algorithm to compute a ranking function given the product automaton P of the DES and the DFA.

We obtain a ranking function by Algorithm <ref>.






As initialization, we set ξ(x) = 0 for each x ∈ X_P and α = |X_P|-|F_P|+1. 
Then, we go on to update the values of ξ by using functions ξ̂: X_P →ℕ 
and 𝗎𝗉_α : ℕ× X_P →ℕ, defined as follows.
For each x ∈ X_P, 

    ξ̂(x) =
    min_σ∈Σ_P,cξ( δ_P(x,σ) )    if Σ_P,uc(x) = ∅, 
    max_σ∈Σ_P,ucξ(δ_P(x,σ))    otherwise.


For any r ∈ℕ and x ∈ X_P, 

    𝗎𝗉_α (r, x) 
    = 
    
    r+1     if  x ∉ F_P  r < α ,  
    
    r     otherwise.


To sum up, the current rank is incremented if the current state is not accepting with at least one uncontrollable event defined and the rank has not hit the upper bound;
otherwise the rank does not change.


