• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    Boundedness and liveness enforcement for labeled Petri nets using transition priority

    2024-01-17 03:06:24YeJiaLiuXunBoLi

    Ye-Jia Liu,Xun-Bo Li

    School of Mechanical and Electrical Engineering,University of Electronic Science and Technology of China,Chengdu,611731,China

    Keywords:Boundedness Control strategy Liveness Petri nets Priority Transition invariant

    ABSTRACT This paper deals with the supervisory control problem of discrete event systems modeled by labeled Petri nets.The system is originally unbounded.First,the solvability of the problem is confirmed.A necessary condition is given and proven for the existence of a feasible priority-based controller based on the notions of liveness and transition invariants.Next,a cyclic behavior graph is constructed,which shows the reachable markings that guarantee the maximum liveness of the system within a given bound vector.Finally,an on-line control strategy is proposed to enforce boundedness and liveness to the given system by appending priority relations to transitions.The dynamic priority relation changes flexibly according to the current state of the system and enforces the system evolving in a bounded and live manner.In addition,numerical examples are studied to verify the validity of the proposed approach that remains the structure of the plant net and is efficient for on-line control.

    1 Introduction

    Discrete event systems (DESs) are a class of dynamic systems driven by events that interact according to certain operational rules,resulting in state evolutions [1].Many practical systems can be considered as DESs,such as mechanical manufacturing systems,power systems,communication network systems,and biological systems.Analyzing DES is to study the process of state evolution caused by the interaction of discrete events.The purpose of controlling DES is to prevent unexpected events from occurring or to make events only occur within a desired range.Both automata and Petri nets are the main modeling tools for DESs [2].Petri nets can clearly express the dynamic process of resource flow in a system using a concise graphical representation and it can uniformly describe concurrency,synchronization,mutual exclusion,and other behaviors.More importantly,Petri nets have strict mathematical formulas based on a large number of theoretical research.Common properties in DESs,including process repetition,state recovery,and capacity for resources,can be mapped in Petri net models and defined as liveness,reversibility,and boundedness.

    The supervisory control theory of DESs stems from the exploratory works of Ramadge and Wonham [3–5].Supervisory controllers in Petri nets utilize external interferences to limit the behaviors of the system in desired manner and to enforce certain properties to the system.The situation that no events occur in DES is defined as a deadlock that is usually undesired.Deadlock avoidance and prevention policies are widely concerned.Feng et al.generalized the liveness condition of ordinary Petri nets to the systems of sequential systems with shared resources [6].Then,they continued to provide a feasible control place related to the control variables for each perfect resource transition-circuit,which causes deadlocks in such systems [7].

    Furthermore,the supervisor simplification problem was considered in the Petri net systems,and the transition cover was used to solve the problem [8].Chen et al.proposed a supervisor for Petri nets using only one control place with data inhibitor arcs,and it is proven to be optimal.The transition-based controller is another way of deadlock prevention [9].The work in Ref.[10] presented an iterative approach to design a set of recovery transitions in Petri nets for deadlock prevention.The transition-based controller proposed by Bashir et al.is to prevent deadlocks by controlling then-met uncontrolled transitions [11].To meet the maximally permissive behavior,Row and Pan proposed a control policy recovering all original deadlock markings [12].

    More strictly,liveness is preferred to appear in DES.A live system excludes deadlocks,and any event may happen after completing a certain sub-process at any reachable state of the system.Therefore,it is important to ensure the liveness of the system.

    To enforce liveness on Petri nets,Kaid et al.developed a two-step approach for supervisory control in colored Petri nets,and the constructed monitors have minimal structural complexity [13].For better supervisor performance,Cong et al.exploited an iterative method to design a maximally permissive pure Petri net for liveness-enforcing [14].The work in Ref.[15] also showed a novel method for constructing a maximally permissive supervisor to make the plant net live with respect to nonlinear constraints.Qin et al.presented an algorithm to append time intervals on controllable transitions for maximally permissive liveness-enforcing controllers [16].To reduce the computational overhead of designing a supervisor,Zhong et al.proposed a decomposition method for Petri nets and designed a controller for each subnet [17].The work in Ref.[18] addressed the forbidden state problem in DESs for supervisor synthesis using the notion of marking masks that can effectively filtrate the forbidden and admissible markings.Considering the presence of unobservable transitions in the forbidden state problem,You et al.computed the optimal policies with respect to an admissible linear constraint [19].

    Boundedness is also an important structural property for Petri nets,which is highly relevant to the capacity requirements of the simulated system for relevant resources.The infinite expansion of states may lead to an explosion in the state space of a system and may also make it difficult for the system to recover.Therefore,in many practical systems,infinite states are undesirable.Boundedness analysis has been done by many researchers.Ding et al.used ordinary differential equations to check boundedness [20].For conflict-free Petri nets,Alimonti et al.determined boundedness and liveness using linear time algorithms [21].The work in Ref.[22] examined the boundedness of a cyber-physical system described by a Petri net,and it is not necessary to compute all place invariants and all reachable states for high efficiency.As for workflow nets,boundedness should be guaranteed for verifying soundness [23].Bashkin and Lomazova studied the decidability ofk-soundness of workflow nets containing unbounded resources [24].

    Many practical systems are originally unbounded,and boundedness-enforcing methods for Petri nets with the help of external controllers are derived as a consequence.The cyclic behavior of unbounded nets is studied in Ref.[25],and an approach based on extended coverability nets is proposed to transform unbounded Petri nets into bounded ones.As a logical control method,time constraints have been widely used for constraining behaviors in Petri nets by researchers.Vázquez and Silva analyzed time-dependent properties for continuous systems and enforced timed-liveness and boundedness through the timing [26].Moreover,time constraints were assigned to Petri nets in Ref.[27] repairing the boundedness of the system.Furthermore,both priority and time constraints are discussed in Ref.[28] to transform a live Petri net into a bounded and live one.In this paper,we try to enforce both liveness and boundedness to Petri nets.Considering that the priority is easy to implement in DESs through software and does not complicate the plant net structure,we assign reasonable priority to transitions for the purpose of boundedness and liveness enforcement.

    Priority in Petri nets was first proposed by Hack [29].Transition priority is to assign priority to controllable transitions and control the firings of transitions.Priority can be easily implemented in DESs using software.Transitions with higher priority enjoy preemptive firing and disabling the firings of low-priority transitions prevents the system from entering undesired reachable states,including deadlocks and overflows.The semantics of priority Petri nets (PPNs) is investigated by researchers.Best and Koutny provided a construction approach that transforms a bounded PPN into an ordinary one such that the modified ordinary Petri net can reserve as much of the semantics of concurrence as possible without transgressing the priority constraints [30].The work in Ref.[31] showed that dynamic priority for transitions is affected by the current markings of the given net.For priority conflict-free Petri nets,Yen studied the boundedness,reachability,and the existence of home states [32].Priority was appended to colored Petri nets for modeling the complex event processing in Ref.[33].Priority can be applied to places or tokens as well.Liu et al.considered that tokens in an extended logical Petri net have a priority function simulating the operation sequences in the business processes [34].The work in Ref.[35] chose to add priority rules on non-free choice places in Petri nets modeling an emergency call center.

    Given an unbounded Petri net,we need to determine whether the system has the possibility of controlling for liveness and boundedness enforcing.That is to say,as long as the system does not meet the proposed necessary condition,it is impossible to find a feasible priority-based controller that can recover the boundedness and liveness of the system.Then,we present a modified reachability graph (RG) that shows the cyclic behavior of the system with the help of transition-invariants (T-invariants).A priority-based control algorithm is developed to enforce boundedness and liveness to the system.The algorithm provides a feasible transition priority relation for the given unbounded Petri net and limits the system evolution in a live and bounded manner.The dynamic priority-based controller is the least restrictive,and it maintains the structure of the plant net.The main contributions of this paper are as follows:

    ? Not all unbounded Petri nets can recover boundedness and liveness using the priority-based method.Necessary conditions are proposed for the solvability of the problem.If there exists a transition priority relation that can ensure boundedness and liveness for the system,realizable cyclic sequences that contain all transitions must exist in the plant net.Note that it is not a sufficient condition.It is not guaranteed that there definitely exists feasible priority enforcing boundedness and liveness to the system even if the proposed necessary condition is met.

    ? Based on the unbounded Petri nets modeling DESs,we study the cyclic behavior of the system and construct modified RG using the notions of reachability sets and T-invariants.The proposed circuit-based graph describes the liveness of the system in a given bound vector.

    ? A control strategy is proposed based on dynamic transition priority.The algorithm calculates the current transition priority matrix according to a given observation,and it can control the behavior of the system.The proposed method preserves the plant net skeleton and is efficient for enforcing boundedness and liveness to the system.Besides,the calculated dynamic priority-based controller is the least restrictive.

    This paper is organized into seven sections.Section 2 recalls the basic preliminaries for Petri nets.A formal statement of the problem is provided in Section 3.In Section 4,we give the necessary conditions for the solvability of the problem,which is the prerequisite for the subsequent study.Section 5 presents the boundedness and liveness of enforcing the control algorithm based on priority in detail.In Section 6,the efficiency of our proposed control method is verified by experimental studies.Finally,we conclude the paper in Section 7.

    2 Preliminaries

    In this section,we review some basic notions and formalisms of Petri nets used in this paper.The readers can find more details of Petri nets in Ref.[2] and Ref.[36].

    2.1 Basics of Petri nets

    A Petri net is a four-tupleN=(P,T,Pre,Post),whereP={p1,p2,p3,…,pm} is a set ofmplaces,T={t1,t2,t3,···,tn} is the set ofntransitions,Pre:P×T→N andPost:P×T→N are the pre-and post-incidence functions that specify the arcs of the net,respectively.The places are represented by circles and the transitions are represented by bars graphically.The incidence matrix of a Petri net is denoted byC=Post-Pre.The set of non-negative integers is denoted by N.

    A Petri net without tokens that are represented by dots graphically is called an unmarked net.Otherwise,tokens exist in a Petri net and a net system (N,M0) is defined whereM0is the initial marking.A marking of a Petri net is a mappingM:P→N assigning a non-negative integer number of tokens to each place.M(p)indicates the number of tokens in a placepat the markingM.Another way to denote a marking isM=∑p∈PM(p)×p.Tokens flow in a Petri net system by firing transitions.A transitionti∈Tis enabled at a markingMif for all pre-places ofti,it holdsM(p)≥Pre(p,ti).An enabled transitiontiis fired atMand then a new markingM′ yields.The state equation isM′=M+Post(?,ti)-Pre(?,ti) and the process of firing is denoted byM[ti〉M′.Similarly,given a transition sequenceσ∈T*and a markingM,M[σ〉M′ denotes thatσis enabled at the markingMand a markingM′ is reachable fromMafter firingσ.

    A markingM′ is reachable atMafter firing a transition sequenceσ∈T*.All markings that are reachable from the initial markingM0comprise the reachability set of the Petri net,denoted byR(N,M0).A markingMcovers a markingM′ ifM(p)≥M′(p) holds for all places inP,denoted byM′≥M.A markingMstrictly covers a markingM′ ifM(p) >M′(p) holds for all places inP,denoted byM′ >M.RG is a deterministic graph that has as many nodes as the number of possible reachable markings when the given Petri net system is bounded.Each node in RG is associated with a reachable markingM∈R(N,M0).Each arc related to a transitiontfromMtoM′ implies thatM[t〉M′.The coverability graph caters to unbounded Petri nets and it displays infinite states of a net system by limited nodes.

    Given a net system (N,M0) and a markingM∈R(N,M0),a marking-transition sequences(M)=Mti,1M1ti,2M2…ti,LMLis defined as an evolution fromMsatisfyingM[ti,1〉M1[ti,2〉M2…[ti,L〉ML,whereiL∈N,ti,L∈T,andML∈R(N,M0).σ[s(M)]=ti,1ti,2…ti,Lis the corresponding transition sequence derived froms(M).An evolutions(M) is cyclic ifσ[s(M)] is enabled at the markingMand firingσ[s(M)] leads back toM.An initial evolutions(M0) starts from the initial markingM0.An evolution is maximal if it is either infinite or ending with a deadlock.A transitiont∈Tis live at the initial markingM0if

    ?M∈R(N,M0),?M′∈R(N,M):M′[t〉.

    In plain words,a transitiont∈Tis live if there exists a transition sequenceσ,and the transitiontis possible to enable at any markingM∈R(N,M0) after firingσ.A Petri net system (N,M0) is live if every transitiont∈Tis live.A deadlock is a markingM∈R(N,M0) that no transitiont∈Tfires atM.A Petri net system (N,M0) is bounded if there is a non-negative integerk∈N such that for any placep∈Pand any reachable markingM∈R(N,M0),it holdsM(p)≤k.A Petri net system is safe ifk=1.Due to different requirements,the bound for each place varies.kis a non-negative integer vector that indicates the bounds of Petri nets andk(p) denotes the bound of placep.

    Ann-dimensional vectory:T*→N is defined as a firing vector of a sequenceσfor a Petri net andy(t)=sdenotes that the transitiontfiresstimes inσ.Given a sequenceσatMsuch thatM[σ〉M′,the state equation is defined asM′=M+C×yσ,whereyσis the firing vector ofσ.Ifσis the transition sequence of a cyclic evolution,C×yσ=0 holds andyσis defined as a T-invariant of the net.Note that the existence of the firing vectoryis a necessary but not sufficient condition for a realizable transition sequence in a Petri net system.

    A labeled Petri net (LPN) is a four-tupleG=(N,M0,E,?) where (N,M0) is a Petri net system,Eis the set of labels,and?: T→E∪{ε} is the labeling function that assigns to each transitiont∈Teither a symbol fromEor the empty wordε.In this paper,we assume that the unobservable transitions do not exist.The observationw?=?(σ) is a sequence of labels that accords with the transition sequenceσ.

    2.2 PPNs

    A classical method for giving the notion of priority in Petri nets is to append them on a set of transitions.Priority belongs to the additional conditions that affect the evolving process of the system.We denote the priority level of a transitiont∈Tbyρ(t).We propose a generalized matrix of relation P=[ri,j]n×nto express the priority levels for transitions and name it as the transition priority matrix.Considering a Petri netNwith a priority relation,a component of the transition priority matrix P ofNis defined by (1):

    where the element 1 forri,jindicates that the transitiontiis in higher-level priority than the transitiontj.If the level of priority oftiis in inferiority compared withtj,ri,jequals–1.If the situation in two transitions shares the same priority appears,the elementri,jis denoted by 0.The elementri,jis symbolled asφif two transitions are without particular priority constraints.

    Some basic properties of priority are mentioned as follows.The relation of priority is transitive,i.e.,forri,j=1,rj,k=1,i,j,k∈{1,2,3,…,n},i≠j,j≠k,andi≠k,we conjecture thatri,k=1.This reasoning can be publicized to the circumstance whereri,j=–1,rj,k=–1,orri,j=0,rj,k=0.For the transitions in diverse priority levels,there existsri,j=–rj,i∈{–1,1},i,j∈{1,2,3,…,n},i≠j.The diagonal elements of P are equal to zero invariably,i.e.,ri,i=0,i∈{1,2,3,…,n}.

    The following firing rules are suitable for Petri nets with priority.High-priority transitions are enforced to fire before other enabled low-priority transitions.A transitionti∈Tis defined asρ-enabled atM,i.e.,M[ti〉ρ,iftiis enabled and it is in the highest level of priority among all enabled transitions atM,i.e.,M[ti〉: ?tj∈T,M[tj〉,rj,i≠1.

    When the situation comes to the same priority level or no constraints among transitions,the probabilityU(ti,M) of firingticonforms to the uniform distribution defined by (2a) and (2b):

    whereU(ti,M) is the possibility of firingtiatM,andTeis the set that comprises all enabled transitions atM.The cardinality ofTeis denoted by |Te|.The aboveρ-enabling rules are under the assumption that only one transition fires at a time.If enabled transitions are required to fire concurrently,we need to set a same priority level on these transitions.Considering that three enabled transitionst1,t2,andt3with no conflicts are demanded to fire in a Petri net,wheret1andt3need to be fired concurrently,the order of firing oft2is not restricted.Hence,r1,3=0,r1,2=φ,andr2,3=φare set in a pre-defined transition priority matrix.Although the firing orders oft2andt1t3affect the evolution,the final reachable markings are the same,i.e.,M1[t2〉M2[t1t3〉M′andM1[t1t3〉M3[t2〉M′.

    The firing sequences of transitions are influenced by priority.Note that priority is only bound to controllable transitions.In the case that the uncontrollable transition is enabled,it fires instantly with regardless control.A PPN is a three-tupleNP=(N,M0,P),where (N,M0) is a Petri net system,and P is the transition priority matrix.

    Example 1.Given a PPN in Fig.1,the initial marking isM0=[1,0,0,1,0]T.The transitiont2has the lowest priority.The same priority level is owned by transitionst1,t3,andt4,which is more prioritized thanρ(t2).Here we denote the transition with low priority by a blank bar and transitions in a high priority level by black bars.The priority matrix P is showed as below:

    Fig.1.PPN.

    RG of the Petri net in Fig.1 is displayed in Fig.2.The sequenceσ=t2t1t2t1t3t4t2t1t3t4is realizable at the initial markingM0and leads back to itself.Obviously,a realizable T-invariant of the system is [3,3,2,2]T.Sinceρ(t2) <ρ(t3),i.e.,r2,3=–1,the transitiont2cannot be fired at the markings [1,0,4,1,0]Tand [1,0,3,1,0]T.We label the disabled transitions with dotted arcs.Furthermore,the plant net of Fig.1 is unbounded since tokens in the placep3may grow arbitrarily without priority constraints.The given priority relation P enforces the system to be bounded.

    Fig.2.RG of PPN in Fig.1.

    Theρ-enabling rules give the constraints to the firing orders of PPN.Considering a situation that all transitions in a system are assigned with the same priority,i.e.,P=0,the maximally permissive behavior can be satisfied.If the priority of transitions varies,some states inR(N,M0) may be prohibited.Hence,the size of RG of Petri net with priority is lessened compared with that of the Petri net without priority.

    3 Problem statement

    Ensuring liveness and boundedness is quite important for DESs.Taking the Petri net based on discrete manufacturing system modeling as an example,places represent storage areas for workpieces,tools,pallets,and automated guided vehicles (AGVs) in a manufacturing system,and it is also used to represent the availability of resources.It is necessary to confirm whether these storage areas are overflowed,that is,to check the capacity of places.The boundedness of Petri nets is an effective criterion to test whether the system modeled by a Petri net has overflowed or not.However,some Petri nets are initially unbounded,so we need to use additional control methods to enforce them bounded.Deadlocks may cause severe damage to manufacturing systems and therefore need to be avoided.More strictly,the liveness of the system should be guaranteed.Transition priority is an effective logical controller that can be implemented through software without changing the plant net skeleton.We propose a dynamic priority-based controller to enforce liveness and boundedness to the unbounded plant net.

    Problem: Given an unbounded LPN systemG=(N,M0,E,?) and a bound vectork,the problem lies in verifying the necessary condition for the existence of a feasible priority matrix P and determining a dynamic priority-based controller that guarantees liveness and boundedness of the plant net.

    4 Solvability analysis

    In this section,we discuss the solvability of the proposed problem and provide a necessary condition for the existence of a live and bounded Petri net with priority after controlling.Not all Petri nets are likely to correspond to a Petri net with priority that the structure coincides with the plant net,and the priority relation is feasible for enforcing boundedness and liveness.For a bounded and live Petri net,the cyclic behavior in the system is noteworthy since it guarantees continuous evolutions of the system.Based on the notion of the cyclic behavior,we propose a necessary condition for the existence of the priority-based controller that enforces liveness and boundedness to the system.

    4.1 Cyclic behavior for unbounded Petri nets

    For unbounded Petri nets with infinite states,RGs make it difficult to describe the system behavior completely.The coverability graph is a representation of infinite system states using finite information.The core of the coverability graph construction lies in the use of the special symbol “w” to denote places where the tokens grow arbitrarily.In the construction process of a coverability graph,if a newly generated markingMstrictly covers any markingM′ which is on the path fromM0toM,i.e.,M≥M′,the places for whichM(p) >M′(p) is marked as “w” and the notation is kept in the subsequent computation.The number of tokens in these places may grow infinitely.The consequent problem is the lack of information such that we cannot directly find out the cyclic behavior in the system by the coverability graph.

    The recurrence of states represents that events in the system are driven repetitively.The cyclic behavior describes a situation in which events occur in succession,but only finite states are reached,and it is pretty important for ensuring system’s liveness.For unbounded Petri nets,infinitely many states exist,and it is difficult for us to find the cyclic behavior directly from the coverability graph.Since the information fromw-marked places is ignored,there is no one-to-one match between the cycle in the coverability graph for an unbounded Petri net and the realizable firing sequence in the system.

    Example 2.Given a Petri net system (N,M0) whereM0=[1,0,0,0,1,0]T,the Petri net shown in Fig.3 is unbounded since the tokens in the placesp3andp4grow infinitely.The coverability graph of the unbounded net is shown in Fig.4.Table 1 gives the details of the generalized markings in the coverability graph.According to the coverability graph,the sequencet4t3fromM7leads the marking back toM7.It is not a realizable cyclic behavior of the given net.After firingt1t3t2t1t2fromM0,we have the new marking[1,0,1,4,0,1]T,which shows the specific tokens ofM7.Firingt4t3yields another marking [1,0,0,3,0,1]T,which differs from [1,0,1,4,0,1]Tbut shares the same generalized marking [1,0,w,w,0,1]T.Therefore,cycles in the coverability graph do not necessarily reflect the realizable cyclic behavior of the system.

    Table 1 Generalized markings of the coverability graph in Fig.4.

    Fig.3.Unbounded Petri net.

    Fig.4.Coverability graph of the Petri net in Fig.3.

    In this paper,we trace the cyclic behavior of a system based on the notion of T-invariants.Since a T-invariant is determined by the system structure only,it is valid for unbounded Petri nets.From the aspect of matrix linear algebra,T-invariants provide a necessary condition for the cyclic behavior of Petri nets.That is to say,for the cyclic behavior of the system,there exist corresponding T-invariants,but the presence of T-invariants does not guarantee that there is a corresponding realizable cyclic transition sequence.

    A T-invariantyTdescribes the dynamic performance of the system.Suppose that the stateMof a Petri net can be recovered after firing a transition sequenceσwhose firing vector isyT.The state equation is denoted byM=M+C×yT.Obviously,it holdsC×yT=0.The solution is limited to non-negative integers,and each element inyTindicates the number of firings for transitions.If only a trivial solution is obtained,it means that no cyclic behavior exists in the Petri net.Moreover,the T-invariant is not unique in a system,and those that are not linear combinations of other T-invariants are defined as basic T-invariants.If the rank of the incidence matrixCfor a system isr,there are (m-r) basic T-invariants.Note that T-invariants can represent all possible permutations of corresponding transitions.A sequenceσ∈T*is said to be realizable if it is enabled at a reachable markingM∈R(N,M0) leading to another marking or the markingMitself of the system.

    Example 3.Given a Petri net in Fig.5,the initial marking isM0=[1,0,0]T.According to the invariant analysis,two basic T-invariants are [0,1,0,1]Tand[1,0,1,0]T.Neither the sequencet2t4nort1t3is realizable atM0.The combination of the basic T-invariants is realizable since the corresponding transition sequencet1t2t3t4is enabled atM0and a cyclic evolution [1,0,0]Tt1[1,0,1]Tt2[0,1,1]Tt3[0,1,0]Tt4[1,0,0]Tcan be observed.

    Fig.5.Petri net with two basic T-invariants.

    4.2 Necessary condition

    Boundedness and liveness are two crucial properties on which we focus for designing a priority-based controller.Propositions concerned with boundedness and liveness for Petri nets are studied.Given an unbounded Petri net,the possibility of converting it into a live and bounded one using transition priority depends on the existence of the transition sequence in a cyclic evolution contains all transitions inT.Furthermore,a relaxed necessary condition that all elements in the corresponding T-invariant are positive is provided.Meeting the necessary conditions is the prerequisite for control algorithm implementation.

    Proposition 1.Given a Petri net system (N,M0) that is live and bounded,there exists a cyclic evolutions(M) that starts fromM∈R(N,M0),and its corresponding transition sequenceσ[s(M)] contains all transitions existing inN.

    Proof.Since the given net is live,there exist no deadlocks.According to the definition of maximal evolutions,the maximal evolutions in such nets are infinitely fired.Moreover,the Petri net is bounded,and the number of markings in the reachability set is finite.The cyclic behavior shows that the firings of transitions are continuous,but the number of reachable markings is limited.We denote the transition sequence of maximal evolutions asσiσc*,whereσiis an initial sequence fromM0andσcdenotes a cyclic sequence that can be repeated infinitely.Based on the notion of liveness,any transitiont∈TinNis able to enable after firing a transition sequence at any reachable markingM∈R(N,M0).Once the state of the system evolves into a cyclic evolution,each transitiont∈Tfires at least once in the cycleσc.Obviously,the cyclic sequence containing all transitions inTguarantees the liveness of the system.

    Corollary 1.Let a Petri net system (N,M0) be live and bounded.There exists a T-invariantyTthat contains only positive integers.

    Proof.The existence of T-invariants is the necessary condition for realizable cyclic behavior.Since each transitiont∈Tfires at least once in the cyclic sequenceσcif the given net is live and bounded,elements inyTshowing the number of firings of transitions must be positive integers.

    Proposition 2.Given a Petri net system (N,M0),the current priority matrix P is appended on transitions of the net and generates a new Petri net with priorityNP=(N,M0,P) retaining the plant net structure.RG of the PPNNPis a subgraph of its plant netN.

    Proof.Priority on transitions is an external policy enforcing specific behaviors for Petri nets.It limits the firings of enabled transitions such that the number of reachable markings inR(N,M0) is reduced.Ideally,in the condition that all controllable transitions inTshare the same priority level,RG of PPNNPcoincides with its plant netN.

    According to the above propositions,a necessary condition is proposed for the solvability of the priority-based control problem.Note that all propositions and corollaries are suitable for LPNs.

    Theorem 1.If a PPNNP=(N,M0,P) is live and bounded where P denotes the current priority on transitions,there exists at least one cyclic evolution whose corresponding sequence contains all transitions in the plant netN.

    Proof.If the PPNNPis live and bounded,there exist cyclic sequences containing all transitions inNP.The RG ofNPis a subgraph of RG for its plant netN.The cyclic behavior existing in RG ofNPis also shown in RG ofN,i.e.,there is a cyclic sequence containing all transitions inTfor the plant netNeven if it is unbounded nor live.

    Corollary 2.Given a Petri netNthat is unbounded,if there exists a priority relation that enforces the netNlive and bounded,there exists a T-invariantyTin the plant netNwhose all elements are positive.

    Proof.Similar to Corollary 1,a positive integer transition invariantyTexists in a live and bounded system.Since the T-invariant only relates to the structure of the Petri net,it retains the same even if the removing of transition priority may make the plant net unbounded.The existence of T-invariants is the necessary condition for realizable cyclic evolutions.Therefore Corollary 2 loosens the condition in Theorem 1.

    5 Control algorithm using transition priority

    In this section,we propose a control algorithm to enforce the behavior of DES such that each event has the potential to occur infinitely,but only a finite number of states are reachable,i.e.,we provide a control policy that makes the Petri nets operate in a live and bounded manner.Therefore,the cyclic behavior must exist in such Petri net systems.Given an LPN systemGand a bound vectork,we check the necessary condition firstly.Once the solvability is confirmed,we propose a method for finding all reachable markings that accord with the boundkand exist in cyclic evolutions containing all transitions inT.A circuit-based graph is constructed in this section showing the maximal liveness of the net within the given boundk.Both static and dynamic priority matrices calculated by the proposed algorithm are discussed.Since the static priority does not change accordingly with the current state,it may forbid some desired states.The dynamic priority is better for the maximally permissive behavior of the system.

    5.1 Cyclic behavior graph construction

    Here,we propose modified RG called a cyclic behavior graph (CBG),showing the realizable cyclic behavior of the system with additional information.Given a Petri net system (N,M0) and a bound vectork,CBG is a deterministic graph which has as many nodes as the number of reachable markings in all maximal evolutionsσiσc*,whereσidenotes initial sequences andσcdenotes cyclic sequences which contains all transitions inT.Each marking in CBG is labeled with a binary vector [b,l],where the value ofbdepends on whether the subsequent nodes violate boundedness and the value ofldepends on whether the next generated nodes violate liveness.We defineΓ={[b,l]|b,l∈{0,1}} as the set of binary vectors.If there exists any transitiont∈Tthat is enabled at a markingM∈Mcand then generates a new markingM′,the vector [b,l]associated with the markingMis defined as

    wherek-R(N,M0) is the reachability set that guaranteesk-boundedness of the system andMcis the set ofk-bounded markings in cyclic evolutions.In plain words,ifb=0 is associated with a markingM,there exists a markingM′ that is generated by firing a transitiont∈T,M[t〉 andM′ obeys thek-boundedness.Otherwise,for markings withb=1,the next generated markingM′ is beyond thek-boundary.The value oflrelates to the liveness.Ifl=1,the next generated marking ofMis not included in the cyclic evolutions that contains all transitions inT;otherwise,l=0.Markings labeled with [0,1] and [1,1] should be paid more attention in the subsequent study since it may reach undesired states.Note that according to the definition,Mcis the subset ofk-R(N,M0),the marking that is beyond the setk-R(N,M0) must be out ofMc.Therefore,the vector [1,0] does not exists.

    We denote the set of basic T-invariants byYmin={ymin|C×ymin=0}.Let CBG be a four-tupleΗ=(Mc,T,Δ,Γ) whereMcis the set of reachable markings that connect with the cyclic behavior ink-bound,Tis the set of transitions,Δ?Mc×T×Mcis the transition relation among markings,andΓis the set of binary label vectors associated withMc.Table 2 shows the way to construct CBG in pseudocode.

    Table 2 Description of Algorithm 1.

    We explain how to construct CBG according to the cyclic behavior in detail.First,we need to find all reachable markingsM∈R(N,M0) within the bound vectork.The set of such markings is denoted byk-R(N,M0).The setMcis the same ask-R(N,M0)initially.For each markingMinMc,an important step is to check whether it is concluded in a maximal evolution that all transitions inTare contained in the corresponding cyclic sequenceσc.Note that all reachable markings inσcobey thek-boundedness.If no realizable sequenceσiσc*exists,Mis excluded fromMc.All markings inMcaccord withk-boundedness and liveness.So far,primary CBG has been constructed in stage 2.The binary vectors for markings help us decide how to control the occurrence of subsequent events.Markings with[0,0] are safe such that all enabled transitions are welcomed for firing.Since markings labeled by [0,1]and [1,1] may generate markings beyond desired cyclic evolutions,the controller should be switched on at these states to enforce boundedness and liveness to the system.

    5.2 Control strategy using the transition priority matrix

    Given an unbounded Petri net with a required bound vectork,we propose a supervisory controller based on transition priority in Table 3.The calculated priority controls the firings of transitions and enforces the Petri net with priority to be live and bounded,maintaining the structure of the plant net.

    Table 3 Description of Algorithm 2.

    We precisely introduce the control mechanism based on transition priority.The proposed algorithm aims to enforce an unbounded Petri net running in a live and bounded manner with the help of priority.First,we need to check whether the necessary condition is met,i.e.,whether there exists a T-invariant with positive integers only.The existence of such a T-invariant indicates that feasible priority may appear.The construction of CBG by Algorithm 1 is the preparatory step for appending priority to transitions.The crucial part of Table 3 is to control the firings of transitions by priority.Once a word is observed,the current state of the system can be estimated.Firing a transition that leads to an undesired marking,i.e.,a marking beyond the setMc,is avoided.The markings labeled with [0,1] or [1,1]are concerned.Iftifires and leads to an undesired state at a marking whose binary vector is not [0,0],we set the priority oftilower than other simultaneously enabled transitions.

    The dynamic priority enforcingk-boundedness and liveness to the system is conflict-free if each label ofTis different and the dynamic priority-based controller is the least restrictive controller.When the system state changes,the arrangement of transition priority may change accordingly since the preference for firing transitions depends on the presence of the new generated marking inMc.Therefore,conflicts may arise while setting static priorities,and the implementation of static priority can prevent some states inMcfrom being reached.Dynamic priority changes according to the current state of the system and it allows more flexibility.

    The existence of a least restrictive controller implies that the system could meet the maximally permissive behavior whilek-boundedness and liveness are enforced.Assuming a markingM∈R(N,M0)exists,we consider the following situations.IfMis a marking that does not belong to the setk-R(N,M0),it is obviously not a reachable marking of the controlled system.IfMis a reachable marking withink-bound but not a part of a maximal evolution,liveness is violated.It is not a reachable state of a bounded and live system either.Therefore,all markings that arek-bounded and are in the maximal evolutions exist in the reachable set of the system after the control by priority.The dynamic priority-based controller maximally preserves all reachable states while enforcing boundedness and liveness to the plant net.The advantages of the dynamic priority-based controller are shown in Example 4.

    Example 4.Consider the unbounded LPN systemG=(N,M0,E,?) in Fig.6 withM0=[1,0,0,1,0]T.Tokens in the placep3grow infinitely whent2fires continuously.The basic T-invariant with positive integersyT=[2,2,1,1]Texists in the system.The capacity is considered ask(p)=2 for each place.The corresponding CBG is shown in Fig.7.There are 12 reachable markings inMc.If we apply static priority on transitions,i.e.,ρ(t2) <ρ(t1),ρ(t1)=ρ(t3)=ρ(t4),four states inMcare forbidden and shown by dotted lines in Fig.7.While applying dynamic priority relations,all states in CBG are reserved.The dynamic priority matrices Pc1and Pc2restrain firingt2at the markings [1,0,2,0,1]Tand [1,0,2,1,0]Trespectively and are shown as

    Fig.6.Unbounded LPN with bound k=2.

    Fig.7.CBG of the Petri net in Fig.6.

    6 Numerical example

    The case presented in this section is to verify how the dynamic priority matrix works to enforce boundedness and liveness to the system.An example manufacturing system modeled by the Petri net is given in Fig.8.The set of places isP={p1,p2,p3,p4,p5,p6,p7,p8,p9},and the set of transitions isT={t1,t2,t3,t4,t5,t6}.The set of labels isl={‘a(chǎn)’,‘b’,‘c’,‘d’,‘e’,‘f’}.The initial marking isM0=[1,0,0,1,0,0,2,1,1]T.The bound vector isk=[2,2,2,2,2,2,2,2,2]T.Three common resources (modeled byp7,p8,andp9)in this system are shared by two production lines that one of them isp1t1p2t2p3t3,and the other one isp4t4p5t5p6t6.

    Fig.8.Example manufacturing system modeled by the Petri net.

    Tokens in the placesp2andp5grow arbitrarily whent1andt4fire.If the observationbe(oreb) is observed after firingad(orda) atM0,transitions in the subsetT′={t2,t3,t5,t6} are disabled such that the system is not live.Therefore,the plant net is neither bounded nor live.

    First,we check the necessary conditions for this problem.Since the basic T-invariants of this system are [1,1,1,0,0,0]Tand [0,0,0,1,1,1]T,the combination of these two basic T-invariants is[1,1,1,1,1,1]Tthat contains all transitions inT.Obviously,t1t2t3t4t5t6is one of the realizable cyclic sequences atM0.The solvability to this problem is certified.Next,thek-bounded reachability setk-R(N,M0) is calculated,and it is shown in Table 4.There are 36 markings in thek-R(N,M0).We check each marking ink-R(N,M0) and find realizable cyclic evolutions for them.Markings [1,x,1,1,y,1,0,0,0]T,x,y∈{0,1,2} are excluded since firingt2,t3,t5,andt6are permanently prohibited.CBG is constructed and shown in Fig.9.Markings in CBG is shown in Table 5 in detail.

    Table 4 k-bounded reachability set of the plant net in Fig.8.

    Table 5 Markings in CBG of Fig.9.

    Fig.9.CBG of the plant net in Fig.8.

    Given an observationwl=abdthat the corresponding transition sequence ist1t2t4,the markingM11=[1,0,1,1,1,0,1,1,0]Tis reached.Transitionst1,t3,t4,andt5are enabled atM11.Ift5fires atM11,the subsequent marking [1,0,1,1,0,1,0,0,0]Tis generated,which is not included in the maximum live reachability set withink-bound.Therefore,the current priority oft5atM11should be lower thant1,t3,andt4,i.e.,r1,5=1,r3,5=1,andr4,5=1 to avoid the system from entering the undesired state.The current priority matrix atM11is shown as

    Similarly,oncewl=ddabis observed fromM0,t4t4t1t2is the corresponding sequence and markingM18=[1,0,1,1,2,0,1,1,0]Tis reached.The firings oft1andt3are preferred,but firingt4ort5is not allowed sincek-boundedness is violated after firingt4and liveness is broken by firingt5.The current priority matrix atM18is shown as

    7 Conclusions

    This paper addresses the supervisory control problem based on priority for discrete event systems modeled by labeled Petri nets.Given a Petri net that is neither bounded nor live,a necessary condition of the existence of a feasible priority relation for enforcing boundedness and liveness to the system is proven in the first place.We construct a modified RG called CBG with the help of transition invariants.The markings in CBG ensure the maximum liveness of the system within a given bound vector.To enforce boundedness and liveness to the plant net,a control algorithm is proposed using dynamic transition priority,and the priority-based controller is proven to be the least restrictive.The proposed approach maintains the structure of the plant net,and it is efficient for on-line control.In our future work,we plan to continue focusing on the priority-based controller.We will explore the supervisory problem for specific types of Petri nets.LPN with unobservable transitions and workflow nets are what we are concerned about.

    Funding

    This work was supported by the Project of Industrial Internet and Integration of Industrialization and Industrialization of Guangxi,China under Grant No.Guigong2021–37.

    Acknowledgement

    We would like to thank Dr.Zhi-Wu Li (with the Institute of Systems Engineering,Macau University of Science and Technology,Macau,China) for the instructive advice and useful suggestions.

    Declaration of competing interest

    The authors declare no conflicts of interest.

    99视频精品全部免费 在线| 精品人妻熟女av久视频| 成人国产麻豆网| 亚洲精品中文字幕在线视频 | 久久久久网色| 不卡视频在线观看欧美| 久久精品久久精品一区二区三区| 波野结衣二区三区在线| 亚洲精品中文字幕在线视频 | 国产在线免费精品| 91在线精品国自产拍蜜月| 亚洲精品久久久久久婷婷小说| 国产一区有黄有色的免费视频| 国产av国产精品国产| 三级经典国产精品| 男人和女人高潮做爰伦理| 国产成人精品久久久久久| 51国产日韩欧美| 亚洲精品视频女| 国产中年淑女户外野战色| 久久久亚洲精品成人影院| 人体艺术视频欧美日本| 欧美日本视频| 日日摸夜夜添夜夜添av毛片| 亚洲国产色片| 亚洲精品国产av成人精品| 国产精品嫩草影院av在线观看| 久久97久久精品| av免费观看日本| 男女免费视频国产| 高清视频免费观看一区二区| 三级国产精品片| 激情五月婷婷亚洲| 亚洲av中文av极速乱| 人人妻人人看人人澡| 夜夜骑夜夜射夜夜干| 菩萨蛮人人尽说江南好唐韦庄| 一级爰片在线观看| 少妇猛男粗大的猛烈进出视频| 免费少妇av软件| 简卡轻食公司| 熟女av电影| 久久久欧美国产精品| 一区二区三区乱码不卡18| 亚洲国产av新网站| 伊人久久精品亚洲午夜| 国产片特级美女逼逼视频| 男女国产视频网站| av国产免费在线观看| 制服丝袜香蕉在线| 亚洲久久久国产精品| 日日摸夜夜添夜夜爱| 日本vs欧美在线观看视频 | 国内揄拍国产精品人妻在线| 日日啪夜夜撸| 国产精品99久久久久久久久| 韩国av在线不卡| 六月丁香七月| 欧美日韩综合久久久久久| 久久精品国产鲁丝片午夜精品| 99九九线精品视频在线观看视频| 91aial.com中文字幕在线观看| 少妇精品久久久久久久| 18禁裸乳无遮挡免费网站照片| 美女主播在线视频| 一个人看视频在线观看www免费| 少妇 在线观看| 欧美国产精品一级二级三级 | 观看免费一级毛片| 嫩草影院新地址| 一级毛片 在线播放| 天天躁夜夜躁狠狠久久av| 精品亚洲成a人片在线观看 | 大香蕉97超碰在线| 免费大片18禁| 3wmmmm亚洲av在线观看| 国产成人freesex在线| 欧美 日韩 精品 国产| 欧美日韩国产mv在线观看视频 | 一边亲一边摸免费视频| 精品酒店卫生间| av不卡在线播放| 国内揄拍国产精品人妻在线| 亚洲国产日韩一区二区| 又黄又爽又刺激的免费视频.| 免费黄色在线免费观看| 舔av片在线| 搡女人真爽免费视频火全软件| 两个人的视频大全免费| 精品视频人人做人人爽| 在线亚洲精品国产二区图片欧美 | 亚洲av中文字字幕乱码综合| 美女cb高潮喷水在线观看| 中文欧美无线码| 国产高清不卡午夜福利| 久久久久久久大尺度免费视频| 中国三级夫妇交换| 久久精品熟女亚洲av麻豆精品| 国产中年淑女户外野战色| 亚洲国产av新网站| 免费看不卡的av| 在线免费十八禁| 视频中文字幕在线观看| 大陆偷拍与自拍| 99久久精品一区二区三区| 97在线人人人人妻| 少妇 在线观看| 3wmmmm亚洲av在线观看| 一个人看视频在线观看www免费| 国产精品一二三区在线看| 成人影院久久| 亚洲精品自拍成人| 亚洲精品一二三| 99久久人妻综合| 高清毛片免费看| 国产男人的电影天堂91| 久久久午夜欧美精品| 黄色配什么色好看| av在线app专区| 最近2019中文字幕mv第一页| 欧美日韩在线观看h| 亚洲在久久综合| 日韩电影二区| 老熟女久久久| 成年人午夜在线观看视频| 黄色怎么调成土黄色| 亚洲av国产av综合av卡| 全区人妻精品视频| 久久99热6这里只有精品| 男男h啪啪无遮挡| 久久人人爽人人爽人人片va| 亚洲av成人精品一二三区| 91aial.com中文字幕在线观看| 午夜免费男女啪啪视频观看| 夜夜骑夜夜射夜夜干| 日本爱情动作片www.在线观看| 日本色播在线视频| 男女边摸边吃奶| 午夜日本视频在线| 欧美日韩在线观看h| 精品久久久久久电影网| 亚洲欧美一区二区三区黑人 | 黄片wwwwww| 国产精品秋霞免费鲁丝片| 国产午夜精品久久久久久一区二区三区| 亚洲欧美精品专区久久| 欧美日韩视频精品一区| 搡女人真爽免费视频火全软件| 欧美bdsm另类| 亚洲美女黄色视频免费看| 在线观看av片永久免费下载| 网址你懂的国产日韩在线| 亚洲国产色片| 日韩成人av中文字幕在线观看| 一本—道久久a久久精品蜜桃钙片| 精华霜和精华液先用哪个| 在线观看人妻少妇| 干丝袜人妻中文字幕| 天堂俺去俺来也www色官网| 熟女人妻精品中文字幕| 大香蕉97超碰在线| 丰满迷人的少妇在线观看| 久久国产精品大桥未久av | 中文欧美无线码| av国产免费在线观看| 伦理电影大哥的女人| 老师上课跳d突然被开到最大视频| 建设人人有责人人尽责人人享有的 | 七月丁香在线播放| 国产女主播在线喷水免费视频网站| 亚洲在久久综合| 人人妻人人澡人人爽人人夜夜| 亚洲人成网站高清观看| 天堂俺去俺来也www色官网| 国内精品宾馆在线| 免费大片18禁| 少妇的逼好多水| 日本wwww免费看| 欧美日韩在线观看h| 久久热精品热| 天堂中文最新版在线下载| 不卡视频在线观看欧美| 亚洲中文av在线| 五月开心婷婷网| 蜜桃在线观看..| 老熟女久久久| 青春草国产在线视频| 国产黄色视频一区二区在线观看| 男人爽女人下面视频在线观看| 国产精品一区二区在线不卡| 各种免费的搞黄视频| 色婷婷av一区二区三区视频| 亚洲av国产av综合av卡| 日韩一本色道免费dvd| 免费观看av网站的网址| 久久久久久九九精品二区国产| 成年女人在线观看亚洲视频| 亚洲国产欧美人成| 看非洲黑人一级黄片| 欧美精品一区二区免费开放| 亚洲欧洲国产日韩| 又大又黄又爽视频免费| 午夜视频国产福利| 日本黄色日本黄色录像| 三级国产精品欧美在线观看| 欧美日韩综合久久久久久| 久久久久国产网址| 久久久久国产网址| 亚洲,欧美,日韩| 国产探花极品一区二区| 美女脱内裤让男人舔精品视频| 九草在线视频观看| 色综合色国产| 亚洲在久久综合| 精品国产一区二区三区久久久樱花 | 日日撸夜夜添| 一级片'在线观看视频| 九色成人免费人妻av| 一区二区av电影网| 网址你懂的国产日韩在线| 国产有黄有色有爽视频| 国产成人a区在线观看| tube8黄色片| 亚洲精品国产av蜜桃| 久热久热在线精品观看| 国产亚洲一区二区精品| 欧美成人精品欧美一级黄| 下体分泌物呈黄色| 国产免费一区二区三区四区乱码| 啦啦啦视频在线资源免费观看| 一区二区三区乱码不卡18| 日韩欧美精品免费久久| 高清欧美精品videossex| 97精品久久久久久久久久精品| 秋霞在线观看毛片| 国产视频内射| 在现免费观看毛片| 美女内射精品一级片tv| 黑人高潮一二区| 亚洲国产欧美在线一区| 黄片无遮挡物在线观看| av播播在线观看一区| 亚洲av欧美aⅴ国产| 制服丝袜香蕉在线| freevideosex欧美| 汤姆久久久久久久影院中文字幕| 一区二区三区精品91| 亚洲av国产av综合av卡| 大香蕉久久网| 91久久精品电影网| 色婷婷av一区二区三区视频| 久久久国产一区二区| 久久99热这里只有精品18| 我的老师免费观看完整版| 最黄视频免费看| 亚洲熟女精品中文字幕| 只有这里有精品99| 日日撸夜夜添| 久久久久久久精品精品| 国产精品一区www在线观看| 麻豆精品久久久久久蜜桃| 日韩 亚洲 欧美在线| 一区二区三区免费毛片| av在线播放精品| 91久久精品国产一区二区三区| 美女国产视频在线观看| 免费高清在线观看视频在线观看| 亚洲一区二区三区欧美精品| av播播在线观看一区| 一区二区av电影网| 免费不卡的大黄色大毛片视频在线观看| 国产精品偷伦视频观看了| 在线观看av片永久免费下载| .国产精品久久| 欧美激情国产日韩精品一区| 亚洲av二区三区四区| 日本黄色日本黄色录像| 一区二区三区精品91| 免费播放大片免费观看视频在线观看| 国产精品三级大全| 久久久色成人| 亚洲高清免费不卡视频| 菩萨蛮人人尽说江南好唐韦庄| 久久精品夜色国产| 久久国产精品男人的天堂亚洲 | 水蜜桃什么品种好| 国产91av在线免费观看| 国产黄片美女视频| freevideosex欧美| 国产亚洲欧美精品永久| 少妇猛男粗大的猛烈进出视频| 男人狂女人下面高潮的视频| 大又大粗又爽又黄少妇毛片口| 女人久久www免费人成看片| 亚洲精品乱码久久久久久按摩| 777米奇影视久久| 王馨瑶露胸无遮挡在线观看| 欧美高清性xxxxhd video| 久久亚洲国产成人精品v| 在线看a的网站| 99热国产这里只有精品6| 亚洲精品国产色婷婷电影| 国产中年淑女户外野战色| 欧美老熟妇乱子伦牲交| 美女脱内裤让男人舔精品视频| 在线观看免费日韩欧美大片 | 嘟嘟电影网在线观看| 直男gayav资源| 人妻 亚洲 视频| 在线看a的网站| 成人国产av品久久久| 美女高潮的动态| 国产伦理片在线播放av一区| 这个男人来自地球电影免费观看 | 精品久久久久久电影网| 大片免费播放器 马上看| 极品教师在线视频| 精品视频人人做人人爽| 日韩,欧美,国产一区二区三区| 亚洲精品乱码久久久久久按摩| 97在线视频观看| 国产成人aa在线观看| 在线观看一区二区三区激情| 久久鲁丝午夜福利片| 婷婷色麻豆天堂久久| 丰满乱子伦码专区| 国产乱来视频区| 人人妻人人爽人人添夜夜欢视频 | 国产深夜福利视频在线观看| 国产白丝娇喘喷水9色精品| 欧美日韩视频精品一区| 国产精品一及| 亚洲高清免费不卡视频| a级毛色黄片| 久久精品国产亚洲av天美| 尾随美女入室| 国产 一区精品| 国产精品爽爽va在线观看网站| 亚洲综合精品二区| 99热这里只有精品一区| 97超碰精品成人国产| 寂寞人妻少妇视频99o| 日韩av免费高清视频| 精品久久久精品久久久| 国产久久久一区二区三区| 蜜桃在线观看..| 身体一侧抽搐| 看非洲黑人一级黄片| 在线观看国产h片| 最近手机中文字幕大全| 亚洲av在线观看美女高潮| 一个人看的www免费观看视频| 寂寞人妻少妇视频99o| 国产成人91sexporn| 国产黄片视频在线免费观看| 99久国产av精品国产电影| 国产乱人偷精品视频| 国产欧美亚洲国产| 亚洲美女黄色视频免费看| 国产精品精品国产色婷婷| 美女高潮的动态| 99re6热这里在线精品视频| 国产精品av视频在线免费观看| 国语对白做爰xxxⅹ性视频网站| 乱码一卡2卡4卡精品| 九九在线视频观看精品| av免费观看日本| 国产精品三级大全| 国产精品熟女久久久久浪| 黄色欧美视频在线观看| 欧美最新免费一区二区三区| 久久久久久久久大av| 天堂8中文在线网| 男人和女人高潮做爰伦理| 国产精品伦人一区二区| 中文字幕久久专区| av在线观看视频网站免费| 综合色丁香网| 亚洲欧美一区二区三区国产| 亚洲丝袜综合中文字幕| 成年美女黄网站色视频大全免费 | 日韩av不卡免费在线播放| 国产精品av视频在线免费观看| 久久久久人妻精品一区果冻| 亚洲欧美一区二区三区国产| 日韩欧美一区视频在线观看 | 亚洲欧美精品自产自拍| 欧美人与善性xxx| 在线观看免费日韩欧美大片 | 日韩在线高清观看一区二区三区| 午夜日本视频在线| 国产亚洲欧美精品永久| 黄色怎么调成土黄色| 国产精品久久久久久精品古装| 免费看不卡的av| 亚洲真实伦在线观看| 少妇裸体淫交视频免费看高清| 久久精品夜色国产| 高清在线视频一区二区三区| 十八禁网站网址无遮挡 | 亚洲四区av| 18禁动态无遮挡网站| av专区在线播放| 2022亚洲国产成人精品| 天美传媒精品一区二区| 国产亚洲av片在线观看秒播厂| 天天躁夜夜躁狠狠久久av| 观看美女的网站| 精品人妻一区二区三区麻豆| 一级毛片黄色毛片免费观看视频| 亚洲一级一片aⅴ在线观看| 久久久久国产精品人妻一区二区| 伦理电影大哥的女人| 99热网站在线观看| 国产精品99久久99久久久不卡 | 18+在线观看网站| 亚洲精品,欧美精品| 中国国产av一级| 国产欧美日韩一区二区三区在线 | 亚洲精品国产成人久久av| 内地一区二区视频在线| 亚洲第一区二区三区不卡| 18禁在线播放成人免费| 纯流量卡能插随身wifi吗| 日本免费在线观看一区| 国产精品一及| a 毛片基地| 亚洲精华国产精华液的使用体验| 久久久久精品久久久久真实原创| 能在线免费看毛片的网站| 成年女人在线观看亚洲视频| 成人毛片60女人毛片免费| 久久人人爽人人爽人人片va| 狂野欧美白嫩少妇大欣赏| 久久久久国产网址| 国产男人的电影天堂91| 极品教师在线视频| 永久网站在线| 激情五月婷婷亚洲| 极品教师在线视频| 美女脱内裤让男人舔精品视频| 97在线视频观看| 久久久久久久久久久丰满| 亚洲精品自拍成人| 亚洲婷婷狠狠爱综合网| 小蜜桃在线观看免费完整版高清| 哪个播放器可以免费观看大片| 欧美日韩国产mv在线观看视频 | 亚洲av中文av极速乱| 舔av片在线| 又爽又黄a免费视频| 国产精品国产三级专区第一集| 在线观看免费高清a一片| 亚洲av在线观看美女高潮| 色网站视频免费| 国产精品三级大全| 国产中年淑女户外野战色| 欧美激情极品国产一区二区三区 | 黑丝袜美女国产一区| 自拍欧美九色日韩亚洲蝌蚪91 | 毛片女人毛片| 欧美日本视频| 欧美日韩精品成人综合77777| 春色校园在线视频观看| 人人妻人人看人人澡| 亚洲av福利一区| 国产片特级美女逼逼视频| 熟女av电影| 最近最新中文字幕免费大全7| 午夜激情福利司机影院| 免费av不卡在线播放| 男女国产视频网站| 97在线人人人人妻| 亚洲欧美日韩无卡精品| 在现免费观看毛片| 色综合色国产| 97在线视频观看| 国产一区有黄有色的免费视频| 国产精品无大码| 久久久久网色| 国产成人freesex在线| 午夜激情久久久久久久| 精品99又大又爽又粗少妇毛片| 亚洲精品乱码久久久久久按摩| 午夜老司机福利剧场| 色5月婷婷丁香| 亚洲自偷自拍三级| 国产精品伦人一区二区| 国产精品一区二区性色av| 美女福利国产在线 | 制服丝袜香蕉在线| 国产成人a∨麻豆精品| 亚洲国产精品999| 久久人人爽人人爽人人片va| 成年av动漫网址| 国产精品偷伦视频观看了| 五月天丁香电影| 免费av不卡在线播放| 精品一区在线观看国产| 高清在线视频一区二区三区| 亚洲真实伦在线观看| 丝袜脚勾引网站| 久久久久久久久久人人人人人人| 99久久精品热视频| 日韩一区二区三区影片| 亚洲av二区三区四区| 精品少妇久久久久久888优播| 精品视频人人做人人爽| 日本与韩国留学比较| 婷婷色综合www| h日本视频在线播放| 亚洲aⅴ乱码一区二区在线播放| 欧美高清成人免费视频www| 97超视频在线观看视频| 伊人久久国产一区二区| 婷婷色综合大香蕉| 青春草国产在线视频| 3wmmmm亚洲av在线观看| 久久6这里有精品| 麻豆成人av视频| 日日撸夜夜添| 妹子高潮喷水视频| 国产永久视频网站| 亚洲综合精品二区| 网址你懂的国产日韩在线| 国产高清国产精品国产三级 | 日本色播在线视频| 韩国高清视频一区二区三区| 国内少妇人妻偷人精品xxx网站| 亚洲高清免费不卡视频| 久久av网站| 精品一区在线观看国产| 男人添女人高潮全过程视频| 一级毛片 在线播放| 内地一区二区视频在线| 亚洲精品,欧美精品| 丝袜脚勾引网站| 精品国产露脸久久av麻豆| 久久影院123| 国产成人a区在线观看| 日本vs欧美在线观看视频 | 国产黄色视频一区二区在线观看| 国产免费福利视频在线观看| 一区二区三区免费毛片| 久久久久国产网址| 午夜免费鲁丝| 欧美日本视频| 久久久精品94久久精品| 男女无遮挡免费网站观看| 亚洲自偷自拍三级| tube8黄色片| 亚洲一级一片aⅴ在线观看| 久久久久久久国产电影| 少妇人妻一区二区三区视频| 国产 精品1| 我的老师免费观看完整版| 亚洲婷婷狠狠爱综合网| 女性生殖器流出的白浆| 最近中文字幕高清免费大全6| 欧美日本视频| 欧美另类一区| 精品一品国产午夜福利视频| 日韩中文字幕视频在线看片 | av播播在线观看一区| 99热6这里只有精品| 久久热精品热| 国产亚洲精品久久久com| 精品国产一区二区三区久久久樱花 | 久久99蜜桃精品久久| 秋霞在线观看毛片| 天天躁夜夜躁狠狠久久av| av女优亚洲男人天堂| 在线看a的网站| 国内精品宾馆在线| 国产有黄有色有爽视频| 日韩欧美精品免费久久| 老司机影院毛片| 亚洲高清免费不卡视频| 免费av不卡在线播放| 亚洲成人手机| 成人亚洲精品一区在线观看 | 午夜激情福利司机影院| 日韩av不卡免费在线播放| 最近的中文字幕免费完整| 午夜日本视频在线| 久久人人爽人人片av| 精品人妻视频免费看| 日本黄色片子视频| 免费高清在线观看视频在线观看| 最近的中文字幕免费完整| 中文字幕av成人在线电影| 丝袜脚勾引网站| av在线蜜桃| 日本欧美国产在线视频| 男女免费视频国产| 国产精品久久久久久精品电影小说 | 亚洲怡红院男人天堂| 国产日韩欧美亚洲二区| 七月丁香在线播放| 一个人免费看片子| 中文精品一卡2卡3卡4更新| 男女无遮挡免费网站观看| 欧美少妇被猛烈插入视频| 日日摸夜夜添夜夜添av毛片| 日本av手机在线免费观看| 国产成人精品福利久久| 18禁在线无遮挡免费观看视频| 精品国产一区二区三区久久久樱花 | 激情 狠狠 欧美| 国产午夜精品一二区理论片| 国产亚洲午夜精品一区二区久久| 午夜视频国产福利| 国产精品精品国产色婷婷| 免费看光身美女| 亚洲成人手机|