1

Supervisor Localization of Discrete-Event
Systems with Infinite Behavior
(October 25, 2017)

arXiv:1710.08751v1 [] 24 Oct 2017

Renyuan Zhang1 , Kai Cai2

Abstract
Recently we developed supervisor localization, a top-down approach to distributed control of discreteevent systems (DES) with finite behavior. Its essence is the allocation of monolithic (global) control action
among the local control strategies of individual agents. In this report, we extend supervisor localization
to study the distributed control of DES with infinite behavior. Specifically, we first employ Thistle and
Wonham’s supervisory control theory for DES with infinite behavior to compute a safety supervisor (for
safety specifications) and a liveness supervisor (for liveness specifications), and then design a suitable
localization procedure to decompose the safety supervisor into a set of safety local controllers, one for
each controllable event, and decompose the liveness supervisor into a set of liveness local controllers,
two for each controllable event. The localization procedure for decomposing the liveness supervisor is
novel; in particular, a local controller is responsible for disabling the corresponding controllable event
on only part of the states of the liveness supervisor, and consequently, the derived local controller in
general has states number no more than that computed by considering the disablement on all the states.
Moreover, we prove that the derived local controllers achieve the same controlled behavior with the
safety and liveness supervisors. We finally illustrate the result by a Small Factory example.
Keywords
Discrete-Event Systems, Supervisory Control, Infinite Behavior, Supervisor Localization
1

R.

Zhang

is

with

School

of

Automation,

Northwestern

Polytechnical

University,

China.

Email:

ryzhang@nwpu.edu.cn.
2

K. Cai is with Department of Electrical and Information Engineering, Osaka City University, Japan. Email:

kai.cai@eng.osaka-cu.ac.jp.

2

I.

I NTRODUCTION

In [1–6] we developed a top-down approach, called supervisor localization, to the distributed control
of multi-agent discrete-event systems (DES). This approach first synthesizes a monolithic supervisor (or
a heterarchical array of modular supervisors), and then decomposes the supervisor into a set of local
controllers for the component agents. Localization creates a purely distributed control architecture in
which each agent is controlled by its own local controller; this is particularly suitable for applications
consisting of many autonomous components, e.g. multi-robot systems. Moreover, localization can significantly improve the comprehensibility of control logic, because the resulting local controllers typically
have many fewer states than their parent supervisor.
These works focus on DES with finite behaviors [7], in which DES are modelled as generators accepting
∗-languages (consisting of finite-length strings) and the specifications are expressed by ∗-languages. In

modelling and control of reactive systems (e.g. automated factories, operating systems, communication
protocols), however, the systems may operate indefinitely, and the specifications may require that every
system component must operate infinitely often. In these cases, ω -automata on infinite inputs and ω languages consisting of infinite-length strings were introduced to model the DES with infinite behavior
and specify the specifications respectively. Notable works on synthesizing supervisors for the DES with
infinite behavior include the following. First, Ramadge [8] models the DES with infinite behavior by
Büchi automata and derives conditions (∗-controllability and ω -closure) for the existences of supervisors;
within the same framework, Young et al. [9] derives another supervisor existence condition (replacing
ω -closure by finite stabilizability) under less restrictive conditions. Then, Thistle and Wonham [10–

12] introduce the concept of ω -controllability which is closed under arbitrary set union, and develop a
procedure to synthesize supervisors satisfying given specifications expressed by ω -languages; Kumar et
al. [13] proposed an alternative algorithm to compute the supremal ω -controllable sublanguage. Later,
Thistle [14] extend the result in [10] to a more general case where the plant DES are modelled by
deterministic Rabin-automata. More recently, Thistle and Lamouchi [15] addressed the issue of partial
observation in the supervisory control of DES with infinite behavior. To the best of our knowledge,
however, there is no result on distributed control for multi-agent DES with infinite behavior reported in
the literature.
In this paper, we extend supervisor localization to address distributed control for DES with infinite
behavior. Our approach is as follows. Given a DES plant with infinite behavior and safety and liveness
specifications, we first synthesize a safety supervisor (for safety specifications) and a liveness supervisor

3

(for liveness specifications) by the method proposed by Thistle and Wonham [10, 12]. The infinite controlled behavior of the plant is restricted through the control actions on finite strings, thus as in DES with
finite behavior [7], we implement the supervisors by ∗-automata. We then adopt the localization procedure
in [1] with suitable modifications to decompose the automata-based safety and liveness supervisors into
local controllers for individual controllable events. Moreover we prove that the derived local controllers
are control equivalent to the synthesized safety and liveness supervisors.
The contributions of this paper are twofold. First, we develop a new supervisor localization theory for
DES with infinite behavior in Thistle and Wonham’s supervisory control framework [12], which supplies
a systematic, computationally effective approach to distributed control of multi-agent DES with infinite
behavior. In particular, we first decompose the safety supervisor into a set of local controllers, one for
each controllable event, by the localization procedure in [1]; then we decompose the liveness supervisor
into a set of local controllers, however, two for each controllable events, by a newly developed localization
procedure. The central idea of the new procedure is the new definition of disabling function with a new
language: only the disablement on part of the states are defined, i.e. an event is defined as disabled at one
state only if the state can be visited by strings in the given language. With this new disabling function,
we define new concepts of control consistency and control cover, and the resultant local controllers in
general have states number no more than that computed by the localization procedure in [1] where the
disablement on all the states are considered.
Second, we identify the essence of localization procedure for DES with infinite behavior: only the
disabling/enabling actions on finite strings need be considered. Namely, if the control equivalence of the
local controllers with their parent supervisors on finite behavior is guaranteed, the control equivalence
on infinite behavior can be derived by Lemma 1 in Section IV-C, which declares that the operator limit
(mapping finite strings to infinite strings whose prefixes are all contained in the given finite strings)
will not change the language equivalence on intersections. Consequently, control consistency relation and
control cover, the central concepts of the localization procedure, are defined only on the disabling and
enabling functions, irrelevant to the infinite behaviors. We demonstrate the above result by a case study
of Small Factory example [10].
Our proposed localization procedure can in principle be used to construct local controllers from
supervisors computed by any other synthesis method for DES with infinite behavior e.g. [8, 9, 14].
In this paper, we adopt the Thistle and Wonham’s supervisory control theory for two reasons. First,
it extends basic results of the supervisory control theory of Ramadge and Wonham [7, 16] for DES
with finite behavior to infinite behavior, and generalizes results of [8] to the case in which specification

4

languages need not be ω -closed relative to plant behavior. Second, the supervisors synthesized by Thistle
and Wonham’s theory can be implemented by ∗-automata, which are eligible to be decomposed into local
controllers by our previous work on supervisor localization procedure with appropriate modifications.
The paper is organized as follows. Section II reviews the preliminaries on DES with infinite behavior
and Thistle and Wonham’s supervisory control theory. Section III formulates the problem of Supervisor
Localization for DES with infinite behavior. Section IV presents the localization procedure and proves
the control equivalence of the derived local controllers with their parent supervisors, and Section V
illustrates the proposed localization procedure by a Small Factory example. Finally Section VI states our
conclusions.
II.

P RELIMINARIES

ON

DES

WITH I NFINITE

B EHAVIOR

In this section, we briefly review Thistle and Wonham’s supervisory control framework of discrete-event
systems (DES) with infinite behavior [10–12].
A. Discrete-Event Systems with Infinite Behavior
A discrete-event system (DES) with infinite behavior (plant to be controlled) is modeled as a deterministic Büchi automaton1
G := (Q, Σ, δ, q0 , BQ ),

(1)

where Q is the finite state set, q0 is the initial state, Σ is the finite event set (alphabet), δ : Q × Σ → Q
is the (partial) state transition function, and BQ ⊆ Q is the Büchi acceptance criterion. In the usual way,
δ is extended to δ : Q × Σ∗ → Q, and we write δ(q, s)! to mean that δ(q, s) is defined. Let Σ∗ be the

set of all finite strings over Σ, including the empty string ǫ, and Σω the set of all infinite strings over
˙ ω . The DES G has both finite
Σ; the disjoint union of Σ∗ and Σω is denoted by Σ∞ , i.e. Σ∞ = Σ∗ ∪Σ

behavior and infinite behavior. The finite behavior of G is the ∗-language L(G) ⊆ Σ∗ accepted by the
∗-automaton (Q, Σ, δ, q0 ), i.e.
L(G) := {s ∈ Σ∗ |δ(q, s)! & δ(q, s) ∈ Q};
1

The DES with infinite behavior can also be modeled by other form of ω-automata with different types of acceptance criteria,

e.g. Muller automata, Rabin automata, Street automata. It is known [17] that deterministic Büchi automata represent a strict subset
of ω-regular languages, having less expressive power than nondeterministic Büchi automata, deterministic and nondeterministic
Muller automata, and deterministic and nondeterministic Rabin automata which represent the full set of ω-regular languages. In
this report, following Thistle and Wonham’s framework [18], we focus on the subset of ω-regular languages that are represented
by deterministic Büchi automata, and leave the extension to the full set for future work.

5

and the infinite behavior of G is the ω -language S(G) accepted by the ω -automaton G with Büchi
acceptance criterion BQ , i.e.
S(G) := {s ∈ Σω |Ω(s) ∩ BQ 6= ∅}

where Ω(s) is set of states that s visits infinitely often.
A string s ∈ Σ∗ is a prefix of a string v ∈ Σ∞ , written s ≤ v , if there exists t ∈ Σ∞ such that v = st.
The (prefix) ∗-closure of a language K ⊆ Σ∞ is defined by
pre(K) := {s ∈ Σ∗ |(∃s1 ∈ K) s ≤ s1 }

(2)

If K = pre(K), we say that K is ∗-closed. In this report, we assume that (i) pre(L(G)) = L(G), i.e.
L(G) is ∗-closed, and (ii) pre(S(G)) = L(G), i.e. G is deadlock-free. Define the limit of a ∗-language
K by
lim(K) := pre−1 (K) ∩ Σω

(3)

where pre−1 (K) := {v ∈ Σ∞ |pre(v) ⊆ K}; then the ω -closure of an ω -language R is given by
clo(R) := lim(pre(R)) = pre−1 (pre(R)) ∩ Σω .

(4)

If R = clo(R), we say that R is ω -closed; if R = clo(R) ∩ S , we say that R is ω -closed with respect
to S . Note that S(G) represents a liveness assumption in the modelling of G, and in general S(G) ⊆
lim(L(G)); so S(G) itself need not be ω -closed.

B. Supervisory Control for DES with Infinite Behavior
For supervisory control, the event set Σ is partitioned into Σc , the subset of controllable events that
can be disabled by an external supervisor, and Σuc , is the subset of uncontrollable events that cannot be
prevented from occurring (i.e. Σ = Σc ∪˙ Σuc ). A supervisory control for G is any map f : L(G) → Γ,
where Γ := {γ ⊆ Σ|γ ⊇ Σu }. Then the finite and infinite closed-loop behaviors of the controlled DES
Gf , representing the action of the supervisor f on G, are respectively given by

(a) L(Gf ), the ∗-language synthesized by f , is defined by the following recursion:
(i) ǫ ∈ L(Gf ),
(ii) (∀s ∈ Σ∗ , σ ∈ Σ) sσ ∈ L(Gf ) ⇔ s ∈ L(Gf ) &
sσ ∈ L(G) & σ ∈ f (s);

6

(b) S(Gf ), the w-language synthesized by f , is given by
S(Gf ) := lim(L(Gf )) ∩ S(G)

(5)

The definition of L(Gf ) means that a string sσ can occur under supervision if and only if the string
s can occur under supervision, and the event σ can take place without violating either the ‘physical’

constraints embodied by L(G) or the control pattern imposed by the supervisor. The definition of S(Gf )
says that an infinite string s ∈ S(G) can eventually occur if and only if it can occur in the absence
of supervision and the supervisor does not prevent the occurrence of any of its its prefixes in pre(s).
Namely, f exert its influence on infinite strings only through the control actions on their finite prefixes.
We say that f : L(G) → Γ is a complete supervisor for G if L(Gf ) ⊆ L(G), and a deadlock-free
supervisor if Gf is a deadlock-free DES, i.e. pre(S(Gf )) = L(Gf ).
There are two classes of control requirements imposed on G: safety specifications describing that some
conditions on G will not occur, and liveness specifications requiring that some other conditions must
occur eventually [19]. The safety and liveness specifications can be specified in terms of ∗-languages
and ω -languages, respectively. In the following we briefly introduce the supervisory control for G with
infinite behavior.
First, for safety specifications, consider supervisory control of the finite behavior of G; it is proved
[20] that there exists a complete supervisor f ∗ : L(G) → Γ that synthesizes a ∗-language K ⊆ L(G) if
and only if K is ∗-controllable with respect to G and ∗-closed with respect to L(G).
Formally, language K ⊆ Σ∞ is ∗-controllable with respect to G (or L(G)) if
pre(K)Σu ∩ pre(L(G)) ⊆ pre(K).

Let ∗-language Es represent a safety specification imposed on G, and
C ∗ (Es ) := {K ⊆ L(G)| K ⊆ Es and
K is ∗-controllable wrt. G and
∗-closed wrt. L(G)}

the set of ∗-controllable and ∗-closed sublanguages of Es . Since ∗-controllability and ∗-closure are
both closed under arbitrary set union, there exists the supremal ∗-controllable and ∗-closed sublanguage
sup C ∗ (Es ) which may be effectively computed, and furthermore, a complete and deadlock-free supervisor
f ∗ : L(G) → Γ

(6)

7

synthesizing sup C ∗ (Es ), i.e.
L(Gf ) = sup C ∗ (Es )
∗

can be constructed [7, 20].
Then for liveness specifications, consider supervisory control of infinite behavior of G; it is proved
[12, Proposition 4.5] that there exists a complete and deadlock-free supervisor f ω : L(G) → Γ that
synthesizes an ω -language T ⊆ S(G) if and only if T is ω -controllable with respect to G and ω -closed
with respect to S(G). To introduce ω -controllability, we need the concept of controllability prefix.
For an ω -language T ⊆ Σω , its controllability prefix is given by
preG (T ) := {t ∈ pre(T )|(∃T ′ ⊆ T /t) [T ′ 6= ∅ is
∗-controllable wrt. L(G)/t

and ω -closed wrt. S(G)/t ]}
where T /t := {s ∈ Σ∞ |ts ∈ T }, and L(G)/t and S(G)/t are defined similarly.
Now, we define that T is ω -controllable with respect to G if
(i) T is ∗-controllable with respect to G;
(ii) pre(T ) = preG (T ).

Note that ω -controllable and ω -closed languages have different closure properties under union and
intersection. Specifically, ω -controllability is preserved under arbitrary unions but not intersections, while
ω -closure is preserved under arbitrary intersections but not unions. It is therefore convenient to define,

below, the separate language classes:
C ω (El ) := {T ⊆ S(G)| T ⊆ El and
T is ω -controllable wrt. G}
F ω (A) := {T ⊆ S(G)| A ⊆ T and
T is ω -closed wrt. S(G)}

where El is an ω -language representing the maximal legal specification and A is also an ω -language
but representing the minimal acceptable specification. Due to the closure property of ω -controllability
and ω -closure described above, there exists [12, Proposition 5.2] the unique supremal ω -controllable
sublanguage sup C ω (El ), given by
sup C ω (El ) := lim(preG (El )) ∩ El

8

and the unique infimal ω -closed superlanguage inf F ω (A), given by
inf F ω (A) := clo(A) ∩ S(G).

Furthermore, it is proved [12, Theorem 5.3] that there exists a ω -controllable and ω -closed language T
such that A ⊂ T ⊆ El if and only if
inf F ω (A) ⊆ sup C ω (El )

(7)

and if exists, a complete and deadlock-free supervisor
f ω : L(G) → Γ

(8)

synthesizing such T , i.e.
ω

A ⊂ T = S(Gf ) ⊆ El
ω

(9)

ω

pre(S(Gf )) = L(Gf )

(10)

can be constructed according to the procedure described in Appendix A.
III.

P ROBLEM F ORMULATION

Let G as in (1) be the plant to be controlled, Es the safety specification, El the maximal legal liveness
specification, and A the minimal acceptable liveness specification. To synthesize supervisors for these
specifications, our approach is in a simple but natural way: first synthesize a supervisor f ∗ for the safety
specification; then treat the closed-loop behavior of G controlled by f ∗ as the new plant to be controlled,
and synthesize another supervisor f ω for the liveness specifications. By this approach, the supervisors f ∗
and f ω work conjunctively, without conflicts, because the controlled behavior of f ∗ is the plant behavior
of f ω and thus a controllable event that has been disabled by f ∗ need not be disabled by f ω again.
First, for the safety specification Es , we synthesize as in (6) a complete supervisor f ∗ : L(G) → Γ
such that the finite behavior of G under the control of f ∗, denoted by Gf , satisfies
∗

L(Gf ) = sup C ∗ (Es ).
∗

According to (5), the infinite controlled behavior of G is S(Gf ) = S(G) ∩ lim(L(Gf )); Gf can be
∗

∗

∗

represented by a deterministic Büchi automaton (X ∗ , Σ, ξ ∗ , x∗0 , BX ∗ ) constructed according to
(i) Select x∗0 ∈ X ∗ corresponding to q0 ∈ Q.
(ii) ξ ∗ : X ∗ × Σ → X ∗ with ξ ∗ (x∗ , σ) = x′∗ if there exists s ∈ Σ∗ such that ξ ∗ (x∗0 , s) = x∗ , δ(q0 , sσ)!,
and σ ∈ f ∗ (s).

9

(iii) BX ∗ := {x∗ ∈ X ∗ |(∃s ∈ Σ∗ ) ξ ∗ (x∗0 , s) = x∗ , δ(q0 , s) ∈ BQ }.
Let
SUP∗ := (X ∗ , Σ, ξ ∗ , x∗0 ).

(11)

Namely SUP∗ has the same transition structure and thus same finite behavior as Gf , i.e. L(SUP∗ ) =
∗

L(Gf ). Then SUP∗ is an implementation [7] of the supervisor f ∗ , i.e.
∗

L(G) ∩ L(SUP∗ ) = L(Gf )
∗

Since L(SUP∗ ) = L(Gf ), it also infers that S(Gf ) = S(G) ∩ lim(L(SUP∗ )).
∗

∗

Second, we consider the supervisor synthesis for the liveness specifications El and A. At this step,
we treat Gf as the new plant to be controlled, and synthesize as in (8) a complete and deadlock-free
∗

supervisor f ω : L(Gf ) → Γ given by



f ω (l)
if l ∈ pre(A),

 0
ω
f (l) :=
if l ∈ k pre(Ek′ ), k ∈ M
fkω (l/k)



 undefined otherwise
∗

(12)

where M is the set of all elements of pre(sup C ω (El )) \ pre(inf F ω (A)) of minimal length, and Ek′ is
the sublanguage of sup C ω (El )/k synthesized by fkω . Under the supervision of f ω , the infinite controlled
behavior of Gf , denoted by Gf
∗

∗

∧f ω

(f ∗ and f ω work conjunctively, i.e. a controllable event will be

disabled if it is disabled by any one of f ∗ and f ω ), satisfies:
A ⊆ S(Gf
pre(S(Gf
Gf

∗

∧f ω

∗

∗

∧f ω

∧f ω

) ⊆ El

)) = L(Gf

∗

∧f ω

).

can be represented by a deterministic Büchi automaton (X ω , Σ, ξ ω , xω0 , BX ω ) constructed by:

(i) Select xω0 ∈ X ω corresponds to x∗0 ∈ X ∗ .
(ii) ξ ω : X ω × Σ → X ω with ξ ω (xω , σ) = x′ ω if there exists s ∈ Σ∗ such that ξ ω (xω0 , s) = xω ,
ξ ∗ (x∗0 , sσ)!, and σ ∈ f ω (s).

(iii) BX ω := {xω ∈ X ω |(∃s ∈ Σ∗ ) ξ ω (xω0 , s) = xω , ξ(x∗0 , s) ∈ BX ∗ }.
The supervisor f ω : Σ∗ → Γ exercises its control action depending on its observation on finite strings
in Σ∗ , and thus f ω also can be implemented by a *-automaton. Let
SUPω := (X ω , Σ, ξ ω , xω0 ).

(13)

10

Namely SUPω has the same transition structure and thus same finite behavior as Gf
L(Gf

∗

∧f ω ).

∗

∧f ω ,

i.e. L(SUPω ) =

Then SUPω is an implementation of the supervisor f ω , i.e.
S(Gf ) ∩ lim(L(SUPω )) = S(Gf
∗

∗

∧f ω

).

Note that SUPω also influences the finite controlled behavior of G, thus L(Gf

(14)
∗

∧f ω )

and S(Gf

∗

∧f ω )

represent respectively the finite and infinite controlled behavior of G under the control of SUP∗ and
SUPω , i.e.
L(Gf

∗

∧f ω

) = L(G) ∩ L(SUP∗ ) ∩ L(SUPω )

(15)

S(Gf

∗

∧f ω

) = S(G) ∩ lim(L(SUP∗ )) ∩ lim(L(SUPω )).

(16)

It is easily verified that the finite controlled behavior of G satisfies the safety specification, i.e.
L(Gf

∗

∧f ω

) ⊆ Es ,

and the infinite controlled behavior fits into the range of liveness specifications El and A, i.e.
A ⊆ S(Gf

∗

∧f ω

) ⊆ El .

The supervisor SUP∗ is constructed for satisfying the safety specification and thus we refer it as the
safety supervisor for G; while SUPω is constructed for the liveness specifications and thus we refer
it as the liveness supervisor for G. Throughout this paper, we assume that S(Gf
L(Gf

∗

∧f

ω

∗

∧f ω )

6= ∅ and thus

) 6= ∅.

The control action of SUP∗ and SUPω are both to enable/disable controllable events; thus the
localizations of SUP∗ and SUPω are similar to that of the monolithic supervisor SUP in [1]. The
differences are illustrated in Fig. 1. First, the localization of SUP generate one local controller for each
controllable event. However, the present localization procedure may generate multiple local controllers for
one controllable event, because an event may be disabled/enabled by both SUP∗ and SUPω . Second, the
localization of SUP∗ is similar to that of SUP in [1], however, the localization of SUPω is particular:
according to whether or not s ∈ pre(A) (see (12) for the definition of f ω ), there are two types of
supervisors included in f ω : f0ω defined on the strings s ∈ pre(A) and fkω defined on the rest of the
strings in L(G), thus the localization of SUPω can be divided into two parts and consequently, we will
get two local controllers for each controllable event.
Remark 1. We remark here that the localization of the control actions after string s ∈
/ pre(A) is treated as
a whole, but not divided corresponding to each fkω (k ∈ M ). The reason is as follows. First, to localize the

11

(a) Localization for DES with finite behavior

(b) Localization for DES with infinite behavior

Fig. 1. Supervisor localization example for illustration: let Σc = {α, β}. For DES G with finite behavior as in (a), the monolithic
supervisor SUP is decomposed into two local controllers LOCα and LOCβ for controllable events α and β respectively.
For DES G with infinite behavior as in (b), there are two supervisors SUP∗ and SUPω constructed for satisfying safety
specification and liveness specifications respectively. The localization procedure decomposes SUP∗ into two local controllers
ω
LOC∗α and LOC∗β , and decomposes SUPω into local controllers LOC∗α,0 and LOC∗α,1 for α, and LOCω
β,0 and LOCβ,1

for β.

control actions after each string k, we need to find in L(SUPω ) the language Ek′ synthesized by fkω , which
will increase the time complexity of the overall algorithm. Second, the number of local controllers will
increase with the states number of SUPω . In our current setting, all the controlled behavior synthesized
by fkω are contained in L(SUPω ), thus we don’t have to find each Ek′ ; consequently for each controllable
event, SUPω will be constantly decomposed into two local controllers: one corresponding to f0ω and the
other to all fkω .
Remark 2. Note that it is also possible to construct a monolithic supervisor SUP that synthesizes the
controlled behavior L(Gf

∗

∧f ω ),

i.e. SUP is control equivalent to SUP∗ and SUPω . In that case, by

applying the localization procedure in [1], we may get for each controllable event a local controller.
In general, this local controller will have more states than the local controllers constructed by our new
localization procedures, as will be demonstrated in the example of Small Factory in Section V. The
reason is that either SUP∗ , or SUPω , disables controllable events on part of the strings in L(G): the
plant of SUP∗ is G and the plant of SUPω is Gf .
∗

Due to the above features specific to SUP∗ and SUPω , we have different types of local controllers

12

for each controllable event α ∈ Σc . First, we say that a *-automaton
∗
LOC∗α = (Yα∗ , Σ, ηα∗ , y0,α
)

is a safety local controller for α if LOC∗α enables/disables event α (and only α) consistently with SUP∗ ,
which means that for all s ∈ Σ∗ there holds
sα ∈ L(LOC∗α ), sα ∈ L(G), s ∈ L(SUP∗ )
⇔ sα ∈ L(SUP∗ )

(17)

Second, for all the strings s ∈ L(Gf ), we divide them into two parts: C1 = pre(A) and C2 =
∗

L(Gf ) \ pre(A). For each part Cn (n = 1, 2), we say that a *-automaton
∗

ω
ω
ω
),
, Σ, ηα,n
, y0,α,n
LOCωα,n = (Yα,n

is a liveness local controller for α if LOCωα,n enables/disables event α (and only α) occurred at string
s ∈ Cn consistently with SUPω , which means that for all s ∈ Cn there holds
sα ∈ L(LOC∗α,n ), sα ∈ L(Gf ), s ∈ L(SUPω )
∗

⇔ sα ∈ L(SUPω )

(18)

We now formulate the Supervisor Localization Problem for DES with infinite behavior:
Construct a set of safety local controllers {LOC∗α | α ∈ Σc }, a set of liveness local controllers
{LOCωα,n | α ∈ Σc , n = 1, 2} such that their collective controlled behaviors are equivalent to those of

supervisors SUP∗ and SUPω with respect to G, i.e.
 \

L(G) ∩
L(LOC∗α )
α∈Σc

∩



\


∗
ω
L(LOCωα,n ) = L(Gf ∧f )

α∈Σc ,n=1,2

S(G) ∩

 \

α∈Σc

∩




lim(L(LOC∗α ))

\


∗
ω
lim(L(LOCωα,n )) = S(Gf ∧f )

α∈Σc ,n=1,2

where L(Gf

∗

∧f

ω

) and S(Gf

∗

∧f

ω

) respectively represent the finite and infinite controlled behaviors of

G under the control of SUP∗ and SUPω (as in (15) and (16)).

13

Having obtained these local controllers for individual controllable event, for the plant consisting of
multiple components, we can allocate each controller to the agent(s) owning the corresponding controllable event. Thereby we build for a multi-agent DES with infinite behavior a nonblocking distributed
control architecture.
IV.

S UPERVISOR L OCALIZATION P ROCEDURE

We solve the Supervisor Localization Problem for DES with infinite behavior by extending the localization procedure proposed in [1]. In particular, localization of SUPω will be divided into two cases by
considering the control action of f0ω and those of fkω separately, for which we introduce new definition
of control consistency relation.
Given a DES plant G = (Q, Σ, δ, q0 , BQ ) (as in (1)) with a safety supervisor SUP∗ = (X ∗ , Σ, ξ ∗ , x∗0 )
and a liveness supervisor SUPω , we present the localization of SUPω (with new control consistency
concept) and that of SUP∗ in the sequel.
A. Localization of SUPω
As mentioned in Section II, an infinite string s can eventually occur if and only if it can occur in
the absence of supervision and the supervisor does not prevent the occurrence of any of its its prefixes
in pre(s). In other words, the supervisor SUPω (implementation of f ω ) exerts its influence on infinite
strings only through the control actions on their finite prefixes. So, the localization procedure for SUPω
is to decompose the control actions on the finite strings s ∈ L(Gf ) (the plant of SUPω ), and as in [1],
∗

the control equivalence of finite behaviors will be guaranteed by the localization procedure. The control
equivalence of infinite behaviors, however, will be derived by the following Lemma once the equivalence
of finite behaviors were confirmed.
Lemma 1. Let A, B, C ⊆ Σ∗ be arbitrary ∗-languages, then we have
A ∩ B = C ⇒ lim(A) ∩ lim(B) = lim(C)

where the operator lim is defined in (3).
Proof: Recall that (see (3)) lim(A) = pre−1(A) ∩ Σω := {t ∈ Σω |pre(t) ⊆ A}.
(⊇) By the above definition and C ⊆ A ∩ B , we have lim(C) ⊆ lim(A) and lim(C) ⊆ lim(B). So
lim(C) ⊆ lim(A) ∩ lim(B).

(⊆) Let s ∈ lim(A)∩lim(B). Then s ∈ lim(A), and thus pre(s) ⊆ A; by the same reason, pre(s) ⊆ B .
Hence pre(s) ⊆ A ∩ B = C , and thus s ∈ lim(C), which completes the proof.



14

The control action of SUPω is to enable or disable controllable events in Σc at strings s ∈ L(Gf ).
∗

As in (12), the control action after a string s is divided into two cases: according to the strings s ∈ C1
or C2 . Thus, for each controllable event α, we propose to decompose SUPω into two local controllers,
one responsible for disabling α at strings s ∈ Cn , n = 1 or 2; in other words, the local controller
corresponding to Cn will not disable α at the string t ∈ Cm (m = 1, or 2, m 6= n), even α is disabled by
SUPω (although it will be disabled by the local controller corresponding to Cm ). Consequently, the two

local controllers generally have states number no more than that obtained by considering the disablement
after all the strings in L(Gf ).
∗

Fix an arbitrary controllable event α ∈ Σc and one part of the language Cn , n = 1, 2 (recall that
C1 = pre(A) and C2 = L(Gf ) \ pre(A)). The control action of SUPω is captured by the following
∗

two functions. First define Eαω : X ω → {1, 0} according to
Eαω (xω ) = 1 iff ξ ω (xω , α)!

(19)

ω : X ω → {1, 0} according
So Eαω (xω ) = 1 means that α is defined at state xω in SUPω . Next define Dα,n
ω (xω ) = 1 iff
to Dα,n

¬ξ ω (xω , α)! & (∃s ∈ Cn )


ξ ω (xω0 , s) = xω & ξ ∗ (x∗0 , sα)!

(20)

ω (x) = 1 means that α must be disabled at x arrived by strings s ∈ C consistently with
Thus Dα,n
n

the supervisor SUPω (i.e. α is disabled at x in SUPω but is defined at some state in the plant Gf

∗

corresponding to x via string s ∈ Cn ). Note that here the plant is Gf , not G, because as in Section III
∗

when synthesizing the supervisor SUPω , Gf is considered as the plant to be controlled.
∗

ω differs from that in [1] in the range of strings s: here D ω (xω ) = 1 only when xω
The function Dα,n
α,n
ω (2) = 1 because
can be arrived by a string s ∈ Cn . For illustration, consider the example in Fig. 2: D21,1
ω (3) = 0, by the reason that
state 2 can be reached by string s = 11.12 ∈ C1 = pre(A); however, D21,1

none of the strings in C1 can reach state 3.
Based on (19) and (20), we define the following binary relation Rωα,n ⊆ X ω × X ω , called control
consistency with respect to controllable event α (cf. [1]), according to (xω , x′ω ) ∈ Rα,n iff
ω
Eα (xω ) · Dα,n
(x′ω ) = 0 = Eα (x′ω ) · Dα,n (xω )

(21)

Thus a pair of states (xω , x′ω ) in SUPω satisfies (xω , x′ω ) ∈ Rωα,n if event α is defined at one state,
but not disabled at the other. It is easily verified as in [1] that Rωα,n is generally not transitive, thus not

15






















Fig. 2.

∗

Example: Plant Gf (Büchi automaton), supervisor SUPω (∗-automaton) and Büchi automaton A representing the

minimal acceptable liveness specification A. Notations: a circle with right input arrow → denotes the initial state, and a circle
in dotted box denotes that this state is an element of the Büchi acceptance criterion; we shall use these notations throughout
this report.

ω = {X ω ⊆ X ω |i ∈ I ω } a cover on X ω .
an equivalence relation. Now let I ω be some index set, and Cα,n
i
ω is a control cover with respect to α if
Cα,n

(i) (∀i ∈ I ω , ∀xω , x′ω ∈ Xiω )(xω , x′ω ) ∈ Rωα,n ,
h
(ii) (∀i ∈ I ω , ∀σ ∈ Σ) (∃xω ∈ Xiω )ξ ω (xω , σ)! ⇒
(∃j ∈ I ω )(∀x′ω ∈ Xiω )ξ ω (x′ω , σ)! ⇒ ξ ω (x′ω , σ) ∈ Xjω

i
.

ω a control congruence if it happens to be a partition on X ω , namely its cells are pairwise
We call Cα,n

disjoint.
ω on X ω , we construct a local controller LOCω = (Y ω , Σ, ζ ω ,
Having defined a preemption cover Cα,n
α,n
α,n
α,n
ω
) for the controllable event α as follows.
y0,α,n
ω := I ω , with each state y ω ∈ Y ω being a cell X ω of the cover C ω . In
(i) The state set is Yα,n
α,n
α,n
i
ω where xω belongs, i.e. xω ∈ X ω .
ω
is a cell Xi,0
particular, the initial state y0,α,n
0
0
i,0
ω : I ω × Σ → I ω over the entire event set Σ by ζ ω (i, σ) = j if
(ii) Define the transition function ζα,n
α,n

(∃xω ∈ Xiω ) ξ ω (xω , σ) ∈ Xjω and


(∀x′ω ∈ Xiω ) ξ ω (x′ω , σ)! ⇒ ξ ω (x′ω , σ) ∈ Xjω .

Similar to Lemma 2 in [6], it is easily verified that LOCωα,n constructed above is a liveness local
controller for α, i.e. condition (18) holds for all s ∈ Cn . By the above two procedures, for one controllable

16







Fig. 3.













Example: Local controllers for event 21 of DES example in Fig. 2

event α, we get two liveness local controllers: LOCωα,1 responsible for the disablement at strings s ∈
C1 = pre(A) and LOCωα,2 for the disablement at strings s ∈ C2 = L(Gf ) \ pre(A).
∗

For the example in Fig. 2, we get two liveness local controllers LOCω21,1 and LOCω21,2 for event
21, as displayed in Fig. 3. In the transition diagram of LOCω21,1 , state 0 corresponds to cell {0, 1, 3}
ω
of the control cover C21,1
= {{0, 1, 3}, {2}} and state 1 corresponds to cell {2}; in LOCω21,2 , state 0
ω
corresponds to cell {0, 2} of the control cover C21,2
= {{0, 2}, {1}, {3}}, state 1 corresponds to cell {1},

and state 2 corresponds to cell {3}. However, if consider the disablement at all the strings in L(Gf )
∗

together, the supervisor SUPω is not localizable and thus we get a 4-states local controller LOCω21 ,
which has more states than any of LOCω21,1 and LOCω21,2 .
B. Localization of SUP∗
The localization of SUP∗ is similar to that of SUP in [1], namely, the disablement at all strings in
L(G) are considered. The control action of SUP∗ is captured by the following two functions.

Fix an arbitrary controllable event α ∈ Σc . First define Eα∗ : X ∗ → {1, 0} according to
Eα∗ (x∗ ) = 1 iff ξ ∗ (x∗ , α)!

(22)

So Eα∗ (x∗ ) = 1 means that α is defined at state x∗ in SUP∗ . Next define Dα∗ : X ∗ → {1, 0} according
to Dα∗ (x∗ ) = 1 iff
¬ξ ∗ (x∗ , α)! & (∃s ∈ Σ∗ ) (ξ ∗ (x∗0 , s) = x∗ & δ(q0 , sα)!)

(23)

Thus Dα∗ (x∗ ) = 1 means that α must be disabled at x∗ (i.e. α is disabled at x∗ in SUP∗ but is defined
at some state in the plant G corresponding to x∗ via string s).
With new definition of Dα∗ , we get new definitions of control consistency relation R∗α and control
cover Cα∗ , and then by the rules (i)-(ii) for constructing liveness local controller replaced with the new

17
∗ ). It is easily verified that LOC∗
definitions, we construct a new local controller LOC∗α = (Yα∗ , Σ, ζα∗ , y0,α
α

constructed above is a safety local controller for α, i.e. condition (17) holds.
C. Main Result
By the same procedure as above, we construct for each controllable event α ∈ Σc a safety local
controller LOC∗α , and two liveness local controllers LOCωα,n (n = 1, 2). We shall verify that these local
controllers collectively achieve the same controlled behaviors as SUP∗ in (11) and SUPω in (13).
Theorem 1. The set of safety local controllers {LOC∗α | α ∈ Σc }, the set of liveness local controllers
{LOCωα,n | α ∈ Σc , n = 1, 2} constructed above solve the Supervisor Localization Problem for DES

with infinite behavior, i.e.
L(G) ∩

 \

α∈Σc

∩




L(LOC∗α )

\


∗
ω
L(LOCωα,n ) = L(Gf ∧f )

(24)

α∈Σc ,n=1,2

S(G) ∩

 \

α∈Σc

∩



∧f

ω


lim(L(LOC∗α ))

\


∗
ω
lim(L(LOCωα,n )) = S(Gf ∧f )

(25)

α∈Σc ,n=1,2

where L(Gf

∗

∧f

ω

) and S(Gf

∗

) respectively represent the finite and infinite controlled behaviors of

∗

G under the control of SUP and SUPω (as in (15) and (16)).

Theorem 1 confirms the control equivalence of the constructed local controllers and supervisors SUP∗
and SUPω . Indeed, according to the definition of (safety and liveness) local controllers, the safety local
controller LOC∗α enables/disables event α consistently with SUP∗ and the liveness local controllers
LOCωα enable/disable α consistently with SUP∗ . Hence, to prove Theorem 1, we show (i) the control

equivalence of {LOC∗α | α ∈ Σc } with SUP∗ and (ii) the control equivalence of {LOCωα,n | α ∈
Σc , n = 1, 2} with SUPω . The proof of the first part is similar to that of the control equivalence of local

controllers with the corresponding monolithic supervisor in [1]. The proof of the second part is particular,
because at each local controller LOCωα,n , we consider the disablement of α on only the strings s ∈ Cn .
In the following, we provide the complete proof of Theorem 1.

18

Proof of Theorem 1: (i) We prove the control equivalence of {LOC∗α | α ∈ Σc } with SUP∗ , i.e.

 \
∗
L(LOC∗α ) = L(Gf )
(26)
L(G) ∩
α∈Σc

S(G) ∩

 \

α∈Σc

where

∗
L(Gf )

and

∗
S(Gf )


∗
lim(L(LOC∗α )) = S(Gf )

(27)

respectively represent the finite and infinite controlled behavior of G under

the control of SUP∗ . The proof of (26) is similar to that of the control equivalence of local controllers
with the corresponding monolithic supervisor; for a detailed proof, see Proposition 1 in [1].
With (26), equation (27) is immediate:
S(Gf ) = S(G) ∩ lim(L(Gf )) (by (5))

\

(by (26))
= S(G) ∩ lim L(G) ∩
L(LOC∗α )
∗

∗

α∈Σc

= S(G) ∩ lim(L(G)) ∩

 \


lim(L(LOC∗α ))

α∈Σc

(by Lemma 1)
 \

= S(G) ∩
lim(L(LOC∗α ))
α∈Σc

(because S(G) ⊆ lim(L(G)))

(ii) We prove the control equivalence of {LOCωα,n | α ∈ Σc , n = 1, 2} with SUPω , i.e.


\
∗
∗
ω
L(Gf ) ∩
L(LOCωα,n ) = L(Gf ∧f )

(28)

α∈Σc ,n=1,2

S(Gf ) ∩
∗

where L(Gf

∗

∧f ω )

and S(Gf

∗



∧f ω )

\

lim(L(LOCωα,n )) = S(Gf

∗

∧f ω

)

(29)

α∈Σc ,n=1,2

respectively represent the finite and infinite controlled behavior of

Gf under the control of SUPω . According to (i), we only need to prove (28): equation (29) will be
∗

obtained from (28) and Lemma 1. Since L(SUPω ) = L(Gf
T
∗
L(LOCωα,n )) = L(SUPω ).
L(Gf ) ∩ (
α∈Σc ,n=1,2

First, we show L(SUPω ) ⊆ L(G) ∩ (

∩

α∈Σc ,n=1,2

∗

∧f ω )

(according to (13)), we must prove

L(LOCωα,n )). It suffices to show for all α ∈ Σc and

n = 1, 2, L(SUP∗ ) ⊆ L(LOCωα,n ). Let α ∈ Σc and s ∈ L(SUPω ); we must show s ∈ L(LOCωα,n ).

Write s = σ0 , ..., σm ; then s ∈ L(SUPω ) and thus there exist xω0 , ..., xωm ∈ X ω such that
ξ ω (xωj , σj ) = xωj+1 , j = 0, ..., m − 1.

19

ω and ζ
Then by the definition of Cα,n
α,n , for each j = 0, ..., m − 1, there exist ij , ij+1 ∈ I such that

xωj ∈ Xiωj & xωj+1 ∈ Xiωj+1 & ζα,n (ij , σj ) = ij+1 .

So ζα,n (i0 , σ0 ...σn )!, i.e. ζα,n (i0 , s)!. Hence we have s ∈ L(LOCα,n ).
Next, we prove L(G) ∩ (

∩

α∈Σc ,n=1,2

L(LOCωα,n )) ⊆ L(SUPω ), by induction on the length of strings.

For the base case, as it was assumed that S(Gf
L(Gf ),
∗

L(LOCωα,n )

∗

∧f ω )

is nonempty, it follows that the languages

ω

and L(SUP ) are all nonempty, the empty string ǫ belongs to each.

For the inductive step, suppose that s ∈ L(Gf )∩(
∗

∩

α∈Σc ,n=1,2

sσ ∈ L(Gf )∩(
∗

∩

α∈Σc ,n=1,2

L(LOCωα,n )) implies s ∈ L(SUPω ), and

L(LOCωα,n )) for an arbitrary event σ ∈ Σ; we must show that sσ ∈ L(SUPω ).

If σ ∈ Σu , then sσ ∈ L(SUPω ) because L(SUPω ) is ∗-controllable (by its ω -controllability).
Otherwise, we have σ ∈ Σc and there exists a local controller LOCωα,n for σ : α = σ ; n = 1 if
s ∈ C1 = pre(A), otherwise n = 2. It follows from sα ∈ (
ω (y ω
and s ∈ L(LOCωα,n ). Namely, ζα,n
0,α,n , sα)! and

∩

L(LOCωα,n )) that sα ∈ L(LOCωα,n )

α∈Σc ,n=1,2
ω
ω
, s)!.
ζα,n (y0,α,n

ω (y ω
Let i := ζα,n
0,α,n , s); then there

ω (i, α). By the definition of ζ ω , there exists xω , x′ω ∈ X ω and x′′ω ∈ X ω such that
exists j = ζα,n
α,n
i
j

ξ ω (xω0 , s) = xω and ξ ω (x′ω , α) = x′′ω . Since xω and x′ω belong to the same cell Xiω , by the definition
ω (x′ω ) = 0,
of control cover they must be control consistent, i.e. (xω , x′ω ) ∈ Rωα,n . Thus Eαω (xω ) · Dα,n
ω (x′ω ) = 0. The latter means that: either (a) ξ ω (xω , α)! or (b) for all t ∈ C with
which implies Dα,n
n

ξ ω (xω0 , t) = xω , ξ ∗ (x∗0 , tα) is not defined. Note that (b) is impossible because by hypothesis that t ∈
L(SUPω ) and tα ∈ L(Gf ) we have ξ ω (xω0 , t)! and ξ ∗ (x∗0 , tα)!. Thus by (a), ξ ω (ξ ω (xω0 , s), α)!, and
∗

therefore sα ∈ L(SUPω ).
We have shown equations (26) and (27), and equations (28) and (29). Combining them together, we
conclude that the equations (24) and (25) hold.



From the proof of Theorem 1, we see that the equivalences of infinite behaviors (equations (27) and
(29)) are immediately derived from their corresponding equivalences of finite behaviors (equations (26)
and (28)) and Lemma 1. This confirms that the definitions of control consistency and control cover
need not contain any consistency relationship on infinite behavior. Thus the localization algorithm (see
[1]) for DES with finite behavior can be easily adapted to construct local controllers in Theorem 1
with suitable modifications: (i) using the current definition of control consistency and control cover;
(ii) for the localization of SUPω , we need to judge if a state x in SUPω can be arrived by a string
s ∈ Cn (n = 1, 2). Assume that a ∗-automaton Cn = (Z, Σ, η, z0 ) represents the ∗-language Cn ; then

the above judgement can be realized by checking if state x is in one of the state pairs of the product of
SUPω and Cn . The complexity of this step is O(|X ω | × |Z|). We have known that the complexities of

20

Fig. 4.

Layout of Small Factory

0

1

0

1

Idle

Working

Empty

Full

Machine

Fig. 5.

Buffer

∗-automata representing finite behaviors of machines Mi , and buffers Bi (i = 1, 2).

the localization algorithms for localizing SUP∗ and SUPω are O(|X ∗ |4 ) and O(|X ω |4 ) respectively,
and thus the overall complexity of the new localization procedure for DES with infinite behavior is
O(|X ∗ |4 + |X ω |4 + |X ω | × |Z|). The Small Factory example in the next section will demonstrate the

above result.
V.

C ASE S TUDY: S MALL FACTORY

A. Model Descriptions: plant and specifications
We illustrate the above supervisor localization for DES with infinite behavior by studying a Small
Factory example, taken from [10, Chapt. 3]. As displayed in Fig. 4, the plant to be controlled, denoted
by SF, consists of two machines Mi (i = 1, 2) that are coupled with two buffers Bi (i = 1, 2). The
alphabet of event symbols for SF is
Σ = {α1 , α2 , β1 , β2 , γ1 , γ2 }.

The finite behavior of the plant is described as follows. There are two routines in the plant. At each
routine i (i = 1, 2), the machine Mi processes workpieces one at a time. When Mi begins a job it
acquires a workpiece from elsewhere in the factory (event αi ). Upon completing the Mi pushes the
workpiece onto buffer Bi (event βi ). Machines not shown in Fig. 4 remove workpieces from buffer Bi
for further processing (event γi ); we assume that some control mechanism prevents such events from
causing buffer Bi to “underflow” - supposing for the sake of simplicity that each buffer has only one
slot. The two machines and two buffers are modelled by the ∗-automata in Fig. 5.

21

0

1

Fig. 6. Büchi automata Fi (i = 1, 2) representing the liveness assumptions on each routine that every βi is eventually followed
by an occurrence of γi .

The infinite behavior of the plant describes that removing workpieces from the buffer are in continual
operation, so that every occurrence of βi is eventually followed by an occurrence of γi . This behavior is
captured by the Büchi automata Fi (i = 1, 2) of Fig. 6.
Now we have a complete model of the uncontrolled DES plant SF: the finite behavior is the intersection
of the languages accepted by the four ∗-automata in Fig. 5, i.e.
L(SF) = L(M1 ) ∩ L(M2 ) ∩ L(B1 ) ∩ L(B2 );

the infinite behavior is the intersection of lim(L(SF)) with the ω -languages accepted by the two Büchi
∗-automata in Fig. 6, i.e.
S(SF) = lim(L(SF)) ∩ S(F1 ) ∩ S(F2 ).

The plant under control must satisfy a number of specifications.
(S1) It should prevent buffer overflows: two occurrences of βi should be separated by an occurrence of
γi .

(S2) Because Mi (i = 1, 2) employ the same resources, they must not be allowed to operate simultaneously: αi should not occur between successive occurrence of αj and βj .
(S3) Because the “mutual exclusion” requirement (S2) raises the possibility that one machine may
continually preempt the other, we add a liveness specification that each machine operates infinitely
often: in other words, each αi should occur infinitely often.
(S4) The two routines in Fig. 4 always work alternately, i.e. M1 (resp. M2 ) should not start (or restart)
to work until the workpiece in B2 (resp. B1 ) has been taken away. Here we assume that initially
M1 starts to work before M2 .

Specifications (S1) and (S2) are represented by the ∗-automata BUFSPECi (i = 1, 2) and MUXSPEC
in Fig. 7. They describe finite behavioral requirements on the system, and thus are considered as safety
specifications. Let Es denote the overall safety specification, i.e.
Es = L(BUFSPEC1 ) ∩ L(BUFSPEC2 ) ∩ L(MUXSPEC).

22

0

Fig. 7.

1

2

0

1

Safety specifications: prevention of buffers’ overflow represented by ∗-automata BUFSPECi (i = 1, 2) and mutual

exclusion requirement represented by ∗-automata MUXSPEC

2

4

1

3

0

Fig. 8.

Fig. 9.

Maximal legal liveness specification represented by Büchi automaton MAXSPEC

5

4

3

0

1

2

Minimal acceptable liveness specification represented by Büchi automaton MINSPEC

(S3) represented by the deterministic Büchi automaton MAXSPEC in Fig. 8, is considered as the
maximal legal liveness specification, i.e.
El = S(MAXSPEC).

(S4) represented by the deterministic Büchi automaton MINSPEC, is selected as the minimal acceptable
liveness specification, i.e.
A = S(MINSPEC).

B. Safety and Liveness Supervisors Synthesis
There are two types of specifications imposed on the system SF: safety specification Es and liveness
specifications El and A.

23

2

4

6

0

7

3

1

Fig. 10.

5

∗

Transition structure of SFf and SUP∗

For safety specification, we compute as in (11) a safety supervisor SUP∗ := (X ∗ , Σ, ξ ∗ , x∗0 ) as
displayed in Fig. 10, which has 8 states and 14 transitions. The controlled behavior of SF under the
control of SUP∗ is represented by Büchi automaton SFf , i.e.
∗

L(SFf ) = L(G) ∩ L(SUP∗ )
∗

S(SFf ) = S(SF) ∩ lim(L(SUP∗ )).
∗

SFf has the same transition structure with SUP∗ , and the Büchi acceptance criterion accepting the
∗

language S(SFf ) is BX ∗ = {0, 1, 2, 3, 4}.
∗

It is easily verified that the safety specifications (S1) and (S2) are both satisfied, i.e.
L(SFf ) = sup C ∗ (Es ∩ L(SF)) ⊆ Es .
∗

However, there may exist the case that one of machines, e.g. M1 , may work recursively all the time. In
other words, M1 may preempt the start of M2 infinitely, violating the liveness specification (S3).
For the maximal legal liveness specifications El and minimal acceptable liveness specification A,
treating SFf as the new plant to be controlled, we construct as in (13) a liveness supervisor SUPω as
∗

displayed in Fig. 11, which has 34 states and 51 transitions. The controlled behavior of SFf , represented
∗

by Büchi automaton SFf

SFf

∗

∧f ω

∗

∧f ω

, i.e.
L(SFf

∗

∧f ω

) = L(SFf ) ∩ L(SUPω )

S(SFf

∗

∧f ω

) = S(SFf ) ∩ lim(L(SUPω )).

∗

∗

has the same transition structure with SUPω , as displayed in Fig. 11, and the Büchi acceptance

criterion accepting the language S(SFf

∗

∧f ω

) is BX ω = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 15, 16, 23, 29, 30}. The

24

Fig. 11.

4

8

15

22

27

31

26

6

11

18

7

13

20

29

23

5

9

16

12

14

24

21

10

33

32

28

17

25

30

0

2

1

3

Transition structure of SFf

∗

∧f ω

19

and SUPω

readers are referred to Appendix B for the detailed steps of constructing SUPω . It is also verified that
the controlled behavior satisfies the given liveness specifications, i.e.
A ⊆ S(Gf

∗

∧f ω

) ⊆ El .

Comparing the transition structure of Gf and SUPω , we find that event α1 should be disabled at
∗

states 20, 23, 27, 31, and event α2 should be disabled at states 8, 19, 22, 26. To illustrate the control
logic of supervisor SUPω , we consider the control actions on event α1 at states 5 and 23. Since the
plant of SUPω is SFf , the finite controlled behavior must satisfy the safety specifications (S1) and
∗

(S3), thus here we only consider the infinite behavior of the controlled plant.
First, α1 is enabled at state 5; the reason is as follows. At state 5, only string s := α1 β1 γ1 has occurred,
namely, a workpiece has been taken by M1 , deposited into B1 and taken away from B1 . At this stage, if
α1 is enabled, there exists sublanguage Lsub = sα1 β1 γ1 (α2 β2 γ2 α1 β1 γ1 )ω synthesized by SUPω , which

satisfies the liveness specification (S3).
However, the supervisor SUPω chooses to disable event α1 at state 23; the reason is as follows. Let
t = ss = α1 β1 γ1 α1 β1 γ1 , and it is easily verified that in Gf , string t re-visits state 0. As described in
∗

the above case, disabling event α1 (on the contrary enabling event α2 ) may bring an infinite controlled
behavior that satisfies the liveness specification (S3). Hence, this disablement is correct. Moreover,
considering a general case when the string s has occured n < ∞ times; it is also safe for M1 to
work again, because the supervisor can prevent M1 from starting to work, but permit M2 to start at
n + 1 times of occurrences of s. However, we cannot enable event α1 infinitely, because the infinite

25

0

Fig. 12.

1

2

0

1

2

Safety local controllers LOC∗α1 and LOC∗α2 for controllable events α1 and α2 respectively

occurrences of string s (i.e. sω ) will violate the liveness specification (S3). Namely, event α1 must be
disabled in a finite time; here SUPω chooses to disable it at string t. Hence, supervisor SUPω is one,
but not the unique supervisor for satisfying the liveness specification (S3).
Now we have a safety supervisor SUP∗ and a liveness supervisor SUPω , whose finite and infinite
controlled behaviors on the plant SF are represented by L(SFf

∗

∧f ω

) and S(SFf

∗

∧f ω

L(SFf

∗

∧f ω

) = L(SF) ∩ L(SUP∗ ) ∩ L(SUPω )

S(SFf

∗

∧f ω

) = S(SFf ) ∩ lim(L(SUPω )) ∩ lim(L(SUPω )).

), i.e.

∗

In the next subsection, we decompose the two supervisors into corresponding local controllers.
C. Supervisor Localization
There are two controllable events α1 and α2 in the plant SF. By applying the localization procedure
in Section IV-B, we first get two safety local controllers LOC∗α1 and LOC∗α2 for controllable events α1
and α2 respectively, as shown in Fig. 12.
The control logic of LOC∗α1 is as follows. First, to prevent the overflow of B1 (specification (S1)),
machine M1 is prohibited by LOC∗α1 to take a workpiece from the source (i.e. event α1 ) when the
buffer B1 is full, i.e. there exists a workpiece in buffer B1 , e.g. LOC∗α1 is at states 1 or 2. Second, to
satisfy the specification (S2), event α1 should be disabled by LOC∗α1 between successive occurrences
of α2 and β2 , e.g. LOC∗α1 is at states 1 and 2. Note that at state 1, the buffer may be empty and α1 is
permitted to occur without violating the specification (S1); however, at this state, α1 must be disabled to
prevent the violation of specification (S2).
The control logic of LOC∗α2 is similar to that of LOC∗α1 , but to disable or enable event α2 .
It is verified that LOC∗α1 and LOC∗α2 are control equivalent to SUP∗ in controlling the plant SF∗ ,
i.e.
L(SF) ∩ L(LOC∗α1 ) ∩ L(LOC∗α2 ) = L(SFf )
∗

(30)

S(SF) ∩ lim(L(LOC∗α1 )) ∩ lim(L(LOC∗α1 )) = S(SFf ).
∗

(31)

26

0

0

5
1

0

5

3

2

2

0

3

1

4
4

ω
ω
Fig. 13. Liveness local controllers LOCω
α1 ,1 and LOCα1 ,2 for controllable event α1 and liveness local controllers LOCα1 ,1

and LOCω
α1 ,2 for α2

Then, applying the localization procedure in Section IV-A, we get two liveness local controllers
LOCωα1 ,1 and LOCωα1 ,2 for event α1 , and two liveness local controllers LOCωα2 ,1 and LOCωα2 ,2 for

event α2 , as displayed in Fig. 13.
Note that the liveness local controller LOCωα1 ,1 (resp. LOCωα2 ,1 ) has only one state, namely event α1
need not be disabled at all the strings s ∈ pre(A). This control logic is consistent with SUPω : comparing
the transition structures of SUP∗ and SUPω , for all the states in SUPω arrived by strings in pre(A),
event α1 (resp. α2 ) is not disabled.
To illustrate the control logics of the liveness local controllers LOCωα1 ,2 and LOCωα2 ,2 , we consider
control action of LOCωα1 ,2 on α1 in the following cases. First, assume that the string s = α1 β1 γ1 has
occurred; LOCωα1 ,2 arrives state 1, and by inspecting the transition diagram of LOCωα1 ,2 , α1 is enabled,
consistent with SUPω . Then, assume that the string t = α1 β1 γ1 α1 β1 γ1 has occurred; now LOCωα1 ,2
arrives state 4, and we can see that α1 is disabled by LOCωα1 ,2 . Again the control logic is consistent
with that of SUPω .
It is also verified these four local controllers achieve the same controlled behavior with SUPω , in

27
Communication

Fig. 14.

Distributed control architecture for SF

controlling the plant SFf . i.e.
∗

L(SFf ) ∩ L(LOCωα1 ,1 ) ∩ L(LOCωα1 ,2 )
∗

∩ L(LOCωα2 ,1 ) ∩ L(LOCωα2 ,2 ) = L(SFf

∗

∧f ω

)

(32)

S(SFf ) ∩ lim(L(LOCωα1 ,1 )) ∩ lim(L(LOCωα1 ,2 ))
∗

∩ lim(L(LOCωα2 ,1 )) ∩ lim(L(LOCωα2 ,2 )) = S(SFf

∗

∧f ω

).

(33)

Combining (30) and (32), (31) and (33), we conclude that the above two safety local controllers LOC∗α1
and LOC∗α2 and the four liveness local controllers LOCωα1 ,1 , LOCωα1 ,2 , LOCωα2 ,1 and LOCωα2 ,2 achieve
the same finite controlled behavior L(SFf

∗

∧f ω

) and infinite controlled behavior S(SFf

∗

∧f ω

), as SUP∗

and SUPω , with respect to the plant SF.
Finally, with the derived local controllers, we build a distributed control architecture for the small
factory SF; see Fig. 14 of which the controlled behavior satisfies the given specifications (S1) - (S4).
VI.

C ONCLUSIONS

We have presented an extension of supervisor localization procedure to solve the distributed control
problem of multi-agent DES with infinite behavior. We first employed Thistle and Wonham’s supervisory
control theory for DES with infinite behavior to compute a safety supervisor (for safety specifications)
and a liveness supervisor (for liveness specifications), and implement them by ∗-automata. Then we
proposed a new supervisor localization theory to decompose the safety and liveness supervisors into a
set of safety local controllers one for each controllable event, and a set of liveness local controllers two
for each controllable event, respectively. Moreover, we have proved that the derived local controllers
achieve the same controlled behavior with the safety and liveness supervisors. Finally, a Small Factory
example has been presented for illustration. In future research we shall consider the supervisory control
and distributed control of DES with infinite behavior under partial observation.

28

A PPENDIX A
E FFECTIVE S YNTHESIS

OF

S UPERVISOR f ω

To construct a complete and deadlock-free supervisor f ω described in Section II-B, we need to compute
sup C ω (El ) and inf F ω (A) in advance. Without lose of generality, we assume that A ⊆ El ⊆ S(G).

If this assumption does not hold, we may replace El and A by El′ := El ∩ S(G) and A′ := El′ ∩ A
respectively; El′ and A′ will be treated as the new maximal legal specification and minimal acceptable
specification, but represent the same requirements on G.
Define a deterministic Rabin-Büchi automaton
A = (Q′ , Σ, δ′ , q0′ , {(Rp′ , Ip′ ) : p ∈ P ′ }, BQ′ )

(34)

such that the ∗-automaton (Q′ , Σ, δ′ , q0′ ) accepts the ∗-behavior L(G) ⊆ Σ∗ of G, the Büchi automaton
(Q′ , Σ, δ′ , q0′ , BQ′ ) accepts the ω -behavior S(G) ⊆ Σ∗ of G, and the Rabin automaton (Q′ , Σ, δ′ , q0′ , {(Rp′ , Ip′ ) :
p ∈ P ′ }) accepts the specification El ⊆ S(G) (such an automaton can be constructed from the DES model
G in (1) and a Rabin automaton accepting El ). Note that if S(G) is ω -closed, then by Proposition 5.6

in [10] it is redundant for the supervisor synthesis, and thus we can assume that S(G) = lim(L(G)). In
that case, it can be interpreted as an absence of liveness assumptions in the modelling of the uncontrolled
DES. Namely, in the DES model G in (1), we may drop the Büchi acceptance criterion. Moreover,
the computation of sup C ω (El ) is different from that when the liveness assumptions are considered; for
details, see [10, Chapter 7].
First, the computation of sup C ω (El ) begins with computing the controllability subset C A ⊆ Q′ of A
in (34). The subset C A , together with a map
φA : C A → Γ,

can be obtained by the subset construction algorithm in [11], which recursively applies the fixpoint
calculus method [21]. By Theorem 8.12 in [10], the deterministic Rabin automaton
Asup = (Q′ , Σ, δ′ , q0′ , {(Rp′ , Ip′ ) : p ∈ P ′ }) | C A

(35)

accepts the ω -language sup C ω (El ). Here the operator ‘|’, restriction to the subset C A ⊆ Q′ , turns all other
states into degenerate states [10] that do not satisfy the Rabin acceptance condition {(Rp′ , Ip′ ) : p ∈ P ′ }.
Note that Asup is a deterministic Rabin automaton because A is deterministic and the operator ‘|’ does
not change this property.
Second, to compute inf F ω (A), we have by Proposition 5.8 in [10], inf F ω (A) = clo(A) ∩ S(G).
Given a deterministic Rabin automaton which accepts the ω -language A, we construct a deterministic

29

Rabin automaton Ainf accepting inf F ω (A) by: first construct an ω -automaton accepting clo(A), and
then intersect it with G which accepts the ω -language S(G).
Now that we have
(i) a deterministic Rabin automaton Asup accepting sup C ω (El ),
(ii) a controllability subset C A together with a map φA : C A → Γ,
(iii) a deterministic Rabin automaton Ainf accepts inf F ω (A),
we may check the existence of the supervisor f ω and construct it if exists.
The existence verification of f ω is equivalent to checking the containment inf F ω (A) ⊆ sup C ω (El ); it
suffices to test the automaton Ainf /Asup accepting inf F ω (A)/ sup C ω (El ) for emptiness. Ainf /Asup can
be obtained by intersect Ainf with the complement of Asup . When the answer is yes, f ω is constructed
as follows.
(i) Write Asup = (Q′′ , Σ, δ′′ , q0′′ , {(Rp′′ , Ip′′ ) : p ∈ P ′′ }); Asup is the deterministic Rabin automaton
accepting E ′ := sup C ω (El ). Then a subset Q′′m ⊆ Q′′ can be computed such that the ∗-automaton
(Q′′m , Σ, δ′′ , q0′′ ) accepts pre(E ′ ). Because E ′′ is ∗-controllable with respect to L(G) (the finite

behavior represented by A), we may define the map φ0 : Q′′m → Γ as
φ0 (q ′′ ) := {σ ∈ Σ|δ(q ′′ , sσ) ∈ Q′′m };

then by the proof of Proposition 4.4 [10], the map f0ω : Σ∗ → Γ given by
f0ω (k) := φ0 (δ′′ (q0′′ , k))

is a complete, deadlock-free supervisor for G that synthesizes the ∗-language pre(E ′ ) and the
ω -language clo(E ′ ) ∩ S(G).

(ii) For each k ∈ pre(E ′ ), let q ′′ = δ′′ (q0′′ , k), and let A′′q = (Q′′ , Σ, δ′′ , q ′′ , {(Rp′′ , Ip′′ ) : p ∈ P }). Define
fkω : Σ∗ → Γ as
fkω (l/k) := φA (δ′′ (q ′′ , l/k)),

where φA : Q′′ → Γ is obtained in the process of computing the controllability subset C A (according
to (35), Q′′ is isomorphic to C A ). It is shown in Theorem 5.9 [10] that fkω : Σ∗ → Γ is a complete,
deadlock-free supervisor for A′′q , which synthesizes some ω -sublanguage Ek′ ⊆ E ′ /k.
(iii) Define the supervisor
f ω : Σ∗ → Γ

(36)

30

according to:



if l ∈ pre(A)
f ω (l)

 0
f ω (l) :=
if l ∈ k pre(Ek′ ) where k ∈ M
fkω (l/k)



 undefined otherwise

where M is the set of all elements of pre(E ′ )/pre(inf F ω (A)) of minimal length.
It is shown by [12, Theorem 5.3] that f ω : Σ∗ → Γ defined above is a complete, deadlock-free
supervisor for G, and the controlled behaviors of G satisfy conditions (9) and (10).
A PPENDIX B
S UPERVISOR S YNTHESIS

OF

SUPω IN S MALL FACTORY E XAMPLE

In the following, we adopt the supervisor synthesis procedure for DES with infinite behavior in
Appendix A (reduced from the synthesis procedure in [22]) to construct a supervisor SUPω satisfying
the maximal legal liveness specifications El and containing the minimal acceptable liveness specification
A. Recall that SFf is the new plant to be controlled, with finite behavior L(SFf ) and infinite behavior
∗

∗

S(SFf ).
∗

Step (i): Compute sup C ω (El ) and inf F(A). First, to compute sup C ω (El ), we construct a Rabin-Büchi
automaton
A = (Q′ , Σ, δ′ , q0′ , {(Rp′ , Ip′ ) : p ∈ P ′ }, BQ′ )

as in (34) such that the ∗-automaton (Q′ , Σ, δ′ , q0′ ) accepts the ∗-behavior
L′ := L(SFf ) ∩ pre(El ),
∗

the Büchi automaton (Q′ , Σ, δ′ , q0′ , BQ′ ) accepts the ω -behavior
S ′ := S(SFf ) ∩ clo(El ),
∗

and the Rabin automaton (Q′ , Σ, δ′ , q0′ , {(Rp′ , Ip′ ) : p ∈ P ′ }) accepts
E ′ := S(SFf ) ∩ El .
∗

The transition structure of A is displayed in Fig.15, where Q′ = {0, 1, ..., 26}, the Büchi acceptance criterion is BQ′ = {1, 2, 3, 4, 5, 6, 7, 8, 9, 14}, and the Rabin acceptance criterion is {(R1′ = {6, 7, 9, 14}, I1′ =
Q′ )}.

It is easily verified that E ′ ⊆ S ′ ⊆ lim(L′ ) and thus by the controllability subset construction algorithm
proposed in [11], we compute the controllability subset C A = Q′ = {0, ..., 26}, together with a map
φA : C A → Γ, as listed in Table I) (in the table, for each q ∈ Q′ , Eδ (q) := {σ ∈ Σ|δ(q, σ)!}).

31

14

20

26

17

8

16

11

23

2

4

7

13

22

1

3

6

10

25

5

19

12

24

9

15

21

18

0

Fig. 15.

Transition structure of Rabin-Büchi automaton A
TABLE I.

S TATE MAP φA : C A → Γ

Q′

0

1

2

3

4

5

6

7

8

9

10

11

12

13

Eδ

α1 , α2

β1

β2

γ1 , α2

α1 , γ2

α1 , α2

γ1 , β2 ,

β1 , γ2

α1 , α2

β2

β2

γ1 , γ2

γ1 , γ2

β1

A

α1 , α2

β1

β2

γ1 , α2

α1 , γ2

α2

γ1 , β2 ,

β1 , γ2

α1

β2

β2

γ1 , γ2

γ1 , γ2

β1

′

14

15

16

17

18

19

20

21

22

23

24

25

26

Eδ

β1

α1 , γ2

α1 , γ2

γ1 , α2

α1 , γ2

γ1 , α2

γ1 , α2 ,

β1 , γ2

α1 , α2

γ1 , β2

β1 , γ2

α1 , α2

γ1 , β2

A

β1

γ2

α1 , γ2

γ1

γ2

γ1 , α2

γ1 ,

β1 , γ2

α1

γ1 , β2

β1 , γ2

α2

γ1 , β2

φ

Q

φ

Then, from A and its controllability subset C A , we construct as in (35) a Rabin automaton Aω accepting
sup C ω (E ′ ). Since C A = Q′ , Aω := (Q′ , Σ, δ′ , q0′ , {(Rp′ , Ip′ ) : p ∈ P ′ }), namely
sup C ω (E ′ ) = S(Aω ) = E ′ .

Hence E ′ is ω -controllable, but need not be ω -closed; indeed, E ′ is not ω -closed, because s = α2 β2 α1 β1
(γ1 α2 β1 )∗ γ2 γ1 (α1 β1 γ1 )ω belongs to E ′ , but clo(s) does not.

Finally, inspecting the transition structure of MINSPEC representing the minimal acceptable language A, we have A = S(MINSPEC) = lim(L(MINSPEC)) = clo(S(MINSPEC)) = clo(A),

32

where clo(A) is the ω -closure of A (for definition see (4)); thus
inf F ω (A) = clo(A) ∩ S ′ = A.

It is verified that
inf F ω (A) ⊆ sup C ω (E ′ ).

Hence by [12, Theorem 5.3] there exists a complete, deadlock-free supervisor f ω such that A ⊆
S(SFf

∗

∧f ω

) ⊆ E ′ ⊆ E , where SFf

∗

∧f ω

is the new plant SFf under the control of f ω .
∗

Step (ii): Synthesize supervisor f ω : Σ∗ → Γ. We first construct a supervisor f0ω : Σ∗ → Γ according
to f0ω (s) = Eδ (δ(q0 , s)), which synthesizes ∗-language E ′′ := pre(sup C ω (E ′ )). Then, for each k ∈ E ′′ ,
let q = δ′ (q0′ , k); we construct a supervisor fkω : Σ∗ → Γ according to fkω (l/k) = φA (δ′ (q, l/k)),
which synthesizes some sublanguage Ek′′ ⊆ E ′′ /k. Next, write MINSPEC = (Z, Σ, ζ, z0 , BZ ) where
Z = {0, 1, ..., 5}, ζ is a partial function as displayed in Fig. 9, and GZ = {0}; we extend the transition

function of MINSPEC to total function by adding an extra state 6, (i.e. Z = {0, 1, ..., 6}) and adding
the transition (z, σ, 6) for every state z ∈ Z including 6 if σ is not defined at z .
Now, we are ready to construct a supervisor f ω : Σ∗ → Γ (as in (36)), according to:



if l ∈ pre(A)
f ω (l)

 0
f ω (l) :=
fkω (l/k)
if l ∈ k pre(Ek′′ ) where k ∈ M



 undefined otherwise

where M is the set of all elements of pre(E ′′ )/pre(A) of minimal length. The supervisor f ω can be
expressed by the state map ψ : (Q′ , Z) → Γ (as listed in Table II) in the form of f ω (s) = ψ((δ′ ×
ζ((q0′ , z0 ), s)). In Table II, Eδ′ ,ζ (q, z) := {σ ∈ Σ|δ′ (q, σ)!&ζ(z, σ)!}. Note that if a string l ∈ pre(A),

then it arrives the state pairs (q, z) with z = 0, ..., 5 and in this case, f ω (l) = f0ω (l); otherwise, it arrives
the state pairs (q, z) with z = 6 and in this case, f ω (l) = fkω (l/k).
Under the control of f ω , as described in Section III, the behavior of the new plant SFf can be
∗

represented by a deterministic Büchi automaton SFf

∗

∧f ω

, as displayed in Fig.11 (the Büchi acceptance

criterion is B = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 15, 16, 23, 29, 30}). It is easily verified that the controlled
behavior satisfies all the specifications in the following sense:
L(SFf

∗

∧f ω

) ⊆ Es

A ⊆ S(SFf

∗

∧f ω

(safety specifications (S1) and S2)

) ⊆ El (liveness specifications (S3) and (S4))

33

S TATE MAP ψ : Q′ × Z → Γ

TABLE II.

(Q′ × Z)

(0,0)

(1,1)

(2,6)

(3,2)

(4,6)

(5,3)

(6,6)

(7,6)

(8,6)

(1,6)

(9,4)

(10,6)

Eδ,ζ

α1 , α2

β1

β2

γ1 , α2

α1 , γ2

α1 , α2

γ1 , β2 ,

β1 , γ2

α1 , α2

β1

β2

β2

ψ

α1 , α2

β1

β2

γ1 , α2

α1 , γ2

α1 , α2

γ1 , β2 ,

β1 , γ2

α1

β1

β2

β2

′

(Q × Z)

(11,6)

(12,6)

(13,6)

(14,6)

(3,6)

(15,5)

(16,6)

(17,6)

(18,6)

(19,6)

(20,6)

(5,6)

Eδ

γ1 , γ2

γ1 , γ2

β1

β1

γ1 , α2

α1 , γ2

α1 , γ2 ,

γ1 , α2

α1 , γ2

γ1 , α2

γ1 , α2

α1 , α2

ψ

γ1 , γ2

γ1 , γ2

β1

β1

γ1 , α2

α1 , γ2

α1 , γ2 ,

γ1

γ2

γ1 , α2

γ1

α2

′

(Q × Z)

(21,6)

(22,0)

(22,6)

(23,6)

(24,6)

(25,6)

(26,6)

(9,6)

(14,1)

(15,6)

(20,2)

(25,3)

Eδ

β1 , γ2

α1 , α2

α1 , α2

γ1 , β2

β1 , γ2

α1 , α2

γ1 , β2 ,

β2

β1

α1 , γ2

γ1 , α2

α1 , α2

ψ

β1 , γ2

α1 , α2

α1

γ1 , β2

β1 , γ2

α2

γ1 , β2 ,

β2

β1

γ2

γ1 , α2

α1 , α2

Step (iii): Implement f ω by ∗-automaton SUPω . The above function-based supervisor f ω can be
implemented by a ∗-automaton SUPω as displayed in Fig. 11, i.e.
L(SFf ) ∩ L(SUPω ) = L(SFf

∗

∧f ω

)

S(SFf ) ∩ lim(L(SUPω )) = S(SFf

∗

∧f ω

)

∗

∗

SUPω has the same transition structure with SFf

∗

∧f ω

.

R EFERENCES
[1] K. Cai and W. M. Wonham, “Supervisor localization: a top-down approach to distributed control
of discrete-event systems,” IEEE Transactions on Automatic Control, vol. 55, no. 3, pp. 605–618,
2010.
[2] K. Cai and W. Wonham, “Supervisor localization for large discrete-event systems: case study
production cell,” International Journal of Advanced Manufacturing Technology, vol. 50, no. 9-12,
pp. 1189–1202, 2010.
[3] R. Zhang, K. Cai, Y. Gan, Z. Wang, and W. Wonham, “Supervision localization of timed discreteevent systems,” Automatica, vol. 49, no. 9, pp. 2786–2794, 2013.
[4] K. Cai and W. Wonham, “New results on supervisor localization, with case studies,” Discrete Event
Dynamic Systems, vol. 25, no. 1-2, pp. 203–226, 2015.
[5] K. Cai and W. M. Wonham, Supervisor Localization: A Top-Down Approach to Distributed Control

34

of Discrete-Event Systems. Lecture Notes in Control and Information Sciences, vol. 459, Springer,
2015.
[6] R. Zhang, K. Cai, and W. Wonham, “Supervisor localization of discrete-event systems under partial
observation,” Automatica, vol. 81, pp. 142–147, 2017.
[7] W. Wonham, Supervisory Control of Discrete-Event Systems.

Systems Control Group,

ECE Dept., University of Toronto, Toronto, ON, Canada, September 2017, available at
http://www.control.utoronto.ca/DES.
[8] P. Ramadge, “Some tractable supervisory control problems for discrete-event systems modeled by
Büchi automata,” IEEE Transactions on Automatic Control, vol. 34, no. 1, pp. 10–19, 1989.
[9] S. Young, D. Spanjol, and V. Garg, “Control of discrete-event systems modeled with deterministic
Büchi automata,” in Proc. 1992 American Control Conference, Chicago, IL, June 24-26 1992, pp.
2809–2813.
[10] J. Thistle, “Control of infinite behavior of discrete event systems,” Ph.D. dissertation, Systems
Control Group, Dept. Electrical Engineering, University of Toronto, 1991.
[11] J. Thistle and W. Wonham, “Control of infinite behavior of finite automata,” SIAM Journal on
Control and Optimization, vol. 32, no. 4, pp. 1075–1097, 1994.
[12] ——, “Supervision of infinite behavior of discrete-event systems,” SIAM Journal on Control and
Optimization, vol. 32, no. 4, pp. 1098–1113, 1994.
[13] R. Kumar, V. Garg, and S. Marcus, “On supervisory control of sequential behaviors,” IEEE
Transactions on Automatic Control, vol. 37, no. 12, pp. 1978–1985, 1992.
[14] J. Thistle, “On control of systems modelled as deterministic rabin automata,” Discrete Event Dynamic
Systems: Theory and Applications, vol. 5, no. 4, pp. 357–381, 1995.
[15] J. Thistle and H. Lamouchi, “Effective control synthesis for partially observed discrete-event
systems,” SIAM Journal on Control and Optimization, vol. 48, no. 3, pp. 1858–1887, 2009.
[16] P. Ramadge and W. Wonham, “Supervisory control of a class of discrete event processes,” SIAM
Journal on Control and Optimization, vol. 25, no. 1, pp. 206–230, 1987.
[17] M. Mukund, Modern Applications of Automata Theory.

World Scientific, 2012, ch. Finite-State

Automata on Infinite Inputs, pp. 45–78, available at http:/doi.org/10.1142/9789814271059 0002.
[18] J. Thistle and W. Wonham, “Supervision of infinite behavior of discrete-event systems,” SIAM
Journal on Control and Optimization, vol. 32, no. 4, pp. 1098–1113, 1994.
[19] L. Lamport, “Proving the correctness of multiprocess programs,” ACM Transactions on Software
Engineering, vol. SE-3, no. 2, pp. 125–143, 1977.

35

[20] C. Golaszewski and P. Ramadge, “Control of discrete event processes with forced events,” in Proc.
26th IEEE Conference on Decision and Control, Los Angeles, CA, 1987, pp. 247–251.
[21] E. Emerson and C. Lei, “Efficient model checking in fragments of the propositional mu-calculus,”
in Proc. IEEE Symposium on Logic in Computer Science, 1986, pp. 267–278.
[22] J. Thistle, “Control of infinite behavior of discrete event systems,” Ph.D. dissertation, Systems
Control Group, Dept. Electrical Engineering, University of Toronto, 1991.

