Tham khảo tài liệu 'petri nets applications part 7', kỹ thuật - công nghệ, cơ khí - chế tạo máy phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả | Hybrid state Petri nets which have the analysis power of stochastic hybrid systems and the formal verification power of automata 231 N A PxTuTxP is a node function which maps each arc A 6 A to a pair of ordered nodes N A where a node is a place or a transition1. The place of N A is denoted by P A the transition of N A is denoted by T A such that for all A 6 Ae u AI N A P A T A and for all A 6 AO either N A P A T A or N A T A P A . Further notation - A T A 6 A T A T denotes the set of arcs connected to transition T Ain T A 6 A T N A P A T is the set of input arcs of T AOut T A 6 A T N A T P A is the set of output arcs of T Ain o T Ain T n Ao is the set of ordinary input arcs of T Ain OE T Ain T n Ae u Ao is the set of input arcs of T that are either ordinary or enabling and - P Ac P A A 6 Ac is the multi-set of places connected to the subset of arcs Ac c A. Finally Ai 6 Al 3A 6 A A Ai N A N Ai 0 . if an inhibitor arc points from a place P to a transition T there is no other arc from P to T. Sc R0 R1 R2 . is a finite set of colour types with R0 0. C P S is a colour type function which maps each place P 6 P to a specific colour type in S. Each token in P is to have a colour in C P . Since C P 6 R0 R1 . there exists a function n P N such that C P Rn p . If C P R0 0 then a token in P has no colour. Further notation if P Ac contains more than one place . P Ac Pi1 . Pik then C P Ac is defined by C Pi1 x . xC P . I N P x C P N 0 1 is a probability measure which defines the initial marking of the net for each place it defines a number 0 of tokens initially in it and it defines their initial colours. Here N P m-1 . m P mi 6 N mi TO i 1 . P and C P N C P1 m1 x . xC P P m P mi 6 N mi TO i 1 . P where C Pi mi Rmin pi for all i 1 . P where P is denoted P P1 . P P . It is assumed that all tokens in a place are distinguishable by a unique identification tag which translates to a unique ordering listing of tokens per place. V Vp P 6 P C P R0 is a set of token colour .
