PETRI NETS AND THEIR PROPERTIES - Modelling with Generalised Stochastic Petri Nets - page 47

semiflows) such that:
0
@ X
p j ∈P

1 0

@ X
p j ∈P

1

y j · max(I(t l ,p j ),I(t m ,p j ))

A

y j · M 0 (p j )

A

> (2.22)

Also for causal connection it is possible to define a structural counterpart
that is a necessary condition for causality, and that we shall call structural
causal connection (SCC).
Definition 2.5.8 Transition t m is structurally causally connected to t l (de-
noted by t l SCC t m ) iff:
I(t m ) · C + (t l ) + H(t m ) · C − (t l ) > 0 (2.23)
where C + is the matrix containing the positive elements of the incidence
matrix C, while C − contains the absolute values of the negative elements of
C.
Structural causal connection between two transitions exists when the firing
of the first transition either increments the marking of some input place,
or decrements the marking of some inhibition place of the second one. The
structural relation of causal connection is a necessary, but not su cient
condition for the firing of a transition to cause the enabling of another
transition.

2.6 State Space Analysis Techniques

As we mentioned before, there exist properties of PN systems that depend
on the initial marking, and that can thus be studied only by taking this
information into account. The techniques used to prove these properties are
called state space (or reachability) analysis techniques. State space analysis
techniques are inherently non parametric with respect to the initial marking,
since they require its complete instantiation. Thus state space techniques
refer to PN systems, not to PN models or Petri nets.
The reachability analysis is based on the construction of the RG of the PN
system, and it is feasible only when the RS and the RG are finite. Even if
the RS and RG are finite, their size can vary widely with the PN structure
and the number of tokens in M 0 . In many cases, the growth in the number
of markings can be combinatorial both in the number of places and in the
number of tokens in M 0 . Reachability analysis techniques are very powerful,
since they allow the proof of most properties of interest by inspection, as
the RS and RG contain all possible evolutions of the PN system. However,
it often happens that the space and time complexity of the RG construction
algorithm exceeds any acceptable limit.
Once the RG has been built, properties may be checked using classical graph
analysis algorithms, as explained in the following. Let us consider separately
each property discussed in section 2.4.