6.2.2 Further properties

DTP: deadlock-trap-property

A net satisfies the deadlock-trap-property , if the maximal trap in each minimal deadlock is sufficiently marked [Sta90, Kapitel 15 (162-175)]. A trap is a set of places that, if it contains tokens, cannot become clean, because every transition which subtracts tokens from one place in this set has a post-place in this set, and thus returns tokens to the set. Hence, the empty set is a trap. A trap is maximal, if it is not a proper subset of a trap. A deadlock is a non-empty set of places that cannot be marked again once it is clean, because every transition which would fire tokens onto a place in this set has a pre-place in this set (and so cannot fire). A deadlock is minimal, if it does not properly contain a deadlock. A set of places is sufficiently marked, if it contains a place which contains sufficiently many tokens to enable all its post-transitions.

Further information can be found in chapter 6.7 on page ff.

SMC: state machine coverable

A component of a net is a set of places which is both a deadlock and a trap. It defines a sub-net comprising these places and the adjoining transitions. If a set of components is given such that the corresponding sub-nets define state machines, and their union equals the set of all places in the net, then this net is said to be state machine coverable [Sta90, Definition 16.2.2 (180)].

Further information can be found in chapter 6.7 on page ff.

SMD: state machine decomposable

If a set of components is given sucht that the corresponding sub-nets define strongly connected state machines, and their union equals the set of all places in the net, then this net is said to be state machine decomposable [Sta90, Definition 16.2.3. (180)].

Further information can be found in chapter 6.7 on page ff.

SMA: state machine allocatable

In a state machine decomposable net, every transition has a pre-place; a pre-place allocation is a mapping which assigns to each transition one of its pre-places. A component is said to be selected in a pre-place allocation, if to all transitions that have a pre-place in the component, a pre-place in the component is assigned. The net is said to be state machine allocatable, if every pre-place allocation selects a strongly connected state machine component [Sta90, Definition 16.3 (182)].

Further information can be found in chapter 6.7 on page ff.

CPI: covered by place invariants

A net is covered by place invariants, if there exists a P-invariant which assigns a positive value to each place [Sta90, Definition 11.4 (114)].

CTI: covered by transition invariants

A net is covered by transition invariants, if there exists a T-invariant which assigns a positive value to each transition [Sta90, Definition 11.3 (112)].

B : bounded

A net is bounded, if there is a number k such that, in any reachable marking, there are never more than k tokens on a place [Sta90, Definition 14.1 (38)].

SB : structurally bounded

A net is structurally bounded, if it is bounded in every initial marking [Sta90, Bemerkung (116)].

REV: reversible

A net is reversible, if the initial state can be reached from every reachable state [Sta90, Definition 6.2 (59)].

A description of the reversibility test can be found in chapter 6.5.4 on page .

DSt: dead state reachable

A dead state is reachable, if a state is reachable in which no transition can fire any more [Sta90, Definition 6.1.1 (54)].

BSt: bad state reachable

If a state satisfies a so-called ``bad'' predicate (see chapter 6.5.4 on page ), it is not further developed when computing a state graph. In this case, the attribute Bst is set. However, after leaving the graph analysis, this attribute is reset to ?.

DTr: dead transition at initial marking

This attribute indicates whether the net has dead transitions in the initial marking, i.e. facts.

DCF: dynamically conflict free

A net is said to be dynamically conflict free, if no state is reachable in which two transitions are enabled and one of them can be disabled by firing the other. [Sta90, Definition 3.4.3 (35)].

L : live

A net is live, if all its transitions are live in the initial marking, i.e., no state is reachable in which a transition is dead. Here, facts are ignored [Sta90, Definition 6.1.5 (55)].

A description of the liveness test can be found in chapter 6.5.4 on page .

LV : live when ignoring dead transitions

A net is live when ignoring dead transitions, if all its transitions, which are not already dead in the initial marking, are live. The transitions thereby ignored can be considered as unspecified facts.

L&S: live and safe

A net is live and safe, if it is live and, in any reachable marking, not more than one token is on a place [Sta90, Definition 4.1 (39)].

Liveness for coloured nets

WL : weakly live

A coloured net is weakly live, if all its transitions are weakly live, i.e. for each transition, there is a colour in which the transition is live in the initial marking [Sta90, Definition 20.6.1 (228)] (see also page in chapter 6.5.4).

CL : collectively live

A coloured net is collectively live, if all its transitions are collectively live. A transition is collectively live, if for every reachable state a colour exists, such that in a state reachable from this marking, the transition can fire in this colour [Sta90, Definition 20.6.2 (228)] (see also page in chapter 6.5.4). In particular, every weakly live transition is also collectively live [Sta90, Folgerung 20.3.2 (229)].