Bounded Delay Timing Analysis of a Class of CSP Programs.
We describe an algebraic technique for performing timing analysis of a class of asynchronous circuits described as CSP programs (including Martins probe operator) with the restrictions that there is no OR-causality and that guard selection is either completely free or mutually exclusive. Such a description is transformed into a safe Petri net with interval time delays specified on the places of the net. The timing analysis we perform determines the extreme separation in time between two communication actions of the CSP program for all possible timed executions of the system. We formally define this problem, propose an algorithm for its solution, and demonstrate polynomial running time on a non-trivial parameterized example. Petri nets with 3000 nodes and 10^16 reachable states have been analyzed using these techniques.
Introduction
There has been much work in the past decade on the synthesis of speed-independent (quasi-delay-
insensitive) circuits. What we develop in this paper are basic results that allow designers to reason
about, and thus synthesize, non-speed-independent or timed circuits. Whether designing timed
asynchronous circuits is a good idea can be debated ad infinitum. In any event, designers have
been applying "seat of the pants" techniques to design timed circuits for years. Our work can be
used to verify such designs. Our vision, however, is much more broad, and includes a complete
synthesis methodology for developing robust and high-performance timed designs. A description
of such a methodology is beyond the scope of this paper but is a major motivation to addressing
this difficult timing analysis problem.
An asynchronous circuit is specified using CSP as a set of concurrent processes. This description
is transformed into a safe Petri net which is the input to the timing analysis algorithm. The analysis
determines the extreme case separation in time between two communication actions in the CSP
specification over all timed executions. Determining tight bounds on separation times between
communication actions (system events) provides information which can be used to answer many
different temporal questions. For example, we may wish to know bounds on the cycle period of an
asynchronous component so we can use it to drive the clock signal of a synchronous component.
Similar information can be used to generate worst-case and amortized performance bounds. We
may also perform minimum separation analyses in order to determine if it is feasible to remove
circuitry from a speed-independent implementation [16]. Our algorithm performs these sorts of
analyses and is useful in many contexts and at many levels of abstraction. Separation analyses at
the high-level can be used to help a designer choose among potential designs to perform a given
computation. At a lower level they can be used to determine the correctness of the implementation,
e.g., whether isochronic fork assumptions are valid [12].
Related work in timing analysis and verification of concurrent systems comes from a variety of
different research communities including: real-time systems, VLSI CAD, and operations research.
Timed automata [1] is one of the more powerful models for which automated verification methods
exists. A timed automaton has a number of clocks (timers) whose values can be used in guards of
the transitions of the automaton. Such models have been extensively studied and several algorithms
exist for determining timing properties for timed automata [8, 9]. As in the untimed case, timed
automata suffer from the state explosion problem when constructing the cross product of component
specifications. Furthermore, the verification time is proportional to the product of the maximum
value of the clocks and also proportional to the number of permutations of the clocks.
To improve the run-time complexity, Burch [7] extends trace theory with discrete time but still
uses automata-based methods for verification. This approach also suffers from exponential runtime
in the size of the delay values but avoids the factorial associated with the permutations of the
clocks. Orbits [19] uses convex regions to represent sets of timed states and thus avoids the explicit
enumeration of each individual discrete timed state. Orbits is based on a Petri net model augmented
with timing information. Other Petri net based approaches include Timed Petri nets [18] and Time
Petri nets [3]. In Timed Petri nets a fixed delay is associated with each transitions while Time
Petri nets use a more general model with delay ranges associated with the transitions.
This paper is composed of seven sections. We follow this introduction with a description of
the CSP specification language and its translation to Petri nets. Timed and untimed execution
semantics of Petri nets are introduced in Section 3. The algorithm for performing timing analysis on
Petri nets is describe in Section 4 and 5. Section 6 presents a parameterizable example which is used
to benchmark the performance of the algorithm. Finally, Section 7 summarizes the contributions
of this paper.
Specification
We now describe the specification language and show how to translate a specification into an
intermediate form that is more suitable for timing analysis.
2.1 CSP Programs
We specify computations using CSP (Martin style [14]). To simplify the timing analysis, we restrict
the expressive power of the specification language. First, we exclude disjunctions in the guards
because they correspond to OR-causality, which is known to be difficult [11, 15]. Second, we
require the semantic property that during all untimed executions, either choice between guards
is completely free (all the guards are identically true), or at most one guard evaluates to true.
As we shall see in Section 3.2, this allows the use of all untimed executions in determining the
possible timed behaviors, which is an important simplification to the timing analysis problem.
These restrictions still allow the analysis of a large and interesting class of CSP programs, including
many programs specifying implementations and abstractions of asynchronous control circuits. The
syntax for a restricted CSP program P is shown in Table 1. Figure 1(a) shows a simple CSP
program with three processes.

Table

1: Syntax for the restricted CSP. P is a program, S a statement, C a communication
action, E an expression, B a guard, and T a term. The terminal
symbols x and X represent a variable identifier and a communication
channel, respectively.
2.2 Petri Nets
The CSP specification is translated into a safe Petri net which is the direct input for the timing
analysis. A net N is a tuple (S; are finite, disjoint, nonempty sets of
respectively places and transitions, and F ' (S \Theta T ) [ (T \Theta S) is a flow relation. A Petri net \Sigma
is a pair (N; M 0 ), where N is a net and is the initial marking. See [17] for further
details on the Petri net model. Graphically, a Petri net is represented as a bipartite graph whose
nodes are S and T and whose edges represent the flow relation F . Circles represent places and
straight lines represent transitions. The initial marking is shown with dots (tokens). Figure 1(b)
shows a simple Petri net. For an element x the preset and postset of x are defined as
fy fy
A marking represents the global state of the system. A transition t is enabled at a marking M
if each input place of t is marked, i.e., 8s Firing the enabled transition t at M
produces a new marking M 0 constructed by removing a token from each of the places in the preset
of t and adding a token to each of the places in the postset of t. The transformation of M into
firing t is denoted by M [tiM 0 . We let [Mi denote the set of markings reachable from the
marking M .
2.3 Translation of CSP into Petri Nets
The CSP specification is translated into a safe Petri net. Petri net transitions are used to model
communication synchronizations and places are used to model control choice. The Petri net can be
constructed by syntax directed translation [4]. The mapping amounts to introducing a single token
corresponding to the program counter in each communicating process. A variable x is modeled
by two places, x 0 and x 1 . If x is true, x 1 is marked, otherwise x 0 is marked. After constructing
nets for each process, transitions are combined corresponding to matching communication actions.

Figure

1 shows a simple CSP specification and the corresponding Petri net.
(a)
a
d
c e
f
(b)

Figure

1: (a) CSP specification and (b) the corresponding Petri net \Sigma.
There are two complications in the translation. One is how to consistently label Petri net transitions
corresponding to communication actions that occur different numbers of times in connected
processes. This labeling problem is illustrated in its simplest form by the following CSP program
composed of a divide by two counter connected to a trivial environment:
The X communication in P 1 has to connect up to two X communications in P 2 . We solve the
labeling problem by introducing a separate label for each possible pairing of communication actions
[4]. In the example, we introduce two labels, X (0) and X (1) , and a choice for each of the
possible communications, obtaining the nets shown in Figure 2.
Y

Figure

2: Petri nets for the individual processes in the divide by two counter.
The second complication is the translation of the probe construct, X. If the probed communication
action X is not completed immediately, we split it in two, '
. The first half implements
the guard of the selection statement, and the second half implements the actual communication
action. Figure 3 illustrates this translation.
2.4 Properties of Petri Net
The Petri net obtained from a CSP specification has the following properties:
A
A

Figure

3: The Petri net for the incomplete CSP program
ffl The Petri net is safe, i.e., there is never more than one token at a place:
be a choice place, i.e., jsfflj ? 1. Then s is either extended free choice or
unique choice. The place s is extended free choice if
The place s is unique choice if at most one of the successor transitions ever becomes enabled.
denote the number of transitions in sffl that are enabled at the marking M . A
place s is unique choice if 8M 2 [M 1. The place s 2 in the net in Figure 1(b)
3 Execution Semantics
To represent the set of all (untimed) executions we introduce the notion of a process. Intuitively,
a process is an unfolding of a Petri net that represents one possible (finite) execution of the Petri
net. Processes are used to give timing semantics to a Petri net; for each process we define the set
of legal assignments of time stamps to the transitions of the process.
3.1
A process for the Petri net \Sigma is a net N and a labeling lab
(We subscript S, T , and F to distinguish between the nets of \Sigma and -.) The net N is acyclic and
without choice, i.e., without branched places. N and lab must satisfy appropriate properties such
that - can be interpreted as an execution of \Sigma [5, 21].

Figure

4 shows a process for the Petri net in Figure 1(b). The only true choice in the net is
at the place s 2 where there is a non-deterministic selection of either transition c or d. The process
represents the execution where the first time transition c fires and the next time transition d fires.
We denote all (untimed) executions of a Petri net \Sigma by the set
is a process of \Sigmag :
A safe Petri net has only a finite number of reachable markings. Processes have the property that
any cut of places corresponds to a reachable marking of \Sigma [5, Lemma 2.7]. Therefore, sufficiently
long processes will contain repeated segments of processes. We represent the potentially infinite
e
a
c
f
a
d

Figure

4: A process - for the Petri net \Sigma in Figure 1(b). The places and transitions
in the process have been labeled (using the lab function) with the names
of their corresponding places and transitions in \Sigma.
set of processes \Pi(\Sigma) by a finite graph we call the process automaton. The vertices of the process
automaton correspond to markings of \Sigma and the edges are annotated with segments of processes.
We let v 0 denote the vertex corresponding to the initial marking M 0 . Consider a path p in a process
automaton from vertex u to v, denoted u p
v. Then -(p) is the process obtained by concatenating
the process segments annotated on the edges of p. The process automaton has the property that
pref (-(p))
v is a path in the process automaton
where pref (-) is the set of prefixes (defined on partial orders [21]) of a process -. We can construct
the process automaton without first constructing the reachability graph [6, 10]. If there is no
concurrency in the net, the size of the process automaton is equal to the size of the reachability
graph. However, if there is a high degree of concurrency, the process automaton will be considerably
smaller. Figure 5 shows the process automaton and the associated processes for the Petri net in

Figure

1(b). The process in Figure 4 is constructed from
a
f
d
e

Figure

5: To the left, the process automaton for the Petri net in Figure 1(b). The
three process segments annotated on the edges are shown to the right
(labeled with elements from S \Sigma [ T \Sigma ).
3.2 Timed Execution
To incorporate timing into the Petri net model, we associate delay bounds with each place in the
net. The lower delay bound, d(s) 2 R 6\Gamma , and the upper delay bound, D(s) 2 R 6\Gamma [f1g, where R 6\Gamma
is the set of non-negative real numbers, satisfy 0 - These delay bounds restrict the
possible executions of the Petri net. During a timed execution of the net, when a token is added
to a place s, the earliest it becomes available for a transition in sffl is later and the
latest is D(s) units later. A transition t must fire when there are available tokens at all places in
fflt unless the firing of the transition is disabled by firing another transition. The firing of t itself is
instantaneous.
More formally, a timing assignment for process - , is a function that maps transitions in a
process to time values,
Definition 3.1 Let \Sigma be a safe Petri net and let - be a process of \Sigma. We consider a cut c ' S -
of - and let T enabled ' T \Sigma be the set of transitions enabled at the corresponding marking, M c . For
a timing assignment, - , and a transition t 2 T enabled , the earliest and latest global firing time of t
is given by
and
starttime(b)
denotes the set of elements of S - which are mapped to s by lab. Note that c "
lab \Gamma1 (fflt) is non-empty because t is enabled at marking M c . The function starttime takes a place
returns the time when a token entered the place lab(b), i.e., -(e) if . If there
is no such transition e, we set starttime(b) to 0. The timing assignment - is consistent at cut c if:
and
A timing assignment - of a process is consistent if it is consistent at all place cuts c of the
process. Let \Pi timed (\Sigma) be the set of all timed executions of \Sigma:
timed
\Pi(\Sigma) and there exists a consistent timing assignment for -
The restrictions on the CSP specification in Section 2 were crafted such that the set of untimed
and timed processes of the underlying Petri net are equivalent. This allows us to use the process
automaton to enumerate the possible processes without referring to timing information, and then
perform timing analysis on each process individually. To prove this, we need two lemmas. The first
states that it is always possible to find a timing assignment satisfying (1) in Definition 3.1. The
second lemma states a simple structural property of extended free choice places.
Lemma 3.2 Let \Sigma be a safe Petri net. For any t 2 T \Sigma , earliest(t) - latest(t) for any process of \Sigma
and for any timing assignment (not necessarily consistent).
Proof: From the definition of earliest and latest and the fact that for all place s,
Lemma 3.3 Let \Sigma be a Petri net and let s 2 S \Sigma be an extended free choice place. Then 8t
Proof: By contradiction: assume fflt 1 6= fflt 2 . Then there is a place s 0 in
Assume without loss of generality that s 0 is in fflt 1 and not in fflt 2 . From the definition of s being
an extended free choice place, it follows that ffl. By the premise of the lemma, t 2 is in sffl,
and thus also in s 0 ffl. A simple fact about pre- and post-sets is that if y 2 xffl then x 2 ffly. As t 2 is
in s 0 ffl, s 0 is in fflt 2 , contradicting the assumption. 2
Theorem 3.4 Let \Sigma be a safe Petri net where choice is either extended free choice or unique
choice. Then \Pi timed
Proof: Clearly, \Pi timed (\Sigma) ' \Pi(\Sigma). We show that \Pi(\Sigma) ' \Pi timed (\Sigma), i.e., there exists a consistent
timing assignment for all - 2 \Pi(\Sigma).
We will prove that for all cuts c of - and any b 2 c, constraint (2) is subsumed by constraint (1).
From Lemma 3.2 it follows that for any process there exists a consistent timing assignment.
Observe that lab(bffl) ' lab(b)ffl, and thus if lab(bffl) " T enabled is non-empty then so is lab(b)ffl "
enabled .
Let c ' S - be a cut of - and let b be a place in c. If and (2) is
trivially satisfied. For bffl 6= ;, let e be the one element in bffl (all places b in a process has jbfflj - 1)
and let s be the place in \Sigma corresponding to b, i.e., lab(b). The observation above then states
that lab(e) 2 enabled . Consider two cases:
lab(e) is the only element in sffl " T enabled and (2) to reduces to -(e) - latest(lab(e)).
1: The choice place s is either extended free choice or unique choice:
s is extended free choice: From Lemma 3.3 we have that
from the definition of latest , it follows that 8t As
minimization is idempotent and lab(e) 2 reduces to -(e) -
latest(lab(e)).
s is unique choice: From the definition of unique choice, thus lab(e) is
the only element in sffl " T enabled . Condition (2) again reduces to -(e) - latest(lab(e)).4 Timing Analysis
Having formally defined the timing semantics of the Petri net, we now state the timing analysis
problem and present an algorithm for solving this problem.
4.1 Problem Formulation
Given two transitions from a Petri net \Sigma, t from ; t to 2 T \Sigma , we wish to determine the extreme-case
separation in time between related firings of t from and t to . We let b
\Pi be a set of triples
dst i, where - 2 \Pi(\Sigma) and t src ; t dst are transitions in the process - with lab(t src
lab(t dst to . The set b
\Pi is used to describe all the possible processes where the distinguished
transitions t src and t dst have the appropriate relationship. The timing analysis we perform is: for
all b
\Pi and for all consistent timing assignments - for -, determine the largest ffi and smallest \Delta
such that
The transitions t src and t dst must be related in order for the timing analysis to yield interesting
information. Consider finding the maximum time between consecutive firings of transition a in

Figure

1(b), corresponding to the maximum cycle time of a transition. For this separation t from
and t to are both a. The occurrences of a, the t src and t dst transitions, must be restricted such that
all the elements of b
\Pi have the property that no other transition t between t src and t dst has label
a. For example, one of the elements in b
\Pi is the process in Figure 4 with t src and t dst being the
left-most and right-most transitions labeled with a, respectively.
The relationship between t src and t dst is defined by backward relative indexing by specifying
two numbers fi and fl, and a reference transition, t ref 2 T \Sigma . For a particular -, we find the
corresponding transitions t src and t dst by the following procedure: start at the end of the process
and move backwards looking for a transition t such that When found, we continue
moving backwards, looking for the fith transition t (starting with this is
t src . Simultaneously, we find the flth transition having to ; this is t dst . When both are
found, we include h-; t src ; t dst i in b
\Pi.
The specification of a separation analysis on the Petri net \Sigma thus consists of three transitions,
t from , t to , and t ref , all in T \Sigma , and two constants fi; fl 2 N. We call fi and fl occurrence indices
relative to the transition t ref . We let
\Pi(\Sigma; t from ; fi; t to ; fl; t ref )
denote the set of triples h-; t src ; t dst i where - 2 \Pi(\Sigma) and t src and t dst have the relation described
above.
One communication action in the CSP program may map to many transitions in \Sigma and these
transitions are to be considered equivalent when performing the timing analysis. Instead of specifying
the separation between individual transitions, we specify it between sets of transitions, i.e.,
a separation analysis is specified by two occurrence indices fi and fl, and three sets of transitions
from \Sigma: From, To, and Ref . Our final formulation is:
It is straightforward, given the communication actions, to determine what transitions should
be included in these sets. Sometimes we may also want to consider several CSP communication
actions as equivalent with respect to the separation analysis (we will see an example of this in
Section 6). This can conveniently be achieved by adding the corresponding Petri net transitions to
the appropriate From , To, and Ref sets.
In the sequel, we will only discuss the maximum separation analysis, i.e., find \Delta, because the
separation ffi can be found from a maximum separation analysis of -(t src dst
This is accomplished by computing b
\Pi using reversed r-oles for From and To, and fi and fl: b
4.2 The CTSE Algorithm
Let \Delta( b
-) be the maximum separation between t src and t dst for some particular execution b -:
\Delta( b
is a consistent timing assignment for
The maximum separation over all executions is then given by
We now show how the elements of b
\Pi are constructed to obtain \Delta, and Section 5 describes the
algorithm for computing \Delta( b
-).
The process automaton represents all possible executions. However, whatever topologically
dst in a process cannot influence the maximum separation between these two
transitions. Any portion of a process following t src and t dst can therefore be ignored and all processes
in b
\Pi will end with some terminal process segment that includes the two transitions t src and t dst .
Let -(p) be a process containing t src and t dst for some path p in the process automaton (starting at
We decompose this process into -(p 0 )- T , where p 0 is a path in the process automaton and - T is
the minimal process segment containing t src and t dst . The process segment - T is called a terminal
segment. We let \Pi T (u) be the finite set of process segments such that for any path v 0
; u in the
process automaton and - T 2 \Pi T (u), the process -(p)- T is in b
\Pi.

Figure

6 shows the two terminal
process segments belonging to \Pi T (v 0 ) for the a-to-a separation analysis in our example. For this
example, all processes in b
\Pi can be constructed by -(p)- T , where v 0
e
a
c
a
f
a
d
a

Figure

Two terminal processes (labeled using lab) for the separation analysis
from a to the next a transition in the Petri net in Figure 1(b).
An algorithm for computing \Delta( b -) can be phrased in algebraic terms. For each segment of a
process, there is a corresponding element in the algebra. We use [-] to denote this element for the
process segment -. The algebra allows us to reuse analysis of shorter processes when computing
\Delta( b -) because the operators of the algebra are associative (the details are shown in the next section).
There are two operations in the algebra: "choice", j, and "concatenation", fi.
Our approach to analyzing the infinite set b
\Pi is to enumerate the processes b
- of increasing length
by unfolding the process automaton using a breadth-first traversal. We traverse the automaton
backwards, starting with the terminal segments. An element of the algebra is stored at each node
v in the process automaton. Let [v] k denote the algebraic element stored at node v in the process
automaton after the k th iteration. Initially, [v]
(v)g.
When traversing the process automaton backwards, the elements of the algebra are composed
(using fi) for two paths in series, and combined (using j ) for two paths in parallel. The choice-
operator combines backward paths when they reach the same marking in the process automaton.
This is illustrated below by showing a backward traversal with reconvergence corresponding to the
process automaton in Figure 5 and the two terminal processes in Figure 6:
For this example, [v 0
Whenever the node v 0 is reached in the k th unfolding, [v 0 represents the maximum separation for
all executions represented by that unfolding, denoted \Delta k . This value is maximized with the values
for the previous unfoldings, \Delta kg. From (3) it follows that \Delta -k is a lower
bound on \Delta and that
For a given node v in the process automaton, we can compute an upper bound on all further
unfoldings; this bound is denoted [v] ?k . Let c be a vertex cut of the process automaton. An upper
bound on \Delta for the k th unfolding is \Delta cg. When \Delta ?k is less than or equal to
\Delta -k for some k we can stop further unfolding and report the exact maximum separation
It is possible that the upper and lower bounds do not converge in which case the bounds may still
provide useful information as \Delta is in the range The main loop of the CTSE algorithm
is shown in Figure 7.
Algorithm: CTSE(G)
For each
(v)g at v;
do f
unfold once(G);
until
return

Figure

7: The CTSE algorithm computing \Delta given a process automaton G.
The run-time of the algorithm depends on the size of the representation of the algebraic elements.
The size of an element may be as large as the number of paths between the two nodes related by the
element, i.e., exponential in the number of iterations, k. In practice, pruning drastically reduces
the element size.
Computing \Delta( b
This section describes the algebra used in the CTSE algorithm. This algebra is used to reformulate
an algorithm by McMillan and Dill [15] for determining the maximum separation of two events in
an acyclic graph.
5.1 Algebras
Before presenting the algorithm for computing \Delta( b -) we introduce two algebras. The first is the
(min; +)-algebra (R [ f1g; \Phi 0
The elements 1 and 0 are the identity elements for \Phi 0
The second algebra is denoted by
Each element in F is a function represented
by a set of pairs. The singleton set, fhl; uig, where u is a row-vector of length n, represents the
where m is a column-vector of length n
and\Omega 0 denotes the inner product in the (min; +)-algebra.
In general, the set fhl represents the function
We associate two binary operators with functions: function maximization, f \Phi g, and function
composition,
f\Omega g. It follows from (4) that function maximization is defined as set union: f \Phi
g. Function composition,
g\Omega h, is defined as f(x; m) = h(g(x; m); m). Notice that we use
left-to-right function composition. For
m) and
Function
composition,\Omega , distributes over function maximization, \Phi. The elements are the
identity elements for function maximization and composition, respectively.
be two pairs in the representation of a function. We can
remove since then for all x and m, min(x
m)
m). Proper application of this observation that can greatly simplify the
representation of a function.
5.2 The Acyclic Time Separation of Events Algorithm
We can now present the algebraic formulation of McMillan and Dill's algorithm for computing
\Delta( b -). For each place and transition in - we compute a pair [f; m] where f 2 F and m 2 R[f1g.
The algorithm is shown in Figure 8.
Informally, this algorithm works as follows: To maximize the value of -(t dst we need to
find a timing assignment that maximizes -(t dst ) and minimizes -(t src ). The first element of [f
represents the longest path (using D(s)) from a transition to t dst and the second element represents
the shortest path (using \Gammad(s)) to t src . The algebra for the f 0 -part is complicated by the fact that
the delay for a given place can not be assigned both d(s) and D(s). The f 0 -part must represent the
longest path respecting the delays assigned by the shortest path computation. For details see [13].
To find the maximum separation represented by a [f; m] pair, we evaluate f at m and 0, computing
the sum of the longest and shortest paths. To compute \Delta( b
-), we maximize over all [f; m] pairs at
the initial marking:
\Delta( b
is the pair at s 2 ffl-g ;
where ffl- denotes the set fs similarly, -ffl denotes the set fs 2 S - j ;g.
5.3 Decomposition
The algebraic formulation allows for a decomposition of the above computation using matrices.
Consider a process segment - having We represent the computation of the
algorithm on - by two n \Theta m matrices, F and M. Given a vector of m-values at -ffl, m, we can
Algorithm: \Delta(b-)
For each element of - in backward topological order:
For a place s, compute the pair [f
ae 0 if
(m)ig\Omega f where [f; m] is the pair stored at
ae
is the pair stored at
For a transition t, compute the pair [f
ae
dst
\Phiff at place s j s 2 tfflg otherwise
ae
\Phi 0 fm at place s j s 2 tfflg otherwise

Figure

8: The algorithm for computing \Delta(b-).
find the vector m-values at ffl-, m 0 , from the (\Phi 0
m. This is
illustrated using the process segment - 1 from Figure 5, shown in Figure 9. We associate the delay
range [1; 2] to each place, i.e., places s. We compute expressions for
refers to the m-value computed for
element x in the process. In backwards topological order of - 1 we compute:
\Gamma1\Omega 0 m(s 5 ) from substitution
substitution
as\Omega 0 distributes over \Phi 0 and is associative
We can represent this computation in matrix form using (\Phi 0

Figure

9: Process segment - 1 from Figure 5.
A similar matrix is constructed for the f-part. For the process segment - 1 the computation is:
)ig\Omega f(s 5 ) from substitution
substitution
from substitution
)ig\Omega fh2; m(s 5
\Delta\Omega
distributes over \Phi
by definition
of\Omega
These expressions depend on the m-values at internal elements of - 1 , e.g., m(t 1 ) in the expression
for f(s 0 ). The m-value for these nodes can be computed as a linear expression in the m-values at
the places in -ffl. This linear expression is encoded by a vector u of length j-fflj. The vector
product
computes the m-value for the internal node where u is stored. E.g., the expression
used in f(s 0 ) is represented by a the vector:
We express the f-computation in matrix form using
Given a process segment -, we denote the corresponding function and m-value matrices by F(-)
and M(-). The algebraic element [-] is then defined as the singleton set f[F(-); M(-)]g. We can
now define the two operators fi and j. The choice operator is defined as set union:
The composition operator is more complex. When composing two segments - 1 and - 2 , the functions
in - 1 need to refer to the m-values in - 2 ffl rather than those at - 1 ffl. We shift the functions in
to make them refer to m-values in - 2 ffl by multiplying the u-vectors in F(- 1 ) with M(- 2 ). For a
singleton function fhl; uig, we obtain the function fhl;
)ig. Non-singleton functions are
shifted by shifting each pair, and a matrix of functions is shifted elementwise. We use the notation
F -M to denote a shift of matrix F by matrix M. For singleton sets the composition operator is
defined as:
\Theta

Non-singleton sets are multiplied out by applying the distributive law.
5.4 Pruning
Consider the element f[F ]g. We can removed [F from the set if we can show
that for any pairs composed to the left and right such that the result is a scalar, this scalar is no
greater than the same composition with the [F sufficient condition for eliminating
is the following: Let
i.e., k is the largest difference between elements in M 2 and M 1 , or 0 if this difference is negative.
The
where 1 is a row-vector of appropriate length with all entries set to 1. This condition is used to
eliminate entire execution paths from further analysis, and is central to obtaining an efficient algo-
rithm. More sophisticated conditions, that use more information about the particular computation,
are possible and may further increase the efficiency of the algorithm.
5.5 Upper Bound Computation
We now consider how to determine an upper bound [v] ?k for node, v, in the process automaton. To
determine a non-trivial upper bound, all further backward paths from v to v 0 have to be considered,
i.e., we need to bound the infinite set of algebraic elements constructed from backward paths:
oe
For any simple path p we just compute [-(p)]. If p is not simple, we write p as
3 is a simple path, p 2 is a simple cycle, and p 1 is finite, but may contain cycles. We introduce an
upper bound operator, r, with the property that
1. Thus, the expression on the right-hand side is an upper
bound on the left-hand side expression. The r operator is recursively applied to the path
until this is a simple path. Hence, we can bound the infinite set in (5) by a finite set of algebraic
elements constructed from all paths consisting of a simple cycle followed by a simple path ending
at v.
The r operator is defined as follows: Assume F is a m+ k \Theta n + k matrix of the form
0m
where 0 i is a vector of lenght i containing 0 and I k is the identity matrix of size k. The operator
r[F; M] is defined as
hi
z m is a vector of length m containing the function z = fh1; 1ig. The function z is a largest
element of F , i.e., z - f for all functions f 2 F . The effect of the r operator is to apply the
function z to the part of the F matrix which is not the identity.
The upper bound is determined individually for each pair in the set for node v. If the upper
bound for a given [F; M] pair is less than or equal to the present global lower bound, \Delta -k , that
pair can be removed from the set, further pruning the backward execution paths that must be
considered.
The order in which [F; M] pairs are multiplied greatly affects the run-time of the algorithm. For
example, consider precomputing for each node in the process automaton the algebraic expression
for the upper bound, i.e., for each node, compute the algebraic element for the set of simple paths
followed by simple cycles (going backwards). Because we don't know what is to be composed with
these elements, few pairs can be pruned from the representation. Therefore it may be more efficient
to multiply the pairs out in each iteration, even though this doesn't allow the reuse of work from
previous iterations. Our experience has been that upper bound expressions become very large when
precomputed and we are better off recomputing them at each iteration because effective pruning
takes place. We only precompute the r of the simple cycles. This observation was key to achieving
polynomial run-time for the example described in the following section.
6 Benchmark Example: The Eager Stack
Replicating a single process in a linear array provides an efficient implementation of a last-in, first-out
memory which we refer to as an eager stack. The eager stack contains an interesting mixture
of choice and concurrency and represents an excellent parameterizable example for explaining analyses
that can be performed by our algorithm, and also benchmarking our implementation of the
algorithm.
6.1 The Eager Stack
A stack capable of storing n elements is constructed from n equivalent processes, arranged in a
linear array. Each process has four ports, In, Out , Put , and Get . The ports Put and Get connect
to the ports In and Out, respectively, in the stage to the right. Figure 10 shows a block diagram
Put
Get
Environment 3-stage eager stack
In
Out
Put
Get
In
Out
Put
Get
In
Out

Figure

10: Block diagram of the 3-stage eager stack.
The CSP specification of a single stage is:
In
The Boolean variables b and rb are used to control communication with the adjacent right stage.
The value of b indicates whether this stage holds valid data. The value of rb is a mirror of the value
of b in the stage to the right. Concurrency occurs when a position must be created or a space must
be filled in.
The choice of whether to do a Put or Get is made in the environment and is potentially
propagated throughout the entire stack. In order to avoid an overflow or underflow condition, the
environment interacting with the stack must not attempt a Put if n elements are already stored in
the stack and it must not attempt a Get if the stack is empty. The following process represents a
suitable environment:
E(P ut; Get) j
This process is unfolded n times and the actual data (x) is eliminated for simplicity. For
get:
The construct is repeated if a guard command with a trailing   is chosen, and
is not repeated otherwise. The number in parenthesis refers to the number of items in the stack
at the time when the communication is performed, so after Put (2) the stack is full and only a Get
communication is possible 1 .
A nice property of this example is that the port names occur the same number of times and along
compatible choice paths in adjacent processes. Thus we can identify a (superscripted) number with
each occurrence of a port name in the program. We use Petri net transition P i for communications
on the Put port in stage i and In port in stage i + 1. Similarly, G i denotes a communications on
the Get port in stage i and on the Out port in stage Figure 10).
1 It is possible to have the stack indicate whether it is empty or full and make the environment behave accordingly,
but this complicates each stage of the stack.
6.2 Timing Analysis
There are numerous interesting time separation analysis we can perform on the eager stacks. We
can determine the minimum and maximum separations between consecutive Put communications
in the environment process. The maximum separation analysis for a 3-stage stack would correspond
to:
If we set the delay between communication actions to be the range [1; 2], we get the maximum
separation This is obtained by filling an empty stack (three Put operations) and then
emptying it again (three Get operation), finally inserting one element (a Put operation). The
maximum separation is achieved between the third and the fourth Put operation. For the minimum
separation, we exchange the sets To and From and negate the result, in this case
A possibly more interesting analysis might be the minimum and maximum separations between
consecutive Put or Get communications. This corresponds to the minimum and maximum response
time of the stack, or equivalently, the minimum and maximum cycle period of the environment.
We must include all Petri net transitions corresponding to Put and Get communications in the
environment. Thus
The results, again for [1; 2] delay ranges between communication actions, are
For fixed delay values, the eager stack has constant response time, i.e., the time between the
environment performs either a Put or a Get operation until the next such operation is independent
of the size of the stack, n. This is not the case when we introduce uncertainty in the delay values.
The maximum response time turns out to be n linear in the stack size. However, if we
look at the maximum response time amortized over m Put or Get communication actions we get
the following maximum separations \Delta:
Dividing \Delta by m, we obtain the amortized separations shown below:
\Delta=m 6 5 4.66 4.5 4.4 4.33 4.29
We can predict that for 4. So although the maximum separation between
two consecutive operations increases linearly with n, if we amortize over a number of operations,
the response time converges to 4. In fact, the maximum response time converges to 4 independently
of n. In this sense, the eager stack has constant response time even when the delays are uncertain.
6.3 Run Time
Execution times of the CTSE algorithm on eager stacks of various sizes, n, are shown in Table 2 using
[1; 2] for all delay ranges. The size of the specification, i.e., number of places, number of transitions,
and the size of the flow relation, is given n the table by jS \Sigma j, jT \Sigma j, and jF \Sigma j, respectively. The
number of nodes in the reachability graph is shown in the jR:G:j column. Note that the reachability
graph is not constructed when performing the timing analysis and is only reported to give an idea
of the complexity of the nets. The separation analysis denoted by \Delta 1 is the maximum separation
between consecutive Put operations and \Delta 2 is the maximum separation between consecutive Put
or Get operations. The CPU times were obtained on a Sparc 10 with 256 MB of memory.
.3
4
43 176 268 2.4 2.3
28 1220 813
36 2000 1333 5366

Table

2: Run times of the CTSE algorithm on eager stack of various sizes.

Figure

11 shows the CPU times for the two separation analysis plotted as a function the size
of the Petri net.
Orbits [19] is, to the authors knowledge, the most developed and efficient tool for answering
temporal questions about Petri nets specifications. Orbits constructs the timed reachability graph,
i.e., the states reachable given the timing information. It should be noted that Orbits is capable
of analyzing a larger class of Petri net specifications than the one described here. Partial order
techniques are also used in Orbits to reduce the state space explosion [20]. However, the time to
construct the timed reachability graph for the eager stack increases exponentially with the size n.
For 6 the time is 234 CPU seconds on a Decstation 5000 with 256 MB, i.e., two orders of
magnitude slower than the CTSE algorithm. For Orbits ran out of memory.
7 Conclusion
We have described an algorithm for solving an important time separation problem on a class of
Petri nets that contains both choice and concurrency. In practice, our algorithm is able to analyze
nets of considerable size, demonstrated by an example whose Petri net specification consists of
more than 3000 nodes and 10 reachable states. While we report a polynomial run-time result for
only a single parameterizable example, we expect similar results for other specifications exhibiting
limited choice and abundant concurrency.

Acknowledgments

We thank Chris Myers of Stanford University for many fruitful discussions as well as supplying
the Orbits runtimes. This work is supported by an NSF YI Award (MIP-9257987) and by the
110010000
Petri net size, jF \Sigma j

Figure

11: Double logarithmic plot of CPU time for the two separation analyses as
a function of the Petri net size, jF \Sigma j.
DARPA/CSTO Microsystems Program under an ONR monitored contract (N00014-91-J-4041).



--R

The theory of timed automata.
Synchronization and Linearity.
Modeling and verification of time dependent systems using time Petri nets.
Its relation to nets and to CSP.
Partial order behavior and structure of Petri nets.
Interleaving and partial orders in concurrency: A formal comparison.
Trace Algebra for Automatic Verification of Real-Time Concurrent Systems
Minimum and maximum delay problems in real-time systems
Computer Aided Verification
Using partial orders to improve automatic verification methods.
Timing analysis of digital circuits and the theory of min-max functions
Practical applications of an efficient time separation of events algorithm.
An algorithm for exact bounds on the time separation of events in concurrent systems.
Programming in VLSI: From communicating processes to delay-insensitive circuits
Algorithms for interface timing verification.
Synthesis of timed asynchronous circuits.
Petri Net Theory and The Modeling of Systems.
Performance evaluation of asynchronous concurrent systems using Petri nets.

Automatic verification of timed circuits.
Modular Construction and Partial Order Semantics of Petri Nets.
--TR

--CTR
Ken Stevens , Shai Rotem , Steven M. Burns , Jordi Cortadella , Ran Ginosar , Michael Kishinevsky , Marly Roncken, CAD directions for high performance asynchronous circuits, Proceedings of the 36th ACM/IEEE conference on Design automation, p.116-121, June 21-25, 1999, New Orleans, Louisiana, United States
asynchronous systems;concurrent systems;time separation of events;timing analysis;abstract algebra