Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems

I. Introduction

EMBEDDED systems are ubiquitous in almost all devices used today, including mobile telephones, network switches, household appliances, and controllers of the internet of things (IoT). Such systems are an important part of large complex networks and often include both software and hardware elements. Real-time behavior, correctness, and good reliability are vital requirements for successful embedded systems [1]. Many models have been proposed to describe such systems, including finite state machines, data flow graphs, and Petri nets.

Petri nets constitute a high-performing model, widely used in many fields of science. The model can be used to express concurrency, synchronization, sequential actions, and non-determinism when designing certain systems. Petri-net-based representation for embedded systems (PRES+) have been proposed for the design and verification of embedded systems [2]. Using PRES+ supports allows for a precise representation of embedded systems, improves expressiveness, and captures timing information.

The PRES+ model is important for the modeling, analysis, and verification of embedded systems [2]–[8]. In order to design and verify these systems, Cortés et al. [2] presented a formal computational model based on PRES+. An industrial example was also provided to illustrate the efficiency of the PRES+ method. To improve its verification efficiency, a translation algorithm from the PRES+ model to a finite state machine with the datapath model was proposed [3]. For systems specified in PRES+, Karlsson et al. [5] put forward a method to integrate them with component-based system level design. The model utilized was a mobile telephone system, consisting of seven connected components, which were modeled in PRES+. The properties of reachability and timing were then verified. Xia [6] proposed several reduction rules to improve the verification efficiency of PRES+. Under some constraints, the properties of reachability, functionality, and timing were preserved.

However, the state space explosion problem for PRES+ struggles to specify and analyze large, complex embedded systems. This problem is of exponential complexity and decreases the modeling and verification abilities of PRES+.

The state space explosion problem is due to the absence of abstraction and compositionality mechanisms. Many researchers have used transformation approaches to resolve the state space explosion problem for Petri nets. It is essential to neither destroy nor create properties under investigation when establishing transformations. Three popular transformations exist among the literature, namely reduction [6], [9]–[16], refinement [7], [17]–[22], and synthesis [23]–[36].

Petri-net-based synthesis is an effective approach to system design and verification. The synthesis method can create a system from several component modules in such a way that the system can be effectively analyzed for design correctness. A review of some approaches in the synthesis of Petri nets is provided below.

A Petri-net-based synthesis methodology to resolve the use-case driven system design problem was proposed in [23]. Zhou et al. [24] presented a hybrid synthesis approach for manufacturing systems by using parallel and sequential mutual exclusions. For distributed liveness-enforcing supervisors of automated manufacturing systems, Hu et al. [25] focused on a synthesis method that allows both multiple resource acquisition operations and flexible process routes. Best et al. [26] characterized the reachability graph of a Petri net marked graph. This work described procedures to synthesize a marked graph solving a labeled transition system benefiting from characterizing properties. Pouyan et al. [27] classified synthesis methods into the following groups: top-down techniques, hybrid approaches, knitting techniques, and bottom-up techniques. For systems of simple sequential processes with resources (${\rm{S}}^3{\rm{PR}}$), Liu et al. [28] proposed several algorithms to synthesize recovery subnets and monitors. Certain conditions were presented to impose on a synthesis shared pp-type subnet that ensures the preservation of the liveness, boundedness, and reversibility properties [29]. Xia [30] investigated a shared pb-type subnets synthesis approach for place/transition (PT) nets. This synthesis method preserves the properties of liveness and boundedness. Liu et al. [31] proposed a synthesis approach of supervisors for flexible manufacturing systems modeled by a class of generalized Petri nets. An effective approach has also been presented for the synthesis of compact and decentralized supervisors for Petri net (PN) systems [31]. Jiao et al. [32] proposed a synthesis approach to merge a set of places of asymmetric choice nets and presented the constraints to preserve the siphon trap (ST) property, reversibility, liveness, and boundedness. For systems specified in hybrid Petri nets, Basile et al. [33] proposed an automated synthesis method for the sequencing of the activities of a robotic cell for the aircraft industry. Both static and behavioral control specifications can be considered using this method [34]. Additionally, Hu et al. [35] proposed a kind of logic Petri net synthesis method.

To solve the PRES+ state space explosion problem, as well as model, analyze, and verify large and complex embedded systems, two kinds of synthesis approaches are investigated in this paper. Compared with some synthesis methods for ordinary Petri nets [23], [29], time Petri nets, and colored nets, these approaches effectively represent important characteristics of embedded systems such as reachability, functionality, and timing. In [7], an approach for expanding the PRES+ model to the desired level of detail was provided, and a transition refinement method was proposed. Reachability, timing, functionality, liveness and boundedness preservation of the refined PRES+ model have also been investigated. To improve the verification efficiency of PRES+, Xia [6] presented a set of reduction rules. Under certain constraints, the reduced PRES+ model preserves reachability, timing, and functionality. A sharing synthesis operation for PRES+ and its liveness and boundedness preservation have been investigated in [8].

The principal motivation of this paper is to solve the synchronous problem in embedded systems, and the embedded subsystem sharing problem. The subsystem-sharing problem is formulated as a problem of merging several sets of subsystems into transition sets. Some constraints for ensuring that these synthesis methods preserve reachability, timing, functionality, and liveness are obtained in this work. The results are then applied to the verification of the modeling problem of embedded systems. First, a synthesis shared transition set for PRES+ is presented, and the property preservation of the method is investigated. Following this, the synthesis shared-transition-set technique of PRES+ is used to investigate the synthesis shared-transition-subnet-set technique by adopting the abstraction-synthesis-refinement representation method. Results obtained are useful for investigating the properties of PRES+ synthesis nets, and establishing models for large and complex embedded systems.

The remainder of this paper is organized as follows. Some preliminaries of PRES+ are proposed in Section II. The synthesis shared-transition-set approach and the synthesis shared-transition-subnet-set approach of PRES+ are presented in Section III. The abstraction-synthesis-refinement representation method is proposed in Section IV, and the preservation of reachability, timing, and functionality is investigated in Section V. Liveness preservation by these two synthesis approaches is discussed in Section VI. A case example is proposed in Section VII to illustrate the effectiveness of the proposed synthesis methods. Finally, conclusions are presented in Section VIII.

II. Preliminaries

In this section, the fundamentals of PRES+ are provided as a foundation for the rest of this article. A more general discussion on PRES+ can be found in [2].

Definition 1: A PRES+ model is $N = (P, T, I, O, M_0)$, where $P = \{p_1, p_2, \dots, p_m\}$ is a set of places, $T = \{t_1, t_2, \dots, t_n\}$ is a set of transitions, $I\subseteq P\times T$ is a set of input arcs, $O\subseteq T\times P$ is a set of output arcs, and $M_0$ is the initial marking. $k = < v$, r > is a token, where $v$ is the token value, and r is the token time.

Fig. 1 shows an example of the definitions of the PRES+ model presented in this section. For the example, we have $P = \{p_1,p_2,p_3,p_4,p_5\}$, $T = \{t_1,t_2,t_3,t_4\}$, $I = \{(p_1,t_1),(p_2,t_2),$ $(p_3,t_3),(p_4,t_3), (p_5,t_4)\}$, and $O = \{(t_1,p_2),(t_1,p_3),(t_2,p_4) ,(t_3,$ $p_5), (t_4,p_1)\}$.

Figure  1.  A simple PRES+ model

DownLoad: Full-Size Img PowerPoint

Definition 2: A marking is an assignment of tokens to places. The marking $M(p)$ of a place $p \in P$ can be represented as a set over $E_p\subseteq\{ < v,r > |v\in\tau(p)\wedge r\in {\mathbb R_0}^{+}\}$, where $\tau(p)$ denotes the set of possible tokens that may be in $p$, and ${\mathbb R_0}^{+}$ is the set of non-negative real numbers.

For example, the initial marking $M_0$ in Fig. 1 shows $p_1$ as the only place initially marked: $M_0(p_1) = \{<3,0>\}$, whereas $M_0(p_2) = M_0(p_3) = M_0(p_4) = M_0(p_5) = \phi$.

Definition 3: The pre-set $^{\bullet} t = \{p\in P|(p,t)\in I\}$ is the set of input places of $t$. The post-set $t^{\bullet} = \{p\in P|(t,p)\in O\}$ is the set of output places of $t$. The pre-set and post-set of $p\in P$ are represented by $^{\bullet} p = \{t\in T|(t,p)\in O\}$ and $p^{\bullet} = \{t\in T | (p,t)\in I\}$, respectively.

Definition 4: For every transition $t\in T$, a transition function $f$ exists that is associated with $t$, i.e., $\exists f:\tau(p_1)\times \tau(p_2)\times\dots\times$$\tau(p_a)\rightarrow\tau(q)$, where $\tau$ is a type function that associates with every place, $^{\bullet} t = \{p_1,p_2,\dots,p_a\}$, $q\in t^{\bullet}$.

In Fig. 1, for example, there exists a transition function $f_1$ associated with $t_1$.

Definition 5: For every transition $t\in T$, a minimum transition delay $d^{-}$ and a maximum transition delay $d^{+}$ exists, which represent the lower and upper limits for the execution time of the function associated with $t$.

For instance, in Fig. 1, the minimum transition delay of $t_1$ is ${d_1}^{-} = 2$, and the maximum transition delay of $t_1$ is $d^{+} = 5$.

Definition 6: A transition $t\in T$ may have a guard $G$, which is the token values’ function of this transition.

The guard of transition $t$ is a function of the token values in the places of its pre-set $^{\bullet} t$. In Fig. 1, the transition $t_3$ has a guard $G_{t3}$ associated with it.

Definition 7: For an enabled transition $t$, there is an enabling time $et$. $et$ is the time instant at which $t$ is enabled and is given by the maximum token time of the tokens in the binding. The earliest trigger time of the enabled transition $t$ is $t^{-} = et+d^{-}$, and $t^{+} = et+d^{+}$ is the latest trigger time.

A PRES+ model is a restricted version of the CPN model. For successor marking definition, a more formal way is proposed in [36]. In this restricted CPN model, a marking $M$ is a tupe $<P_M,val_M>$, where $P_M$ is a subnet of places and $val_M$ is a mapping from places to token values. $T_M$ is the set of enabled transitions for a marking $M$. $f_t$ is a function associated with transition $t$.

Definition 8 [36]: A marking $M^{+} = <P_{M^{+}},val_{M^{+}}>$ is said to be a successor of the marking $M = <P_M,val_M>$, if i) the first component $P_{M^{+}}$, referred to as the successor place marking of $P_M$, contains all the post-places of the enabled transitions of $P_M$ and all the places of $P_M$ whose post-transitions are not enabled; symbolically, $P_{M^{+}} = \{p|p\in t^{\bullet}$${\rm and}\;t\in T_M \}\cup\{p|p\in P_M\;{\rm and}\;p\not\in^{\bullet} T_M\}$, and ii) $\forall p\in P_{M^{+}}$, if $p = t^{\bullet}$ for some $t\in T_M$, then $val_{M^{+}}(p) = f_t(val_M(^{\bullet} t))$ and if $p\not\in^{\bullet} T_M$, then $val_{M^{+}}(p) = val_M(p)$.

Note that, for verification purposes, the PRES+ nets can be restricted to safe PRES+ nets [2], that is, every place $p\in P$ holds at most one token for every marking M reachable from $M_0$.

III. Synthesis Operations

In this section, the synthesis shared transition set operation and the synthesis shared transition subnet set operation for the PRES+ model are proposed.

A Shared Transition Set Synthesis Operation

Definition 9: A PRES+ model $N = (P,T,I,O,M_0)$ is called a shared transition set synthesis PRES+ model of $N_1 = (P_1,T_1,I_1,O_1,M_{10})$ and $N_2 = (P_2,T_2,I_2,O_2,M_{20})$, if $P_1\cap P_2 = \phi$, $T_1\cap T_2 = T_m \ne \phi$ (where $T_m$ is the shared transition set); $P = P_1\cup P_2$, $T = T_1\cup T_2$; $I = I_1\cup I_2$; $O = O_1\cup O_2$;

${M_0}^{\prime} (P) = \left\{ {\begin{array}{*{20}{c}} {{M_{10}}(p)}&{p \in {P_1}}\\ {{M_{20}}(p)}&{p \in {P_2}} \end{array}} \right.$.

Definition 10: Suppose$N_1$ has a transition set $\{t_{11}, t_{12},\dots,$$t_{1k}\}$ (where $^{\bullet} t_{1i} \cap ^{\bullet} t_{1j} = \phi$, ${t_{1i}}^{\bullet} \cap {t_{1j}}^{\bullet} = \phi$, $i\ne j$ $(1\leq i, j\leq k$)). $N_2$ has the same type of transition set $\{t_{21},t_{22},\dots,t_{2k}\}$ (where $^{\bullet} t_{2i} \cap ^{\bullet} t_{2j} = \phi$, ${t_{2i}}^{\bullet} \cap {t_{2j}}^{\bullet} = \phi$, $i\ne j$ ($1\leq i, j\leq k$). In the synthesis procedure, the same type transition $t_{1i}\in T_1$ of $N_1$ and $t_{2i}\in T_2$ of $N_2$ are merged into transition $t_{mi}\in T_m$ of $N$, where $1\leq i\leq k$.

Definition 11: Let $f_{1i}$ be the transition function of $t_{1i}\in T_1$ $(1\leq i\leq k)$, $f_{2i}$ be the transition function of $t_{2i}\in T_2$ $(1\leq i\leq k)$, and $f_{1i} = f_{2i}$. We define $f_{mi} = f_{1i}$ $(1\leq i\leq k)$.

Definition 12: Let $[{d_{1i}}^{-},{d_{1i}}^{+}]$ and $[{d_{2i}}^{-},{d_{2i}}^{+}]$ be the transition delays of $t_{1i}\in T_1$ and $t_{2i}\in T_2$ $(1\leq i\leq k)$, respectively, and $[{d_{1i}}^{-},{d_{1i}}^{+}]$ = $[{d_{2i}}^{-},{d_{2i}}^{+}]$. We define $[{d_{mi}}^{-},{d_{mi}}^{+}] = [{d_{1i}}^{-},{d_{1i}}^{+}]$ $(1\leq i\leq k)$.

Definition 13: Let $et_{1i}$ and $et_{2i}$ be the enable times of enabled transitions $t_{1i}\in T_1$ and $t_{2i}\in T_2$ $(1\leq i\leq k)$, respectively. Suppose $et_{1i} = et_{2i}$ $(1\leq i\leq k)$. Let $d_{1ie} = et_{1i} +$ ${d_{1i}}^{-}$ and $d_{1il} = et_{1i} + {d_{1i}}^{+}$ be the earliest trigger time and the latest trigger time of $t_{1i}$ $(1\leq i\leq k)$, respectively. Let $d_{2ie} = et_{2i} + {d_{2i}}^{-}$ and $d_{2il} = et_{2i} + {d_{2i}}^{+}$ be the earliest trigger time and the latest trigger time of $t_{2i}$ $(1\leq i\leq k)$, respectively. For $t_{mi}$ $(1\leq i\leq k)$, $d_{mie}$ is the earliest trigger time and $d_{mil}$ is the latest trigger time. We define $d_{mie} = d_{1ie}$ and $d_{mil} = d_{1il}$ $(1\leq i\leq k)$.

From the above, it is clear that $d_{1ie} = d_{2ie}$ and $d_{1il} = d_{2il}$ $(1\leq i\leq k)$.

B Transition Subnet

Definition 14: A PRES+ model $N_T = (P_T, T_T, I_T, O_T,$ $M_{T,0})$ is called a transition subnet of $N = (P, T, I, O, M_0)$ if $P_T\subseteq P$, $T_T\subseteq T$ and $P_T\ne \phi$, $T_T\ne \phi$, $^{\bullet} P_T \cup P_T^{\bullet} \subseteq T_T$, $I_T = I\cap (P_T\times$$T_T)$, $O_T = O\cap (T_T\times P_T)$; $N_T$ is connected, $\{t_{{\rm{in}}},t_{{\rm{out}}}\}\subseteq T_T$ (where $t_{{\rm{in}}}$ is the input transition of $N_T$, and $t_{{\rm{out}}}$ is the output transition of $N_T$); $\forall t\in T_T$, and there exists a transition function $f$ and a transition delay $[d^{-},d^{+}]$ (where $d^{-}\leq d^{+}$).

Definition 15: For the transition set $T_T-\{t_{{\rm{in}}},t_{{\rm{out}}}\}$ of $N_T$, a transition set delay $[{d_s}^{-},{d_s}^{+}]$, and a transition set function $f_s$ are presented.

Supposition 1: Suppose $N_T$ satisfies:

1) In a procedure (tokens from outside flow into $t_{\rm in}$, across $N_T$, then flow out from $t_{\rm out}$), $t_{\rm out}$ is fired if and only if $t_{\rm in}$ is fired.

2) $P_T$ has a token in neither the initial state nor after a procedure.

3) Before $t_{\rm in}$ is fired and after $t_{\rm out}$ is fired, $\forall t\in T_T- \{t_{\rm in},t_{\rm out}\}$, $t$ can not be enabled.

C Shared Transition Subnet Set Synthesis Operation

In this section, we present the shared transition subnet set synthesis operation. Fig. 2 shows a schematic diagram of synthesis operation.

Figure  2.  A schematic diagram of the shared transition subnet set synthesis operation

DownLoad: Full-Size Img PowerPoint

Definition 16: Let $N_1 = (P_1,T_1,I_1,O_1,M_{10})$ and $N_2 = (P_2,T_2,I_2,O_2,M_{20})$ be two PRES+ models. Then $N = (P,T,I,O,M_0)$ is called a synthesis net of the shared transition subnet set if the following conditions are satisfied: $P = P_1\cup P_2$; $T = T_1\cup T_2$; $I = I_1\cup I_2$; $O = O_1\cup O_2$; If $p\in P_1\cap$$P_2$, then $M_{10}(p) = M_{20}(p)$; ${M_0}(p) = \left\{ {\begin{array}{*{20}{c}} {{M_{10}}(p)}&{p \in {P_1}}\\ {{M_{20}}(p)}&{p \in {P_2}} \end{array}} \right.$.

In Fig. 2, the PRES+ model $N$ is the synthesis net of $N_1$ and $N_2$, where $N_{1r} = N_1-\{N_{T11}\cup N_{T12}\}$ and $N_{2r} = N_2-\{N_{T21}\cup$$N_{T22}\}$.

Supposition 2: Suppose $N_1$ and $N_2$ satisfy:

1) $N_1$ and $N_2$ have the same type of transition subnet set $N_{T1} = (N_{T11},N_{T12},\dots,N_{T1k})$ and $N_{T2} = (N_{T21},$ $N_{T22},\dots,N_{T2k})$, where $N_{T1i}$ and $N_{T2i}$ ($i = 1,2,\dots,k$) are transition subnets.

2) Let $t_{T1i_{\rm in}}$ and $t_{T1i_{\rm out}}$ be the input transition and the output transition of $N_{T1i}$ $(1\leq i\leq k)$, respectively. Suppose $^{\bullet} t_{T1i_{\rm in}} \cap ^{\bullet} t_{T1j_{\rm in}} = \phi$, and ${t_{T1i_{\rm out}}}^{\bullet} \cap {t_{T1j_{\rm out}}}^{\bullet} = \phi$, where $i\ne j$ $(1\leq i, j\leq k)$.

3) Let $t_{T2i_{\rm in}}$ and $t_{T2i_{\rm out}}$ be the input transition and the output transition of $t_{T2i}$ $(1\leq i\leq k)$, respectively. Suppose $^{\bullet} t_{T2i_{in}} \cap ^{\bullet} t_{T2j_{\rm in}} = \phi$, and ${t_{T2i_{\rm out}}}^{\bullet} \cap {t_{T2j_{\rm out}}}^{\bullet} = \phi$, where $i\ne j$ $(1\leq i, j\leq k)$.

For example, in Fig. 2, $N_1$ and $N_2$ have the same type of transition subnet set $N_{T1} = (N_{T11}, N_{T12})$ and $N_{T2} = (N_{T21},$$N_{T22})$. Here, $t_{T1i_{\rm in}}$ and $t_{T1i_{\rm out}}$ are the input transition and the output transition of $N_{T1i}(i = 1,2)$, with $^{\bullet} t_{T11_{\rm in}} \cap ^{\bullet} t_{T12_{\rm in}} = \phi$, and ${t_{T11_{\rm out}}}^{\bullet} \cap {t_{T12_{\rm out}}}^{\bullet} = \phi$. $t_{T2i_{\rm in}}$ and $t_{T2i_{\rm out}}$ are the input transition and the output transition of $N_{T1i}$ $(i = 1,2)$, with $^{\bullet} t_{T21_{\rm in}} \cap ^{\bullet} t_{T22_{\rm in}} = \phi$, and ${t_{T21_{\rm out}}}^{\bullet} \cap {t_{T22_{\rm out}}}^{\bullet} = \phi$.

Definition 17 (Synthesis Operation): $N_{T1} = (N_{T11},$ $N_{T12},\dots, N_{T1k})$ and $N_{T2} = (N_{T21},N_{T22},\dots,N_{T2k})$ are merged as transition subnets $N_{Tm} = (N_{Tm1},N_{Tm2},\dots,N_{Tmk})$ in $N$. The arcs that link $N_{Ti}$ $(i = 1,2,\dots,k)$ in $N_1$ and $N_2$ are then linked to the synthesis subnets $N_{Tmi}$ $(i = 1,2,\dots,k)$. Weights on arcs are preserved.

For instance, in Fig. 2, $N_{T1} = (N_{T11}, N_{T12})$ and $N_{T2} =$ $(N_{T21}, N_{T22})$ are merged as transition subnets $N_{Tm} = (N_{Tm1}, N_{Tm2})$ in $N$.

Supposition 3: It is assumed that $f_{T1i_{\rm in}} (f_{T1i_{\rm out}})$ is the transition function of input transition $t_{T1i_{\rm in}}$ (output transition $t_{T1i_{\rm out}}$) of $N_{T1i}$ $(1\leq i\leq k)$, and $f_{T2i_{\rm in}}(f_{T2i_{\rm out}})$ is the transition function of input transition $t_{T2i_{\rm in}}$ (output transition $t_{T2i_{\rm out}}$ of $N_{T2i}$ $(1\leq i\leq k)$. Suppose $f_{T1i_{\rm in}}$ = $f_{T2i_{\rm in}}$, $f_{T1i_{\rm out}}$ = $f_{T2i_{\rm out}}$, and $f_{Tmi_{\rm in}}$ = $f_{T1i_{\rm in}}$, $f_{Tmi_{\rm out}}$ = $f_{Ti_{\rm out}}$ $(1\leq i\leq k)$.

Note that, in Fig. 2, for convenience, the transition function and transition delay were omitted. For example, in Fig. 2, let $f_{T11_{\rm in}}$ be the transition function of $t_{T1i_{\rm in}}$, and $f_{T11_{\rm out}}$ be the transition function of $t_{T1i_{\rm out}}$. Let $f_{T21_{\rm in}}$ be the transition function of $t_{T21_{\rm in}}$, and $f_{T21_{\rm out}}$ be the transition function of $t_{T21_{\rm out}}$. Let $f_{Tm1_{\rm in}}$ be the transition function of $t_{Tm1_{\rm in}}$, and $f_{Tm1_{\rm out}}$ be the transition function of $t_{Tm1_{\rm out}}$. Suppose $f_{T11_{\rm in}} = f_{T21_{\rm in}}$, $f_{T11_{\rm out}} = f_{T21_{\rm out}}$, and $f_{Tm1_{\rm in}} = f_{T11_{\rm in}}$, $f_{Tm1_{\rm out}} =$$f_{T11_{\rm out}}$.

Supposition 4: Assume $[{d_{T1i_{\rm in}}}^{-},{d_{T1i_{\rm in}}}^{+}]$ is the transition delay of input transition $t_{T1i_{\rm in}}$ and $[{d_{T1i_{\rm out}}}^{-},{d_{T1i_{\rm out}}}^{+}]$ is the transition delay of output transition $t_{T1i_{\rm out}}$ of $N_{T1i}$ $(1\leq i\leq k)$, $[{d_{T2i_{\rm in}}}^{-},{d_{T2i_{\rm in}}}^{+}]$ is the transition delay of input transition $t_{T2i_{\rm in}}$ and $[{d_{T2i_{\rm out}}}^{-},{d_{T2i_{\rm out}}}^{+}]$ is the transition delay of output transition $t_{T2i_{\rm out}}$ of $N_{T2i}$ $(1\leq i\leq k)$. Suppose $[{d_{T1i_{\rm in}}}^{-},{d_{T1i_{\rm in}}}^{+}] =$$[{d_{T2i_{\rm in}}}^{-}, {d_{T2i_{\rm in}}}^{+}]$, $[{d_{T1i_{\rm out}}}^{-}, {d_{T1i_{\rm out}}}^{+}] = [{d_{T2i_{\rm out}}}^{-},{d_{T2i_{\rm out}}}^{+}]$, and $[{d_{Tmi_{\rm in}}}^{-},{d_{Tmi_{\rm in}}}^{+}] = [{d_{T1i_{\rm in}}}^{-}, {d_{T1i_{\rm in}}} ^{+}], [{d_{Tmi_{\rm out}}} ^{-},{d_{Tmi_{\rm out}}} ^{+}] =[{d_{T1i_{\rm out}}}^{-},$ ${d_{T1i_{\rm out}}}^{+}]$ $(1\leq i\leq k)$.

For example, in Fig. 2, let $[{d_{T11_{\rm in}}}^{-}, {d_{T11_{\rm in}}}^{+}]$ be the transition delay of $t_{T11_{\rm in}}$, and $[{d_{T11_{\rm out}}}^{-},{d_{T11_{\rm out}}}^{+}]$ be the transition delay of $t_{T11_{\rm out}}$. Let $[{d_{T21_{\rm in}}}^{-},{d_{T21_{\rm in}}}^{+}]$ be the transition delay of $t_{T21_{\rm in}}$ and $[{d_{T21_{\rm out}}}^{-},{d_{T21_{\rm out}}}^{+}]$ be the transition delay of $t_{T21_{\rm out}}$. Let $[{d_{Tm1_{\rm in}}}^{-},{d_{Tm1_{\rm in}}}^{+}]$ be the transition delay of $t_{Tm1_{\rm in}}$, $[{d_{T21_{\rm out}}}^{-},{d_{T21_{\rm out}}}^{+}]$ be the transition delay of $t_{Tm1_{\rm out}}$. Suppose $[{d_{T11_{\rm in}}}^{-},$ ${d_{T1_{\rm in}}}^{+}] = [{d_{T21_{\rm in}}}^{-},{d_{T21_{\rm in}}}^{+}] = [{d_{Tm1_{\rm in}}}^{-},{d_{Tm1_{\rm in}}}^{+}]$, and $[{d_{T11_{\rm out}}}^{-},{d_{T1_{\rm out}}}^{+}] = [{d_{T21_{\rm out}}}^{-},{d_{T21_{\rm out}}}^{+}] = [{d_{Tm1_{\rm out}}}^{-},{d_{Tm1_{\rm out}}}^{+}]$.

IV. Abstraction-Synthesis-Refinement Representation Method

In this section we will present an abstraction-synthesis-refinement representation method and propose the transition subnet refinement operation and the transition subnet abstraction operation.

Since it is difficult to operate directly on the synthesis of shared transition subnets, we adopt the solution from an abstraction operation and a synthesis operation to a refinement operation. This solution is useful in proving certain theorems in Sections V and VI.

Fig. 3 illustrates a synthesis of shared transition subnet solution.

Figure  3.  A synthesis of shared transition subnet solution

DownLoad: Full-Size Img PowerPoint

In Fig. 3, ${N_1}'$ is obtained from $N_1$ by the abstraction operation, i.e., transition subnets $N_{T11}, \dots, N_{T1k}$ of $N_1$ are abstracted to $t_{T11}, \dots, t_{T1k}$ respectively. ${N_2}'$ is obtained from $N_2$ by an abstraction operation. $N'$ is obtained from ${N_1}'$ and ${N_2}'$ by using the shared transition set synthesis operation. $N$ is obtained from $N'$ by using the transition refinement operation. So, by using the abstraction-synthesis-refinement representation method, the synthesis shared transition subnet technique of PRES+ can be investigated through the synthesis shared transition set technique.

In this section, definitions of the transition subnet refinement operation and the transition subnet abstraction operation are proposed.

Definition 18 (Transition Subnet Refinement Operation) [7]: the refined net $N' = (P',T',I',O',{M_0}')$ is assumed to be obtained from $N = (P,T,I,O,M_0)$ by using subnet $N_T = (P_T,T_T,I_T,O_T,M_{T,0})$ to replace $\bar{t}$ (where $\bar{t} \in T)$ of $N$, where

i) $P' = P\cup P_T$;

ii) $T' = T\cup T_T-\{\overline t\}$;

iii) $\left(p,t\right)\in I'$, if $\left(p,t\right)\in I\cup I_T$; $\left(t,p\right)\in O'$, if $\left(t,p\right)\in O\cup O_T$;

iv) $\left(p,t_{\rm in}\right)\in I'$, if $\left(p,\overline t\right)\in I$; $\left(t_{\rm out},p\right)\in O'$, if $\left(\overline t,p\right)\in O$;

v) ${M_0}^{\prime} \left( p \right) = \left\{ {\begin{array}{*{20}{c}} {{M_0}\left( p \right)}&{\forall p \in P}\\ {{M_{T,0}}\left( p \right)}&{\forall p \in {P_T}} \end{array}} \right.$;

vi) $f_{\rm out}\circ f_s\circ f_{\rm in} = f_{\bar{t}}$ (where $\circ$ is the compounding operator);

vii) ${d_{\rm in}}^{-}+{d_s}^{-}+{d_{\rm out}}^{-} = {d_{\bar{t}}}^{-}$; ${d_{\rm in}}^{+}+{d_s}^{+}+{d_{\rm out}}^{+} = {d_{\bar{t}}}^{+}$.

Note that, in the following, the process of the transition subnet abstraction operation (Definition 19) is the inverse of the process of the transition subnet refinement operation (Definition 18).

Definition 19 (Transition Subnet Abstraction Operation): here $N' = (P',T',I',O',{M_0}')$ is assumed to be obtained from $N = (P,T,I,O,M_0)$ by using $\bar{t}$ (where $\bar{t}\not\in T$, $\bar{t}\in T'$) to replace $N_T = (P_T,T_T,I_T,O_T,M_{T,0})$, where

i) $P' = P-P_T$;

ii) $T' = T\cup\{\overline t\}-T_T$;

iii) $\left(p,\overline t\right)\in I'$ (where $p\in^{\bullet} t_{\rm in})$ and $(p,t)\in I'$, if $(p,t)\in I-I_T$; $(\bar{t},p)\in O'$ (where $p\in {t_{\rm out}}^{\bullet}$) and $(t,p)\in O'$, if $(t,p)\in O-O_T$;

iv) ${M_0}'(p) = M_0(p)$ where $p\in P-P_T$;

v) $f_{\bar{t}} = f_{\rm out}\circ f_s\circ f_{\rm in}$;

vi) ${d_{\bar{t}}}^{-} = {d_{\rm in}}^{-}+{d_s}^{-}+{d_{\rm out}}^{-}$; ${d_{\bar{t}}}^{+} = {d_{\rm in}}^{+}+{d_s}^{+}+{d_{\rm out}}^{+}$.

Note that $f_{\bar{t}}$ is the transition function of $\bar{t}$. Then $f_{\rm in}$, $f_{\rm out}$, and $f_s$ are the transition functions of input transition $t_{\rm in}$ of $N_T$, output transition $t_{\rm out}$ of $N_T$, and $T_T-\{t_{\rm in},t_{\rm out}\}$, respectively. $[{d_{\bar{t}}}^{-},{d_{\bar{t}}}^{+}]$, $[{d_{\rm in}}^{-},{d_{\rm in}}^{+}]$, $[{d_{\rm out}}^{-},{d_{\rm out}}^{+}]$, and $[{d_{s}}^{-},{d_{s}}^{+}]$, are the transition delays of $\bar{t}$, $t_{\rm in}$, $t_{\rm out}$, and $T_T-\{t_{\rm in},t_{\rm out}\}$, respectively.

V. Reachability, Functionality, and Timing Preservations

In this section, some fundamentals of two PRES+ models with the same reachability, timing, and functionality are initially reviewed [7]. Reachability, timing, and functionality preservations of these two synthesis PRES+ models are then discussed.

Two PRES+ subnets $N_a$ and $N_b$ are considered, which have the same number of input places and output places. If the same number of tokens are put into the input places of $N_a$ and $N_b$, and the number of tokens in the output places of $N_a$ is equal to that of $N_b$, then $N_a$ and $N_b$ are labeled as having the same reachability.

If $N_a$ and $N_b$ have the same reachability, and if the tokens’ type of input places of $N_a$ is equal to that of $N_b$, and the tokens’ type of output places of $N_a$ is equal to that of $N_b$, then $N_a$ and $N_b$ are considered to have the same functionality. If $N_a$ and $N_b$ have the same reachability, the tokens’ time of input places of $N_a$ is equal to that of $N_b$, and the tokens’ time of output places of $N_a$ is equal to that of $N_b$, then $N_a$ and $N_b$ are observed to have the same timing.

In this section, we investigate the shared transition set synthesis PRES+ model’s preservation of reachability, functionality, and timing.

Theorem 1: Suppose that $N_1 = (P_1,T_1,I_1,O_1,M_{10})$ and $N_2 = (P_2,T_2,I_2,O_2,M_{20})$ are two PRES+ models that have the same type transition set. Let $N = (P,T,I,O,M_0)$ be the shared transition set synthesis PRES+ model of $N_1$ and $N_2$. Then the reachability, functionality, and timing of $N$ are the same as those of $N_1$ and $N_2$.

Proof: Assume that $\{t_{11},t_{12},\dots,t_{1k}\}$ is the transition set of $N_1 = (P_1,T_1,I_1,O_1,M_{10})$. According to transition $t_{1i}\in T_1$ $(1\leq i\leq k)$, a place bordered subnet $N_{1i} = (P_{1i},T_{1i},I_{1i},$ $O_{1i},M_{1i0})$ $(1\leq{i}\leq{k})$ of $N_1$ exists, where $P_{1i} = P_{1i{\rm in}}\cup P_{1i{\rm out}}$, $P_{1i{\rm in}} = \{p|p\in ^{\bullet} t_{1i}\}$, $P_{1iout} = \{p|p\in {t_{1i}}^{\bullet}\}$; $I_{1i} = \{(p,t_{1i})|p\in P_{1i{\rm in}}\}$; $O_{1i} = \{(t_{1i},p)|p\in P_{1i{\rm out}}\}$; and $M_{1i0}$ is the projection of $M_{10}$ on $P_{1i}$. It is assumed that $\{t_{21},t_{22},\dots,t_{2k}\}$ is the transition set of $N_2 = (P_2,T_2,I_2,O_2,M_{20})$. Corresponding to transition $t_{2i}\in T_2$ $(1\leq i\leq k)$, a place bordered subnet $N_{2i} = (P_{2i},T_{2i},I_{2i},$ $O_{2i},M_{2i0})$ $(1\leq i\leq k)$ of $N_2$ exists, where $P_{2i} = P_{2i{\rm in}}\cup P_{2i{\rm out}}$, $P_{2i{\rm in}} = \{p|p\in ^{\bullet} t_{2i}\}$, $P_{2i{\rm out}} = \{p|p\in {t_{2i}}^{\bullet}\}$; $I_{2i} = \{(p,t_{2i}) | p\in P_{2i{\rm in}} \}$; $O_{2i} = \{(t_{2i},p)|p\in P_{2i{\rm out}}\}$; and $M_{2i0}$ is the projection of $M_{20}$ on $P_{2i}$. Suppose $N_{mi} = (P_{mi},T_{mi},I_{mi},O_{mi},M_{mi0})$ of $N = (P,T,I,$ $O,M_0)$ is the synthesis subnet of $N_{1i}$ and $N_{2i}$. Here, $P_{mi} = P_{1i}\cup P_{2i}$; $t_{1i}$ and $t_{2i}$ are merged as $t_{mi}$; $I_{mi} = I_{1i}\cup I_{2i}$; and $O_{mi} = O_{1i}\cup O_{2i}$, $M_{m0}(p) = \left\{\begin{array}{lc}M_{i10}(p)&p\in P_{i1}\\M_{i20}(p)&p\in P_{i2}\end{array}\right.$.

The input places and output places of $N_{1i}$ and $N_{2i}$ are the same as those of $N_{mi}$. The tokens’ number of input places of $N_{1i}$ and $N_{2i}$ is the same as that of $N_{mi}$. Since $N_{mi}$ is the synthesis model of $N_{1i}$ and $N_{2i}$, by the concept of shared transition set synthesis, the tokens’ number of output places of $N_{1i}$ and $N_{2i}$ is the same as that of $N_{mi}$. Then the reachability of $N_{mi}$ is the same as that of $N_{1i}$ and $N_{2i}$.

By the concept of shared transition set synthesis, the tokens’ type in the input places of $N_{1i}$ and $N_{2i}$ is the same as that of $N_{mi}$. The transition function of $t_{1i}$ is $f_{1i}$, and the transition function of $t_{2i}$ is $f_{2i}$. As $f_{1i} = f_{2i}$ and $f_{mi} = f_{1i}$, then the tokens’ type in the output places of $N_{1i}$ and $N_{2i}$ is the same as that of $N_{mi}$. The functionality of $N_{mi}$ is then the same as that of $N_{1i}$ and $N_{2i}$.

By the shared transition set synthesis operation, the tokens’ time in the input places of $N_{1i}$ and $N_{2i}$ is the same as that of $N_{mi}$. The transition delay of $t_{1i}$ is $[{d_{1i}}^{-},{d_{1i}}^{+}]$, and the transition delay of $t_{2i}$ is $[{d_{2i}}^{-},{d_{2i}}^{+}]$. The earliest trigger time of $t_{1i}$ is $d_{1ie} = et_{1i}+{d_{1i}}^{-}$, and the latest trigger time of $t_{1i}$ is $d_{1il} = et_{1i}+{d_{1i}}^{+}$ $(1\leq i\leq k)$. The earliest trigger time of $t_{2i}$ is $d_{2ie} = et_{2i}+{d_{2i}}^{-}$, and the latest trigger time of $t_{2i}$ is $d_{2il} = et_{2i}+{d_{2i}}^{+}$ $(1\leq i\leq k)$. Because $[{d_{mi}}^{-},{d_{mi}}^{+}] = [{d_{1i}}^{-},{d_{1i}}^{+}]$, $[{d_{1i}}^{-},{d_{1i}}^{+}] = [{d_{2i}}^{-},{d_{2i}}^{+}]$, $d_{mie} = d_{1ie} = d_{2ie}$, and $d_{mil} = d_{1il} =$$d_{2il}$, by the shared transition set synthesis operation, the tokens’ time in the output places of $N_{1i}$ and $N_{2i}$ is the same as that of $N_{mi}$. The timing of $N_{mi}$ is thus the same as that of $N_{1i}$ and $N_{2i}$.

Let ${\overline{N}}_1$ be the remaining part of $N_1$, i.e., ${\overline{N}}_1 = N_1-\{N_{11},N_{12},\dots,N_{1k}\}$, and ${\overline{N}}_2$ the remaining part of $N_2$, that is, ${\overline{N}}_2 = N_2-\{N_{21},N_{22},\dots,N_{2k}\}$. Let ${\overline{N}}$ be the remaining part of $N$, i.e., ${\overline{N}} = N-\{N_{m1},N_{m2},\dots,N_{mk}\}$. As ${\overline{N}} = {\overline{N}}_1\cup {\overline{N}}_2$, the reachability, functionality, and timing of $N$ are the same as those of $N_1$ and $N_2$.■

In this section, we will use the abstraction-synthesis-refinement representation method to investigate the preservation of reachability, functionality, and timing of the shared transition subnet set synthesis PRES+ model. In this synthesis process, Lemmas 1 and 2 play an important role.

Lemma 1: Let $N' = (P',T',I',O',M_0')$ be obtained from $N = (P,T,I,O,M_0)$ by using the transition subnet abstraction operation. The reachability, functionality, and timing of $N'$ are then the same as those of $N$.

Proof: Let subnet $N_{\overline{T}} = (P_{\overline{T}},T_{\overline{T}},I_{\overline{T}},O_{\overline{T}},M_{\overline{T},0})$, where $P_{\overline{T}} = P_T\cup \{p\in P|p\in ^{\bullet} t_{\rm in}\cup {t_{\rm out}}^{\bullet}\}$; $T_{\overline{T}} = T_T$; $I_{\overline{T}} = I_T\cup \{(p,t_{\rm in}))$ $|p\in ^{\bullet} t_{\rm in}\}$; $O_{\overline{T}} = O_T\cup \{(t_{\rm out},p)|p\in {t_{\rm out}}^{\bullet}\}$;

$M_{\overline{T},0} = \left\{\begin{array}{lc}M_{T,0}(p)&p\in P_{T}\\M_0|(^{\bullet} t_{\rm in}\cup {t_{\rm out}}^{\bullet})(p)&p\in ^{\bullet} t_{\rm in}\cup {t_{\rm out}}^{\bullet}\end{array}\right.$.

Let subnet $N_{\overline{t}} = (P_{\overline{t}},T_{\overline{t}},I_{\overline{t}},O_{\overline{t}},M_{\overline{t},0})$, where

$P_{\overline{t}} = \{p|p\in ^{\bullet} t_{\rm in}\cup {t_{\rm out}}^{\bullet}\}$; $T_{\overline{t}} = \{\overline{t}\}$;

$I_{\overline{t}} = \{(p,\overline{t})|p\in ^{\bullet} t_{\rm in}\}$;

$O_{\overline{t}} = \{(\overline{t},p)|p\in {t_{\rm out}}^{\bullet}\}$;

$M_{\overline{t},0} = M_0|\{p|p\in (^{\bullet} t_{\rm in}\cup {t_{\rm out}}^{\bullet})\}$.

$N_{\overline{T}} = (P_{\overline{T}},T_{\overline{T}},I_{\overline{T}},O_{\overline{T}},M_{\overline{T},0})$ and $N_{\overline{t}} = (P_{\overline{t}},T_{\overline{t}},I_{\overline{t}},$$O_{\overline{t}},M_{\overline{t},0})$ from above have the same input places $\{p|p\in^{\bullet} t_{\rm in}\}$ and output places $\{p|p\in {t_{\rm out}}^{\bullet}\}$. According to Definition 19, the number of tokens in the input places of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$. As $N' = (P',T',I',O',{M_0}')$ is obtained from $N = (P,T,I, O,$ $M_0)$ by using the transition subnet abstraction operation, and by the concept of transition subnet and Definition 19, the number of tokens of output places for $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$. As such, the reachability of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$.

By Definition 19, the type of tokens in the input place of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$. Since $f_{\overline{t}} = f_{\rm out}\circ f_s\circ f_{\rm in}$, the type of tokens in the output places of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$. Thus, the functionality of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$.

By Definition 19, the token time of tokens in the input place of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$. As ${d_{\overline{t}}}^{-} = {d_{\rm in}}^{-}+$ ${{d_s}}^{-}+{d_{\rm out}}^{-}$ and ${d_{\overline{t}}}^{+} = {d_{\rm in}}^{+}+{{d_s}}^{+}+{d_{\rm out}}^{+}$, thus the token time of tokens in the output places of $N_{\overline{T}}$ is the same as that of $N_{\overline{t}}$. The timing of $N_{\overline{T}}$ is thus the same as that of $N_{\overline{t}}$.

As $N'-N_{\overline{t}} = N-N_{\overline{T}}$, the reachability, functionality, and timing of $N'$ are the same as those of $N$.■

Lemma 2 [7]: Let $N' = (P',T',I',O',{M_0}')$ be obtained from $N = (P,T,I,O,M_0)$ by using the transition subnet refinement operation. Then the reachability, functionality, and timing of $N'$ are the same as those of $N$.

The abstraction-synthesis-refinement representation method is used in the following proof for Theorem 2. First, the original PRES+ models $N_1$ and $N_2$ are abstracted as ${N_1}'$ and ${N_2}'$, respectively. Then the synthesis net $N'$ of ${N_1}'$ and ${N_2}'$ is obtained by using the shared transition set synthesis operation. Finally, $N'$ is refined as $N$. The properties of reachability, functionality, and timing are guaranteed to be preserved by Lemmas 1, 2, and Theorem 1.

Theorem 2: Let $N_1 = (P_1,T_1,I_1,O_1,M_{10})$ and $N_2 = (P_2,T_2,$ $I_2,O_2,M_{20})$ be two PRES+ models. $N = (P,T,I,O,M_0)$ is the synthesis net of the $N_1$ and $N_2$ shared transition subnet set. The reachability, functionality, and timing of $N$ are subsequently those of $N_1$ and $N_2$.

Proof: Let ${N_1}' = ({P_1}',{T_1}',{I_1}',{O_1}',{M_{10}}')$ be obtained from $N_1 = (P_1,T_1,I_1,O_1,M_{10})$ by using the transition subnet abstraction operation (Definition 19), i.e., the transition subnet set $N_{T1} = \{N_{T11},N_{T12},\dots,N_{T1k}\}$ of $N_1 = (P_1,T_1,I_1,O_1,$ $M_{10})$ is replaced by the transition set $T_{T1} = \{{\overline{t}}_{11},{\overline{t}}_{12},\dots,{\overline{t}}_{1k}\}$ of ${N_1}' = ({P_1}',{T_1}',{I_1}',{O_1}',{M_{10}}')$. According to Lemma 1, the reachability, functionality, and timing of $N_1'$ are the same as those of $N_1$. Let ${N_2}' = ({P_2}',{T_2}',{I_2}',{O_2}',{M_{20}}')$ be obtained from $N_2 = (P_2,T_2,I_2,O_2,M_{20})$ by using the transition subnet abstraction operation (Definition 19); that is, the transition subnet set $N_{T2} = \{N_{T21},N_{T22},\dots,N_{T2k}\}$ of $N_2 = (P_2,T_2,I_2,O_2,$ $M_{20})$ is replaced by the transition set $T_{T2} = \{{\overline{t}}_{21},{\overline{t}}_{22},\dots,{\overline{t}}_{2k}\}$ of ${N_2}' = ({P_2}',{T_2}',{I_2}',{O_2}',{M_{20}}')$. By Lemma 1, the reachability, functionality, and timing of $N_2'$ are the same as those of $N_2$.

The shared transition set synthesis PRES+ model $N' = (P',T',I',O',{M_0}')$ of ${N_1}' = ({P_1}',{T_1}',{I_1}',{O_1}',{M_{10}}')$ and ${N_2}' = ({P_2}',{T_2}',{I_2}',{O_2}',{M_{20}}')$ is obtained by using the shared transition set synthesis operation. The same-type transition sets $T_{T1} = \{{\overline{t}}_{11},{\overline{t}}_{12},\dots,{\overline{t}}_{1k}\}$ of ${N_1}'$ and $T_{T2} = \{{\overline{t}}_{21},{\overline{t}}_{22},\dots,{\overline{t}}_{2k}\}$ of ${N_2}'$ are merged as the transition set $T_{Tm} = \{{\overline{t}}_{m1},{\overline{t}}_{m2},\dots,{\overline{t}}_{mk}\}$ of $N'$. According to Theorem 1, the reachability, functionality, and timing of $N$ are the same as those of $N_1$ and $N_2$.

$N = (P,T,I,O,M_0)$ is obtained from $N' = (P',T',I',O',{M_0}')$ by using the transition subnet refinement operation (Definition 18). In this operation, the transition set $T_{Tm} = \{{\overline{t}}_{m1},{\overline{t}}_{m2},\dots,$ ${\overline{t}}_{mk}\}$ is replaced by the transition subnet set $N_{Tm} =$ $\{N_{Tm1},N_{Tm2},\dots,N_{Tmk}\}$. By Lemma 2, the reachability, functionality, and timing of $N'$ are the same as those of $N$. Thus, the reachability, functionality, and timing of N are those of $N_1$ and $N_2$.■

VI. Liveness Preservation

In this section, several fundamentals of the state, liveness, and boundedness of the PRES+ model are reviewed [7], and the liveness preservation of these synthesis approaches for PRES+ model is investigated.

The pair $S = (M,J)$ is a state of the PRES+ model $N$, where M is a marking and $J:T\to R^{+}\cup \{\# \}$ (where $\#$ is a symbol which describes unusable status) is the vector of all possible firing intervals representing the firing domain. Here, $S_0 = (M_0,J_0)$ with

is the initial state of $N$. Then, $\Sigma = (Z,S_0)$ is a PRES+ net system corresponding to $N$, where $Z = (P,T,I,O)$ is the skeleton of $N$. State $S' = (M',J')$ is obtained from $S = (M,J)$ by firing $t$, denoted by $S\xrightarrow tS'$. State $S' = (M',J')$ is obtained from $S = (M,J)$ by the time elapsing $\tau\in {\mathbb R}^{+}$, denoted by $S\xrightarrow\tau S'$. A transition $t$ is live at state $S$ if $\forall S'(S'\in R_N(S)\rightarrow\exists S''(S''\in$$R_N(S'))\wedge S''\xrightarrow t))$. A PRES+ net system $\Sigma = (Z,S_0)$ is live if all transitions are live in $S$. Additionally, place $p\in P$ is considered bounded iff a natural number $K>0$ exists with $M(p)\leq K$ for each $S\in R_N(S_0)$. Similarly, $\Sigma = (Z,S_0)$ is bounded iff all places are bounded.

To investigate the preservation of liveness of these two synthesis approaches, the concept of a PRES+ closed net must be presented.

A net ${\overline N}_T = (\overline P,\overline T,\overline I,\overline O,{\overline M}_0)$ is called a PRES+ closed net if a subnet (from $^{\bullet} t_{\rm in}$, across $N_T$, then to ${t_{\rm out}}^{\bullet}$ in the refined net $N' = (P',T',I',O',M_0')$) is acquired, and a transition $t_T$ is added (where ${d_{t_T}}^{-} = \max\{{d_t}^{-}\vert t\in ^{\bullet} (^{\bullet} t_{\rm in})\wedge t\in T'\}$, ${d_{t_T}}^{+} = \min$ $\{{d_t}^{+} \vert t\in ( {t_{\rm out}}^{\bullet})^{\bullet} \wedge t\in T'\}$, and $f_{t_T}$ is the transition function associated to $t_T$). Arcs $\{(p,t_T)\vert p\in {t_{\rm out}}^{\bullet} \}\cup\{(t_T,p)\vert p\in ^{\bullet} t_{\rm in}\}$ are added. $\overline{\Sigma} = ({\overline Z}_T,{\overline S}_0)$ is the corresponding PRES+ net system, where ${\overline Z}_T = (\overline P,\overline T,\overline I,\overline O)$ and ${\overline S}_0 = ({\overline M}_0,{\overline J}_0)$.

Suppose $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ are two PRES+ net systems. If $N$ is the synthesis net of the $N_1$ and $N_2$ shared transition set (shared transition subnet set), then $\Sigma = (Z,S_0)$ is said to be the synthesis net system of the $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ shared transition set (shared transition subnet set).

Let $\Sigma = (Z,S_0)$ be a net system, where $Z = (P,T,I,O)$. Assume that $T = T_1\cup T_2$ and $T_1\cap T_2 = \phi$. If $t_u, t_v\in T_1$ (where $u\neq v$), and step $\sigma\in {T_2}^\ast$ or $\sigma = \phi$ exists, such that $t_u\sigma t_v$ is a fireable transition sequence, then $(t_u,t_v)$ is called a fireable transition ordered pair of $\Sigma$ on $T_1$.

In this section, we investigate the liveness preservation of the shared transition set synthesis PRES+ model.

Theorem 3: Let PRES+ net system $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ be live and bounded. Suppose $\Sigma = (Z,S_0)$ is the shared transition set synthesis net system of $\Sigma_1$ and $\Sigma_2$. Then $\Sigma$ is live iff for every transition $t$ of $T_m$, $t$ is live.

Proof: (If) For every transition $t$ of $T_m$ and every state $S$ of $R_N(S_0)$, as $t$ is live, then transition steps $\sigma_0$, $\sigma$, time elapsing $\tau_0$, $\tau$, and state $S_1$ of $R_N(S)$ are present, such that $S_0\xrightarrow{\sigma_0,\tau_0}S\xrightarrow{\sigma,\tau}S_1\xrightarrow t$. In this case, $T_m$ is live. For every transition $t$ of $T-T_m$, and every state $S$ of $R_N(S_0)$, without loss of generality, suppose $t\in T_1$. As $\Sigma_1$ is live, state $S\vert_{P1}\in R_N(S')$ and ${S\vert_{P1}}'\in R_N(S\vert_{P1})$ exist, such that ${S\vert_{P1}}'\xrightarrow t$, that is $\exists\sigma_1\in {T_1}^\ast$, $S\vert_{P1}\xrightarrow{\sigma_1,\tau_1}{S\vert_{P1}}'$. If for every transition $t'\in \sigma_1$, and $t'\not\in T_m$, it is assumed that $S_1 = ({S\vert_{P1}}',S\vert_{P2})$, then $S_1\in R_N(S)$ and $S_1\xrightarrow t$. If $t_i\in \sigma_1$, and $t_i\in T_m$ are present, with the following properties: 1) transition delay $\lbrack {d_{mi}}^{-},{d_{mi}}^{+}\rbrack = \lbrack {d_{1i}}^{-},{d_{1i}}^{+}\rbrack$, $\lbrack {d_{1i}}^{-},{d_{1i}}^{+}\rbrack = \lbrack {d_{2i}}^{-},{d_{2i}}^{+}\rbrack$; 2) the earliest trigger time $d_{1ie} = d_{2ie}$ and $d_{mie} = d_{1ie}$; 3) the latest trigger time $d_{1il} = d_{2il}$ and $d_{mie} = d_{1ie}$; 4) transition functions $f_{1i} = f_{2i}$ and $f_{mi} = f_{1i}$; and $T_m$ and $\Sigma_2$ are live, then $\sigma_2\in {T_2}^\ast$ exists, such that $S\vert_{P2}\xrightarrow{\sigma_2,\tau_2}{S\vert_{P2}}'$ and ${S\vert_{P2}}'\xrightarrow t$. Suppose $S_1 = ({S\vert_{P1}}',{S\vert_{P2}}')$, $S_1\in R_N(S)$ exists, such that $S_1\xrightarrow t$. In this case $\Sigma$ is live.

(Only if) Since $\Sigma = (Z,S_0)$ is live and $T_m\subseteq T$, it will be obvious that, for every transition $t$ of $T_m$, $t$ is live.■

Theorem 4: Let the PRES+ net systems $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ be live and bounded. Suppose $\Sigma = (Z,S_0)$ is the shared transition set synthesis net system of $\Sigma_1$ and $\Sigma_2$. $\Sigma_1$ and $\Sigma_2$ hold the same fireable transition ordered pair set on $T_m$. If $S\in R_N(S_0)$ and $t\in T_m$ are present, such that $S\xrightarrow t$, then $\Sigma$ is live.

Proof: It is assumed here that $T_m = \{t_i,t_j,t_k,\dots,t_u,t_v\}$. $\Sigma_1$ and $\Sigma_2$ hold the same fireable transition ordered pair set $\{(t_i,t_j),(t_j,t_k),\dots,(t_u,t_v),(t_v,t_i)\}$ on $T_m$. As $\Sigma_1 = (Z_1,S_{10})$ is live and bounded, then in $\Sigma_1$, there exists $S_{11}\in R_N(S_{10})$ such that $S_{11}\xrightarrow {t_i}$. As $\Sigma_2 = (Z_2,S_{20})$ is live and bounded, and in $\Sigma_2$, there exists $S_{21}\in R_N(S_{20})$ such that $S_{21}\xrightarrow {t_i}$. Suppose $S_0 =(S_0\vert_{P1}, S_0\vert_{P2})$, where $S_0\vert_{P1} = S_{11}$, $S_0\vert_{P2} = S_{21}$. As the transition delay $\lbrack {d_i}^{-},{d_i}^{+}\rbrack = \lbrack {d_{1i}}^{-},{d_{1i}}^{+}\rbrack = \lbrack {d_{2i}}^{-},{d_{2i}}^{+}\rbrack$, the earliest trigger time $d_{ie} = d_{1ie} = d_{2ie}$, the latest trigger time $d_{il} = d_{1il} = d_{2il}$, and the transition function $f_{i} = f_{1i} = f_{2i}$, then $S_0\xrightarrow {t_i}$. Because $(t_i,t_j)$ is a fireable transition ordered pair on $T_m$, by the concept of fireable transition ordered pairs, in $\Sigma_1$, $\sigma_1\in(T_1-T_m)^\ast$ exists such that $t_i\sigma_1t_j$ is a fireable transition sequence of $\Sigma_1$. Additionally, in $\Sigma_2$, there exists $\sigma_2\in(T_2-T_m)^\ast$ such that $t_i\sigma_2t_j$ is a fireable transition sequence of $\Sigma_2$. As the transition delay $\lbrack {d_j}^{-},{d_j}^{+}\rbrack = \lbrack {d_{1j}}^{-},{d_{1j}}^{+}\rbrack = \lbrack {d_{2j}}^{-},{d_{2j}}^{+}\rbrack$, the earliest trigger time $d_{je} = d_{1je} = d_{2je}$, the latest trigger time $d_{jl} = d_{1jl} = d_{2jl}$, and the transition function $f_{j} = f_{1j} = f_{2j}$; thus $S_j\in R_N(S_0)$ is present, such that $S_j\xrightarrow {t_i}$. As $(t_i,t_j),(t_j,t_k),\dots, (t_u,t_v)$, and $(t_v,t_i)$ are fireable transition sequences on $T_m$, for the same reason there is the presence of $S_h\in R_N(S_0)$, $S_h\xrightarrow{t_h}$, where $h = k,\dots,u,v$. That is $T_m$ is live in $\Sigma$. Thus, according to Theorem 3, $\Sigma$ is live.■

In this section, we will use the abstraction-synthesis-refinement representation method to investigate the liveness preservation of the shared transition subnet set synthesis PRES+ model. Lemmas 3 and 4, Theorems 3 and 4 ensure the correctness of the proofs of Theorems 5 and 6.

Lemma 3 [7]: Let the PRES+ net system $\Sigma' = (Z',{S_0}')$ be obtained from $\Sigma = (Z,S_0)$ by the transition subnet refinement operation, i.e., in $\Sigma$, $\overline t$ is replaced by $N_T = (P_T,T_T,I_T,O_T,M_{T,0})$. If $\forall p\in ^{\bullet} t_{\rm in}$, $M'(p)\geq W'(p,t_{\rm in})$, then $\Sigma'$ is live if $\Sigma$ and $\overline{\Sigma}$ are live.

Lemma 4: Let the PRES+ net system $\Sigma' = (Z',{S_0}')$ be obtained from $\Sigma = (Z,S_0)$ by the transition subnet abstraction operation, i.e., in $\Sigma$, $N_T = (P_T,T_T,I_T,O_T,M_{T,0})$ is replaced by $\overline t$. If $\forall p\in ^{\bullet} t_{\rm in}$, $M(p)\geq W(p,t_{\rm in})$, then $\Sigma'$ is live if $\Sigma$ and $\overline{\Sigma}$ are live.

Note that the proof process of Lemma 4 is the inverse of the proof process of Lemma 3.

Theorem 5: Here it is assumed that $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ are two live and bounded PRES+ net systems, $\Sigma = (Z,S_0)$ is the synthesis net system of $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ with shared transition subnet set $N_T = \left\{N_{T1},N_{T2},\dots,N_{Tk}\right\}$, and $\forall p\in ^{\bullet} t_{j{\rm in}}$, $M'(p)\geq W'(p,t_{j{\rm in}})$ (where $t_{j{\rm in}}$ is the input transition of $N_{Tj}$, $j = 1,2,\dots,k$). ${\Sigma_1}'({\Sigma_2}')$ is obtained from $\Sigma_1(\Sigma_2)$ by using the transition subnet refinement operation. Then $N_T$ is abstracted as the transition set ${T_m}'$, and $\Sigma'$ is the shared transition set synthesis PRES+ net system of ${\Sigma_1}'$ and ${\Sigma_2}'$. In this situation, $\Sigma$ is live iff $\forall t'\in {T_m}'$, $t'$ is live.

Proof: Consider $N_T = \left\{N_{T1},N_{T2},\dots,N_{Tk}\right\}$ as the transition subnet set. Let ${\Sigma_1}' = ({Z_1}',{S_{10}}')$ and ${\Sigma_2}' = ({Z_2}',{S_{20}}')$ be obtained from $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$, respectively, by using the PRES+ transition subnet abstraction operation. Let the transition set ${T_m}' = \left\{\overline t_1,\overline t_2,\dots,\overline t_k\right\}$ be obtained from $N_T = \left\{N_{T1},N_{T2},\dots,N_{Tk}\right\}$ by using the PRES+ transition subnet abstraction operation. As $\forall p\in ^{\bullet} t_{j{\rm in}}$, $M'(p)\geq W'(p,t_{j{\rm in}})$ (where $t_{j{\rm in}}$ is the input transition of $N_{Tj}$, $j = 1,2,\dots,k$), then $\forall p\in^{\bullet}\overline t_j$, $M'(p)\geq W'(p,\overline t_j)$ $(j = 1,2,\dots.k)$. As $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ are two live and bounded PRES+ net systems, then by Lemma 4, ${\Sigma_1}' = ({Z_1}',{S_{10}}')$ and ${\Sigma_2}' = ({Z_2}',{S_{20}}')$ are live and bounded PRES+ net systems. In addition, the closed net systems $\overline {\Sigma}_{N_{T1}} = (\overline Z_{T1},\overline S_{T10})$, $\overline{\Sigma}_{N_{T2}} = (\overline Z_{T2},\overline S_{T20}) ,\dots$, $\overline{\Sigma}_{N_{Tk}} = (\overline Z_{Tk},\overline S_{Tk0})$ are live and bounded. As $\Sigma'$ is the shared transition set synthesis PRES+ net system of ${\Sigma_1}'$ and ${\Sigma_2}'$, according to Theorem 3, $\Sigma'$ is live if $\forall t'\in {T_m}'$, $t'$ is live. Here, $\Sigma$ is obtained from $\Sigma'$ by using the transition refinement operation, i.e., ${T_m}' = \left\{\overline t_1,\overline t_2,\dots,\overline t_k\right\}$ is replaced by $N_T = \left\{N_{T1},N_{T2},\dots,N_{Tk}\right\}$. Since $\overline{ \Sigma}_{N_{T1}} = (\overline Z_{T1},\overline S_{T10})$, $\overline{ \Sigma}_{N_{T2}} = (\overline Z_{T2},\overline S_{T20}) \,,\dots$, $\overline{ \Sigma}_{N_{Tk}} = (\overline Z_{Tk},\overline S_{Tk0})$ are live and bounded. By Lemma 3 and Theorem 3, $\Sigma$ is live if $\forall t'\in {T_m}'$, $t'$ is live.■

Note that the same procedure can be easily adapted by using Lemmas 3 and 4 and Theorem 4 to obtain the following results.

Theorem 6: Suppose $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ are two live and bounded PRES+ net systems, $\Sigma = (Z,S_0)$ is the synthesis net system of $\Sigma_1 = (Z_1,S_{10})$ and $\Sigma_2 = (Z_2,S_{20})$ with shared transition subnet set $N_T = \left\{N_{T1},N_{T2},\dots,N_{Tk}\right\}$, and $\forall p\in ^{\bullet} t_{j{\rm in}}$, $M'(p)\geq W'(p,t_{j{\rm in}})$ (where $t_{j{\rm in}}$ is the input transition of $N_{Tj}$, $j = 1,2,\dots,k$). Here, ${\Sigma_1}'({\Sigma_2}')$ is obtained from $\Sigma_1(\Sigma_2)$ by using the transition subnet refinement operation. Then, $N_T$ is abstracted as the transition set ${T_m}'$. ${\Sigma_1}'$ and ${\Sigma_2}'$ have the same fireable transition ordered pair set on ${T_m}'$. If $\exists S'\in R_N(S'_0)$, $\exists t'\in {T_m}'$ such that $S'\xrightarrow{t}$, then $\Sigma$ is live.

VII. APPLICATION

To demonstrate the effectiveness of our synthesis methods for PRES+, we will use these two methods to model and analyze an embedded subsystem based on PRES+.

Xia [7] constructed a model of the temperature measure and control system of a fire protection system (FPS) in an intelligent building by using the transition refinement operation for PRES+.

In this section, we construct a model of two control embedded systems that share the temperature measure and control subsystems in the FPS. This subsystem can measure or display temperature, and deliver signals to other subsystems.

A model of two control systems sharing two transitions and a transition subnet in the embedded system design is built, then the property preservations of these synthesis methods are verified.

A Building PRES+ Model for an Embedded Control System

In this section, the PRES+ model for an embedded control system is constructed. The PRES+ models of two embedded control systems are first presented. The synthesized PRES+ model is then provided by using the synthesis shared transition set method and the synthesis shared transition subnet set method. The abstraction-synthesis-refinement operation representation method is used to carry out the synthesis approach.

In this paper, we will adopt the synthesis operation to model and analyze this system. The PRES+ models of the two control subsystems are illustrated in Figs. 4 and 5 (adapted from [7]).

Figure  4.  Subsystem $N_1$

DownLoad: Full-Size Img PowerPoint

Figure  5.  Subsystem $N_2$

DownLoad: Full-Size Img PowerPoint

In Fig. 4 (Fig. 5), $t_1(t_3)$ sends the demand signal; the transition subnet $N_{T1}(N_{T2})$ (as shown by the dotted box) sets up, measures and displays temperature; in addition, $t_2(t_4)$ is the system process.

In the transition subnet $N_{T1}(N_{T2})$, the transitions have the following meanings: $t_{11}(t_{21})$: subsystem initial transition; $t_{12}(t_{22})$: setup the upper limit temperature value; $t_{13}(t_{23})$: setup the lower limit temperature value; $t_{14}(t_{24})$: modify the upper limit temperature value; $t_{15}(t_{25})$: modify the lower limit temperature value; $t_{16}(t_{26})$: A/D transformation; $t_{17}(t_{27})$: exchange the upper limit temperature value for the lower limit temperature value; and $t_{18}(t_{28})$: A/D transformation; $t_{19}(t_{29})$: D/A transformation.

The PRES+ models $N_1$ and $N_2$ are two embedded control subsystems. These two subsystems have three of the same operating steps ($t_1 \leftrightarrow t_3$, $N_{T1} \leftrightarrow N_{T2}$, $t_2 \leftrightarrow t_4$). The synthesized net $N$ (Fig. 6) is obtained by the PRES+ synthesis shared transition set operation and the synthesis shared transition subnet set operation, i.e., $t_1$, $N_{T1}$ and $t_2$ of $N_1$ and $t_3$, $N_{T2}$ and $t_4$ of $N_2$ are merged as $t_{m13}$, $N_{Tm}$ and $t_{m24}$ of $N$, respectively.

Figure  6.  Synthesis control system N

DownLoad: Full-Size Img PowerPoint

B Property Preservation Analysis of the PRES+ Model

In this section, the reachability, functionality, timing, and liveness preservations of the synthesis PRES+ model are analyzed.

1) Reachability, Functionality, and Timing Preservation: Let ${N_1}' = ({P_1}', {T_1}',{I_1}',{O_1}',{M_{10}}')$ be obtained from $N_1 = (P_1,T_1,$ $I_1,O_1,M_{10})$ (Fig. 4) by using the transition subnet abstraction operation.

Here, N_T1 = (P_T1, T_T1, I_T1, O_T1, M_T10) , where P_T1 = {p₁₁, p₁₂, p₁₃, p₁₄, p₁₅, p₁₆}; T_T1 = {t₁₁, t₁₂, t₁₃, t₁₄, t₁₅, t₁₆, t₁₇, t₁₈, t₁₉}; I_T1 = {(p₁₁, t₁₂), (p₁₁, t₁₃), (p₁₂, t₁₄), (p₁₃, t₁₅), (p₁₄, t₁₆), (p₁₄, t₁₇), (p₁₅, t₁₈), (p₁₆, t₁₉)}; O_T1 = {(t₁₁, p₁₁), (t₁₁, p₁₄), (t₁₂, p₁₂), (t₁₃, p₁₃), (t₁₄, p₁₁), (t₁₄, p₁₄), (t₁₅, p₁₄), (t₁₅, p₁₁), (t₁₆, p₁₆), (t₁₇, p₁₅), (t₁₈, p₁₆)}; M_T10 = $\phi$.

Then, $N_{T1} = (P_{T1},T_{T1},I_{T1},O_{T1},M_{T10})$ is abstracted as ${\overline t_{T1}}$. Next, ${N_1}' = ({P_1}',{T_1}',{I_1}',{O_1}',{M_{10}}')$, where

${P_1}' = \{p_1,p_2,p_3,p_4,p_5\}$,

${T_1}' = \{t_1,{\overline t_{T1}},t_2\}$,

${I_1}' = \{(p_1,{\overline t_{T1}}),(p_2,{\overline t_{T1}}),(p_3,t_2),(p_4,t_2),(p_5,t_1)\}$,

${O_1}' = \{(t_1,p_1),(t_1,p_2),(t_1,p_4),({\overline t_{T1}},p_3),(t_2, p_5)\}$,

$M_{10}(p_5) \neq \phi$.

$f_{\overline t_{T1}} = f_{t_{19}} \circ f_{s1} \circ f_{t_{11}}$,

${d_{{\overline t_{T1}}}}^{-} = {d_{t_{11}}}^{-} + {d_{s1}}^{-} + {d_{t_{19}}}^{-}$,

${d_{{\overline t_{T1}}}}^{+} = {d_{t_{11}}}^{+} + {d_{s1}}^{+} + {d_{t_{19}}}^{+}$ (where $f_{s1}$ is the transition set function for the transition set $T_{T1} - \{t_{11},t_{19}\}$, and ${d_{s1}}^{-}$ and ${d_{s1}}^{+}$ are the minimum transition set delay and the maximum transition set delay for transition set $T_{T1} - \{t_{11},t_{19}\}$, respectively).

Let ${N_2}' = ({P_2}', {T_2}', {I_2}', {O_2}', {M_{20}}')$ be obtained from N₂ = (P₂, T₂, I₂, O₂, M₂₀) (Fig. 5) by using transition subnet abstraction operation. Thus, N_T2 = (P_T2, T_T2, I_T2, O_T2, M_T20), where P_T2 = {p₂₁, p₂₂, p₂₃, p₂₄, p₂₅, p₂₆}, T_T2 = {t₂₁, t₂₂, t₂₃, t₂₄, t₂₅, t₂₆, t₂₇, t₂₈, t₂₉}, I_T2 = {(p₂₁, t₂₂), (p₂₁, t₂₃), (p₂₂, t₂₄), (p₂₃, t₂₅), (p₂₄, t₂₆), (p₂₄, t₂₇), (p₂₅, t₂₈), (p₂₆, t₂₉)}, O_T2 = {(t₂₁, p₂₁), (t₂₁, p₂₄), (t₂₂, p₂₂), (t₂₃, p₂₃), (t₂₄, p₂₁), (t₂₄, p₂₄), (t₂₅, p₂₄), (t₂₅, p₂₁), (t₂₆, p₂₆), (t₂₇, p₂₅), (t₂₈, p₂₆)}, M_T20 = $\phi$.

Next, $N_{T2} = (P_{T2},T_{T2},I_{T2},O_{T2},M_{T20})$ is abstracted as ${\overline t_{T2}}$. As such, ${N_2}' = ({P_2}',{T_2}',{I_2}',{O_2}',{M_{20}}')$, where

${P_2}' = \{p_6,p_7,p_8,p_9,p_{10}\}$,

${T_2}' = \{t_3,{\overline t_{T2}},t_4\}$,

${I_2}' = \{(p_6,t_3),(p_7,{\overline t_{T2}}),(p_8,t_4),(p_9,t_4),(p_{10},t_3)\}$,

${O_2}' = \{(t_3,p_7),(t_3,p_9),({\overline t_{T2}},p_6),({\overline t_{T2}},p_8),(t_4, p_{10})\}$,

$M_{20}(p_6) \neq \phi$, $M_{20}(p_{10}) \neq \phi$.

$f_{\overline t_{T2}} = f_{t_{29}} \circ f_{s2} \circ f_{t_{21}}$,

${d_{{\overline t_{T2}}}}^{-} = {d_{t_{21}}}^{-} + {d_{s2}}^{-} + {d_{t_{29}}}^{-}$,

${d_{{\overline t_{T2}}}}^{+} = {d_{t_{21}}}^{+} + {d_{s2}}^{+} + {d_{t_{29}}}^{+}$ (where $f_{s2}$ is the transition set function for transition set $T_{T2} - \{t_{21},t_{29}\}$, and ${d_{s2}}^{-}$ and ${d_{s2}}^{+}$ are the minimum transition set delay and the maximum transition set delay for transition set $T_{T2} - \{t_{21},t_{29}\}$, respectively).

In accordance with Lemma 1, the reachability, functionality and timing of ${N_1}'$ are the same as those of $N_1$. The reachability, functionality and timing of ${N_2}'$ are the same as those of $N_2$.

Here, in the shared transition set synthesis process, $t_1$ of ${N_1}'$ and $t_3$ of ${N_2}'$ are merged as $t_{m13}$ of $N'$. Thus, ${N_{11}}' = ({P_{11}}',{T_{11}}',{I_{11}}',{O_{11}}',{M_{110}}')$ is a transition subnet of ${N_1}' = ({P_1}',{T_1}',{I_1}',{O_1}',{M_{10}}')$, where ${P_{11}}' = \{p_1,p_2, p_4, p_5\}$, ${T_{11}}' = \{t_1\}$, ${I_{11}}' = \{(p_5,t_1)\}$, ${O_{11}}' = \{(t_1,p_1),(t_1,p_2),(t_1,p_4)\}$, ${M_{110}}'(p_5) \neq \phi$. Then, ${N_{21}}' =$ $({P_{21}}',{T_{21}}',{I_{21}}',{O_{21}}',{M_{210}}')$ is a transition subnet of ${N_2}' = ({P_2}',{T_2}',{I_2}',{O_2}',{M_{20}}')$, where ${P_{21}}' = \{p_6,p_7,p_9,p_{10}\}$, ${T_{21}}' = \{t_3\}$, ${I_{21}}' = \{(p_6,t_3),(p_{10},t_3)\}$, ${O_{21}}' = \{(t_3,p_7),$ $(t_3,p_9)\}$, ${M_{210}}'(p_6) \neq \phi$, and ${M_{210}}'(p_{10}) \neq \phi$.

As such ${N_{m1}}' = ({P_{m1}}',{T_{m1}}',{I_{m1}}',{O_{m1}}',{M_{m10}}')$ of $N' = (P', T', I',O',{M_0}')$ is the shared transition set synthesis net of ${N_{11}}'$ and ${N_{21}}'$, where ${P_{m1}}' = \{p_1,p_2,p_4,p_5,p_6,p_7,p_9,$ $p_{10}\}$,

${T_{m1}}' = \{t_{m13}\}$,

${I_{m1}}' = \{(p_5,t_{m13}),(p_6,t_{m13}),(p_{10},t_{m13})\}$,

${O_{m1}}' = \{(t_{m13},p_1),(t_{m13},p_2),(t_{m13},p_4),(t_{m13},p_7),(t_{m13}, p_9)\} .$ ${M_{m10}}' (p_5) = {M_{110}}'(p_5)$, and ${M_{m10}}'(p_6) = {M_{210}}'(p_6)$, ${M_{m10}}' {(p_{10}) =M_{210}}'(p_{10})$.

As the transition function $f_{t_{m13}} = f_{t_1} = f_{t_3}$, and transition delay $[{d_{t_{m13}}}^{-},{d_{t_{m13}}}^{+}] = [{d_{t_1}}^{-},{d_{t_1}}^{+}] = [{d_{t_3}}^{-},{d_{t_3}}^{+}] = [1,2]$, according to Theorem 1, the reachability, functionality, and timing of ${N_{m1}}'$ are those of ${N_{11}}'$ and ${N_{21}}'$.

The same method can be used to discuss the reachability, functionality, and timing preservation of $\overline t_{T1}$ and $t_2$ of ${N_1}'$ and $\overline t_{T2}$ and $t_4$ of ${N_2}'$, which are merged as $\overline t_{Tm}$ and $t_{m24}$ of $N'$, respectively.

By Theorem 1, the reachability, functionality, and timing of $N'$ are the same as those of ${N_1}'$ and ${N_2}'$.

Let $N = (P,T,I,O,M_0)$ be obtained from $N' = (P',$ $T',I',O',{M_0}')$ by using the transition refinement operation, i.e., $\overline t_{Tm}$ is replaced by the transition subnet N_Tm = (P_Tm, T_Tm, I_Tm, O_Tm, M_Tm0), where P_Tm = {p_m1, p_m2, p_m3, p_m4, p_m5, p_m6}, T_Tm = {t_m1, t_m2, t_m3, t_m4, t_m5, t_m6, t_m7, t_m8, t_m9}, I_Tm = {(p_m1, t_m2), (p_m1, t_m3), (p_m2, t_m4), (p_m3, t_m5), (p_m4, t_m6), (p_m4, t_m7), (p_m5, t_m8), (p_m6, t_m9)}, O_Tm = {(t_m1, p_m1), (t_m1, p_m4), (t_m2, p_m2), (t_m3, p_m3), (t_m4, p_m1), (t_m4, p_m4), (t_m5, p_m1), (t_m5, p_m4), (t_m6, p_m6), (t_m7, p_m5), (t_m8, p_m6)}, M_Tm0 = $\phi$. According to Lemma 2, the reachability, functionality, and timing of $N$ are the same as those of $N'$. As the reachability, functionality, and timing of $N'$ are the same as those of ${N_1'}$ and ${N_2'}$, the reachability, functionality, and timing of ${N_1'}$ are the same as those of $N_1$. Additionally, the reachability, functionality, and timing of ${N_2'}$ are the same as those of $N_2$. By Theorem 2, the reachability, functionality, and timing of $N$ are the same as those of $N_1$ and $N_2$.

2) Liveness Preservation: Suppose that $\Sigma_1 = (Z_1,S_{10})$, $\Sigma_2 = (Z_2,S_{20})$, and $\Sigma = (Z,S_0)$ are the corresponding PRES+ net systems of $N_1$, $N_2$, and $N$. It is easy to see that $\Sigma_1$ and $\Sigma_2$ are live and bounded. ${\Sigma_1}' = ({Z_1}',{S_{10}}')$ is obtained from $\Sigma_1 = (Z_1,S_{10})$ by using the transition abstraction operation. Similarly, ${\Sigma_2}' = ({Z_2}',{S_{20}}')$ is obtained from $\Sigma_2 = (Z_2,S_{20})$ by using the transition abstraction operation. Next, $N_{Tm} = (P_{Tm},T_{Tm},I_{Tm},O_{Tm},M_{Tm0})$ is abstracted as $\overline t_{Tm}$. As ${\Sigma_1}'$ and ${\Sigma_2}'$ have the same fireable transition ordered pair set $\{(t_{m13},\overline t_{Tm}),(\overline t_{Tm},t_{m24}),(t_{m24},t_{m13})\}$ on $\{t_{m13},\overline t_{Tm},t_{m24}\}$, and $\exists S'\in R_N(S_0)$, where $S' = ({M_0}',J')$, ${M_0}' = (1,0,0,0,0,1,0,$ 1,0,0) such that $S'\xrightarrow{t_{m13}}$, by Theorem 5, $\Sigma$ is live.

VIII. Conclusions

Embedded systems have many applications in everyday life. Petri-net-based representation for embedded systems (PRES+) is an excellent tool to model and verify embedded systems. However, the state space explosion is a serious problem for using PRES+ to model and analyze large complex embedded systems. The Petri net synthesis method can avoid the state space explosion problem, and in this paper, the preservation of properties of the synthesized PRES+ model was investigated to help solve this problem. The synthesis shared transition set approach and the synthesis shared transition subnet set approach of the PRES+ method were proposed. Under several additional conditions, reachability, functionality, timing, and liveness were preserved after merging some transitions or transition subnets of PRES+ models. The results of this paper can be successfully applied to solve design problems in embedded control systems of intelligent buildings and manufacturing engineering.

Further research is required to investigate other more general synthesis operations for PRES+ and their applications.