On computing the supremal right-closed control invariant subset of a right-closed set of markings for an arbitrary petri net

Abstract

A set of non-negative integral vectors is said to be right-closed if the presence of a vector in the set implies all term-wise larger vectors also belong to the set. A set of markings is control invariant with respect to a Petri Net (PN) structure if the firing of any uncontrollable transition at any marking in this set results in a new marking that is also in the set. Every right-closed set of markings has a unique supremal control invariant subset, which is the largest subset that is control invariant with respect to the PN structure. This subset is not necessarily right-closed. In this paper, we present an algorithm that computes the supremal right-closed control invariant subset of a right-closed of markings with respect to an arbitrary PN structure. This set plays a critical role in the synthesis of Liveness Enforcing Supervisory Policies (LESPs) for a class of PN structures, and consequently, the proposed algorithm plays a key role in the synthesis of LESPs for this class of PN structures.

1 Introduction

In this paper we consider Petri Net (PN) structures that model Discrete Event Dynamic Systems (DEDS). The PN structure consists of a finite set of places, transitions, and arcs that have weights associated with them. The PN structure is initialized by placing a non-negative number of tokens in each of its places, known as the initial marking, represented as a non-negative integral vector. If the number of tokens in each input place of a transition is no less than the weight associated with the arc from the input place to transition, the transition is said to be enabled. An enabled transition can fire, which results in a different set of tokens associated with each place; that is, the firing of the transition can result in a new marking. This process can be repeated as often as necessary. Each marking of a PN structure is an integral vector whose dimension is the same as the number of places of the PN.

It is of interest to control the behavior of a PN model by supervision such that the markings of the supervised-PN never leaves a desired set. To this end, the set of transitions is partitioned into controllable- and uncontrollable subsets. A supervisory policy can (resp. cannot) prevent the firing of a controllable (resp. uncontrollable) transition that is enabled at a marking of the PN.

A set of integral vectors, which represents different markings of a PN structure, is said to be control invariant with respect to the PN structure if the firing of any uncontrollable transition at any marking that belongs to this set results in a new marking that also belongs to the same set. Stated differently, only the firing of a controllable transition at a marking belonging to a control invariant set of markings will result in a new marking that does not belong to the set. There is a supervisory policy that ensures the markings of a supervised-PN stays within a set of integral vectors if and only if the desired set is control invariant with respect to the PN structure (Ramadge and Wonham 1987).

Every set of integral vectors, corresponding to the markings of a PN, has a unique, largest subset that is control invariant with respect to a given PN structure, identified as its supremal control invariant subset. This follows from the fact that the union of two sets of control invariant markings is also control invariant with respect to the PN structure (Ramadge and Wonham 1987). The supervisory policy of permitting a (controllable) transition at a marking that belongs to the supremal control invariant subset only if its firing results in a new marking that also belongs to the same set, is the minimally restrictive policy that ensures the marking of the PN remains in the original set of markings.

A set of integral vectors is said to be right-closed if the presence of a vector in the set implies all integral vectors that are term-wise larger also belong to the same set (Valk and Jantzen 1985). The empty-set is right-closed by definition. Any vector of a right-closed set which is not term-wise larger than other vectors of the set is known as a minimal element of the right-closed set. Consequently, a non-empty right-closed set is uniquely identified by its finite set of minimal elements.

The supremal control invariant subset of a right-closed set of markings is not necessarily right-closed for a PN structure. However, it always contains a right-closed subset that is control invariant with respect to the PN structure. This follows from the observations that (i) the empty-set is right-closed by definition, (ii) the union of two sets of markings that are control invariant with respect to a PN structure is also control invariant with respect to the PN structure, and (iii) the union of two right-closed sets of markings is also right-closed.

Section 1.1 highlights an important application of supervisory control where it is of interest to identify the supremal right-closed control invariant subset of a right-closed set of markings. In this paper, we present the formal details of an algorithm for computation of the supremal right-closed control invariant subset of a right-closed desirable set with respect to an arbitrary PN structure. Our proposed algorithm, discussed in detail in Section 3, follows an exhaustive search approach based on the Depth-First-Search (DFS) strategy on a decision tree. The results of this paper present the formal treatment of a critical component of a software tool developed for the application reviewed below (Chandrasekaran et al. 2015).

1.1 Motivation

A Discrete Event System is live if, irrespective of the past, all its events can be executed in the future (Alpern and Schneider 1985). Equivalently, a PN is said to be live if all its transitions can be fired, although not immediately, from every reachable marking. A Liveness Enforcing Supervisory Policy (LESP) determines the set of controllable transitions that can be permitted to fire at a marking such that the supervised-PN is live. For any PN structure, the set of initial markings for which there is an LESP is control invariant with respect to its structure. The minimally restrictive LESP effectively prevents the firing of a controllable transition at a marking if its firing would result in a new marking for which no LESP exists. The existence of an LESP for an arbitrary PN structure is undecidable (Sreenivas 1997, 2012). However, there are families of PN structures for which the existence of an LESP is decidable, and for each of these families the above mentioned set of initial markings is right closed, and control invariant with respect to the PN structure (cf. Sreenivas2012; Salimi et al. 2015; Chen et al. 2020). The synthesis of an LESP for any member of these families of PN structures requires the computation of the supremal right-closed control invariant subset of a right-closed set of markings. This paper presents the formal treatment of the algorithm for this important step, which has been used, without formal proof, in the algorithms for LESP-synthesis in reference (Chandrasekaran et al. 2015). Regarding the practical application of our proposed methodology, reference (Khaleghi et al. 2019) provides an example of LESP-synthesis, which necessitates computation of control invariant subset of a right-closed set, in a manufacturing setting. The example in reference (Khaleghi et al. 2019) describes a simplified Petri Net model of an automated system that paints automobile bodies using two paint-booths, and two robots. A more detailed discussion of this practical example is presented in Section 4.3. It should be noted that the LESP-synthesis, as discussed in Khaleghi et al. (2019), involves additional work than just computing the largest right-closed control invariant subset of a given right-closed set.

Prior work that is relevant to the algorithm in this paper is reviewed in the next subsection.

1.2 Prior work

Ramadge and Wonham (1987) considered the synthesis of a supervisory policy that ensures the set of states reachable under supervision is a desired subset of the set of all possible states for a given Discrete Event System (DES). The desired supervisory policy exists if and only if the desired subset is control invariant with respect to the set of states of the DES; that is, if the occurrence of an uncontrollable event at any state within the desired subset results in a new state that is also within the desired subset as well.

There can be instances of supervisory control of DES where the objective of supervisory control is to avoid a set of undesirable states. Kumar and Garg (2005) considered PN models of DES where the undesirable set of states (i.e. markings) are right-closed. That is, if a marking is undesirable, then all term-wise larger markings are undesirable, as well. The goal of supervisory control for this class of problems is to ensure the marking of the PN structure stay within a desired set of markings, which is the complement of the right-closed set of forbidden markings. Kumar and Garg showed that the existence of a supervisory policy for this class of problems is decidable. To illustrate the fact that this class of supervisory control problems are different from the problem considered in this paper, we note that the supremal control invariant subset of desired markings for this class of problems is also a complement of a right-closed set of markings (cf. Lemma 2, Section IV, Kumar and Garg 2005). This is not the case for the class of problems considered in this paper, in that the supremal control invariant subset of the desirable set of right-closed markings is not necessarily right-closed.

There is a large volume of literature on liveness enforcement in PN models of DES systems that do not invoke Ramadge and Wonham’s Theory of Supervisory Control (Ramadge and Wonham 1987). Most of these approaches augment the existing PN structure with additional structure, using concepts from the theory of PNs (Murata 1989; Peterson 1981), to arrive at a new PN structure that satisfies the desired property. These approaches involve the use of linear constraints, place-invariants, and other artefacts from PN theory to arrive at the required structural modifications. References (Moody and Antsaklis 1998; Iordache and Ansaklis 2006) consider situations where linear inequalities, if known in advance to enforce liveness, can be enforced by the use of monitor-places. To synthesize minimally restrictive, closed-loop liveness for a class of Marked Graph Petri Nets, Basile et al. (2009) provided sufficient conditions enforced by Generalized Mutual Exclusion Constraints (GMECs). Proposing a constraint transformation/constrain reduction approach, Luo and Nonami (Luo and Nonami 2011) investigated the problem of eliminating redundant constraints in synthesis of supervisory policies, which can result in reduction of the number of monitors in invariant-based supervisors. Dideban and Alla (2008) introduced a set of linear constraints that prevents reachability of specific states. They presented the concept of over-state in order to build the simplest constraints, which forbid a greater number of states and which reduces the number of monitors in an invariant-based controller for safe PNs. Reference (Dideban and Zeraatkar 2018) employs the place-invariant property of Petri Nets for synthesis of controllers for large-scale systems by breaking down the original Petri Net model into smaller models. Their proposed algorithm addresses the problem of forbidden states that results either from deadlocks or from presence of uncontrollable transitions. To design maximally permissive liveness enforcing supervisors, which avoid deadlocks in flexible manufacturing systems, reference (Chen et al. 2011) proposed a computationally efficient approach to design optimal control places. The reachability graph is computed by using a combination of a vector covering approach and binary decision diagrams. In general, not all liveness enforcement problems involving PNs can be represented as the requirement that the markings satisfy a (finite) set of linear constraints (cf. figure 1, Salimi et al. 2015), and oftentimes there is no choice but to use a supervisory policy to prevent the firing of a controllable transition, as opposed to using the augmented-PN structure to do the same. When applicable, the additional structural enhancements to the original PN can be implicitly interpreted as a supervisory policy. That said, these methods do not explicitly deal with the notion of control invariance, which is the main focus of the algorithm presented in this paper.

The paper is organized as follows: Section 2 introduces the definitions and notations. Section 3 presents the preliminary results and introduces a Depth-First-Search based algorithm for finding the supremal right-closed control invariant subset of a right-closed set. Section 4 contains three PN examples which illustrate the algorithm introduced in Section 3. Section 5 includes main results of this paper. We conclude with some discussion and future research directions in Section 6.

2 Definitions and notations

We use $\mathbb {Z}$ (resp. $\mathbb {Z}^{+}$) to denote the set of non-negative (resp. positive) integers, and $\mathbb {Z}^{n}$ denotes the set of n-dimensional integral vectors, where $n \in \mathbb {Z}^{+}$. We use x_i to denote the i-th component of a vector $\textbf {x} \in \mathbb {Z}^{n}$. The set of n × m non-negative integral matrices is represented by $\mathbb {Z}^{n \times m}$. For any $\textbf {A} \in \mathbb {Z}^{n \times m}, \textbf {A}_{i,j}$ denotes the value of the i-th row and j-th column of the n × m matrix A. Given two vectors $\textbf {x}, \textbf {y} \in \mathbb {Z}^{n}$, we use the notation x ≥y if x_i ≥y_i for all i ∈{1,2,…n}. We use the term max{x,y} to denote the term-wise maximum of the two vectors in the argument. The cardinality of a set argument is denoted by card(∙).

2.1 Petri nets

A Petri Net structure N = (π,T,IN,OUT) is a bipartite weighted directed graph, where π = {p₁,p₂,...,p_n} and T = {t₁,t₂,...,t_m} denote two disjoint sets of vertices called places and transitions, respectively. $\textbf {IN} \in \mathbb {Z}^{n \times m}$ (resp. $\textbf {OUT} \in \mathbb {Z}^{n \times m}$) represents the adjacency relationship (π×T) (resp. (T×π)). Specifically, IN_i,j = w (resp. OUT_i,j = w) denotes that there is a directed arc from p_i to t_j (resp. t_j to p_i) with weight w. The incidence matrix C of the PN structure N is an n × m matrix, where C = OUT −IN. We use the notation $\textbf {IN}_{t_{j}}$ ($\textbf {OUT}_{t_{j}}$) to denote the column of the input (resp. output) matrix corresponding to transition t_j. For purposes of supervisory control, the set of transitions are partitioned as T = T_u ∪ T_c, where T_u (resp. T_c) represents the subset of uncontrollable (reps. controllable) transitions.

Each structure N has an initial marking $\textbf {m}^{0} \in \mathbb {Z}^{n}$ associated with it, where the place p_i is assigned $\textbf {m}^{0}_{i}$-many tokens at initialization. We will use the term Petri net (PN) and the symbol N(m⁰) to denote a PN structure N along with its initial marking m⁰.

In graphic representations of PN structures, controllable (resp. uncontrollable) transitions are shown by filled (resp. unfilled) rectangles. Places are represented by circles, and tokens are represented by smaller filled-circles that are inside the circles representing the places. Arcs are represented by directed edges; for the sake of brevity, only non-unitary weights are explicated in graphical representations of PN structures. Any given marking m can be interpreted as an integral vector in $\mathbb {Z}^{n}$ which illustrates the distribution of tokens among places at any instant. The supervisory policy $\mathcal {P}:\mathbb {Z}^{n} \times T \rightarrow \{0,1\}$ is a function that assigns a 0 or 1 for each transition and each marking. Additionally, $\forall \textbf {m} \in \mathbb {Z}^{n}, \forall t_{u} \in T_{u}, \mathcal {P}(\textbf {m}, t_{u}) = 1$.

A transition t_j ∈ T is said to be state-enabled (resp. control-enabled) at a marking $\textbf {m}^{k} \in \mathbb {Z}^{n}$ if $\textbf {m}^{k} \geq \textbf {IN}_{t_{j}}$ (resp. $\mathcal {P}(\textbf {m}^{k}, t_{j}) = 1$). The set of state-enabled transitions at marking m^k is denoted by $T_{e}(N,\textbf {m}^{k})$. The set of uncontrollable transitions are control-enabled for all markings. A transition t_j ∈ T that is state and control-enabled can fire, which results in a new marking $\textbf {m}^{k+1} \in \mathbb {Z}^{n}$, where $\textbf {m}^{k+1} = \textbf {m}^{k} + \textbf {C}_{t_{j}}$. This is represented as $\textbf {m}^{k} \xrightarrow {t_{j}} \textbf {m}^{k+1}$.

2.2 Right-closed set of markings

A set of markings ${\mathscr{M}} \subseteq \mathbb {Z}^{n}$ is right-closed if $((\textbf {m}^{1}\in {\mathscr{M}}) \land (\textbf {m}^{2} \geq \textbf {m}^{1}) \Rightarrow (\textbf {m}^{2}\in {\mathscr{M}}))$. Every right-closed set ${\mathscr{M}}$ contains a finite set of minimal elements denoted by $min({\mathscr{M}})\subseteq {\mathscr{M}}$; the set of minimal elements, $min({\mathscr{M}})$, can be used to represent ${\mathscr{M}}$. The set of markings $\{\widehat {\textbf {m}}^{k+1} \in \mathbb {Z}^{n} \mid \widehat {\textbf {m}}^{k} \geq \textbf {m}^{k}, \widehat {\textbf {m}}^{k} \geq \textbf {IN}_{t_{j}},\widehat {\textbf {m}}^{k+1} = \widehat {\textbf {m}}^{k} + \textbf {C}_{t_{j}}\}$ is right-closed, and is identified by the minimal element $\max \limits (\textbf {m}^{k}, \textbf {IN}_{t_{j}}) + \textbf {C}_{t_{j}}$. The empty-set is right-closed by definition.

We use the notation $\textbf {m}^{k} \stackrel {t_{j}}{\leadsto } \textbf {m}^{k+1}$ to denote the fact $\textbf {m}^{k+1} = \max \limits (\textbf {m}^{k}, \textbf {IN}_{t_{j}}) + \textbf {C}_{t_{j}}$. To elaborate, this notation is used to denote that if transition t_j ∈ T were enabled to fire at a marking which is greater than or equal to m^k, the marking that results from the firing of t_j will be greater than or equal to marking m^k+ 1.

2.3 Control invariance property

A set of marking ${\mathscr{M}}$ is said to be control invariant with respect to a PN structure N if $((\textbf {m}^{1}\in {\mathscr{M}})\land (t_{u}\in T_{u}) \land (\textbf {m}^{1} \geq \textbf {IN}_{t_{u}}) \land (\textbf {m}^{2} = \textbf {m}^{1} + \textbf {C}_{t_{u}})\Rightarrow (\textbf {m}^{2}\in {\mathscr{M}}))$. That is, the firing of any state-enabled, uncontrollable transition at a marking in ${\mathscr{M}}$ will result in a new marking that is also in ${\mathscr{M}}$. If ${\mathscr{M}}_{1}, {\mathscr{M}}_{2} \subseteq {\mathscr{M}}$ are two control invariant subsets of ${\mathscr{M}}$, then ${\mathscr{M}}_{1} \cup {\mathscr{M}}_{2} \subseteq {\mathscr{M}}$ is also a control invariant subset of ${\mathscr{M}}$. Consequently, there is a unique largest (in terms of set-containment) subset of ${\mathscr{M}}$, the supremal control invariant subset ${\mathscr{M}}^{\uparrow } \subseteq {\mathscr{M}}$, that is control invariant with respect to N (Section 7, Ramadge and Wonham 1987). We drop the reference to the PN structure N if its identity is unambiguous.

If ${\mathscr{M}}$ is right-closed, then ${\mathscr{M}}$ is control invariant if and only if $\forall \textbf {m}^{i} \in min({\mathscr{M}}), \forall t_{u}\in T_{u}, \exists \textbf {m}^{j} \in min({\mathscr{M}})$ such that:

$$ max\{\textbf{m}^{i},\textbf{IN}_{t_{u}}\} + \textbf{C}_{t_{u}} \geq \textbf{m}^{j} \text{(Lemma 5.10, Sreenivas 2012)}. $$

(1)

That is, $(\textbf {m}^{i} \stackrel {t_{u}}{\leadsto } \widehat {\textbf {m}}^{i}) \Rightarrow (\widehat {\textbf {m}}^{i} \in {\mathscr{M}})$, where $\widehat {\textbf {m}}^{i} = \max \limits (\textbf {m}^{i}, \textbf {IN}_{t_{u}}) + \textbf {C}_{t_{u}}$. This is the control invariance (CI) condition, where minimal element mⁱ is covered by minimal element m^j for transition t_u ∈ T_u. For a PN structure N and a right-closed set of markings ${\mathscr{M}}$, the supremal control invariant subset ${\mathscr{M}}^{\uparrow }$ is not necessarily right-closed. However, there is a unique supremal subset ${\mathscr{M}}^{\Uparrow } \subseteq {\mathscr{M}}^{\uparrow }$ that is right-closed, and control invariant with respect to N. This follows directly from the fact that (a) the empty-set is right-closed by definition, (b) the union of two right-closed sets is also right-closed, and (c) the union of two control invariant sets of markings is also control invariant with respect to N. The right-closed set ${\mathscr{M}}^{\Uparrow }$ is characterized by the property: $\forall \textbf {m}^{1} \in min({\mathscr{M}}^{\Uparrow }), \forall {t_{u} \in T_{u}}, (\textbf {m}^{1} \stackrel {t_{u}}{\leadsto } \widehat {\textbf {m}}^{1}) \Rightarrow (\widehat {\textbf {m}}^{1} \in {\mathscr{M}}^{\Uparrow })$.

For the PN structure N₁ shown in Fig. 1a, consider the right-closed set ${\mathscr{M}}_{0}$ identified by minimal elements $min({\mathscr{M}}_{0}) = \{(1,0)^{T}, (0,2)^{T}\}$, where (1,0)^T (resp. (0,2)^T) corresponds to transpose of (1,0) (resp. (0,2)). For ${\mathscr{M}}_{0}$, we have ${\mathscr{M}}_{0}^{\uparrow } = {\mathscr{M}}_{1} \cup \{(1,0)^{T}\}$, where ${\mathscr{M}}_{1}$ is the right-closed set identified by minimal elements $min({\mathscr{M}}_{1}) = \{(3,0)^{T}, (1,1)^{T}, (0,2)^{T}\}$. That is, ${\mathscr{M}}_{0}^{\uparrow }$ is not right-closed, and ${\mathscr{M}}_{1} (= {\mathscr{M}}_{0}^{\Uparrow })$ is the supremal right-closed control invariant subset of ${\mathscr{M}}_{0}$.

Fig. 1

The PN structure N₁, the CI-graph of N₁ for $min({\mathscr{M}}_{0})=\{(1\ 0)^{T}, (0\ 2)^{T}\}$ and $min({\mathscr{M}}_{1})=\{(3\ 0)^{T}, (1\ 1)^{T}, (0\ 2)^{T}\}$. a N₁ b $\mathcal {G}({\mathscr{M}}_{0}, N_{1})$ c $\mathcal {G}({\mathscr{M}}_{1}, N_{1})$

Our proposed algorithm for finding the supremal right-closed control invariant subset of an initial right-closed set will require elevating the minimal elements of the current estimate of the subset in various ways. We introduce some of the notations pertaining to the elevation process in the next section using the example shown in Fig. 1.

3 Computing the supremal right-closed control invariant subset of a right-closed set

The Control Invariance Graph (CI-graph) of the right-closed set ${\mathscr{M}}$ with respect to the Petri Net structure N is defined as $\mathcal {G}({\mathscr{M}}, N)=(min({\mathscr{M}}),E)$ where $min({\mathscr{M}})=\{\textbf {m}^{1}, \textbf {m}^{2}, \ldots , \textbf {m}^{k}\}$ are the nodes of the graph and

$$ E = \{e_{\textbf{m}^{i}, t_{u}, \textbf{m}^{j}} \mid max\{ \textbf{m}^{i}, \textbf{IN}_{t_{u}} \} + \textbf{C}_{t_{u}} \geq \textbf{m}^{j}\}. $$

That is, there is a directed arc from node mⁱ to m^j with a label t_u ∈ T_u if mⁱ is covered by m^j for t_u ∈ T_u. The markings of the CI-graph may have self-loops since a marking such as mⁱ can be covered by itself upon firing of an uncontrollable transition such as t_u. This also implies that m^j can be the same as mⁱ in Eq. 1. The set of minimal elements $min({\mathscr{M}})$ can be partitioned into two sets – $min({\mathscr{M}})= \mathcal {A}^{fail} \cup \mathcal {A}^{pass}$, where $\mathcal {A}^{fail} \cap \mathcal {A}^{pass} = \emptyset$. For each $\textbf {m}^{i} \in \mathcal {A}^{pass}, \forall t_{u} \in T_{u}, \exists \textbf {m}^{j} \in \mathcal {A}^{pass}$ where Eq. 1 is satisfied; and $\mathcal {A}^{fail} = min({\mathscr{M}})-\mathcal {A}^{pass}$. Also, for each $\textbf {m}^{i} \in \mathcal {A}^{fail}$, the set of critical transitions, denoted by $\mathcal {C}\mathcal {R}\mathcal {T}(\textbf {m}^{i})$, contains all uncontrollable transitions for which mⁱ fails the CI condition test; i.e., for all $t_{j}\in \mathcal {C}\mathcal {R}\mathcal {T}(\textbf {m}^{i})$, $(\textbf {m}^{i} \stackrel {t_{j}}{\leadsto } \widehat {\textbf {m}}^{i})$ and $(\widehat {\textbf {m}}^{i} \notin {\mathscr{M}})$. In graphical representation of a CI-graph, we use red color-coding for mⁱ if $\textbf {m}^{i} \in \mathcal {A}^{fail}$ and $\mathcal {C}\mathcal {R}\mathcal {T}(\textbf {m}^{i})\neq \emptyset$, yellow color-coding if $\textbf {m}^{i} \in \mathcal {A}^{fail}$ and $\mathcal {C}\mathcal {R}\mathcal {T}(\textbf {m}^{i}) = \emptyset$, and green color-coding if $\textbf {m}^{i} \in \mathcal {A}^{pass}$.

As an illustration, consider the PN structure N₁ of Fig. 1a, and the right-closed set ${\mathscr{M}}_{0}$, where $min({\mathscr{M}}_{0})=\{(1\ 0)^{T}, (0\ 2)^{T}\}$. For N₁, both transitions are uncontrollable; consequently, the supervisory policy cannot prevent the firing of transitions t₁ or t₂. Figure 1(b) shows the CI-graph of ${\mathscr{M}}_{0}$ with respect to the PN structure N₁. The nodes of this directed graph are members of ${\mathscr{M}}_{0}$; each directed edge $e_{\textbf {m}^{i}, t_{u}, \textbf {m}^{j}}$ originates from mⁱ and terminates on m^j with label t_u ∈ T_u. For brevity, if there are multiple parallel edges between two nodes with different labels, we draw it as a single directed edge with multiple labels.

If we apply (1) to the minimal element (1 0)^T for t₁ ∈ T_u, the left-hand-side expression evaluates to (0 1)^T, which is not in ${\mathscr{M}}_{0}$. Consequently, there is no outgoing arc from (1 0)^T with a label t₁ in $\mathcal {G}({\mathscr{M}}_{0}, N_{1})$; and minimal element {(1 0)^T} cannot be in $\mathcal {A}^{pass}({\mathscr{M}}_{0})$. When Eq. 1 is applied to (1 0)^T for t₂ ∈ T_u, we get the vector (4 0)^T(≥ (1 0)^T), which means (1 0)^T is covered by itself for transition t₂ and therefore, there is a self-loop from (1 0)^T to itself with label t₂. For the minimal element (1 0)^T, we have $\mathcal {C}\mathcal {R}\mathcal {T}((1\ 0)^{T})=\{t_{1}\}$ and we use red color-coding for this marking as it fails the CI test for at least one uncontrollable transition, i.e. t₁. When Eq. 1 is applied to the minimal element (0 2)^T for t₂ ∈ T_u, we get the vector $(3\ 0)^{T} (\geq (1\ 0)^{T} \notin \mathcal {A}^{pass}({\mathscr{M}}_{0}))$, therefore (0 2)^T cannot be in $\mathcal {A}^{pass}({\mathscr{M}}_{0})$ either. However, in this case, we use yellow color-coding for this marking to signify the fact that although $\mathcal {C}\mathcal {R}\mathcal {T}((0\ 2)^{T})=\emptyset$, (0 2)^T is still a member of $\mathcal {A}^{fail}({\mathscr{M}}_{0})$. From Fig. 1(b), we infer $\mathcal {A}^{pass}({\mathscr{M}}_{0}) = \emptyset$ and $\mathcal {A}^{fail}({\mathscr{M}}_{0}) = \{(1\ 0)^{T}, (0\ 2)^{T}\}$. The right-closed set ${\mathscr{M}}_{0}$ is not control invariant with respect to the PN structure N₁. Figure 1c shows the CI-graph of ${\mathscr{M}}_{1}$ where $min({\mathscr{M}}_{1})=\{(3\ 0)^{T}, (1\ 1)^{T}, (0\ 2)^{T}\}$ with respect to the PN structure N₁. From Fig. 1c, we can see that $\mathcal {A}^{fail}({\mathscr{M}}_{0}) = \emptyset$ and $\mathcal {A}^{pass}({\mathscr{M}}_{0}) = \{(3\ 0)^{T}, (1\ 1)^{T}, (0\ 2)^{T}\}$ and thus, all the markings are color-coded as green. Therefore, the right-closed set ${\mathscr{M}}_{1}$ is control invariant with respect to the PN structure N₁.

We note that there can be multiple outgoing arcs with the same label from a vertex in the CI-graph. In general, if $card(min({\mathscr{M}})) = k$ and card(T_u) = l, then number of edges in the CI-graph of ${\mathscr{M}}$ with respect to the PN structure N is bounded by k²l.

For a right-closed set ${\mathscr{M}}$, the observations introduced below follow directly from the above discussion.

Observation 1

There is a non-empty (right-closed) control invariant subset of the right-closed set ${\mathscr{M}}$ if $\mathcal {A}^{pass}({\mathscr{M}}) \neq \emptyset$. This is indeed true because based on the definition of $\mathcal {A}^{pass}$, all minimal elements of $\mathcal {A}^{pass}({\mathscr{M}})$ will always satisfy the CI test of equation 1, which implies $\mathcal {A}^{pass}({\mathscr{M}})$, if not empty, will serve as a non-empty control invariant subset for ${\mathscr{M}}$.

Observation 2

${\mathscr{M}}$ is control invariant if and only if $\mathcal {A}^{fail}({\mathscr{M}}) = \emptyset$. Given the definition of $\mathcal {A}^{fail}$, if $\mathcal {A}^{fail}({\mathscr{M}})$ is empty, it implies that all minimal elements of ${\mathscr{M}}$ belong to $\mathcal {A}^{pass}({\mathscr{M}})$ and therefore, no minimal element of ${\mathscr{M}}$ will ever violate the CI test of Eq. 1, which means ${\mathscr{M}}$ is control invariant. Similarly, if ${\mathscr{M}}$ is control invariant, it implies that none of its minimal element fail the CI test, resulting in an empty $\mathcal {A}^{pass}({\mathscr{M}})$.

Observation 3

$\mathcal {A}^{pass}({\mathscr{M}}) \subseteq min({\mathscr{M}}^{\Uparrow })$. This is due to the fact that minimal elements of $\mathcal {A}^{pass}({\mathscr{M}})$ will always satisfy the CI test of equation 1 and therefore, members of $\mathcal {A}^{pass}({\mathscr{M}})$ need not to be removed or replaced by a term-wise larger vector. So, minimal elements of $\mathcal {A}^{pass}({\mathscr{M}})$ will be contained in the final supremal right-closed control invariant subset, $min({\mathscr{M}}^{\Uparrow })$.

The elevation of selected members of $\mathcal {A}^{fail}({\mathscr{M}})$ to term-wise larger vectors forms the basis of the algorithm that computes $min({\mathscr{M}}^{\Uparrow })$. The procedural aspects to this operation are described in detail in the remainder of this section.

3.1 Description of the elevation process

Let ${\mathscr{M}}_{0}$ be an initial, right-closed set of markings. Suppose ${\mathscr{M}}_{i} \subset {\mathscr{M}}_{0}$ is the current estimate of a control invariant subset of ${\mathscr{M}}_{0}$. Let $\textbf {m}^{1} \in \mathcal {A}^{fail}({\mathscr{M}}_{i})$, and t_u ∈ T_u such that $\textbf {m}^{1} \stackrel {t_{u}}{\leadsto } \widehat {\textbf {m}}$, and $\widehat {\textbf {m}} \notin {\mathscr{M}}_{i}$. This implies that m¹ is a minimal element that fails the CI test for t_u. Since we are looking for a right-closed subset of ${\mathscr{M}}_{i}$, the next estimate will have m¹ replaced by a set of minimal elements that are larger than m¹ so they satisfy equation 1. Consequently, m¹ is to be elevated by the smallest vector $\textbf {x} \in \mathbb {Z}^{n}$ such that $(\textbf {m}^{1} + \textbf {x}) \stackrel {t_{u}}{\leadsto } \widehat {\textbf {m}}^{1}$, and $\widehat {\textbf {m}}^{1} \geq \textbf {m}^{2}$, where $\textbf {m}^{2} \in (min({\mathscr{M}}_{i}) - \{\textbf {m}^{1}\})$. The p-th component of x, denoted by x(p), if elevated, should be such that $\max \limits \{\textbf {m}^{1}(p) + \textbf {x}(p), \textbf {IN}_{t_{u}}(p)\} + \textbf {C}_{t_{u}}(p) = \textbf {m}^{2}(p)$. Let $\overline {\textbf {m}^{1}}$ be the marking that results from elevating m¹ with respect to m². As a result of the elevation, for the p-th component of $\overline {\textbf {m}^{1}}$, we have:

$$ \overline{\textbf{m}^{1}}(p)= \begin{cases} \textbf{m}^{2}(p)-\textbf{C}_{t_{u}}(p), & \text{if}\ max\{\textbf{m}^{1}(p),\textbf{IN}_{t_{u}}(p)\} < \textbf{m}^{2}(p)-\textbf{C}_{t_{u}}(p) \\ \textbf{m}^{1}(p), & \text{otherwise} \end{cases} $$

(2)

If $\overline {\textbf {m}^{1}}$ is term-wise larger than some member of $\min \limits ({\mathscr{M}}_{i}) - \{\textbf {m}^{1}\}$, the process of elevating m¹ with respect to m² for t_u is ignored ($\overline {\textbf {m}^{1}}$ is said to be dismissed). If $\overline {\textbf {m}^{1}}$ is not dismissed, to complete the elevation process of m¹, we also elevate m¹ with respect to the new minimal element $\overline {\textbf {m}^{1}}$ by the same process as in Equation 2. The process of elevation of m¹ with respect to the newly generated minimal elements continues till the generated minimal element is dismissed by any of the existing minimal elements. We refer to this whole process as the operation for elevating m¹ for control invariance with respect to t_u and m², and it is formally described in Algorithm 1, Raise_for_CI(m¹, m², t_u, N) of the Appendix section. We show that Algorithm 1 terminates in finite number of steps in Section 5.

Considering one iteration of Algorithm 1 where m¹ is elevated by x with respect to m² for transition t_u, resulting in the new non-dismissed marking $\overline {\textbf {m}^{1}} (=\textbf {m}^{1} + \textbf {x})$, we introduce the following notations/terminologies:

• 1. $\overline {\textbf {m}^{1}}$ is a (direct) child of m²; likewise, m² is a parent for $\overline {\textbf {m}^{1}}$.

• 2. The notation $\overline {\mathbf {m}^{1}} \Rightarrow {t_{u}} \mathbf {m}^{2}$ is used to show child-parent relationship of markings $\overline {\mathbf {m}^{1}}$ and m² through transition t_u.

• 3. $\overline {\textbf {m}^{1}}$ is a descendant of m¹. The set of all descendants of m¹ for transition t_u is denoted by $\mathcal { D}(\textbf {m}^{1}, t_{u})$. The set of all descendants of m¹ raised with respect to m² for transition t_u is denoted by $\mathcal {D}(\textbf {m}^{1}, \textbf {m}^{2}, t_{u})$; therefore, $\mathcal {D}(\textbf {m}^{1}, \textbf {m}^{2}, t_{u}) \subseteq \mathcal {D}(\textbf {m}^{1}, t_{u})$.

• 4. In general, mⁱ is a child of m^k if there is a child-parent sequence of markings in $min({\mathscr{M}}_{i})$ and transitions in T_u through which mⁱ is connected to m^k; e.g. $\textbf {m}^{i} \Rightarrow {t_{1}} \textbf {m}^{i+1} \Rightarrow {t_{2}} ... \Rightarrow {t_{l}}\textbf {m}^{k-1} \Rightarrow {t_{u}}\textbf {m}^{k}$. Note that in this given sequence, m^k− 1 is the only direct child of m^k. The set of all children of a marking m^k is denoted by $\mathcal {C}(\textbf {m}^{k})$.

• 5. The combination of all existing child-parent sequences of markings in $min({\mathscr{M}}_{i})$ forms the collection of child-parent trees of ${\mathscr{M}}_{i}$ with respect to N defined as $\mathcal {T}({\mathscr{M}}_{i}, N)=(min({\mathscr{M}}_{i}),E)$ where $min({\mathscr{M}}_{i})=\{\textbf {m}^{1}, \textbf {m}^{2}, \ldots , \textbf {m}^{k}\}$ are the nodes of the tree and

  $$ E = \{e_{\textbf{m}^{i}, t_{u}, \textbf{m}^{j}} \mid \textbf{m}^{i} \text{ is a direct child of } \textbf{m}^{j} \}. $$

  That is, there is a directed arc from node mⁱ to m^j with a label t_u if mⁱ is a direct child of m^j for t_u ∈ T_u.

Starting from a right-closed set ${\mathscr{M}}_{i}$, Algorithm 1 elaborates the elevation process for a marking such as $\textbf {m}^{1} \in \mathcal {A}^{fail}({\mathscr{M}}_{i})$ which fails to satisfy the CI condition of Eq. 1 for transition t_u. A valid question here is “what happens to the child(ren) of m¹ given the fact that $\mathcal {C}(\textbf {m}^{1})\neq \emptyset$?”.

So, to consider a more general case, for a given right-closed set ${\mathscr{M}}_{i}$ with minimal elements $min({\mathscr{M}}_{i})$ and child-parent tree collection $\mathcal {T}({\mathscr{M}}_{i},N)$, Algorithm 2 outlines a complete round of elevation process for a marking $\textbf {m}^{p}\in min({\mathscr{M}}_{i})$ which fails to satisfy the CI condition test for transition t_u. This process consists of two main stages. The first stage is the elevation of m^p for control invariance with respect to transition t_u. In this stage, m^p is elevated with respect to all $\textbf {m}^{k} \in min({\mathscr{M}})-\{\textbf {m}^{p}\}-\{\mathcal {C}(\textbf {m}^{p})\}$, using Algorithm 1. The output of this stage would be the descendant markings of m^p for transition t_u, $\mathcal {D}(\textbf {m}^{p}, t_{u})$. The second stage involves the process called as elevation for control invariance forced by the parent; for this, all children of m^p (if any) needs to be raised with respect to all descendant markings of m^p in $\mathcal {D}(\textbf {m}^{p}, t_{u})$, again using Algorithm 1. Clearly, the second stage is only performed if $\mathcal {D}(\textbf {m}^{p}, t_{u})$ is non-empty. If $\mathcal {D}(\textbf {m}^{p}, t_{u})$ is empty, m^p along with all its children, $\mathcal {C}(\textbf {m}^{p})$, will be deleted from the current control invariant estimate. Throughout both stages of the elevation process, $\mathcal {T}({\mathscr{M}}_{i},N)$ will be updated to reflect all newly formed child-parent relations. At the end of the elevation round, both $min({\mathscr{M}}_{i})$ and $\mathcal {T}({\mathscr{M}}_{i},N)$ will be checked to remove any dismissed markings along with their children and to obtain the updated right-closed subset ${\mathscr{M}}_{i+1} \subseteq {\mathscr{M}}_{0}$. The Pseudocode of Algorithm 2 is presented in the Appendix section. The first illustrative example of Section 4 elaborates the implementation of the elevation principles discussed in Algorithm 1 and Algorithm 2.

In the next subsection, we present a procedure to compute (the minimal elements of) ${\mathscr{M}}_{0}^{\Uparrow }$ using a Depth-First-Search (DFS) strategy on an appropriately defined tree-structure.

3.2 A Depth-First-Search strategy for finding the supremal right-closed control invariant subset

For a right-closed set ${\mathscr{M}}_{i} \subseteq {\mathscr{M}}_{0}$, if ${\mathscr{M}}_{i}$ is not a control invariant set, multiple minimal elements of ${\mathscr{M}}_{i}$ may fail the CI condition test for multiple uncontrollable transitions. This implies that at the start of each elevation round, there might be multiple elevation choices to explore. In fact, at the start of an elevation round with $card(min({\mathscr{M}}_{i})) = k$ and card(T_u) = l, the combination of all possible computational choices to explore will be bounded by kl. In order to explore all possible computational choices, we introduce an algorithm based on the Depth-First-Search (DFS) strategy for a decision tree. In this tree structure, each node corresponds to a right-closed set represented by a finite set of minimal elements, where the root node is $min({\mathscr{M}}_{0})$. Considering the node for $min({\mathscr{M}}_{i})$, for each elevation process of a marking $\textbf {m}^{k} \in min({\mathscr{M}}_{i})$ with respect to an uncontrollable transition t_u ∈ T_u, a branch with label $(\textbf {m}^{k},t_{u},min({\mathscr{M}}_{i}),\mathcal {T}({\mathscr{M}}_{i},N))$ is created down the node $min({\mathscr{M}}_{i})$. Starting from any node and given the elevation labels for each branch, the algorithm keeps exploring the path that originated from that node until a termination condition is reached for the path. In fact, for each leaf node of the tree such as $min({\mathscr{M}}_{f})$, we must have $\mathcal {A}^{fail}({\mathscr{M}}_{f}) = \emptyset$ as the termination condition.

So, given an initial right-closed set ${\mathscr{M}}_{0}$, the algorithm for creating the decision tree and performing the DFS-based strategy for finding the supremal right-closed control invariant subset of ${\mathscr{M}}_{0}$ with respect to PN structure N, denoted by ${\mathscr{M}}_{0}^{\Uparrow }$, is briefly described as follows:

• 1. For the initial iteration, the root node of the decision tree represents the initial set ${\mathscr{M}}_{0}$ and its minimal elements. The minimal elements of $min({{\mathscr{M}}_{0}})$ are partitioned into $\mathcal {A}^{pass}({\mathscr{M}}_{0})$ and $\mathcal {A}^{fail}({\mathscr{M}}_{0})$:

  • (a) If $\mathcal {A}^{fail}({\mathscr{M}}_{0})$ is empty, ${\mathscr{M}}_{0}$ is control invariant and the algorithm terminates with $\mathcal {A}^{pass}({\mathscr{M}}_{0})$ as the supremal right-closed control invariant subset ${\mathscr{M}}_{0}^{\Uparrow }$.

  • (b) If $\mathcal {A}^{fail}({\mathscr{M}}_{0})$ is not empty, for each $\textbf {m}^{k} \in \mathcal {A}^{fail}({\mathscr{M}}_{0})$ and for each $t_{u} \in \mathcal {C}\mathcal {R}\mathcal {T}(\textbf {m}^{k})$, a new branch is created with label $(\textbf {m}^{k}, t_{u}, min({\mathscr{M}}_{0}), \mathcal {T}({\mathscr{M}}_{0},N))$. At this point, by convention, the leftmost created branch is selected to be explored for the next elevation round. Each elevation round is implemented by calling Algorithm 2 with input $(\textbf {m}^{k}, t_{u}, min({\mathscr{M}}_{0}), \mathcal {T}({\mathscr{M}}_{0},N))$. Note that the output from Algorithm 2 will be an updated right-closed set, resulting in creation of a new node in the decision tree.

• 2. For the n^th iteration, suppose the algorithm picks a branch with label $(\textbf {m}^{k}, t_{u}, min({\mathscr{M}}_{i}), \mathcal {T}({\mathscr{M}}_{i},N))$. In this case, one round of elevation is performed, using algorithm 2, to obtain updated $min({\mathscr{M}}_{n+1})$ and $\mathcal {T}({\mathscr{M}}_{n+1},N)$:

  • (a) If $min({\mathscr{M}}_{n+1})$ is empty, the path terminates with the empty set as a control invariant subset. At this point, the algorithm will backtrack to perform the next elevation round on the last leftmost unexplored branch, if any.

  • (b) If $min({\mathscr{M}}_{n+1})$ is not empty, $min({\mathscr{M}}_{n+1})$ is partitioned into $\mathcal {A}^{pass}({\mathscr{M}}_{n+1})$ and $\mathcal {A}^{fail}({\mathscr{M}}_{n+1})$:

    • i If $\mathcal {A}^{fail}({\mathscr{M}}_{n+1})$ is empty, ${\mathscr{M}}_{n+1}$ is control invariant and the current path terminates with $\mathcal {A}^{pass}({\mathscr{M}}_{n+1})$ as a control invariant subset and the algorithm will backtrack to perform the next elevation round on the last leftmost unexplored branch, if any.

    • ii If $\mathcal {A}^{fail}({\mathscr{M}}_{n+1})$ is not empty, for each $\textbf {m}^{k} \in \mathcal {A}^{fail}({\mathscr{M}}_{n+1})$ and for each $t_{u} \in \mathcal {C}\mathcal {R}\mathcal {T}(\textbf {m}^{k})$, a new branch is created with label $(\textbf {m}^{k}, t_{u}, min({\mathscr{M}}_{n+1}), \mathcal {T}({\mathscr{M}}_{n+1},N))$. At this point, the leftmost created branch is selected to be explored for the next elevation round.

Once no unexplored branches are left in the decision tree and all paths reach a termination condition, the algorithm will output the union of all right-closed control invariant subsets found at the termination-point of each path as ${\mathscr{M}}_{0}^{\Uparrow }$. This DFS-based elevation process is formally described in Algorithm 3 of the Appendix section. The second PN example of Section 4 illustrates the application of algorithms 3.

4 Illustrative examples

In this section we present a set of examples that illustrate the algorithms introduced in the previous section. The first example illustrates the finite-termination of the elevation process, resulting in a right-closed control invariant subset of the original right-closed set. The right-closed control invariant subset that results from this procedure is dependent on the choices made in due course of the algorithm. While the end-result is right-closed and control invariant (with respect to a PN structure), it is not guaranteed to be the supremal right-closed control invariant subset of the initial right-closed set – for this, one would need to record the control invariant subset arising from each possible choice of the elevation procedure, and present their union as the supremal right-closed control invariant subset. This is effectively done by the DFS-based procedure of Algorithm 3, illustrated in the second example. Regarding the practical application of the proposed algorithm, the third example presents a PN structure in a simplified manufacturing setting and highlights the importance of computation of the largest right-closed control invariant subset of an initial right-closed set, as a prerequisite and necessary step, for the procedure of design and synthesis of LESPs for PN models.

4.1 Example 1: Illustration of the elevation process

Consider the PN structure N₂ of Fig. 2a, and the right-closed set $min({\mathscr{M}}_{0}) =\{(1\ 0\ 0\ 0\ 0)^{T}$, (0 2 0 0 6)^T,(0 0 1 0 0)^T,(0 0 0 6 6)^T}. In the PN structure N₂ of Fig. 2a, all transitions except t₁ and t₆ are uncontrollable. Figure 2(b) shows the CI-graph $\mathcal {G}({\mathscr{M}}_{0}, N_{2})$; $\mathcal {A}^{pass}({\mathscr{M}}_{0}) = \{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}\}$. Also, note that there are no outgoing arcs labeled with t₄ and t₅ for minimal elements (0 2 0 0 6)^T and (0 0 1 0 0)^T; therefore, (0 2 0 0 6)^T and (0 0 1 0 0)^T fail the CI test for transitions t₄ and t₅, respectively. Figure 2c shows the initial child-parent tree collection/structure $\mathcal {T}({\mathscr{M}}_{0}, N_{2})$, where all markings of $min({\mathscr{M}}_{0})$ are considered as root vertices and the tree has no arcs since no child-parent relation is formed yet.

Fig. 2

The PN structure N₂, the CI-graph of ${\mathscr{M}}_{0}$ with respect to N₂, and the child-parent tree structure of ${\mathscr{M}}_{0}$, where $min({\mathscr{M}}_{0}) =\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 2\ 0\ 0\ 6)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}\}$, and $\mathcal {A}^{pass}({\mathscr{M}}_{0}) = \{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}\}$. a N₂ b $\mathcal {G}({\mathscr{M}}_{0}, N_{2})$ c $\mathcal {T}({\mathscr{M}}_{0}, N_{2})$

The elevation process can start with either one of the minimal elements that failed the CI test (viz. (0 2 0 0 6)^T or (0 0 1 0 0)^T), and this elevation can be done with respect to either one of the uncontrollable transitions in the set {t₄,t₅}. Suppose we start by elevating the minimal element (0 0 1 0 0)^T for transition t₅ with respect to all members of $(min({\mathscr{M}}_{0})-\{(0\ 0\ 1\ 0\ 0)^{T}\}=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 2\ 0\ 0\ 6)^{T}, (0\ 0\ 0\ 6\ 6)^{T}\})$. If we perform the elevation process once, we will get the new markings (descendants), ε₀ = {(1 0 1 0 0)^T,(0 0 1 6 0)^T,(0 2 1 0 0)^T}; it is clear that marking (1 0 1 0 0)^T is term-wise larger than minimal element (1 0 0 0 0)^T and, therefore, it can be discarded. So, we update ε₀ to ε₀ = {(0 0 1 6 0)^T,(0 2 1 0 0)^T}. Now, to complete the elevation process, (0 0 1 0 0)^T needs to be elevated with respect to members of ε₀, resulting in ε₁ = {(0 0 4 6 0)^T,(0 2 4 0 0)^T}; all members of ε₁ are dismissed by members of ε₀. Therefore, the first round of elevation will terminate, and the updated estimate is $min(\widehat {{\mathscr{M}}}_{1})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 2\ 0\ 0\ 6)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 2\ 1\ 0\ 0)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{1}, N_{2})$ and the child-parent tree structure $\mathcal {T}(\widehat {{\mathscr{M}}}_{1}, N_{2})$ are shown in Fig. 3. Note that the thick blue arrows of Fig. 3b shows the existing child-parent relations.

Fig. 3

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{1}$, where $min(\widehat {{\mathscr{M}}}_{1}) =\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 2\ 0\ 0\ 6)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 2\ 1\ 0\ 0)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$, and $\mathcal {A}^{pass}(\widehat {{\mathscr{M}}}_{1}) = \{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$. a $(\widehat {{\mathscr{M}}}_{1}, N_{2})$ b $\mathcal {T}(\widehat {{\mathscr{M}}}_{1}, N_{2})$

From Fig. 3a, it is clear that both markings {(0 2 1 0 0)^T,(0 2 0 0 6)^T} fail the CI test for transition t₃ and t₄, as there is no outgoing arcs for either of these two markings which is labeled with t₃ and t₄. Our proposed algorithm dictates two rules; based on the first rule, (0 2 0 0 6)^T should not be elevated with respect to its children that is, (0 2 0 0 6)^T is not elevated with respect to (0 2 1 0 0)^T. The second rule states that each time a parent marking is elevated and replaced by some non-dismissed descendants, all children of that parent should also be elevated accordingly with respect to the new descendants. However, if the descendants of the parent marking are all dismissed and therefore, deleted, the children should be deleted, as well. We apply the two mentioned guidelines to this example. Let’s assume we decide to elevate the parent marking (0 2 0 0 6)^T for transition t₄; in fact, (0 2 0 0 6)^T needs to be raised with respect to the members of $(min(\widehat {{\mathscr{M}}}_{1})-\{(0\ 2\ 0\ 0\ 6)^{T}, (0\ 2\ 1\ 0\ 0)^{T}\} =\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\})$. If we perform the elevation process once, we will get the new markings (descendants), ε₀ = {(1 2 0 0 6)^T,(0 2 0 3 6)^T,(0 2 1 3 6)^T}; it is clear that markings (1 2 0 0 6)^T and (0 2 1 3 6)^T are term-wise larger than minimal elements (1 0 0 0 0)^T and (0 2 0 3 6)^T respectively; therefore, we remove these two minimal elements to update ε₀ to ε₀ = {(0 2 0 3 6)^T}. Now, to complete the elevation process, (0 2 0 0 6)^T needs to be elevated with respect to members of ε₀, resulting in ε₁ = {(0 4 0 0 6)^T}. We repeat the elevation process once more to raise (0 2 0 0 6)^T with respect to members of ε₁ to get ε₂ = {(0 6 0 0 6)^T}. As we can see the only marking of ε₂ is term-wise larger than the only marking of ε₁. So, the final set of descendants for marking (0 2 0 0 6)^T will be {(0 2 0 3 6)^T,(0 4 0 0 6)^T}. Now, in the next step, we need to raise the child(ren) of (0 2 0 0 6)^T with respect to the set of new descendants. As shown in Fig. 3b, (0 2 1 0 0)^T is the only child of (0 2 0 0 6)^T connected through transition t₅. Therefore, (0 2 1 0 0)^T needs to be checked and elevated (if necessary) with respect to members of {(0 2 0 3 6)^T,(0 4 0 0 6)^T} for t₅. This process will result in the set of new markings ε₀₁ = {(0 2 1 3 0)^T,(0 4 1 0 0)^T}. Next, to complete the elevation process, (0 2 1 0 0)^T is elevated with respect to members of ε₀₁, resulting in ε₁₁ = {(0 2 4 3 0)^T,(0 4 4 0 0)^T}; all members of ε₁₁ are dismissed by members of ε₀₁, and are discarded. Therefore, the second round of elevation will terminate, and the updated estimate will be $min(\widehat {{\mathscr{M}}}_{2})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}, (0\ 2\ 0\ 3\ 6)^{T}, (0\ 4\ 0\ 0\ 6)^{T}, (0\ 2\ 1\ 3\ 0)^{T}, (0\ 4\ 1\ 0\ 0)^{T}\}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{2}, N_{2})$ and the child-parent tree structure $\mathcal {T}(\widehat {{\mathscr{M}}}_{2}, N_{2})$ are shown in Fig. 4.

Fig. 4

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{2}$, where $min(\widehat {{\mathscr{M}}}_{2})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}, (0\ 2\ 0\ 3\ 6)^{T}, (0\ 4\ 0\ 0\ 6)^{T}, (0\ 2\ 1\ 3\ 0)^{T}, (0\ 4\ 1\ 0\ 0)^{T}\}$, and $\mathcal {A}^{pass}(\widehat {{\mathscr{M}}}_{2}) = \{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$. a $\mathcal {G}(\widehat {{\mathscr{M}}}_{2}, N_{2})$ b $\mathcal {T}(\widehat {{\mathscr{M}}}_{2}, N_{2})$

Based on Fig. 4a, markings {(0 2 0 3 6)^T,(0 4 0 0 6)^T,(0 2 1 3 0)^T,(0 4 1 0 0)^T} fails the CI test for transitions t₃. Suppose we decide to elevate (0 2 0 3 6)^T for transition t₃. Given the rules of the algorithm, (0 2 0 3 6)^T should be raised with respect to members of $(min(\widehat {{\mathscr{M}}}_{2})-\{(0\ 2\ 0\ 3\ 6)^{T}, (0\ 2\ 1\ 3\ 0)^{T}, (0\ 4\ 0\ 0\ 6)^{T}, (0\ 4\ 1\ 0\ 0)^{T}\} =\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\})$. This process will result in the generation of the set ε₀ = {(1 2 0 3 6)^T,(0 2 0 6 6)^T,(0 2 0 6 6)^T}, all being term-wise larger than members of $(min(\widehat {{\mathscr{M}}}_{2})-\{(0\ 2\ 0\ 3\ 6)^{T}, (0\ 2\ 1\ 3\ 0)^{T}, (0\ 4\ 0\ 0\ 6)^{T}$, (0 4 1 0 0)^T}. At this point, since (0 2 0 3 6)^T has no non-dismissed descendants, we need to remove it from the current estimate; upon removal of (0 2 0 3 6)^T, all its children, i.e. {(0 2 1 3 0)^T,(0 4 0 0 6)^T,(0 4 1 0 0)^T}, will also get removed based on the discipline dictated by the algorithm. Therefore, the third round of elevation will terminate, and the updated estimate will be $min(\widehat {{\mathscr{M}}}_{3})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{3}, N_{2})$ and the child-parent tree collection $\mathcal {T}(\widehat {{\mathscr{M}}}_{3}, N_{2})$ are shown in Fig. 5. Note that $\widehat {{\mathscr{M}}}_{3}$ is control invariant with respect to PN structure N₂ as we have $\mathcal {A}^{fail}(\widehat {{\mathscr{M}}}_{3})=\emptyset$.

Fig. 5

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{3}$, where $min(\widehat {{\mathscr{M}}}_{3})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$, and $\mathcal {A}^{pass}(\widehat {{\mathscr{M}}}_{3}) = \{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 0\ 6\ 6)^{T}, (0\ 0\ 1\ 6\ 0)^{T}\}$. a $\mathcal {G}(\widehat {{\mathscr{M}}}_{3}, N_{2})$b $\mathcal {T}(\widehat {{\mathscr{M}}}_{3}, N_{2})$

For this example, the process of elevation resulted in a right-closed set $\mathcal {\widehat {M}}_{3} \subset {\mathscr{M}}_{0}$ that is control invariant (with respect to the PN structure N₂) that is also the supremal right-closed control invariant subset ${\mathscr{M}}_{0}^{\Uparrow }$. In general, the control invariant set that results from this process of repeated elevation is not guaranteed to be the supremal right-closed control invariant subset. The example in the next subsection illustrates the need for the DFS-based procedure of Algorithm 3.

4.2 Example 2: DFS-based approach for computing the supremal right-closed control invariant subset

Consider the PN structure N₃ of Fig. 6a, and the right-closed set $min({\mathscr{M}}_{0}) =\{(1\ 0\ 0\ 0\ 0)^{T}$, (0 1 0 0 0)^T,(0 0 1 0 0)^T,(0 0 0 1 1)^T}. In the PN structure N₃ of Fig. 6a, all transitions are uncontrollable. Figure 6(b) shows the CI-graph $\mathcal {G}({\mathscr{M}}_{0}, N_{3})$; as we can see from the graph, $\mathcal {A}^{pass}({\mathscr{M}}_{0})$ is empty. Figure 6(c) shows the initial child-parent tree structure $\mathcal {T}({\mathscr{M}}_{0}, N_{3})$, where all markings of $min({\mathscr{M}}_{0})$ are considered as root vertices and the tree has no arcs since no child-parent relation is formed yet.

Fig. 6

The PN structure N₃, the CI-graph of ${\mathscr{M}}_{0}$ with respect to N₃, and the child-parent tree structure of ${\mathscr{M}}_{0}$, where $min({\mathscr{M}}_{0}) =\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 1\ 0\ 0\ 0)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}\}$, and $\mathcal {A}_{pass}({\mathscr{M}}_{0}) = \emptyset$. a N₃ b $\mathcal {G}({\mathscr{M}}_{0}, N_{3})$ c $\mathcal {T}({\mathscr{M}}_{0}, N_{3})$

As we can see from Fig. 6b, markings (1 0 0 0 0)^T and (0 1 0 0 0)^T fail the CI test for transitions t₁ and t₃, respectively. So, there will be two elevation choices to start from. The first one is labeled as $((1\ 0\ 0\ 0\ 0)^{T}, t_{1}, min({\mathscr{M}}_{0}), \mathcal {T}({\mathscr{M}}_{0},N_{3}))$, which corresponds to elevation of (1 0 0 0 0)^T with respect to t₁ given $min({\mathscr{M}}_{0})$ and $\mathcal {T}({\mathscr{M}}_{0},N_{3})$. The second one is labeled as $((0\ 1\ 0\ 0\ 0)^{T}, t_{3}, min({\mathscr{M}}_{0}), \mathcal {T}({\mathscr{M}}_{0},N_{3}))$, which corresponds to elevation of (0 1 0 0 0)^T with respect to t₃ given $min({\mathscr{M}}_{0})$ and $\mathcal {T}({\mathscr{M}}_{0},N_{3})$. Figure 7 provides a schematic decision tree showing the initial elevation choices for the given example, where each edge label corresponds to a specific elevation choice. This decision tree will get updated as we go through different elevation rounds of the algorithm.

Fig. 7

Summary of different elevation choices starting from ${\mathscr{M}}_{0}$, where $min({\mathscr{M}}_{0})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 1\ 0\ 0\ 0)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}\}$

Starting from $((1\ 0\ 0\ 0\ 0)^{T}, t_{1}, min({\mathscr{M}}_{0})), \mathcal {T}({\mathscr{M}}_{0},N_{3}))$, first we elevate (1 0 0 0 0)^T for t₁ with respect to (0 1 0 0 0)^T to get (1 1 0 0 0)^T, which is term-wise larger than (0 1 0 0 0)^T; so, it will get deleted. Next, we raise (1 0 0 0 0)^T for t₁ with respect to (0 0 1 0 0)^T to get (1 0 1 0 0)^T, which is term-wise larger than (0 0 1 0 0)^T and gets deleted. Finally, (1 0 0 0 0)^T is elevated for t₁ with respect to (0 0 0 1 1)^T resulting in (1 0 0 0 1)^T, which is not term-wise larger than (0 0 0 1 1)^T; so, (1 0 0 0 1)^T is a child of the parent marking (0 0 0 1 1)^T. At this point, we also need to raise (1 0 0 0 0)^T for t₁ with respect to the newly generated marking, (1 0 0 0 1)^T; this results in generation of the marking (2 0 0 0 1)^T which is term-wise larger than (1 0 0 0 1)^T and is therefore, deleted. So, at the end of this elevation round, we get the updated estimate $min(\widehat {{\mathscr{M}}}_{1})=\{(0\ 1\ 0\ 0\ 0)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (1\ 0\ 0\ 0\ 1)^{T}\}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{1}, N_{3})$ and the child-parent tree structure $\mathcal {T}(\widehat {{\mathscr{M}}}_{1}, N_{3})$ is shown in Fig. 8, where $\mathcal {A}^{pass}(\widehat {{\mathscr{M}}}_{1}) = \emptyset$. Note that the thick blue arrows of Fig. 8b shows the existing child-parent relations.

Fig. 8

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{1}$, where $min(\widehat {{\mathscr{M}}}_{1}) =\{(0\ 1\ 0\ 0\ 0)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (1\ 0\ 0\ 0\ 1)^{T}\}$, and $\mathcal {A}_{pass}(\widehat {{\mathscr{M}}}_{1}) = \emptyset$. a $\mathcal {G}(\widehat {{\mathscr{M}}}_{1}, N_{3})$ b $\mathcal {T}(\widehat {{\mathscr{M}}}_{1}, N_{3})$ c Current Decision Tree of the DFS algorithm

As we can see from Fig. 8a, marking (0 1 0 0 0)^T fails the CI test for transitions t₃. So, at this point, there will be only one elevation choice to perform, which is labeled as $((0\ 1\ 0\ 0\ 0)^{T}, t_{3}, min(\widehat {{\mathscr{M}}}_{1}), \mathcal {T}(\widehat {{\mathscr{M}}}_{1},N_{3}))$. If (0 1 0 0 0)^T is elevated for t₃ with respect to (0 0 1 0 0)^T, the resulting marking will be (0 1 1 0 0)^T, which is term-wise larger than (0 0 1 0 0)^T; so, it will be discarded. Next, we would raise (0 1 0 0 0)^T for t₃ with respect to (0 0 0 1 1)^T to get (0 1 0 1 0)^T, which is not term-wise larger than (0 0 0 1 1)^T; so, (0 1 0 1 0)^T is a child of the parent marking (0 0 0 1 1)^T. Since we have a new non-dismissed minimal element, we also need to elevate (0 1 0 0 0)^T with respect to (0 1 0 1 0)^T for t₃, resulting in (0 2 0 1 0)^T which is term-wise larger than (0 1 0 1 0)^T and is therefore, discarded. Finally, (0 1 0 0 0)^T is raised with respect to (1 0 0 0 1)^T for t₃; it results in generation of (1 1 0 0 0)^T, which is not term-wise larger than (1 0 0 0 1)^T; so, (1 1 0 0 0)^T is a child of the parent marking (1 0 0 0 1)^T. Again, (0 1 0 0 0)^T needs to be raised with respect to the newly generated marking, (1 1 0 0 0)^T; the resulting marking will be (1 2 0 0 0)^T which is term-wise larger than (1 1 0 0 0)^T and is therefore, deleted. At the end of this elevation round, we get the updated estimate $min(\widehat {{\mathscr{M}}}_{2})=\{(0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (1\ 0\ 0\ 0\ 1)^{T}, (0\ 1\ 0\ 1\ 0)^{T}, (1\ 1\ 0\ 0\ 0)^{T} \}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{2}, N_{3})$ and the child-parent tree structure $\mathcal {T}(\widehat {{\mathscr{M}}}_{2}, N_{3})$ is shown in Fig. 9, where $\mathcal {A}^{fail}(\widehat {{\mathscr{M}}}_{2}) = \emptyset$, implying that $\widehat {{\mathscr{M}}}_{2}$ is control invariant. Therefore, this path terminates with $\widehat {{\mathscr{M}}}_{2}$ as the first control invariant subset found for ${\mathscr{M}}_{0}$.

Fig. 9

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{2}$, where $min(\widehat {{\mathscr{M}}}_{2}) =\{(0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (1\ 0\ 0\ 0\ 1)^{T}, (0\ 1\ 0\ 1\ 0)^{T}, (1\ 1\ 0\ 0\ 0)^{T}\}$, and $\mathcal {A}_{fail}(\widehat {{\mathscr{M}}}_{2}) = \emptyset$. a $\mathcal {G}(\widehat {{\mathscr{M}}}_{2}, N_{3})$ b $\mathcal {T}(\widehat {{\mathscr{M}}}_{2}, N_{3})$ c Current Decision Tree of the DFS algorithm

Now, we go back to the last unexplored elevation choice; as shown in Fig. 9c, this choice is labeled as $((0\ 1\ 0\ 0\ 0)^{T}, t_{3}, min({\mathscr{M}}_{0}), \mathcal {T}({\mathscr{M}}_{0},N_{3}))$, corresponding to elevation of (0 1 0 0 0)^T with respect to t₃ given $min({\mathscr{M}}_{0})$ and $\mathcal {T}({\mathscr{M}}_{0},N_{3})$ as shown in Fig. 6. If (0 1 0 0 0)^T is elevated for transition t₃ with respect to (1 0 0 0 0)^T, we get (1 1 0 0 0)^T, which is term-wise larger than (1 0 0 0 0)^T; so, it will get deleted. Next, we would raise (0 1 0 0 0)^T for t₃ with respect to (0 0 1 0 0)^T to get (0 1 1 0 0)^T, which is term-wise larger than (0 0 1 0 0)^T and gets deleted. Finally, (0 1 0 0 0)^T is raised for t₃ with respect to (0 0 0 1 1)^T, resulting in (0 1 0 1 0)^T, which is not dismissed by (0 0 0 1 1)^T; so, (0 1 0 1 0)^T is a child of the parent marking (0 0 0 1 1)^T. At this point, we also need to elevate (0 1 0 0 0)^T for transition t₃ with respect to the newly generated marking (0 1 0 1 0)^T, which results in (0 2 0 1 0)^T and this marking is term-wise larger than (0 1 0 1 0)^T and is therefore, discarded. At the end of this elevation round, we get the updated estimate $min(\widehat {{\mathscr{M}}}_{3})=\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (0\ 1\ 0\ 1\ 0)^{T}\}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{3}, N_{3})$ and the child-parent tree structure $\mathcal {T}(\widehat {{\mathscr{M}}}_{3}, N_{3})$ is shown in Fig. 10, where $\mathcal {A}^{pass}(\widehat {{\mathscr{M}}}_{3}) = \emptyset$.

Fig. 10

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{3}$, where $min(\widehat {{\mathscr{M}}}_{3}) =\{(1\ 0\ 0\ 0\ 0)^{T}, (0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T},(0\ 1\ 0\ 1\ 0)^{T}\}$, and $\mathcal {A}_{pass}(\widehat {{\mathscr{M}}}_{3}) = \emptyset$. a $\mathcal {G}(\widehat {{\mathscr{M}}}_{3}, N_{3})$ b $\mathcal {T}(\widehat {{\mathscr{M}}}_{3}, N_{3})$ c Current Decision Tree of the DFS algorithm

As we can see from Fig. 10a, marking (1 0 0 0 0)^T fails the CI test for transitions t₁. So, at this point, there will be only one elevation choice to perform, which is labeled as $((1\ 0\ 0\ 0\ 0)^{T}, t_{1}, min(\widehat {{\mathscr{M}}}_{3})), \mathcal {T}(\widehat {{\mathscr{M}}}_{3},N_{3}))$. If (1 0 0 0 0)^T is elevated for transition t₁ with respect to (0 0 1 0 0)^T, it results in the marking (1 0 1 0 0)^T, which is term-wise larger than (0 0 1 0 0)^T; so, it will get deleted. Next, (1 0 0 0 0)^T is elevated for transition t₁ with respect to (0 0 0 1 1)^T to get (1 0 0 0 1)^T; this marking is not term-wise larger than (0 0 0 1 1)^T; so, (1 0 0 0 1)^T is a child of the parent marking (0 0 0 1 1)^T. At this point, (1 0 0 0 0)^T needs to be elevated for transition t₁ with respect to the newly generated marking (1 0 0 0 1)^T, resulting in (2 0 0 0 1)^T which is term-wise larger than (1 0 0 0 1)^T and is therefore, discarded. Finally, we raise (1 0 0 0 0)^T for t₁ with respect to (0 1 0 1 0)^T to get (1 1 0 0 0)^T, which is not term-wise larger than (0 1 0 1 0)^T; so, (1 1 0 0 0)^T is a child of the parent marking (0 1 0 1 0)^T. If (1 0 0 0 0)^T is raised with respect to the newly generated marking (1 1 0 0 0)^T, the resulting marking (2 1 0 0 0)^T will be dismissed by (1 1 0 0 0)^T and is therefore, deleted. At the end of this elevation round, we get the updated estimate $min(\widehat {{\mathscr{M}}}_{4})=\{(0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (0\ 1\ 0\ 1\ 0)^{T}, (1\ 0\ 0\ 0\ 1)^{T}, (1\ 1\ 0\ 0\ 0)^{T} \}$. The CI-graph $\mathcal {G}(\widehat {{\mathscr{M}}}_{4}, N_{3})$ and the child-parent tree structure $\mathcal {T}(\widehat {{\mathscr{M}}}_{4}, N_{3})$ is shown in Fig. 11, where $\mathcal {A}^{fail}(\widehat {{\mathscr{M}}}_{4}) = \emptyset$, implying that $\widehat {{\mathscr{M}}}_{4}$ is control invariant. Therefore, this path terminates with $\widehat {{\mathscr{M}}}_{4}$ as the second control invariant subset found for ${\mathscr{M}}_{0}$.

Fig. 11

The CI-graph and the child-parent tree structure of $\widehat {{\mathscr{M}}}_{4}$, where $min(\widehat {{\mathscr{M}}}_{4})=\{(0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (0\ 1\ 0\ 1\ 0)^{T}, (1\ 0\ 0\ 0\ 1)^{T}, (1\ 1\ 0\ 0\ 0)^{T} \}$, and $\mathcal {A}_{fail}(\widehat {{\mathscr{M}}}_{4}) = \emptyset$. a $\mathcal {G}(\widehat {{\mathscr{M}}}_{4}, N_{3})$ b $\mathcal {T}(\widehat {{\mathscr{M}}}_{4}, N_{3})$ c Current Decision Tree of the DFS algorithm

As shown in Fig. 11c, $\widehat {{\mathscr{M}}}_{4} = \widehat {{\mathscr{M}}}_{2}$, since there are no other elevation choices to be explored, the algorithm will terminate and will return ${\mathscr{M}}_{0}^{\Uparrow } = \widehat {{\mathscr{M}}}_{4} \cup \widehat {{\mathscr{M}}}_{2} = \widehat {{\mathscr{M}}}_{2}$; and, $min({\mathscr{M}}_{0}^{\Uparrow }) = \{(0\ 0\ 1\ 0\ 0)^{T}, (0\ 0\ 0\ 1\ 1)^{T}, (0\ 1\ 0\ 1\ 0)^{T}, (1\ 0\ 0\ 0\ 1)^{T}, (1\ 1\ 0\ 0\ 0)^{T} \}$. In the Section 5 we formally consolidate the various observations and results introduced via illustrative examples in this section.

4.3 Example 3: A practical example on control invariance property and its implication in LESP-synthesis

In this section, a practical PN example is presented to illustrate the importance of control invariance property in synthesizing LESPs for Discrete Event Systems (Khaleghi et al. 2019). Computation of the minimally restrictive LESP for PN models requires computation of the supremal right-closed control invariant subset of a right-closed set of markings.

Let us consider an automated system that paints automobile bodies using Booth 1 and Booth 2 and Robot 1 and Robot 2, where Robot 1 and Robot 2 are used for transportation tasks and painting tasks, respectively. A base-coat is applied to an unfinished body in Booth 1, following this it is transferred to Booth 2, where a coat of clear resin is applied. After sufficient time has elapsed for the solvents to evaporate, the finished automobile frame is transported out of Booth 2, and a new unfinished frame is placed in Booth 1 for painting. The base-coat operation can commence only after Robot 1 has placed an unfinished automobile body in Booth 1, and the base-coat paint nozzle is affixed to Robot 2. After the completion of this task, the automobile body with the base-coat is ready to be transported to Booth 2 by Robot 1. At this stage, Robot 2 can either be directed to do another base-coat operation in Booth 1; or, it can be commissioned to commence a clear-coat operation in Booth 2. The clear-coat operation can start only after Robot 1 has placed the body with the base-coat in Booth 2, and the clear-coat nozzle is affixed to Robot 2. After this task is completed, the finished automobile body is ready to be transported out of Booth 2 by Robot 1, which then places a new unfinished automobile body in Booth 1 for its base-coat.

Figure 12 shows the PN model representing the task sequence for Robot 1 and Robot 2. For N_4a representing the task flow of Robot 1, transition t₁ corresponds to the operation of putting the base-coat in Booth 1. Transition t₂ represents the operation of putting the clear coat in Booth 2. Transition t₃ denotes the operation of removing the painted automobile body from Booth 2, along with the process of placing a new, unfinished body on the fixture in Booth 1. The presence of a token in place p₁ (resp. p₂) denotes the resource state fact that an automobile body is on the fixture in Booth 1 (resp. Booth 2). A token in place p₃ denotes the resource state that a finished automobile body is at the fixture in Booth 2 to be removed. For N_4b representing the task sequence for Robot 2, similar to N_4a, transitions t₁ and t₂ corresponds to the operations of putting the base-coat and the clear-coat in Booth 1 and Booth 2, respectively. Transition t₄ (resp. t₅) represents the operation where Robot 2 is commissioned to the clear-coat (resp. base-coat) paint-operation. The presence of a token in place p₄ indicates Robot 2 is ready to be commissioned for any of the two paint tasks. The presence of a token in place p₅ (resp. place p₆) indicates Robot 2 is ready to apply the clear-coat (resp. the base-coat) in Booth 2 (resp. Booth 1).

Fig. 12

The PN structures representing task flows for Robot 1 and Robot 2. a PN N_4a representing the task ow for Robot 1. b PN N_4b representing the task flow for Robot 2

Figure 13a shows the PN structure N₄ that results from merging the two PNs of Fig. 12. PN N₄ belongs to the family of PNs for which the liveness property can be enforced by a proper right-closed set of minimal elements (cf. (Sreenivas 2012; Salimi et al. 2015; Chen et al. 2020)); as long as N₄ operates within the boundary defined by this proper right-closed set, the liveness property is guaranteed to be satisfied. Consequently, to synthesis a liveness policy for N₄, computation of the control invariant subset of its corresponding proper right-closed set is required in order to ensure that firing of no uncontrollable transition would result in a marking which is outside the boundary of the proper right-closed set. For N₄, transitions t₄ and t₅ are controllable, in that the decisions about how Robot 2 is commissioned is to be made by the supervisory policy which enforces the liveness property. On the other hand, all the transportation tasks assigned to Robot 1, represented by transitions t₁, t₂, and t₃, are uncontrollable; this means that as soon as a body part becomes available in any of the places p₁, p₂, or p₃, the transportation task can be started by Robot 1, without any restrictions from the liveness enforcing supervisory policy. Therefore, to reflect the fact that the supervisory policy has no control over the commencement of uncontrollable transitions, the proper right-closed set which enforces the liveness policy is required to satisfy the control invariance property, or, otherwise, commencement of transportation tasks by Robot 1 (i.e. firing of any of the transitions t₁, t₂, or t₃) may result in a state which violates the liveness property.

The LESP-synthesis, as discussed in (Khaleghi et al. 2019; Chandrasekaran et al. 2015), requires additional work than computing the largest right-closed control invariant subset of a given right-closed set. Without getting into the details of LESP-synthesis procedure, which is beyond the scope of this paper, let us assume, for N₄, the right-closed set ${\mathscr{M}}_{0}$, where $min({\mathscr{M}}_{0})=\{(1\ 0\ 0\ 0\ 0\ 1)^{T}, (0\ 0\ 1\ 0\ 0\ 0)^{T},(0\ 1\ 0\ 0\ 1\ 0)^{T},(1\ 0\ 0\ 1\ 0\ 0)^{T}, \\(0\ 1\ 0\ 1\ 0\ 0)^{T}\}$ denotes the candidate right-closed set for enforcing the liveness property. Figure 13b shows the CI-graph of ${\mathscr{M}}_{0}$ with respect to the PN structure N₄. If we apply Eq. 1 to the minimal element (0 0 1 0 0 0)^T for t₃, the left-hand-side expression evaluates to (1 0 0 0 0 0)^T, which is not in ${\mathscr{M}}_{0}$. This means that if a finished automobile body is at the fixture in Booth 2 (i.e. (0 0 1 0 0 0)^T), Robot 1 can start the transportation task to remove it from Booth 2 and then, put an unfinished body in the fixture of Booth 1 (i.e. (1 0 0 0 0 0)^T). As a result of this operation, the net will get trapped in state (1 0 0 0 0 0)^T, which is outside the boundary of the set defined by $min({\mathscr{M}}_{0})$, and where no other operations can take place (deadlock state). This implies that the right-closed set ${\mathscr{M}}_{0}$ is not control invariant with respect to the PN structure N₄. Following the procedure dictated by the proposed algorithm for computing the supremal control invariant subset of a right-closed set, marking (0 0 1 0 0 0)^T will be replaced by two new minimal elements {(0 0 1 0 0 1)^T,(0 0 1 1 0 0)^T}, resulting in the right-closed set ${\mathscr{M}}_{1}$, where $min({\mathscr{M}}_{1})=\{(1\ 0\ 0\ 0\ 0\ 1)^{T}, (0\ 0\ 1\ 0\ 0\ 1)^{T},(0\ 0\ 1\ 1\ 0\ 0)^{T},(0\ 1\ 0\ 0\ 1\ 0)^{T},(1\ 0\ 0\ 1\ 0\ 0)^{T},(0\ 1\ 0\ 1\ 0\ 0)^{T}\}$.Figure 13b shows the CI-graph of ${\mathscr{M}}_{1} (={\mathscr{M}}_{0}^{\Uparrow })$, the largest right-closed control invariant subset of ${\mathscr{M}}_{0}$ with respect to the PN structure N₄. In fact, ${\mathscr{M}}_{1}$ represents the largest controllable right-closed set which enforces the minimally restrictive liveness policy for the manufacturing system represented by PN N₄ (Khaleghi et al. 2019).

Fig. 13

The PN structure N₄, the CI-graph of N₄ for $min({\mathscr{M}}_{0})=\{(1\ 0\ 0\ 0\ 0\ 1)^{T}, (0\ 0\ 1\ 0\ 0\ 0)^{T},(0\ 1\ 0\ 0\ 1\ 0)^{T},(1\ 0\ 0\ 1\ 0\ 0)^{T},(0\ 1\ 0\ 1\ 0\ 0)^{T}\}$ and $min({\mathscr{M}}_{1})=\{(1\ 0\ 0\ 0\ 0\ 1)^{T}, (0\ 0\ 1\ 0\ 0\ 1)^{T},(0\ 0\ 1\ 1\ 0\ 0)^{T},(0\ 1\ 0\ 0\ 1\ 0)^{T},(1\ 0\ 0\ 1\ 0\ 0)^{T},(0\ 1\ 0\ 1\ 0\ 0)^{T}\}$. a N₄ b $\mathcal {G}({\mathscr{M}}_{0}, N_{4})$ c $\mathcal {G}({\mathscr{M}}_{1}, N_{4})$

5 Main results

Observation 4 follows directly from the elevation process and Algorithm1, and is stated without proof. Theorem 1 establishes the fact that any elevation process terminates in finite time.

Observation 4

$\overline {\textbf {m}^{1}}$, as obtained from Eq. 1 and algorithm 1, is the smallest marking (term-wise) greater than or equal to m¹ such that $\overline {\textbf {m}^{1}} \Rightarrow {t_{u}} \textbf {m}^{2}$.

Theorem 1

Algorithm 1, Raise_for_CI(m¹, m², t_u, N), will terminate in finite time.

Proof

: Following the notation of algorithm 1, let $\overline {\textbf {m}}^{1}(p)$ be the marking that results from elevation of m¹(p) with respect to m²(p) for transition t_u. If ∀p ∈π, $\overline {\textbf {m}}^{1}(p) \geq \textbf {m}^{2}(p)$, then $\overline {\textbf {m}}^{1}(p)$ is dismissed by m² and the algorithm terminates. If this is not the case, m¹ will be elevated with respect to $\overline {\textbf {m}}^{1}$. Let $\overline {\textbf {m}}^{1}_{1}$ be the marking that results from this elevation process. Let us divide the vector $\textbf {C}_{t_{u}}$ into three partitions for p ∈π and consider the following three cases:

• 1. $\textbf {C}_{t_{u}}(p)=0$: using the following two scenarios, we show that for this case $\overline {\textbf {m}}^{1}_{1}(p)=\overline {\textbf {m}}^{1}(p)$:

  • 1.1. If $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{1}(p)$, which implies $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} \geq \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Now, if m²(p) is replaced by $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{1}(p)$ on the right-hand side and given the fact that $\textbf {C}_{t_{u}}(p)=0$, we get $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} \geq \textbf {m}^{1}(p)-0=\textbf {m}^{1}(p)$. Therefore, we will have $\overline {\textbf {m}}^{1}_{1}(p)=\overline {\textbf {m}}^{1}(p)$.

  • 1.2. If $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$, which implies $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} < \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Now, if m²(p) is replaced by $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$ on the right-hand side and given the fact that $\textbf {C}_{t_{u}}(p)=0$, we get $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} < \textbf {m}^{2}(p)-2\textbf {C}_{t_{u}}(p)=\textbf {m}^{2}(p)-2*0=\textbf {m}^{2}(p)$. Therefore, we will have $\overline {\textbf {m}}^{1}_{1}(p)=\overline {\textbf {m}}^{1}(p)$.

• 2. $\textbf {C}_{t_{u}}(p)<0$: using the following two scenarios, we show that for this case $\overline {\textbf {m}}^{1}_{1}(p)\geq \overline {\textbf {m}}^{1}(p)$:

  • 2.1. $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{1}(p)$, which implies $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} \geq \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Now, if m²(p) is replaced by $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{1}(p)$ on the right-hand side and given the fact that $\textbf {C}_{t_{u}}(p)<0$, $\overline {\textbf {m}}^{1}_{1}(p)$ will either be equal to m¹(p) or $\textbf {m}^{1}(p)-\textbf {C}_{t_{u}}(p)$. Therefore, we will have $\overline {\textbf {m}}^{1}_{1}(p)\geq \overline {\textbf {m}}^{1}(p)$.

  • 2.2. $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$, which implies $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} < \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Now, if m²(p) is replaced by $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$ on the right-hand side and given the fact that $\textbf {C}_{t_{u}}(p)<0$, we get $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} < \textbf {m}^{2}(p)-2\textbf {C}_{t_{u}}(p)$. Therefore, $\overline {\textbf {m}}^{1}_{1}(p)=\textbf {m}^{2}(p)-2\textbf {C}_{t_{u}}(p)>\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$.

• 3. $\textbf {C}_{t_{u}}(p)>0$:

  • 3.1. $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{1}(p)$, which implies $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} \geq \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Now, if m²(p) is replaced by $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{1}(p)$ on the right-hand side and given the fact that $\textbf {C}_{t_{u}}(p)>0$, we get $max\{\textbf {m}^{1}(p), \textbf {IN}_{t}(p)\} > \textbf {m}^{1}(p)-\textbf {C}_{t}(p)$. Therefore, we will have $\overline {\textbf {m}}^{1}_{1}(p)=\overline {\textbf {m}}^{1}(p)$.

  • 3.2. $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$, which implies $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} < \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Now, if m²(p) is replaced by $\overline {\textbf {m}}^{1}(p)=\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$, $\overline {\textbf {m}}^{1}_{1}(p)$ will either be equal to $\textbf {m}^{2}(p)-2\textbf {C}_{t_{u}}(p)$ or m¹(p). Also, note that since $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} < \textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$, we can conclude $\textbf {m}^{1}(p)<\textbf {m}^{2}(p)-\textbf {C}_{t_{u}}(p)$. Therefore, we will have $\overline {\textbf {m}}^{1}_{1}(p)\leq \overline {\textbf {m}}^{1}(p)$.

  The three cases explained above can be generalized to when m¹(p) is to be raised with respect to $\overline {\textbf {m}}^{1}_{k}(p)$ in the k^th iteration of the algorithm. However note that for the first two cases, we will always have $\overline {\textbf {m}}^{1}_{k}(p)\geq \overline {\textbf {m}}^{1}_{k-1}(p)$. For the third case, if scenario [3.1] happens, then it is clear that $\overline {\textbf {m}}^{1}_{k}(p)= \overline {\textbf {m}}^{1}_{k-1}(p)=\textbf {m}^{1}(p)$ and the algorithm will terminate as $\overline {\textbf {m}}^{1}_{k-1}(p)$ will dismiss $\overline {\textbf {m}}^{1}_{k}(p)$. Regarding scenario [3.2], we might observe a non-increasing trend/token load from $\overline {\textbf {m}}^{1}_{k-1}(p)$ to $\overline {\textbf {m}}^{1}_{k}(p)$. However, this trend will turn into a constant non-decreasing one in finite number of iterations. For the k^th iteration of algorithm ??, the right-hand side of step 7 will be equal to $\textbf {m}^{2}(p)-k\textbf {C}_{t_{u}}(p)$. If $\textbf {m}^{2}(p)-k\textbf {C}_{t_{u}}(p)$ turns out to be a negative value, the value of $\overline {\textbf {m}}^{1}_{k}(p)$ for the current and subsequent iterations will be fixed at m¹(p); that is due to the fact that $max\{\textbf {m}^{1}(p), \textbf {IN}_{t_{u}}(p)\} \geq 0$. Therefore, as soon as the fixed value of m¹(p) is obtained for all p ∈π where $\textbf {C}_{t_{u}}(p)>0$, the algorithm will terminate. Consequently, the number of iterations of the Algorithm 1 will be bounded by $\max \limits _{\textbf {C}_{t_{u}}(p)\geq 0} \lceil \frac {\textbf {m}^{2}(p)}{\textbf {C}_{t_{u}}(p)} \rceil$.

□

The directives listed below play an important role in establishing the correctness of Algorithm 3 and its constituent components.

Directive 1

If during an iteration of Algorithm 3, a parent marking such as m^k fails the CI test for some uncontrollable transition such as t_u, no member of $\mathcal {C}(\textbf {m}^{k})$ (where $\mathcal {C}(\textbf {m}^{k})$ denotes the set of children of m^k) should be used to elevate m^k for t_u.

Directive 2

If during an iteration of Algorithm 3, a parent marking such as m^k fails the CI test for some uncontrollable transition and is replaced by the descendant set $\mathcal {D}(\textbf {m}^{k})$ as the result of the elevation process, then all its children, $\mathcal {C}(\textbf {m}^{k})$, might have to be elevated accordingly. This process is referred to as “elevation for control invariance forced by the parent” and it seeks to maintain the existing child-parent relations. In the simple $\overline {\textbf {m}^{1}} \Rightarrow {t_{u}} \textbf {m}^{2}$ example, if m² fails the CI test for some uncontrollable transition and is replaced by $\mathcal {D}(\textbf {m}^{2})$, we need to perform Raise_for_CI($\overline {\textbf {m}^{1}}, \mathcal {D}({\textbf {m}^{2}}), t_{u}, N$) as dictated by Algorithm 1.

Directive 3

If during an iteration of Algorithm 3, as m^k fails the CI test for some uncontrollable transition and when elevated, $\mathcal { D}(\textbf {m}^{k})$ turns out to be empty (i.e. all descendants of m^k are dismissed), as m^k gets removed from the current control invariant estimate, so do all children of m^k, $\mathcal {C}(\textbf {m}^{k})$. The reasoning behind this policy is explained in more details in Theorem 2.

Theorem 2

Suppose $\mathcal {\widehat {M}}$ is an estimate of the right-closed control invariant subset of the initial set. Also, let’s assume we have $\textbf {\textup {m}}^{1}_{2}, \textbf {\textup {m}}^{2} \in \min \limits (\mathcal {\widehat {M}})$ and $\textbf {\textup {m}}^{1}_{2} \in \mathcal {D}(\textbf {\textup {m}}^{1}, t_{1})$ such that $\textbf {\textup {m}}^{1}_{2} \Rightarrow {t_{1}} \textbf {\textup {m}}^{2}$, which implies $\textbf {\textup {m}}^{1}_{2}$ is a child of m². Let there exists a transition t₂ ∈ T_u such that $\textbf {\textup {m}}^{2} \stackrel {t_{2}}{\leadsto } \widehat {\textbf {\textup {m}}}^{2}$ and $\widehat {\textbf {\textup {m}}}^{2} \notin \mathcal {\widehat {M}}$. Next, suppose that if m² is elevated for t₂, $\nexists \overline {\textbf {\textup {m}}}^{2} \in \mathcal {D}(\textbf {\textup {m}}^{2},t_{2})$ such that (a) $\overline {\textbf {\textup {m}}}^{2} \ngeq \textbf {\textup {m}}^{i}$ for any $\textbf {\textup {m}}^{i} \in \min \limits (\mathcal { \widehat {M}}) - \{\textbf {\textup {m}}^{2}\}$; and, (b) $\overline {\textbf {\textup {m}}}^{2} \stackrel {t_{2}}{\leadsto } \underline {\textbf {\textup {m}}}^{2}$, $\underline {\textbf {\textup {m}}}^{2} \geq \textbf {\textup {m}}^{i}$ for some $\textbf {\textup {m}}^{i} \in \min \limits (\mathcal {\widehat {M}}) - \{\textbf {\textup {m}}^{2}\}$; i.e. $\mathcal {D}(\textbf {m}^{2}, t_{2})=\emptyset$. We seek to prove that once the parent marking m² is dropped without having any descendants, there is no need to keep its child, and $\textbf {m}^{1}_{2}$ can also be removed from the current control invariant estimate that is, $\nexists \overline {\textbf {\textup {m}}}^{1}_{2} \in \mathcal {D}(\textbf {\textup {m}}^{1}_{2})$ such that:(a) $\overline {\textbf {\textup {m}}}^{1}_{2} \ngeq \textbf {\textup {m}}^{i}$ for any $\textbf {\textup {m}}^{i} \in \min \limits (\mathcal {\widehat {M}}) - \{\textbf {\textup {m}}^{2}\}-\{\textbf {\textup {m}}^{1}_{2}\}$; and, (b) $\overline {\textbf {\textup {m}}}^{1}_{2} \stackrel {t_{1}}{\leadsto } \underline {\textbf {\textup {m}}}^{1}_{2}$ and $\overline {\textbf {\textup {m}}}^{1}_{2} \stackrel {t_{2}}{\leadsto } \underline {\underline {\textbf {\textup {m}}}}^{1}_{2}$ such that $\underline {\textbf {\textup {m}}}^{2}, \underline {\underline {\textbf {\textup {m}}}}^{1}_{2} \geq \textbf {\textup {m}}^{i}$ for some $\textbf {\textup {m}}^{i} \in \min \limits (\mathcal {\widehat {M}}) - \{\textbf {\textup {m}}^{2}\}-\{\textbf {\textup {m}}^{1}_{2}\}$.

Proof

. Since m² is the only parent of $\textbf {m}^{1}_{2}$ for t₁, if we re-write $\textbf {m}^{1}_{2}$ as m¹ + x for a vector x ≥0, we used to have $max\{\textbf {m}^{1}+\textbf {x}, \textbf {IN}_{t_{1}}\}+\textbf {C}_{t_{1}}\geq \textbf {m}^{2}$. It is clear that upon removal of m² from $\mathcal {\widehat {M}}$, $\textbf {m}^{1}_{2}$ will fail the requirement of CI test for transition t₁. Now, let’s suppose $\textbf {m}^{1}_{2}$ is to be raised for t₁ with respect to a marking $\textbf {m}^{3} \in \min \limits (\mathcal {\widehat {M}})-\{\textbf {m}^{2}\}$. In other words, we seek to find vector z ≥ 0 such that: $max\{\textbf {m}^{1}_{2}+\textbf {z}, \textbf {IN}_{t_{1}}\}+\textbf {C}_{t_{1}}\geq \textbf {m}^{3}$; let’s call this newly formed marking ${\textbf {m}^{1}_{2}}^{\uparrow }$ (where ${\textbf {m}^{1}_{2}}^{\uparrow }=\textbf {m}^{1}+\textbf {x}+\textbf {z}$). We will have either of the two following scenarios:

• 1. $\exists {\textbf {m}^{1}_{3}} \in \min \limits (\mathcal {\widehat {M}})-\{\textbf {m}^{2}\}$ and $\textbf {m}^{1}_{3} \in \mathcal {D}(\textbf {m}^{1}, t_{1})$ such that $\textbf {m}^{1}_{3} \Rightarrow {t_{1}} \textbf {m}^{3}$, which implies $\textbf {m}^{1}_{3}$ is a child of m³. In other words, if we re-write $\textbf {m}^{1}_{3}$ as m¹ + y for a vector y ≥0, we have $max\{\textbf {m}^{1}+\textbf {y},\textbf {IN}_{t_{1}}\}+\textbf {C}_{t_{1}}\geq \textbf {m}^{3}$. It is not hard to show that x(p) + z(p) ≥y(p),∀p ∈π, viz. ${\textbf {m}^{1}_{2}}^{\uparrow }=\textbf {m}^{1}+ \textbf {x} + \textbf {z}\geq \textbf {m}^{1}_{3}=\textbf {m}^{1}+\textbf {y}$. Therefore, $\textbf {m}^{1}_{3}$ will dismiss ${\textbf {m}^{1}_{2}}^{\uparrow }$ (as ${\textbf {m}^{1}_{2}}^{\uparrow }$ is term-wise larger than $\textbf {m}^{1}_{3}$) and there is no need to elevate $\textbf {m}^{1}_{2}$ with respect to m³ for transition t₁.

• 2. $\nexists {\textbf {m}^{1}_{3}} \in \min \limits (\mathcal {\widehat {M}})-\{\textbf {m}^{2}\}$ and $\textbf {m}^{1}_{3} \in \mathcal {D}(\textbf {m}^{1}, t_{1})$ such that $\textbf {m}^{1}_{3} \Rightarrow {t_{1}} \textbf {m}^{3}$. The primary reason for non-existence of $\textbf {m}^{1}_{3}$ could be that during a previous iteration of the algorithm, $\textbf {m}^{1}_{3}$ got dismissed by a marking such as m⁴:

  • (a) If $\textbf {m}^{4} \in \min \limits (\mathcal {\widehat {M}})-\{\textbf {m}^{2}\}$, it means that m⁴ is still a minimal element of the current control invariant subset estimate. In this case, since $\textbf {m}^{1}_{3}\geq \textbf {m}^{4}$ and from scenario 1, ${\textbf {m}^{1}_{2}}^{\uparrow }\geq \textbf {m}^{1}_{3}$, then we can conclude ${\textbf {m}^{1}_{2}}^{\uparrow }\geq \textbf {m}^{4}$, which implies that m⁴ will dismiss ${\textbf {m}^{1}_{2}}^{\uparrow }$ and there is no need to elevate $\textbf {m}^{1}_{2}$ with respect to m³ for transition t₁.

  • (b) If $\textbf {m}^{4} \notin \min \limits (\mathcal {\widehat {M}})-\{\textbf {m}^{2}\}$, it means that m⁴ is no longer a minimal element of the current control invariant subset. In other words, during a previous iteration of the algorithm with estimate ${\mathscr{M}}^{current}$, m⁴ must have failed in some transition such as t₃ and when elevated for transition t₃, $\nexists \overline {\textbf {m}}^{4} \in \mathcal {D}(\textbf {m}^{4}, t_{3})$ such that: (a) $\overline {\textbf {m}}^{4} \ngeq \textbf {m}^{i}$ for any $\textbf {m}^{i} \in \min \limits ({\mathscr{M}}^{current}) - \{\textbf {m}^{4}\})$; and, (b) $\overline {\textbf {m}}^{4} \stackrel {t_{3}}{\leadsto } \underline {\textbf {m}}^{4}$ and $\underline {\textbf {m}}^{4} \geq \textbf {m}^{i}$ for some $\textbf {m}^{i} \in \min \limits ({\mathscr{M}}^{current}) - \{\textbf {m}^{4}\}$. We know that $\textbf {m}^{1}_{3}\geq \textbf {m}^{4}$ and from scenario 1, ${\textbf {m}^{1}_{2}}^{\uparrow }\geq \textbf {m}^{1}_{3}$; So, we get ${\textbf {m}^{1}_{2}}^{\uparrow }\geq \textbf {m}^{4}$. Note that here, ${\textbf {m}^{1}_{2}}^{\uparrow }$ may or may not fail the CI test for transition t₃. In the latter case, it will get dismissed by the same marking which covers ${\textbf {m}^{1}_{2}}^{\uparrow }$ for t₃ (or the same marking that dismissed the elevated version of m⁴ for t₃). In the former case, ${\textbf {m}^{1}_{2}}^{\uparrow }$ does not satisfy the requirement of CI test for transition t₃ and there cannot exist any non-dismissed descendant for ${\textbf {m}^{1}_{2}}^{\uparrow }$ which satisfies the CI test for t₃ (i.e. $\mathcal {D}({\textbf {m}^{1}_{2}}^{\uparrow }, t_{3})=\emptyset$); or otherwise, $\exists \overline {\textbf {m}}^{4} \in \mathcal {D}(\textbf {m}^{4}, t_{3})$ such that $\overline {\textbf {m}}^{4} \stackrel {t_{3}}{\leadsto } \underline {\textbf {m}}^{4}$ and $\underline {\textbf {m}}^{4}\geq \textbf {m}^{i}$ for some $\textbf {m}^{i} \in \min \limits ({\mathscr{M}}^{current})$, which is a contradiction. So, there is no need to elevate $\textbf {m}^{1}_{2}$ with respect to m³ for transition t₁.

□

The following Theorem notes that Algorithm 3 will raise a minimal element at most once with respect to an uncontrollable transitions. In fact, repeated elevation of a minimal element can only occur via Directive 2.

Theorem 3

Algorithm 3 ensures that each marking (and its descendants) is at most elevated once with respect to the same transition, unless through Directive 2.

Proof

. Suppose $\mathcal {\widehat {M}}$ is an estimate of the right-closed control invariant subset of the initial set. Also, let’s assume we have $\textbf {m}^{i} \in \min \limits (\mathcal { \widehat {M}})$. First it should be noted that if mⁱ is not the child of any other minimal element of $\min \limits (\mathcal {\widehat {M}})$, then it means it has never been elevated before with respect to any transitions. Now, let us assume there exist $\textbf {m}^{j} \in \min \limits (\mathcal {\widehat {M}})$ such that $\textbf {m}^{i} \Rightarrow {t_{u}} \textbf {m}^{j}$, which implies mⁱ is a child of m^j through transition t_u.

• 1. If $\textbf {m}^{j}\in \mathcal {A}^{pass}(\mathcal {\widehat {M}})$, it implies that the parent marking for mⁱ will never get dropped or elevated/updated:

  • (a) If $\textbf {m}^{i}\in \mathcal {A}^{pass}(\mathcal {\widehat {M}})$, then $\textbf {m}^{i} \Rightarrow {t_{u}} \textbf {m}^{j}$ will hold for the remaining elevation rounds of the algorithm (if any).

  • (b) If $\textbf {m}^{i}\in \mathcal {A}^{fail}(\mathcal {\widehat {M}})$, then it means mⁱ fails/might fail in at least one more transition except t_u; consider one such transition t_l:

    • (i) . If $\mathcal {D}(\textbf {m}^{i}, t_{l})\neq \emptyset$,then mⁱ will be replaced by some larger descendants such as $\overline {\textbf {m}}^{i}$ and, therefore, $\overline {\textbf {m}}^{i} \Rightarrow {t_{u}} \textbf {m}^{j}$ will still hold.

    • (ii) If $\mathcal {D}(\textbf {m}^{i}, t_{l})=\emptyset$,then mⁱ will be removed and no future elevation for mⁱ with respect to t_u is ever needed.

• 2. If $\textbf {m}^{j}\in \mathcal {A}^{fail}(\mathcal {\widehat {M}})$, it implies that m^j fails/might fail in at least one transition; consider one such transition t_s:

  • (a) If $\mathcal {D}(\textbf {m}^{j}, t_{s})=\emptyset$, then by Theorem 2, as m^j gets removed, so does mⁱ and no future elevation for mⁱ with respect to t_u is ever needed.

  • (b) If $\mathcal {D}(\textbf {m}^{j}, t_{s})\neq \emptyset$, then mⁱ will be replaced by some larger descendants such as $\overline {\textbf {m}}^{i}$ resulting from Directive 2. Therefore, $\overline {\textbf {m}}^{i} \Rightarrow {t_{u}} \overline {\textbf {m}}^{j}$ will still hold, where $\overline {\textbf {m}}^{j}\in \mathcal {D}(\textbf {m}^{j}, t_{s})$.

□

The following observation identifies conditions under which Algorithm 3 terminates, and follows directly from its constituent procedures.

Observation 5

At the point of termination for each of the computational paths of the DFS-tree structure of Algorithm 3, either of the following termination conditions is reached for the corresponding leaf node denoted by $min({\mathscr{M}}_{i})$: (1) $min({\mathscr{M}}_{i})=\emptyset$; (2) $\mathcal {A}^{fail}({\mathscr{M}}_{i})=\emptyset$.

Theorem 4 notes that Algorithm 3 terminates in finite-time, a sketch of the proof of this claim in presented below, as well.

Theorem 4

Algorithm 3 will terminate in finite time.

Proof

(Sketch). This Theorem can be inferred based on the following results: (1) Theorem 1 which proves each elevation round will eventually converge; (2) Theorem 3 which implies no marking is elevated more than once for the same uncontrollable transition; (3) Number of uncontrollable transitions of the PN structure N being finite; (4) Number of descendants generated at each elevation round for a marking which fails the test for CI condition being finite. □

As the culmination of the various observations and Theorem in this section, the following observation notes that the union of the control invariant subsets obtained at the conclusion of each branch of the DFS-based approach is the supremal right-closed control invariant subset of the original right-closed set.

Observation 6

Algorithm 3 returns the largest right-closed control invariant subset of the initial set ${\mathscr{M}}_{0}$. This result can be argued using Observation 4 and the brute-force approach implemented by the DFS-based strategy which checks all possible computational paths for the elevation process exhaustively.

6 Discussion

The supremal right-closed control invariant subset of a right-closed set ${\mathscr{M}} \subseteq \mathbb {Z}^{n}$ (with respect to a PN structure N), denoted by ${\mathscr{M}}^{\Uparrow }$ (${\mathscr{M}}^{\Uparrow } \subseteq {\mathscr{M}}^{\uparrow } \subseteq {\mathscr{M}}$), satisfies the requirement – $\forall \textbf {m}^{1} \in min({\mathscr{M}}^{\Uparrow }), \exists \textbf {m}^{2} \in min({\mathscr{M}})$ such that m¹ ≥m². In addition, $\forall \textbf {m}^{1} \in min({\mathscr{M}}^{\Uparrow }), \forall {t_{u} \in T_{u}}, (\textbf {m}^{1} \stackrel {t_{u}}{\leadsto } \widehat {\textbf {m}}^{1}) \Rightarrow (\widehat {\textbf {m}}^{1} \in {\mathscr{M}}^{\Uparrow })$.

If a right-closed set ${\mathscr{M}} \subseteq \mathbb {Z}^{n}$ is not control invariant with respect to a PN structure N, then $\exists \textbf {m}^{1} \in min({\mathscr{M}}), \exists {t_{u}} \in T_{u}$, such that $\textbf {m}^{1} \stackrel {t_{u}}{\leadsto } \widehat {\textbf {m}}^{1}$, and $\widehat {\textbf {m}}^{1} \notin {\mathscr{M}}$. The process of computing the minimal elements of ${\mathscr{M}}^{\Uparrow }$ is about developing a systematic approach to elevating m¹ with respect to the other minimal elements, for each t_u ∈ T_u where the CI-test (cf. Equation 1) has been violated. At any given stage, there are many decision choices involved in this elevation process (i) the choice of the other minimal element, and (ii) the choice of the uncontrollable transition that featured in the violation of Eq. 1. Using a DFS-based approach, the algorithm outlined in this paper explores all such choices. At its termination point, each computational path of this DFS-based approach computes a right-closed control invariant subset of the original right-closed set, and the termination is shown to happen in finite-time. The set ${\mathscr{M}}^{\Uparrow }$ is the union of the control invariant right-closed sets generated at the termination of each path of the DFS-based tree. Reference (Chandrasekaran et al. 2015) contains an implementation of a single-branch of the DFS-based procedure outlined in this paper.

The ${\mathscr{H}}$-class of PN structures is identified by the following structural properties: (1) for each place, the weights associated with the outgoing arcs that terminate on uncontrollable transitions must be the smallest of all outgoing arc-weights; (2) the set of input places to each uncontrollable transition is no larger than the set of input places of any transition which shares a common input place with it (cf. Salimi et al. 2015; Chen et al. 2020). All PN examples in this paper belong to the ${\mathscr{H}}$-class of PN structures. In all our experiments of PN structures from this class, we have found that each branch of the DFS-based procedure outputs the same control invariant subset. As an illustration, $min(\widehat {{\mathscr{M}}}_{2}) = min(\widehat {{\mathscr{M}}}_{4})$ in the example shown in Fig. 11c. This leads us to hypothesize that for the ${\mathscr{H}}$-class of PN structures, the supremal right-closed control invariant subset can be identified as soon as a single branch of the DFS-procedure terminates. We suggest formal investigations into this hypothesis as a future research topic.

In terms of running time, the total number of nodes of the DFS-tree is a measure of the upper-bound of execution time of the proposed algorithm, which depends on the depth-bound (α) and the breadth-bound (β) of the DFS-structure (which in turn depends on the minimal elements of ${\mathscr{M}}_{0}$ and the PN structure N). As a consequence of Directive 1, Directive 2 and Theorem 3, we have $\alpha \leq O(|min({\mathscr{M}}_{0})||T_{u}|$. For a given node, $min({\mathscr{M}}_{i})$, the max number of branches that originates from this node at the breadth level is bounded by $|min({\mathscr{M}}_{i})||T_{u}|$. Consequently, $\beta \leq \max \limits _{i}{O(|min({\mathscr{M}}_{i})||T_{u}|)}$, and the (conservative) upper-bound of the execution-time is O(α^β), which is the conservative estimate of the total number of nodes in the aforementioned DFS-structure. We hypothesize that if the PN structure belongs to the ${\mathscr{H}}$-class, then all branches of the DFS-structure yield the same right-closed set, if this hypothesis is true, then the upper-bound of the execution-time is O(α).

7 Conclusion

In context of District Event Systems modeled by Petri Net structures, a Liveness Enforcing Supervisory Policy (LESP) enforces the liveness property by disabling controllable events which result in states which are not live. Therefore, the set of initial markings for which an LESP exists needs to be control invariant with respect to its corresponding PN structure. The control invariance property ensures that firing of no uncontrollable transition would result in a state that violates the liveness property, which is intended to be enforced by the LESP. As a prerequisite step in synthesis of an LESP for certain classes of PN structures, this paper presented a formal algorithm to compute the largest (aka the supremal) right-closed control invariant subset of a right-closed set with respect to its corresponding PN structure. The supremal property is, in particular, necessary for computation of minimally restrictive LESPs. The proposed algorithm works based on a step-by-step elevation framework performed on the minimal elements of the initial right-closed set which fail to satisfy the control invariance property. During each elevation iteration of the algorithm, a target marking which fails the control invariance property for at least one uncontrollable transition is investigated, resulting in either its removal from the current control invariant estimate or its replacement by a set of elevated descendants. To obtain the supremal property, a tree-based Depth-First-Search (DFS) strategy is implemented which ensures for each pair of minimal elements and transitions of a given right-closed set, all necessary elevation procedures are tested exhaustively. The termination point of each path of the DFS tree corresponds to a right-closed control invariant subset of the initial right-closed set. Once, all paths of the DFS tree reach the termination condition, the algorithm returns the union of all right-closed control invariant subsets found at each leaf node as the final supremal right-closed control invariant subset of the initial right-closed set. The elevation process is designed in such a way that the algorithm is guaranteed to terminate in finite number of iterations. The paper presented several PN examples to illustrate the fundamental elevation process which lies at the heart of the DFS strategy. All illustrative examples of this paper belong to ${\mathscr{H}}$-class of PN structures, where the output of each leaf node of the DFS tree outputs the same control invariant subset. For future work, we suggest a deeper investigation into the hypothesis that for the ${\mathscr{H}}$-class of PN structures, as soon as a single path of the DFS tree terminates, the supremal right-closed control invariant subset of the initial right-closed set can be obtained.

Appendix