Supervisory control and reactive synthesis: a comparative introduction

Abstract

This paper presents an introduction to and a formal connection between synthesis problems for discrete event systems that have been considered, largely separately, in the two research communities of supervisory control in control engineering and reactive synthesis in computer science. By making this connection mathematically precise in a paper that attempts to be as self-contained as possible, we wish to introduce these two research areas to non-expert readers and at the same time to highlight how they can be bridged in the context of classical synthesis problems. After presenting general introductions to supervisory control theory and reactive synthesis, we provide a novel reduction of the basic supervisory control problem, non-blocking case, to a problem of reactive synthesis with plants and with a maximal permissiveness requirement. The reduction is for fully-observed systems that are controlled by a single supervisor/controller. It complements prior work that has explored problems at the interface of supervisory control and reactive synthesis. The formal bridge constructed in this paper should be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas.

Appendices

A Proof of theorem 1

We use the formalism defined in Section 2.1 to show that the concept of maximally permissive solution, which is a central requirement in problem BSCP-NB of Section 2.1.8, is well defined. This will provide a proof of Theorem 1 that is self-contained.

For this purpose, we must first define the disjunction of two supervisors.

Let G be a DES plant and let S ₁,S ₂ be two supervisors for G. We define S ₁∪S ₂ to be a new supervisor, denoted by S _1∪2 for G, such that S _1∪2(σ) = S ₁(σ)∪S ₂(σ) for all σ∈E ^∗. We call S _1∪2 the disjunction of S ₁ and S ₂, since S _1∪2 allows all strings that S ₁ and S ₂ respectively allow.

We now wish to characterize the controlled behavior $\mathcal {L} (S_{1\cup 2}/G)$ under the disjunction of S ₁ and S ₂. Recall that when S _i is applied to G in isolation, the definition of S _i over $E^{*} \setminus \mathcal {L}(S_{i}/G)$ is irrelevant, since these strings will never occur in the controlled system. However, in the context of disjunction, this is no longer true since the controlled behavior will in general exceed $\mathcal {L}(S_{i}/G)$ due to the actions of the other supervisor(s). In order to allow for a simple characterization of $\mathcal {L} (S_{1\cup 2}/G)$, we make the following assumption:

$$ S_{i} (\sigma) = E_{uc} \text{~for all~} \sigma \in E^{*} \setminus \mathcal{L}(S_{i}/G). $$

(3)

We refer to supervisors that satisfy this assumption as “ G-matched supervisors.”

We can think of S _i as being “out of range” when the controlled language leaves $\mathcal {L}(S_{i}/G)$. Hence, when this occurs, S _i will not enable any events, other than uncontrollable ones, as it assumes that the controlled behavior is now in the range of another supervisor. Any supervisor $S^{\prime }_{i}$, when applied in isolation to G, can be replaced by a G-matched one, S _i , that results in the same controlled behavior $\mathcal {L} (S^{\prime }_{i}/G) = \mathcal {L}(S_{i}/G)$.

It follows directly from the G-matched assumption and from the definition of disjunction that

$$ \mathcal{L} (S_{1\cup 2}/G) = \mathcal{L}(S_{1}/G) \cup \mathcal{L} (S_{2}/G) . $$

(4)

Since marking is a property of the plant, we similarly have that

$$\begin{array}{@{}rcl@{}} \mathcal{L}_{m} (S_{1\cup 2}/G) & = & \mathcal{L}(S_{1\cup 2}/G) \cap \mathcal{L}_{m}(G) \end{array} $$

(5)

$$\begin{array}{@{}rcl@{}} & = & [ \mathcal{L}(S_{1}/G) \cup \mathcal{L} (S_{2}/G) ] \cap \mathcal{L}_{m}(G) \end{array} $$

(6)

$$\begin{array}{@{}rcl@{}} & = & [ \mathcal{L}(S_{1}/G) \cap \mathcal{L}_{m}(G) ] \cup \left[\right. \mathcal{L} (S_{2}/G)\left.\right) \cap \mathcal{L}_{m}(G)\left.\right] \end{array} $$

(7)

$$\begin{array}{@{}rcl@{}} & = & \mathcal{L}_{m}(S_{1}/G) \cup \mathcal{L}_{m}(S_{2}/G) \end{array} $$

(8)

Remark 5 (Supervisor disjunction)

It is worth noting that, without the assumption in Eq. (3), the closed-loop language under disjunction of supervisors may not be the union of their respective languages. As an example, consider again plant G ₃ of Fig. 5, with L _{a m} :={ε,c ₁}. Consider supervisors S ₁ and S ₂ where S ₁ always disables c ₁ and enables c ₂, whereas S ₂ always disables c ₂ and enables c ₁. Both S ₁ and S ₂ are non-blocking for G ₃, because all states in the closed-loop system are accepting. Moreover, both S ₁ and S ₂ are safe w.r.t. the above L _{a m} . Indeed, S ₂ always disables c ₂, while S ₁, by disabling c ₁, prevents G ₃ from reaching state x ₁, thus indirectly preventing c ₂. However, S ₁∪S ₂ is not safe, since it allows both c ₁ and c ₂ at any state.

The following result establishes a key property of supervisor disjunction.

Theorem 5

Let G be a DES plant and let $L_{am} \subseteq \mathcal {L}_{m}(G)$ be the admissible marked language. If S ₁ ,S ₂ are two non-blocking and safe supervisors that are G-matched,

then S ₁ ∪S ₂ is also a non-blocking and safe supervisor, and it is G-matched.

Proof

We have that $\overline {\mathcal {L}_{m}(S_{i}/G)} = \mathcal {L}(S_{i}/G)$ and $\mathcal {L}_{m}(S_{i}/G) \subseteq {L_{am}}$, for i=1,2.

Safety: Clearly,

$$\mathcal{L}_{m}(S_{1\cup 2}/G) = \mathcal{L}_{m}(S_{1}/G) \cup \mathcal{L}_{m}(S_{2}/G) \subseteq {L_{am}} $$

and thus S ₁∪S ₂ is a safe supervisor.

Non-blockingness: Since prefix-closure can be distributed over union (the proof of this fact is straightforward), we have that

$$\begin{array}{@{}rcl@{}} \overline{\mathcal{L}_{m}(S_{1 \cup 2}/G)} &=& \overline{\mathcal{L}_{m}(S_{1}/G) \cup \mathcal{L}_{m}(S_{2}/G)} \end{array} $$

(9)

$$\begin{array}{@{}rcl@{}} &=& \overline{\mathcal{L}_{m}(S_{1}/G)} \cup \overline{\mathcal{L}_{m}(S_{2}/G)} \end{array} $$

(10)

$$\begin{array}{@{}rcl@{}} &=& \mathcal{L}(S_{1}/G) \cup \mathcal{L}(S_{2}/G) \end{array} $$

(11)

$$\begin{array}{@{}rcl@{}} &=& \mathcal{L}(S_{1 \cup 2}/G). \end{array} $$

(12)

which proves that S ₁∪S ₂ is a non-blocking supervisor.

Finally, it is clear that S _1∪2 is G-matched as it inherits this property from the definitions of S ₁ and S ₂ outside of $\mathcal {L}(S_{1 \cup 2}/G)$.

Corollary 3

Theorem 5 holds for infinite disjunctions of supervisors.

Proof

All steps in the proof of Theorem 5 hold for an arbitrary number of disjunctions.

The hypothesis of Theorem 1 is that there exists at least one non-blocking supervisor for G that is safe w.r.t. L _{a m} . If there exists a single supervisor with these properties, then it is necessarily the unique desired S _{m p n b} , as no other safe non-blocking supervisor exists. Let us assume then that there are several safe and non-blocking supervisors. If a supervisor S is not G-matched, then we can always make it G-matched without changing $\mathcal {L}(S/G)$ or $\mathcal {L}_{m}(S/G)$. By taking the disjunction of all G-matched non-blocking supervisors for G that are safe w.r.t. L _{a m} , we obtain a unique G-matched supervisor that is also safe and non-blocking by Corollary 3; let us denote it by $S_{disj}^{G}$. Then $\mathcal {L}_{m}(S_{disj}^{G})$ contains all the sublanguages of L _{a m} that can be achieved by any safe and non-blocking supervisor. Otherwise, if the sublanguage of L _{a m} achieved by one supervisor is not contained in $\mathcal {L}_{m}(S_{disj}^{G})$, then the G-matched version of that supervisor would not have been added in the disjunction of all G-matched safe and non-blocking supervisors, a contradiction.

Once we have the unique maximally-permissive closed-loop behavior $\mathcal {L}_{m}(S_{disj}^{G})$, we take S _{m p n b} to be the unique maximally permissive supervisor that achieves it. To obtain S _{m p n b} , we simply add to $S_{disj}^{G}$ all infeasible (in G) controllable events for strings in $\mathcal {L}(S_{disj}^{G} / G)$ and all controllable events for strings in $E^{*} \setminus \mathcal {L}(S_{disj}^{G} /G)$. Since $\mathcal {L}(S_{mpnb}/G) = \mathcal {L}(S_{disj}^{G}/G)$ and $\mathcal {L}_{m}(S_{mpnb}/G) = \mathcal {L}_{m}(S_{disj}^{G}/G)$, then S _{m p n b} is non-blocking for G and safe w.r.t. L _{a m} . S _{m p n b} is not G-matched anymore, but this is of no consequence in the later developments in the paper.

This completes the proof of Theorem 1.

B Proof of theorem 2

First, we state and prove the following lemma.

Lemma 5

Let G=(X,x ₀ ,X _m ,E,δ), $L_{am}\subseteq \mathcal {L}_{m}(G)$ , and assume that L _am is $\mathcal {L}_{m}(G)$ -closed. Let A be a complete DFA such that $\mathcal {L}_{m}(A)=L_{am}$. Let S be a supervisor for G, and therefore also for G×A. Then, the following hold:

• 1. If S is non-blocking for plant G×A, then S is non-blocking for plant G.

• 2. If S is non-blocking for plant G×A, then S is safe for plant G w.r.t. L _am .

• 3. If S is non-blocking for plant G and safe for plant G w.r.t. L _am , then S is non-blocking for plant G × A.

• 4. S is safe for plant G×A w.r.t. $\mathcal {L}_{m}(G\times A)$.

Proof

• 1. To show that S is non-blocking for G, we need to show $\mathcal {L}(S/G)\subseteq \overline {\mathcal { L}_{m}(S/G)}$. Let $\sigma \in \mathcal {L}(S/G)$. We need to find σ ^′ such that $\sigma \cdot \sigma ^{\prime } \in \mathcal {L}_{m}(S/G)$. We know that $\sigma \in \mathcal {L}(S/G\times A)$ because A is complete. Also, S is non-blocking for G×A, thus $\sigma \in \overline {\mathcal {L}_{m}(S/G\times A)}$. Therefore there exists σ ^′ such that $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(S/G\times A)$. By definition of the marked states of G×A, both G and A accept σ⋅σ ^′. Therefore, $\sigma \cdot \sigma ^{\prime } \in \mathcal {L}_{m}(S/G)$.

• 2. To show that S is safe for G w.r.t. L _{a m} , we need to show $\mathcal {L}_{m}(S/G) \subseteq L_{am}$. Let $\sigma \in \mathcal {L}_{m}(S/G)$. We need to show σ∈L _{a m} . $\sigma \in \mathcal {L}_{m}(S/G)$ implies $\sigma \in \mathcal { L}(S/G)$, and therefore $\sigma \in \mathcal {L}(S/G\times A)$ because A is complete. Consider the (unique) run of G×A on σ. We claim that this run ends on a product state that is marked for both G and A. $\sigma \in \mathcal {L}_{m}(S/G)$, therefore the product state must indeed be marked for G. We show that $\sigma \in \mathcal {L}_{m}(A)$ which implies that the product state is also marked for A. Since S is non-blocking for G×A, there exists σ ^′ such that $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(S/G\times A)$. But this means $\sigma \cdot \sigma ^{\prime }\in \mathcal { L}_{m}(A)$, which implies $\sigma \in \overline {\mathcal {L}_{m}(A)}$. Also, $\sigma \in \mathcal {L}_{m}(S/G)$ implies $\sigma \in \mathcal {L}_{m}(G)$. Therefore, we have $\sigma \in \mathcal {L}_{m}(G)\cap \overline {\mathcal {L}_{m}(A)}$.

  Since $\mathcal {L}_{m}(A)$ (i.e., L _{a m} ) is $\mathcal {L}_{m}(G)$-closed, $\sigma \in \mathcal {L}_{m}(A)$.

• 3. To show that S is non-blocking for plant G×A, we need to show $\mathcal {L}(S/G\times A) \subseteq \overline {\mathcal {L}_{m}(S/G\times A)}$. Let $\sigma \in \mathcal {L}(S/G\times A)$. We need to find σ ^′ such that $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(S/G\times A)$. $\sigma \in \mathcal {L}(S/G\times A)$ implies $\sigma \in \mathcal {L}(S/G)$ and $\sigma \in \mathcal {L}(A)$. Since S is non-blocking for G, there exists σ ^′ such that $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(S/G)$. Since $\mathcal {L}_{m}(S/G)\subseteq L_{am}=\mathcal {L}_{m}(A)$, $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(A)$. $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(S/G)$ and $\sigma \cdot \sigma ^{\prime }\in \mathcal { L}_{m}(A)$ implies $\sigma \cdot \sigma ^{\prime }\in \mathcal {L}_{m}(S/G\times A)$. Therefore $\sigma \in \overline {\mathcal {L}_{m}(S/G\times A)}$.

• 4. Trivially, since safe w.r.t. $\mathcal {L}_{m}(G \times A)$ means $\mathcal {L}_{m}(S/G \times A)\subseteq \mathcal { L}_{m}(G \times A)$, which holds for any S.

We can now present the proof of Theorem 2.

Proof

2⇒1 : We need to show that S is non-blocking for G, safe w.r.t. L _{a m} , and maximally-permissive. Non-blockingness follows from Lemma 5, part 1. Safety follows from Lemma 5, part 2.

To show that S is maximally-permissive in G, suppose there exists a non-blocking and safe w.r.t. L _{a m} supervisor S ^′ which is strictly more permissive than S. By Lemma 5, parts 3 and 4, S ^′ is non-blocking for G×A and safe for G×A w.r.t. $\mathcal {L}_{m}(G\times A)$. The fact that S ^′ is strictly more permissive than S in G also means that S ^′ is strictly more permissive than S in G×A. This contradicts the hypothesis that S is maximally-permissive in G×A.

1⇒2 : We need to show that S is non-blocking for G×A, safe for G×A w.r.t. $\mathcal { L}_{m}(G \times A)$, and maximally-permissive. Non-blockingness follows from Lemma 5, part 3. Safety follows from Lemma 5, part 4.

To show that S is maximally-permissive in G×A, suppose there exists a non-blocking supervisor S ^′ for G×A (and also trivially safe w.r.t. $\mathcal {L}_{m}(G\times A)$) which is strictly more permissive than S.

By Lemma 5, parts 1 and 2, S ^′ is non-blocking for G and safe for G w.r.t. L _{a m} . The fact that S ^′ is strictly more permissive than S in G×A also means that S ^′ is strictly more permissive than S in G. This contradicts the hypothesis that S is maximally-permissive in G.

C An algorithm for SSCP

For the sake of completeness of this paper, a simple algorithm to solve SSCP is presented below. The algorithm starts by labeling as Blocking all states that cannot reach a marked state (note that this generally requires reachability analysis). Then the algorithm iterates, repeatedly labeling more states as Blocking, until no more can be labeled. A state is labeled during this iteration, if either it has an uncontrollable successor already labeled, or all its successors are already labeled. At the end, if the initial state is labeled Blocking then no supervisor exists. Otherwise, a state-based supervisor can easily be constructed by avoiding all controllable transitions leading to Blocking states.

The above algorithm essentially computes a fixpoint of a function that takes a set of blocking states and returns those states that have an uncontrollable transition to a blocking successor or all of whose successor states are blocking. The fixpoint evaluation starts from the set of states that do not have a path to a marked state. The algorithm is furthermore an adaptation of the standard algorithm in Wonham and Ramadge (1987) for solving BSCP-NB to the special case of SSCP. Examples of the application of the standard algorithm for solving BSCP-NB can be found in Wonham (2015), Cassandras and Lafortune (2008), for instance.

As a simple example of how the algorithm operates, consider the plant G ₁ of Figure 3. After initialization, Blocking contains a single state, namely x ₂. (Note that x ₁ has no path to itself, but is not considered blocking because it is marked.) After executing the body of the repeat loop no more states are added to the set Blocking. Indeed, no state has an uncontrollable transition to x ₂, therefore the set StatesWithUncontrollablyBlockingSuccs turns out to be empty. The set NewDeadlocks also turns out to be empty because there is no state whose only successors, if any, are blocking, i.e., x ₂ (note that, again, the marked state x ₁ is exempted). Since Blocking does not change, the loop is exited after one iteration. The initial state is not blocking, therefore a supervisor exists and is defined as follows: S(x ₀)={u,c ₁}, S(x ₁) = S(x ₂)={u,c ₁,c ₂}, and S(x ₃)={c ₂}. The computed supervisor corresponds to supervisor S ₂ shown in Fig. 3.