Loading [MathJax]/jax/element/mml/optable/BasicLatin.js
A journal of IEEE and CAA , publishes high-quality papers in English on original theoretical/experimental research and development in all areas of automation
Chuanliang Xia, Chengdong Li, "Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems," IEEE/CAA J. Autom. Sinica, vol. 8, no. 4, pp. 905-915, Apr. 2021. doi: 10.1109/JAS.2020.1003003
Citation: Chuanliang Xia, Chengdong Li, "Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems," IEEE/CAA J. Autom. Sinica, vol. 8, no. 4, pp. 905-915, Apr. 2021. doi: 10.1109/JAS.2020.1003003

Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems

doi: 10.1109/JAS.2020.1003003
Funds:  This work was financially supported by the National Natural Science Foundation of China (61503220), the Natural Science Foundation of Shandong Province (ZR2016FM19), the Taishan Scholar Project of Shandong Province (TSQN201812092), the Key Research and Development Program of Shandong Province (2019GGX101072, 2019JZZY010115, 2018GGX106006), and the Youth Innovation Technology Project of Higher School in Shandong Province (2019KJN005)
More Information
  • Embedded systems have numerous applications in everyday life. Petri-net-based representation for embedded systems (PRES+) is an important methodology for the modeling and analysis of these embedded systems. For a large complex embedded system, the state space explosion is a difficult problem for PRES+ to model and analyze. The Petri net synthesis method allows one to bypass the state space explosion issue. To solve this problem, as well as model and analyze large complex systems, two synthesis methods for PRES+ are presented in this paper. First, the property preservation of the synthesis shared transition set method is investigated. The property preservation of the synthesis shared transition subnet set method is then studied. An abstraction-synthesis-refinement representation method is proposed. Through this representation method, the synthesis shared transition set approach is used to investigate the property preservation of the synthesis shared transition subnet set operation. Under certain conditions, several important properties of these synthetic nets are preserved, namely reachability, timing, functionality, and liveness. An embedded control system model is used as an example to illustrate the effectiveness of these synthesis methods for PRES+.

     

  • 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 (S3PR), 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.

    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,M0), where P={p1,p2,,pm} is a set of places, T={t1,t2,,tn} is a set of transitions, IP×T is a set of input arcs, OT×P is a set of output arcs, and M0 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={p1,p2,p3,p4,p5}, T={t1,t2,t3,t4}, I={(p1,t1),(p2,t2), (p3,t3),(p4,t3),(p5,t4)}, and O={(t1,p2),(t1,p3),(t2,p4),(t3, p5),(t4,p1)}.

    Figure  1.  A simple PRES+ model

    Definition 2: A marking is an assignment of tokens to places. The marking M(p) of a place pP can be represented as a set over Ep{<v,r>|vτ(p)rR0+}, where τ(p) denotes the set of possible tokens that may be in p, and R0+ is the set of non-negative real numbers.

    For example, the initial marking M0 in Fig. 1 shows p1 as the only place initially marked: M0(p1)={<3,0>}, whereas M0(p2)=M0(p3)=M0(p4)=M0(p5)=ϕ.

    Definition 3: The pre-set t={pP|(p,t)I} is the set of input places of t. The post-set t={pP|(t,p)O} is the set of output places of t. The pre-set and post-set of pP are represented by p={tT|(t,p)O} and p={tT|(p,t)I}, respectively.

    Definition 4: For every transition tT, a transition function f exists that is associated with t, i.e., f:τ(p1)×τ(p2)××τ(pa)τ(q), where τ is a type function that associates with every place, t={p1,p2,,pa}, qt.

    In Fig. 1, for example, there exists a transition function f1 associated with t1.

    Definition 5: For every transition tT, 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 t1 is d1=2, and the maximum transition delay of t1 is d+=5.

    Definition 6: A transition tT 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 t. In Fig. 1, the transition t3 has a guard Gt3 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 <PM,valM>, where PM is a subnet of places and valM is a mapping from places to token values. TM is the set of enabled transitions for a marking M. ft is a function associated with transition t.

    Definition 8 [36]: A marking M+=<PM+,valM+> is said to be a successor of the marking M=<PM,valM>, if i) the first component PM+, referred to as the successor place marking of PM, contains all the post-places of the enabled transitions of PM and all the places of PM whose post-transitions are not enabled; symbolically, PM+={p|ptandtTM}{p|pPMandpTM}, and ii) pPM+, if p=t for some tTM, then valM+(p)=ft(valM(t)) and if pTM, then valM+(p)=valM(p).

    Note that, for verification purposes, the PRES+ nets can be restricted to safe PRES+ nets [2], that is, every place pP holds at most one token for every marking M reachable from M0.

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

    Definition 9: A PRES+ model N=(P,T,I,O,M0) is called a shared transition set synthesis PRES+ model of N1=(P1,T1,I1,O1,M10) and N2=(P2,T2,I2,O2,M20), if P1P2=ϕ, T1T2=Tmϕ (where Tm is the shared transition set); P=P1P2, T=T1T2; I=I1I2; O=O1O2;

    M0(P)={M10(p)pP1M20(p)pP2.

    Definition 10: SupposeN1 has a transition set {t11,t12,,t1k} (where t1it1j=ϕ, t1it1j=ϕ, ij (1i,jk)). N2 has the same type of transition set {t21,t22,,t2k} (where t2it2j=ϕ, t2it2j=ϕ, ij (1i,jk). In the synthesis procedure, the same type transition t1iT1 of N1 and t2iT2 of N2 are merged into transition tmiTm of N, where 1ik.

    Definition 11: Let f1i be the transition function of t1iT1 (1ik), f2i be the transition function of t2iT2 (1ik), and f1i=f2i. We define fmi=f1i (1ik).

    Definition 12: Let [d1i,d1i+] and [d2i,d2i+] be the transition delays of t1iT1 and t2iT2 (1ik), respectively, and [d1i,d1i+] = [d2i,d2i+]. We define [dmi,dmi+]=[d1i,d1i+] (1ik).

    Definition 13: Let et1i and et2i be the enable times of enabled transitions t1iT1 and t2iT2 (1ik), respectively. Suppose et1i=et2i (1ik). Let d1ie=et1i+ d1i and d1il=et1i+d1i+ be the earliest trigger time and the latest trigger time of t1i (1ik), respectively. Let d2ie=et2i+d2i and d2il=et2i+d2i+ be the earliest trigger time and the latest trigger time of t2i (1ik), respectively. For tmi (1ik), dmie is the earliest trigger time and dmil is the latest trigger time. We define dmie=d1ie and dmil=d1il (1ik).

    From the above, it is clear that d1ie=d2ie and d1il=d2il (1ik).

    Definition 14: A PRES+ model NT=(PT,TT,IT,OT, MT,0) is called a transition subnet of N=(P,T,I,O,M0) if PTP, TTT and PTϕ, TTϕ, PTPTTT, IT=I(PT×TT), OT=O(TT×PT); NT is connected, {tin,tout}TT (where tin is the input transition of NT, and tout is the output transition of NT); tTT, and there exists a transition function f and a transition delay [d,d+] (where dd+).

    Definition 15: For the transition set TT{tin,tout} of NT, a transition set delay [ds,ds+], and a transition set function fs are presented.

    Supposition 1: Suppose NT satisfies:

    1) In a procedure (tokens from outside flow into tin, across NT, then flow out from tout), tout is fired if and only if tin is fired.

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

    3) Before tin is fired and after tout is fired, tTT{tin,tout}, t can not be enabled.

    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

    Definition 16: Let N1=(P1,T1,I1,O1,M10) and N2=(P2,T2,I2,O2,M20) be two PRES+ models. Then N=(P,T,I,O,M0) is called a synthesis net of the shared transition subnet set if the following conditions are satisfied: P=P1P2; T=T1T2; I=I1I2; O=O1O2; If pP1P2, then M10(p)=M20(p); M0(p)={M10(p)pP1M20(p)pP2.

    In Fig. 2, the PRES+ model N is the synthesis net of N1 and N2, where N1r=N1{NT11NT12} and N2r=N2{NT21NT22}.

    Supposition 2: Suppose N1 and N2 satisfy:

    1) N1 and N2 have the same type of transition subnet set NT1=(NT11,NT12,,NT1k) and NT2=(NT21, NT22,,NT2k), where NT1i and NT2i (i=1,2,,k) are transition subnets.

    2) Let tT1iin and tT1iout be the input transition and the output transition of NT1i (1ik), respectively. Suppose tT1iintT1jin=ϕ, and tT1iouttT1jout=ϕ, where ij (1i,jk).

    3) Let tT2iin and tT2iout be the input transition and the output transition of tT2i (1ik), respectively. Suppose tT2iintT2jin=ϕ, and tT2iouttT2jout=ϕ, where ij (1i,jk).

    For example, in Fig. 2, N1 and N2 have the same type of transition subnet set NT1=(NT11,NT12) and NT2=(NT21,NT22). Here, tT1iin and tT1iout are the input transition and the output transition of NT1i(i=1,2), with tT11intT12in=ϕ, and tT11outtT12out=ϕ. tT2iin and tT2iout are the input transition and the output transition of NT1i (i=1,2), with tT21intT22in=ϕ, and tT21outtT22out=ϕ.

    Definition 17 (Synthesis Operation): NT1=(NT11, NT12,,NT1k) and NT2=(NT21,NT22,,NT2k) are merged as transition subnets NTm=(NTm1,NTm2,,NTmk) in N. The arcs that link NTi (i=1,2,,k) in N1 and N2 are then linked to the synthesis subnets NTmi (i=1,2,,k). Weights on arcs are preserved.

    For instance, in Fig. 2, NT1=(NT11,NT12) and NT2= (NT21,NT22) are merged as transition subnets NTm=(NTm1,NTm2) in N.

    Supposition 3: It is assumed that fT1iin(fT1iout) is the transition function of input transition tT1iin (output transition tT1iout) of NT1i (1ik), and fT2iin(fT2iout) is the transition function of input transition tT2iin (output transition tT2iout of NT2i (1ik). Suppose fT1iin = fT2iin, fT1iout = fT2iout, and fTmiin = fT1iin, fTmiout = fTiout (1ik).

    Note that, in Fig. 2, for convenience, the transition function and transition delay were omitted. For example, in Fig. 2, let fT11in be the transition function of tT1iin, and fT11out be the transition function of tT1iout. Let fT21in be the transition function of tT21in, and fT21out be the transition function of tT21out. Let fTm1in be the transition function of tTm1in, and fTm1out be the transition function of tTm1out. Suppose fT11in=fT21in, fT11out=fT21out, and fTm1in=fT11in, fTm1out=fT11out.

    Supposition 4: Assume [dT1iin,dT1iin+] is the transition delay of input transition tT1iin and [dT1iout,dT1iout+] is the transition delay of output transition tT1iout of NT1i (1ik), [dT2iin,dT2iin+] is the transition delay of input transition tT2iin and [dT2iout,dT2iout+] is the transition delay of output transition tT2iout of NT2i (1ik). Suppose [dT1iin,dT1iin+]=[dT2iin,dT2iin+], [dT1iout,dT1iout+]=[dT2iout,dT2iout+], and [dTmiin,dTmiin+]=[dT1iin,dT1iin+],[dTmiout,dTmiout+]=[dT1iout, dT1iout+] (1ik).

    For example, in Fig. 2, let [dT11in,dT11in+] be the transition delay of tT11in, and [dT11out,dT11out+] be the transition delay of tT11out. Let [dT21in,dT21in+] be the transition delay of tT21in and [dT21out,dT21out+] be the transition delay of tT21out. Let [dTm1in,dTm1in+] be the transition delay of tTm1in, [dT21out,dT21out+] be the transition delay of tTm1out. Suppose [dT11in, dT1in+]=[dT21in,dT21in+]=[dTm1in,dTm1in+], and [dT11out,dT1out+]=[dT21out,dT21out+]=[dTm1out,dTm1out+].

    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

    In Fig. 3, N1 is obtained from N1 by the abstraction operation, i.e., transition subnets NT11,,NT1k of N1 are abstracted to tT11,,tT1k respectively. N2 is obtained from N2 by an abstraction operation. N is obtained from N1 and N2 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,M0) is assumed to be obtained from N=(P,T,I,O,M0) by using subnet NT=(PT,TT,IT,OT,MT,0) to replace ˉt (where ˉtT) of N, where

    i) P=PPT;

    ii) T=TTT{¯t};

    iii) (p,t)I, if (p,t)IIT; (t,p)O, if (t,p)OOT;

    iv) (p,tin)I, if (p,¯t)I; (tout,p)O, if (¯t,p)O;

    v) M0(p)={M0(p)pPMT,0(p)pPT;

    vi) foutfsfin=fˉt (where is the compounding operator);

    vii) din+ds+dout=dˉt; din++ds++dout+=dˉ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,M0) is assumed to be obtained from N=(P,T,I,O,M0) by using ˉt (where ˉtT, ˉtT) to replace NT=(PT,TT,IT,OT,MT,0), where

    i) P=PPT;

    ii) T=T{¯t}TT;

    iii) (p,¯t)I (where ptin) and (p,t)I, if (p,t)IIT; (ˉt,p)O (where ptout) and (t,p)O, if (t,p)OOT;

    iv) M0(p)=M0(p) where pPPT;

    v) fˉt=foutfsfin;

    vi) dˉt=din+ds+dout; dˉt+=din++ds++dout+.

    Note that fˉt is the transition function of ˉt. Then fin, fout, and fs are the transition functions of input transition tin of NT, output transition tout of NT, and TT{tin,tout}, respectively. [dˉt,dˉt+], [din,din+], [dout,dout+], and [ds,ds+], are the transition delays of ˉt, tin, tout, and TT{tin,tout}, respectively.

    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 Na and Nb 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 Na and Nb, and the number of tokens in the output places of Na is equal to that of Nb, then Na and Nb are labeled as having the same reachability.

    If Na and Nb have the same reachability, and if the tokens’ type of input places of Na is equal to that of Nb, and the tokens’ type of output places of Na is equal to that of Nb, then Na and Nb are considered to have the same functionality. If Na and Nb have the same reachability, the tokens’ time of input places of Na is equal to that of Nb, and the tokens’ time of output places of Na is equal to that of Nb, then Na and Nb 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 N1=(P1,T1,I1,O1,M10) and N2=(P2,T2,I2,O2,M20) are two PRES+ models that have the same type transition set. Let N=(P,T,I,O,M0) be the shared transition set synthesis PRES+ model of N1 and N2. Then the reachability, functionality, and timing of N are the same as those of N1 and N2.

    Proof: Assume that {t11,t12,,t1k} is the transition set of N1=(P1,T1,I1,O1,M10). According to transition t1iT1 (1ik), a place bordered subnet N1i=(P1i,T1i,I1i, O1i,M1i0) (1ik) of N1 exists, where P1i=P1iinP1iout, P1iin={p|pt1i}, P1iout={p|pt1i}; I1i={(p,t1i)|pP1iin}; O1i={(t1i,p)|pP1iout}; and M1i0 is the projection of M10 on P1i. It is assumed that {t21,t22,,t2k} is the transition set of N2=(P2,T2,I2,O2,M20). Corresponding to transition t2iT2 (1ik), a place bordered subnet N2i=(P2i,T2i,I2i, O2i,M2i0) (1ik) of N2 exists, where P2i=P2iinP2iout, P2iin={p|pt2i}, P2iout={p|pt2i}; I2i={(p,t2i)|pP2iin}; O2i={(t2i,p)|pP2iout}; and M2i0 is the projection of M20 on P2i. Suppose Nmi=(Pmi,Tmi,Imi,Omi,Mmi0) of N=(P,T,I, O,M0) is the synthesis subnet of N1i and N2i. Here, Pmi=P1iP2i; t1i and t2i are merged as tmi; Imi=I1iI2i; and Omi=O1iO2i, Mm0(p)={Mi10(p)pPi1Mi20(p)pPi2.

    The input places and output places of N1i and N2i are the same as those of Nmi. The tokens’ number of input places of N1i and N2i is the same as that of Nmi. Since Nmi is the synthesis model of N1i and N2i, by the concept of shared transition set synthesis, the tokens’ number of output places of N1i and N2i is the same as that of Nmi. Then the reachability of Nmi is the same as that of N1i and N2i.

    By the concept of shared transition set synthesis, the tokens’ type in the input places of N1i and N2i is the same as that of Nmi. The transition function of t1i is f1i, and the transition function of t2i is f2i. As f1i=f2i and fmi=f1i, then the tokens’ type in the output places of N1i and N2i is the same as that of Nmi. The functionality of Nmi is then the same as that of N1i and N2i.

    By the shared transition set synthesis operation, the tokens’ time in the input places of N1i and N2i is the same as that of Nmi. The transition delay of t1i is [d1i,d1i+], and the transition delay of t2i is [d2i,d2i+]. The earliest trigger time of t1i is d1ie=et1i+d1i, and the latest trigger time of t1i is d1il=et1i+d1i+ (1ik). The earliest trigger time of t2i is d2ie=et2i+d2i, and the latest trigger time of t2i is d2il=et2i+d2i+ (1ik). Because [dmi,dmi+]=[d1i,d1i+], [d1i,d1i+]=[d2i,d2i+], dmie=d1ie=d2ie, and dmil=d1il=d2il, by the shared transition set synthesis operation, the tokens’ time in the output places of N1i and N2i is the same as that of Nmi. The timing of Nmi is thus the same as that of N1i and N2i.

    Let ¯N1 be the remaining part of N1, i.e., ¯N1=N1{N11,N12,,N1k}, and ¯N2 the remaining part of N2, that is, ¯N2=N2{N21,N22,,N2k}. Let ¯N be the remaining part of N, i.e., ¯N=N{Nm1,Nm2,,Nmk}. As ¯N=¯N1¯N2, the reachability, functionality, and timing of N are the same as those of N1 and N2.

    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,M0) be obtained from N=(P,T,I,O,M0) 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¯T=(P¯T,T¯T,I¯T,O¯T,M¯T,0), where P¯T=PT{pP|ptintout}; T¯T=TT; I¯T=IT{(p,tin)) |ptin}; O¯T=OT{(tout,p)|ptout};

    M¯T,0={MT,0(p)pPTM0|(tintout)(p)ptintout.

    Let subnet N¯t=(P¯t,T¯t,I¯t,O¯t,M¯t,0), where

    P¯t={p|ptintout}; T¯t={¯t};

    I¯t={(p,¯t)|ptin};

    O¯t={(¯t,p)|ptout};

    M¯t,0=M0|{p|p(tintout)}.

    N¯T=(P¯T,T¯T,I¯T,O¯T,M¯T,0) and N¯t=(P¯t,T¯t,I¯t,O¯t,M¯t,0) from above have the same input places {p|ptin} and output places {p|ptout}. According to Definition 19, the number of tokens in the input places of N¯T is the same as that of N¯t. As N=(P,T,I,O,M0) is obtained from N=(P,T,I,O, M0) 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¯T is the same as that of N¯t. As such, the reachability of N¯T is the same as that of N¯t.

    By Definition 19, the type of tokens in the input place of N¯T is the same as that of N¯t. Since f¯t=foutfsfin, the type of tokens in the output places of N¯T is the same as that of N¯t. Thus, the functionality of N¯T is the same as that of N¯t.

    By Definition 19, the token time of tokens in the input place of N¯T is the same as that of N¯t. As d¯t=din+ ds+dout and d¯t+=din++ds++dout+, thus the token time of tokens in the output places of N¯T is the same as that of N¯t. The timing of N¯T is thus the same as that of N¯t.

    As NN¯t=NN¯T, the reachability, functionality, and timing of N are the same as those of N.

    Lemma 2 [7]: Let N=(P,T,I,O,M0) be obtained from N=(P,T,I,O,M0) 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 N1 and N2 are abstracted as N1 and N2, respectively. Then the synthesis net N of N1 and N2 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 N1=(P1,T1,I1,O1,M10) and N2=(P2,T2, I2,O2,M20) be two PRES+ models. N=(P,T,I,O,M0) is the synthesis net of the N1 and N2 shared transition subnet set. The reachability, functionality, and timing of N are subsequently those of N1 and N2.

    Proof: Let N1=(P1,T1,I1,O1,M10) be obtained from N1=(P1,T1,I1,O1,M10) by using the transition subnet abstraction operation (Definition 19), i.e., the transition subnet set NT1={NT11,NT12,,NT1k} of N1=(P1,T1,I1,O1, M10) is replaced by the transition set TT1={¯t11,¯t12,,¯t1k} of N1=(P1,T1,I1,O1,M10). According to Lemma 1, the reachability, functionality, and timing of N1 are the same as those of N1. Let N2=(P2,T2,I2,O2,M20) be obtained from N2=(P2,T2,I2,O2,M20) by using the transition subnet abstraction operation (Definition 19); that is, the transition subnet set NT2={NT21,NT22,,NT2k} of N2=(P2,T2,I2,O2, M20) is replaced by the transition set TT2={¯t21,¯t22,,¯t2k} of N2=(P2,T2,I2,O2,M20). By Lemma 1, the reachability, functionality, and timing of N2 are the same as those of N2.

    The shared transition set synthesis PRES+ model N=(P,T,I,O,M0) of N1=(P1,T1,I1,O1,M10) and N2=(P2,T2,I2,O2,M20) is obtained by using the shared transition set synthesis operation. The same-type transition sets TT1={¯t11,¯t12,,¯t1k} of N1 and TT2={¯t21,¯t22,,¯t2k} of N2 are merged as the transition set TTm={¯tm1,¯tm2,,¯tmk} of N. According to Theorem 1, the reachability, functionality, and timing of N are the same as those of N1 and N2.

    N=(P,T,I,O,M0) is obtained from N=(P,T,I,O,M0) by using the transition subnet refinement operation (Definition 18). In this operation, the transition set TTm={¯tm1,¯tm2,, ¯tmk} is replaced by the transition subnet set NTm= {NTm1,NTm2,,NTmk}. 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 N1 and N2.

    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:TR+{#} (where # is a symbol which describes unusable status) is the vector of all possible firing intervals representing the firing domain. Here, S0=(M0,J0) with

    J0(t)={0M0(p)W(p,t)pt#otherwise

    is the initial state of N. Then, Σ=(Z,S0) 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 StS. State S=(M,J) is obtained from S=(M,J) by the time elapsing τR+, denoted by SτS. A transition t is live at state S if S(SRN(S)S(SRN(S))St)). A PRES+ net system Σ=(Z,S0) is live if all transitions are live in S. Additionally, place pP is considered bounded iff a natural number K>0 exists with M(p)K for each SRN(S0). Similarly, Σ=(Z,S0) 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 ¯NT=(¯P,¯T,¯I,¯O,¯M0) is called a PRES+ closed net if a subnet (from tin, across NT, then to tout in the refined net N=(P,T,I,O,M0)) is acquired, and a transition tT is added (where dtT=max, {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.

    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.

    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
    Figure  5.  Subsystem N_2

    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

    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, NT1 = (PT1, TT1, IT1, OT1, MT10) , where PT1 = {p11, p12, p13, p14, p15, p16}; TT1 = {t11, t12, t13, t14, t15, t16, t17, t18, t19}; IT1 = {(p11, t12), (p11, t13), (p12, t14), (p13, t15), (p14, t16), (p14, t17), (p15, t18), (p16, t19)}; OT1 = {(t11, p11), (t11, p14), (t12, p12), (t13, p13), (t14, p11), (t14, p14), (t15, p14), (t15, p11), (t16, p16), (t17, p15), (t18, p16)}; MT10 = \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 N2 = (P2, T2, I2, O2, M20) (Fig. 5) by using transition subnet abstraction operation. Thus, NT2 = (PT2, TT2, IT2, OT2, MT20), where PT2 = {p21, p22, p23, p24, p25, p26}, TT2 = {t21, t22, t23, t24, t25, t26, t27, t28, t29}, IT2 = {(p21, t22), (p21, t23), (p22, t24), (p23, t25), (p24, t26), (p24, t27), (p25, t28), (p26, t29)}, OT2 = {(t21, p21), (t21, p24), (t22, p22), (t23, p23), (t24, p21), (t24, p24), (t25, p24), (t25, p21), (t26, p26), (t27, p25), (t28, p26)}, MT20 = \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 NTm = (PTm, TTm, ITm, OTm, MTm0), where PTm = {pm1, pm2, pm3, pm4, pm5, pm6}, TTm = {tm1, tm2, tm3, tm4, tm5, tm6, tm7, tm8, tm9}, ITm = {(pm1, tm2), (pm1, tm3), (pm2, tm4), (pm3, tm5), (pm4, tm6), (pm4, tm7), (pm5, tm8), (pm6, tm9)}, OTm = {(tm1, pm1), (tm1, pm4), (tm2, pm2), (tm3, pm3), (tm4, pm1), (tm4, pm4), (tm5, pm1), (tm5, pm4), (tm6, pm6), (tm7, pm5), (tm8, pm6)}, MTm0 = \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.

    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.

  • [1]
    M. Ashjaei, N. Khalilzad, and S. Mubeen, “Modeling, designing and analyzing resource reservations in distributed embedded systems,” RealTime Modelling and Processing for Communication Systems. Springer, 2018, pp. 203–256.
    [2]
    L. A. Cortés, P. Eles, and Z. Peng, “Modeling and formal verification of embedded systems based on a Petri net representation,” J. Systems Architecture, vol. 49, no. 12, pp. 571–598, 2003.
    [3]
    S. Bandyopadhyay, K. Banerjee, D. Sarkar, and C. R. Mandal, “Translation validation for PRES+ models of parallel behaviours via an FSMD equivalence checker,” Progress in VLSI Design and Test. Springer, 2012, pp. 69–78.
    [4]
    D. Karlsson, P. Eles, and Z. Peng, “Model validation for embedded systems using formal method-aided simulation,” IET Computers &Digital Techniques, vol. 2, no. 6, pp. 413–433, 2008.
    [5]
    D. Karlsson, P. Eles, and Z. Peng, “Formal verification of componentbased designs,” Design Automation for Embedded Systems, vol. 11, no. 1, pp. 49–90, 2007. doi: 10.1007/s10617-006-9723-3
    [6]
    C. Xia, “Reduction rules for Petri net based representation for embedded systems,” J. Front. Comput. Sci. Technol, vol. 2, no. 6, pp. 614–626, 2008.
    [7]
    C. Xia, “Property preservation of refinement for Petri net based representation for embedded systems,” Cluster Computing, vol. 19, no. 3, pp. 1373–1384, 2016. doi: 10.1007/s10586-016-0597-2
    [8]
    C. Xia, B. Shen, H. Zhang, and Y. Wang, “Liveness and boundedness preservations of sharing synthesis of Petri net based representation for embedded systems,” Computer Systems Science and Engineering, vol. 33, no. 5, pp. 345–350, 2018.
    [9]
    J. Wang, Y. Deng, and M. Zhou, “Compositional time Petri nets and reduction rules,” IEEE Trans. Systems,Man,and Cybernetics,Part B, vol. 30, no. 4, pp. 562–572, 2000. doi: 10.1109/3477.865173
    [10]
    S. A. Shah, E. L. Bohez, K. Shah, I. ul Haq, K. Azam, and S. Anwar, “Colored Petri net model for significant reduction of invariants in flexible manufacturing systems,” Int. J. Advanced Manufacturing Technology, vol. 88, no. 5–8, pp. 1775–1787, 2017. doi: 10.1007/s00170-016-8864-1
    [11]
    P.-A. Bourdil, B. Berthomieu, S. Dal Zilio, and F. Vernadat, “Symmetry reduction for time Petri net state classes,” Science of Computer Programming, vol. 132, pp. 209–225, 2016. doi: 10.1016/j.scico.2016.08.008
    [12]
    J. Esparza, P. Hoffmann, and R. Saha, “Polynomial analysis algorithms for free choice probabilistic workflow nets,” Performance Evaluation, vol. 117, pp. 104–129, 2017. doi: 10.1016/j.peva.2017.09.006
    [13]
    B. Berthomieu, D. L. Botlan, and S. D. Zilio, “Petri net reductions for counting markings,” in Int. Symp. Model Checking Software, 2018.
    [14]
    S. M. Shatz, S. Tu, T. Murata, and S. Duri, “An application of Petri net reduction for ADA tasking deadlock analysis,” IEEE Trans. Parallel and Distributed Systems, vol. 7, no. 12, pp. 1307–1322, 1996. doi: 10.1109/71.553301
    [15]
    Y. Chen, Z. Li, K. Barkaoui, and M. Uzam, “New Petri net structure and its application to optimal supervisory control: interval inhibitor arcs,” IEEE Trans. Systems,Man,and Cybernetics:Systems, vol. 44, no. 10, pp. 1384–1400, 2014. doi: 10.1109/TSMC.2014.2307284
    [16]
    L. Salum, “Avoiding state explosion in a class of Petri nets,” Expert Systems with Applications, vol. 42, no. 1, pp. 519–526, 2015. doi: 10.1016/j.eswa.2014.07.037
    [17]
    Z. Ding, C. Jiang, M. Zhou, and Y. Zhang, “Preserving languages and properties in stepwise refinement-based synthesis of Petri nets,” IEEE Trans. Systems,Man,and Cybernetics-Part A:Systems and Humans, vol. 38, no. 4, pp. 791–801, 2008. doi: 10.1109/TSMCA.2008.923064
    [18]
    L. Bernardinello, E. Mangioni, and L. Pomello, “Local state refinement and composition of elementary net systems: An approach based on morphisms,” Trans. Petri Nets and Other Models of Concurrency VIII. Springer, 2013, pp. 48–70.
    [19]
    M. Khalgui, O. Mosbahi, Z. Li, and H.-M. Hanisch, “Reconfigurable multiagent embedded control systems: from modeling to implementation,” IEEE Trans. Computers, vol. 60, no. 4, pp. 538–551, 2010.
    [20]
    D.-E. Gratie and C. Gratie, “Composition colored Petri nets for the refinement of reaction-based models,” Electronic Notes in Theoretical Computer Science, vol. 326, pp. 51–72, 2016. doi: 10.1016/j.entcs.2016.09.018
    [21]
    P. Baldan, F. Bonchi, F. Gadducci, and G. V. Monreale, “Modular encoding of synchronous and asynchronous interactions using open Petri nets,” Science of Computer Programming, vol. 109, pp. 96–124, 2015. doi: 10.1016/j.scico.2014.11.019
    [22]
    J. Li, M. Zhou, and X. Dai, “Reduction and refinement by algebraic operations for Petri net transformation,” IEEE Trans. Systems,Man,and Cybernetics-Part A:Systems and Humans, vol. 42, no. 5, pp. 1244–1255, 2012. doi: 10.1109/TSMCA.2012.2186440
    [23]
    K. S. Cheung, T. Cheung, and K. Chow, “A Petri-net-based synthesis methodology for use-case-driven system design,” J. Systems and Software, vol. 79, no. 6, pp. 772–790, 2006. doi: 10.1016/j.jss.2005.06.018
    [24]
    M. Zhou, F. DiCesare, and A. A. Desrochers, “A hybrid methodology for synthesis of Petri net models for manufacturing systems,” IEEE Trans. Robotics and Automation, vol. 8, no. 3, pp. 350–361, 1992. doi: 10.1109/70.143353
    [25]
    H. Hu, R. Su, M. Zhou, and Y. Liu, “Polynomially complex synthesis of distributed supervisors for large-scale amss using Petri nets,” IEEE Trans. Control Systems Technology, vol. 24, no. 5, pp. 1610–1622, 2015.
    [26]
    E. Best and R. Devillers, “Characterisation of the state spaces of marked graph Petri nets,” Information and Computation, vol. 253, pp. 399–410, 2017. doi: 10.1016/j.ic.2016.06.006
    [27]
    A. A. Pouyan, H. T. Shandiz, and S. Arastehfar, “Synthesis a Petri net based control model for a FMS cell,” Computers in Industry, vol. 62, no. 5, pp. 501–508, 2011. doi: 10.1016/j.compind.2011.01.001
    [28]
    G. Liu, Z. Li, K. Barkaoui, and A. M. Al-Ahmari, “Robustness of deadlock control for a class of Petri nets with unreliable resources,” Information Sciences, vol. 235, pp. 259–279, 2013. doi: 10.1016/j.ins.2013.01.003
    [29]
    C. Xia, “Analysis of properties of petri synthesis net,” in Proc. Int. Conf. Theory and Applications of Models of Computation. Springer, 2006, pp. 576–587.
    [30]
    C. Xia, “Liveness and boundedness analysis of Petri net synthesis,” Mathematical Structures in Computer Science, vol. 24, no. 5, Article No. 2014.
    [31]
    D. Liu, Z. Li, and M. Zhou, “A parameterized liveness and ratioenforcing supervisor for a class of generalized Petri nets,” Automatica, vol. 49, no. 11, pp. 3167–3179, 2013. doi: 10.1016/j.automatica.2013.07.023
    [32]
    L. Jiao, T.-Y. Cheung, and W. Lu, “On liveness and boundedness of asymmetric choice nets,” Theoretical Computer Science, vol. 311, no. 1–3, pp. 165–197, 2004. doi: 10.1016/S0304-3975(03)00359-1
    [33]
    F. Basile, F. Caccavale, P. Chiacchio, J. Coppola, A. Marino, and D. Gerbasio, “Automated synthesis of hybrid Petri net models for robotic cells in the aircraft industry,” Control Engineering Practice, vol. 31, pp. 35–49, 2014. doi: 10.1016/j.conengprac.2014.05.008
    [34]
    F. Basile, R. Cordone, and L. Piroddi, “A branch and bound approach for the design of decentralized supervisors in Petri net models,” Automatica, vol. 52, pp. 322–333, 2015. doi: 10.1016/j.automatica.2014.12.004
    [35]
    Q. Hu, Y. Du, and S. Yu, “Service net algebra based on logic Petri nets,” Information Sciences, vol. 268, pp. 271–289, 2014. doi: 10.1016/j.ins.2013.10.014
    [36]
    S. Bandyopadhyay, D. Sarkar, and C. Mandal, “Equivalence checking of Petri net models of programs using static and dynamic cut-points,” Acta Informatica, vol. 56, no. 4, pp. 321–383, 2019. doi: 10.1007/s00236-018-0320-2
  • Related Articles

    [1]Tao Qin, Li Yin, Gaiyun Liu, Naiqi Wu, Zhiwu Li. Strong Current-State Opacity Verification of Discrete-Event Systems Modeled With Time Labeled Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2025, 12(1): 54-68. doi: 10.1109/JAS.2024.124560
    [2]Xiaofeng Yuan, Weiwei Xu, Yalin Wang, Chunhua Yang, Weihua Gui. A Deep Residual PLS for Data-Driven Quality Prediction Modeling in Industrial Process[J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11(8): 1777-1785. doi: 10.1109/JAS.2024.124578
    [3]Wei Ren, Zhuo-Rui Pan, Weiguo Xia, Xi-Ming Sun. Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization[J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11(10): 2082-2098. doi: 10.1109/JAS.2024.124473
    [4]Yifan Dong, Naiqi Wu, Zhiwu Li. State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11(5): 1274-1291. doi: 10.1109/JAS.2023.124128
    [5]Wei He, Xinxing Mu, Liang Zhang, Yao Zou. Modeling and Trajectory Tracking Control for Flapping-Wing Micro Aerial Vehicles[J]. IEEE/CAA Journal of Automatica Sinica, 2021, 8(1): 148-156. doi: 10.1109/JAS.2020.1003417
    [6]Fajun Yang, Naiqi Wu, Yan Qiao, Rong Su. Polynomial Approach to Optimal One-wafer Cyclic Scheduling of Treelike Hybrid Multi-Cluster Tools via Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2018, 5(1): 270-280. doi: 10.1109/JAS.2017.7510772
    [7]Dongming Xiang, Guanjun Liu, Chungang Yan, Changjun Jiang. Detecting Data-flow Errors Based on Petri Nets With Data Operations[J]. IEEE/CAA Journal of Automatica Sinica, 2018, 5(1): 251-260. doi: 10.1109/JAS.2017.7510766
    [8]Ran Ning, Su Hongye, Wang Shouguang. An Improved Approach to Test Diagnosability of Bounded Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2017, 4(2): 297-303. doi: 10.1109/JAS.2017.7510406
    [9]Jiacai Huang, YangQuan Chen, Haibin Li, Xinxin Shi. Fractional Order Modeling of Human Operator Behavior with Second Order Controlled Plant and Experiment Research[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(3): 271-280.
    [10]Yan Ma, Xiuwen Zhou, Bingsi Li, Hong Chen. Fractional Modeling and SOC Estimation of Lithium-ion Battery[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(3): 281-287.
    [11]Bingsan Chen, Chunyu Li, Benjamin Wilson, Yijian Huang. Fractional Modeling and Analysis of Coupled MR Damping System[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(3): 288-294.
    [12]Xiaoyu Lu, Mengchu Zhou, Ahmed Chiheb Ammari, Jingchu Ji. Hybrid Petri Nets for Modeling and Analysis of Microgrid Systems[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(4): 349-356.
    [13]Xian Li, Zengfu Wang. A HMM-based Mandarin Chinese Singing Voice Synthesis System[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(2): 192-202.
    [14]Themistoklis Giitsidis, Georgios Ch. Sirakoulis. Modeling Passengers Boarding in Aircraft Using Cellular Automata[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(4): 365-384.
    [15]Kecai Cao, YangQuan Chen, Dan Stuart, Dong Yue. Cyber-physical Modeling and Control of Crowd of Pedestrians: A Review and New Framework[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(3): 334-344.
    [16]Hong Mo, Jie Wang, Xuan Li, Zhanlin Wu. Linguistic Dynamic Modeling and Analysis of Psychological Health State Using Interval Type-2 Fuzzy Sets[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(4): 366-373.
    [17]Naizhou Wang, Hailong Pei, Yong Tang. Anti-windup-based Dynamic Controller Synthesis for Lipschitz Systems under Actuator Saturation[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(4): 358-365.
    [18]Shouguang Wang, Mengdi Gan, Mengchu Zhou, Dan You. A Reduced Reachability Tree for a Class of Unbounded Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(4): 345-352.
    [19]Tianmu Ma, Xiaochuan Luo, Tianyou Chai. Modeling and Hybrid Optimization of Batching Planning System for Steelmaking-continuous Casting Process[J]. IEEE/CAA Journal of Automatica Sinica, 2014, 1(2): 113-126.
    [20]Manoj Kumar, Karthikeyan Rajagopal, Sivasubramanya Nadar Balakrishnan, Nhan T. Nguyen. Reinforcement Learning Based Controller Synthesis for Flexible Aircraft Wings[J]. IEEE/CAA Journal of Automatica Sinica, 2014, 1(4): 435-448.

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(6)

    Article Metrics

    Article views (1206) PDF downloads(89) Cited by()

    Highlights

    • The property preservation of Petri net synthesis is investigated.
    • The synthesis shared transition subnet set approach is presented.
    • The abstraction-synthesis-refinement representation method is proposed.
    • The synthesis method is applied to the embedded control system.
    • The proposed two synthesis methods for PRES+ can bypass the state space explosion issue.

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return