Timed Petri nets (TPN) or Duration Petri nets (DPN) is a well-know approach to extend \classic" Petri nets in order to allow the modeling of time [1]. In [2], a state equation for TPN was provided that describes the net's marking in an algebraic manner, but not its transitions clocks. Hence, proo ng the nonreachability of a marking is mainly done by symbolic manipulation of the state equation, which is impractical for the automated generation of such proofs. Here, we introduce a holistic state equation that allows for modeling the clocks algebraically in addition to markings and thus provides a more automatical way to show the nonreachablity of speci c markings. This section introduces the basic notations we use in our paper. N+ = N n f0g denotes the set of natural numbers without 0, and Q0+ denotes the set of nonnegative rational numbers. Let S be a nite set. jSj is the number of elements of S. Multisets can contain an element multiple times and are designated by Fraktur letters. The ]-operator denotes the union of multisets. The number of occurrences of each element in the result of the ]-operation is given by the sum of the occurrences of this element in both operands. jSje denotes the multiplicity of e in the multiset S. 1c is the indicator function which yields 1 i the condition c holds or 0 otherwise. A matrix A 2 M(m; n) is a matrix with m rows and n columns. A superindex in parentheses distinguishes di erent matrices or vectors, and their elements, respectively. Zm n = (zi;j ) 2 M(m; n) is the zero matrix with zi;j = 0 and En = (ei;j ) 2 M(n; n) denotes the identity matrix with:
2.1
The relation r(
i
The relation r(
The structure N = (P; T; F; V; m(0)) is called a Petri net (PN), i 1. P , T are nite sets with P \ T = ; and P [ T 6= ;, 2. F (P T ) [ (T P ) (relation between places and transitions), 3. V : F ! N+ (weight of the arcs), 4. m(0) : P ! N (initial marking) A marking of a Petri net is a function m : P ! N, such that m(p) denotes the number of tokens at the place p. The pre- and post-sets of a transition t are given by t = fp : (p; t) 2 F g and t = fp : (t; p) 2 F g, respectively. Each transition t 2 T induces the marking change t and t+, de ned as follows: t (p) = (V (p; t) (p; t) 2 F 0 else t+(p) = (V (t; p) (t; p) 2 F 0 else A transition t 2 T is enabled (may re) at a marking m, i t (p) m(p) for every place p 2 P . When an enabled transition t at a marking m res, this yields a new marking m0 given by m0(p) := m(p) t (p) + t+(p). The ring is denoted by m !t m0.
The structure Z = (N ; D) is called a Timed Petri net (TPN) i : 1. N (called Skeleton of Z) is a Petri net, 2. D : T ! Q0+.
D(t) is the duration of the ring transition t and denotes the delay of t. It is easy to see, that considering TPNs with D : T ! N will not result in a loss of generality. Therefore, only such time functions D will be considered subsequently.
An active transition t passes through three phases. First it consumes tokens from t which leads to a new marking m0(p) := m(p) t (p). This change takes no time. Then time D(t) passes. During this time, the marking m0 may change to m00 by the ring of other transitions. Finally t delivers tokens to t which leads to the marking m000(p) := m00(p) + t+(p).
Let z = (m; u) be a state in the Timed Petri net Z = (P; T; F; V; m0; D). Then M T is a maximal step in z, if m ^ u(t^) = 0 =) t^ 6 m
P t . t2M In a Timed Petri net, an enabled transition must re immediately. In case of nonself-concurrent transitions, a transition can only be enabled, if it is not active at the moment. Please note, immediate transitions are implicitly self-concurrent. In the following we will consider all delayed transitions as not self-concurrent.
Let z1 = (m1; u1) be a state in the Timed Petri net Z and M
re in z1 (notation: z1 M!), if M is a maximal step in z1. After the ring of M the net Z changes into the state z2 = (m2; u2) (notation: z1 M! z2) with: T . Then M can To ensure nite global steps, we do not allow Timed Petri nets with time deadlocks, i.e., with a closed directed path that contains immediate transitions only.
Let z1 = (m1; u1) be a state in the Timed Petri net Z. Then, the elapsing of one time unit is possible in Z (notation: z1 !1), if 8t 2 T : u1(t) = 0 =) t 6 m1 After the elapsing of one time unit the Timed Petri net Z is in the state z2 = (m2; u2) (notation: z1 !1 z2) with:
X t+ and u2(t) := (u1(t) 0 1 u1(t) else 1
Like in classical Petri nets, we describe the structure of a Timed Petri net by two matrices C+; C 2 M(jP j; jT j) over the base set N, with ci+;j = tj+(pi) and ci;j = tj (pi). Furthermore the delay of each transition is encoded in a delay matrix 2 M(jT j; d), where d = maxfD(t) : t 2 T g + 1 speci es the maximum delay. The matrix is given by the following de nition: i;j = (1 j = D(ti) + 1
0 else 3.2
The dynamic of a Petri net at each point of time, is unambiguously decribed by its state. In our model, the state consists of two parts, the place marking m and the clock matrix U. The place marking is given by a vector m 2 M(jP j; 1) over N, which speci es how many tokens are on each place. In contrast to classical Petri nets not only the marking is part of the state. The clock matrix U 2 M(jT j; d) accounts for all active transitions. The element ui;j speci es how often a transition ti has consumed D(ti) j +1 time steps ago, and therefore how often it will deliver in j 1 time steps from now. Thus, the rst row of U states how many times each transition will nish right now. Because a zero delay transition tk is intrinsically self-concurrent, the value of uk;1 may have any value from N. But the row sum of delayed transitions is at most 1, due to the lack of self-concurrency. It is easy to see, that all values ui;j for j > D(ti) + 1 are zero.
To calculate the state reached by a given ring sequence, we have to represent the sequence inside our equation. In classical Petri nets this is done by the Parikh vector. We extend the Parikh vector to the Parikh matrix. The Parikh matrix 2 M(jT j; jT j) of a global step G is de ned by = diag( 1; : : : ; jT j) with i = jGjti To use m, U and together, three operators A 2 M(d; 1) (adoption operator), R 2 M(d; d) (progress operator) and 2 M(jT j; d) (selection operator) are necessary, speci ed by the corresponding matrices:
A = 1 0 : : : 0 T ri;j = (1 i 0 else j = 1 i;j = (1 j = 1 0 else _ = A gains the \classical" Parikh vector. The term (i) later used is an abbreviation of Pij=1 _ (j) and speci es how often each transition has red until time step i.
Using the de nitions of the section above, we can derive an algebraic description for a single state change:
U0 = U + U00 = U0 R m0 = m
C m00 = m0 + C+ U0 R A
A + C+
A (Firing) (Time elapsing)
To apply Equations (
G(!i) (m^ (i); U^ (i)) and (m^ (i); U^ (i))
! (m~ (i+1); U~ (i+1))
1
respectively. Every ring sequence can then be represented by alternating ring
and time elapsing steps, where some of the G can be empty sets of course:
: (m~ (
G(1!) (m^ (
G(
G(!i) (m^ (i); U^ (i))
The term m~ (
We now consider the actual state equation. From Equations (
i U^ (i) = X j=1 (j)
Ri j m^ (i) = m(0) + C+
(j) 0 i
X
C C (i) (i) With de ning in a more compact way: (i) := ( k(i D(tk)) +
+ k(
C (i)
Let ^(i) := U^ (i) 0 1 1 T dennote all transition which are active immediately after the zero delay transitions in ring step i have delivered. Since each delayed transition can only be active once at each point of time, only clock matrices U^ (i) are valid, which ful ll the following constraint: 1 T ! U^ (i) (6) (7) (8) (9) The right part of Equation (6) helps reformulating Equation (4) into m^ (i) = m(0) + (C+
C ) (i)
C
^(i)
The vector (i) sums up all transition which have completed until time step i.
It is easy to see that (i) + ^(i) yields the Parikh vector (i). An equation for
m~ (i) can be obtained by applying Equations (
BjT j, with Bk = (f0; 1g f0g
D(tk) > 0
else
The vector ~(i) := U~ (i) 0 1 1 T speci es all transition which are in progress
after the i-th time step has nished. This vector is elementwise less or equal than
^(i 1), because we have to subtract the elements of the second column of U^ (i 1)
to yield ~(i). Furthermore ~(i) is elementwise less or equal than ^(i), which
follows directly from Equation (
State equations provide a criterion to decide whether a given marking is not reachable in a speci ed Petri net. When the state equation does not have a solution, the marking is not reachable. In case of Timed Petri nets, Equations (7) and (9) as well es the constraint Equations (10) form a system of diophantene (in-)equalities. If this system does not have a valid solution, a given m^ -marking and m~ -marking, resp., is not reachable. A solution is valid if and only if the Parikh vector candidate does not contain a negative element. Furthermore we can draft on predecessor markings and maximal step conditions to further discard some valid solutions of the state equation.
In this section we show how the state equation in the recent section can be used for a more systematical nonreachability proof of the example given in [2]. Consider the following Timed Petri net Z: t1h1i 1 p2 1 2 1 p1 3 t3h1i
2 t4h1i 1
2 p3 t2h1i We want to show that the marking m = 0 2 0 T is not reachable. To do so, one has to show that both m~ (i) = m and m^ (i) = m are not reachable in Z. Lets consider the m~ (i)-case rst. First we have to determine all (i 1) + ^(i 1) which solve Equation (9). The solution space St depends on ~(i) and can be calculated by the Gauss-Algorithm: ~(i) + k 011 B@B01CAC : k 2 Z 1 In this special case it follows from Equation (10) that ~(i) must be the zero vector, so only one solution space has to be considered during the further calculation. As stated, a valid solution cannot contain a negative component. Thus, we can rule out all ^(i 1) for which the set NjT j \ fS ^(i 1) : S 2 Stg is empty. Algorithmically this problem can be decided by integer linear programming techniques. In our example at least ~3(i 1) must be zero, which narrows the set of possible ^(i 1) down to eight distinct cases, shown in the following table. With the aid of Equation (8), we can calculate the corresponding m^ (i 1): candidates for ^(i 1) corresp. m^ (i 1) 001 011 B0C B0C B@0CA B@0CA 0 0 001 B1C B@0CA 0 011 B1C B@0CA 0 001 B0C B@0CA 1 011 B0C B@0CA 1 001 B1C B@0CA 1 011 B1C B@0CA 1 11 1A 2 Because places cannot contain a negative amount of tokens, we can rule out the last six cases. The remaining two cases can be discarded by aid of De nition 3. According to the de nition of a maximal step for all active transitions tk, i.e., all transitions tk for which ^k = 0, it must hold m^ 6 tk . Now we consider t4 which is active in both cases. The maximal step condition m^ (i 1) 6 0 1 0 T resulting from t4 is not ful lled. Thus, the two remaining solutions are not valid in Z. Consequently m cannot be reached as a m~ -marking.
Now, we show m is not reachable as a m^ -marking. First, we calculate the set Y of possible ^(i) by using the de nition of the maximal step:
Y(m^ (i)) = f ^ : (8k : ^k = 0 =) m^ (i) 6 tk )g In our example, at least ^(i) = 1 and ^(i) = 1, otherwise the maximal step 3 4 condition for t3 and t4, resp., would not be ful lled. Then we calculate the solution set Sf of Equation (7).
80 11 02 > > Sf ( ^(i)) = <BB 00CCA + BB@10 >@ :> 0 2 6 1 0 0C 1 2 1CA 0 0 0 0 31 In the example every possible ^(i) yields at least one Parikh vector m^ (i) we can calculate m~ (i) by: (i). From m~ (i) = m^ (i) + C+ ~(i)
C+ ^(i) Due to Equation (10) the vector ~(i) must be the zero vector in this example. Consequently we can calculate m~ (i) without further case discriminations on ~(i): ^(i) corresp. m~ (i) 001 B0C B@1CA 1 011 B0C B@1CA 1 001 B1C B@1CA 1 011 B1C B@1CA
1 0 31 0 1A 2 This leads to an invalid solution for the marking in each case. Thus, m is not reachable as a m^ -marking, too. 5
We have presented a new state equation for Timed Petri nets. In contrast to [2] the new equation is a holistic one: It describes the marking as well as the clocks, whereas [2] has dealt with the net's marking only.
Also, we have demonstrated in an example how the new state equation can be used to prove non-reachability.