Toward Automated Abstraction for
Branching Networks
Michael Jones, Ganesh Gopalakrishnan
School of Computing, University of Utah
mjones, ganesh@ cs. utah. edu
Protocols on
Abstract- We have used various manual abstraction tech-niques
to formally verify a transaction ordering property for
an IO protocol over bus/ bridge networks. In the context
of network protocol verification, an abstraction is needed
to reduce the unbounded number of network configurations
to a small number of representative networks that can be
checked using algorithmic methods. The manually derived
abstraction was both brittle and difficult to validate. In this
report, we discuss the need for abstraction techniques in the
formal verification of protocols over networks and present
our recent efforts to create an automatic abstraction tech-nique
for network protocols using predicate abstraction as
a starting point.
Keywords- Formal verification methods, parameterized
systems, predicate abstraction
We address the problem of abstraction in the formal veri-fication
of safety properties at the bus/ bridge level for pro-tocols
defined over acyclic branching networks. Abstrac-tion
is needed in this context because formal methods ap-plied
directly to protocols over networks are either not ap-plicable,
or at best difficult and time- consuming. The main
source of difficulty is the unbounded nature of branching
networks. Because there are an unbounded number of con-figurations
that must be checked, tt is not possible to apply
algorithmic methods, such as model checking, to all pos-sible
network configurations. We have found [ MHJGOO]
that it is prohibitively difficult to apply interactive theorem
proving in the context of protocols on branching networks.
In this report, we discuss our recent efforts to increase the
amount of automation available for creating and reasoning
about abstractions of protocols defined over branching net-works.
The problem with manually derived abstractions is
that they need to be validated. Validating an abstraction
is the process of showing which properties are preserved by
the abstract model. We have found [ JGOO] that building
a validation proof for a manually derived abstraction for
protocols over networks is also difficult.
The significance of this work is that it will provide a tech-nique
for creating abstractions of protocols over branching
networks such that certain properties of the protocol can be
checked with minimal manual effort. The novel feature of
this work is a predicate abstraction technique suitable for
use on protocols which are defined over networks in which
the states and connectivity of intermediate nodes affect the
property being checked.
We begin by reviewing relevant results from predicate ab-straction
and parameterized system verification. Section I1
contains a detailed presentation of the abstraction scheme.
The formal presentation in section I1 is closely patterned
after the presentation in [ GS97]. Section 111 gives an ex-ample,
and we close with our thoughts on abstractions for
networks in the final section.
I. RELATEDW ORK
The ideas presented here are an extension of predicate
abstraction as described in [ GS97]. Predicate abstraction is
a form of abstraction in which the reduction is constructed
manually but the validation and checking tasks are auto-mated.
To create a predicate abstraction, the user specifies
a set of predicates which are used to divide the abstract
state space depending on the truth , or falsity, of the pred-icates.
Given the predicates, an abstract transition relation
is constructed such that the original infinite state model is
a refinement of the abstract finite state model. In practice,
predicate abstraction requires several rounds of verification
in which the user adds invariants to eliminate false nega-tives
between rounds. The PVS theorem prover contains
support for predicate abstraction and invariant strength-ening
[ SS99]. Predicate abstraction has been applied to
limited forms of networks [ LS97] in which the particular
shape of the network is unimportant to the property be-ing
verified. A form of predicate abstraction using BDDs
to represent sets of reachable states has been implemented
using the Murd, model checker [ DDP99]. It is difficult to
apply predicate abstraction to parameterized systems due
to the quantification required to describe arrays of pro-cesses.
Quantification makes predicate abstraction difficult
because determining if a transition is enabled for a state
description containing quantification is either undecidable
or requires a complex decision procedure. We address the
quantification problem by introducing a second variable for
each predicate that encodes whether or not a node exists
in the array that satisfies the predicate.
The proposed abstraction scheme applies to branching
parameterized systems. While the verification problem for
parameterized systems is in general undecidable [. 4K86],
methods for reasoning about limited classes of protocols
and properties have been developed. Other methods for
reasoning about parameterized systems are based on reg-ular
expressions [ KMM+ 97], [ SG89], [ CGJ95], rather than
abstract state variables. While regular expression based
techniques have found success primarily in linear or ring
shaped topologies ( see [ BJNTOO], [ PSOO] for recent results),
the early papers consider extensions to include reasoning
about branching topologies. Despite the ability of regu-lar
expression representations to describe and reason about
branching topologies, no results for complex protocols have
0- 7695- 0786- 7/$ 0100 .00 0 2000 IEEE
147
yet appeared in the literature. By using a different rep-resentation
and abstraction scheme over a limited class
of properties, we hope to derive an abstraction scheme
that can be applied to larger examples such as commer-cial
multi- bus IO protocols. The added restriction in our
work is that we consider only safety properties defined over
a constant number of terminal nodes rather than safety
properties in general.
11. PREDICATE ABSTRACTION FOR NETWORKS
The idea behind the abstraction scheme is project the
subnetwork containing the terminal nodes in the property
being checked then model the state of each network seg-ment
using a variant of predicate abstraction. The variant
of predicate abstraction uses an additional boolean vari-able
for each predicate to indicate whether or not a node
exists which satisfies the predicate represented by the state
variable. The additional existence variable is used to en-code
quantification which is required to model parameter-ized
systems using predicate abstraction. In the remainder
of this section we formally define the model of computa-tion
and abstraction scheme. The next section contains
an example of the abstraction scheme applied to a trivial
property on a simplified version of the PCI protocol
A network of processes is created by instantiating a pa-rameterized
finite state protocol pa at each node. - 4 routing
table defines the connectivity in the network.
Definztzon 1. Network of nodes. A network of nodes is a
six- tuple ( N, A, R, X , T, 13) where:
N = 1.. . n, a list of node indices.
A C N , a list of agent, or terminal, nodes.
R = {( Aa-, 4 ,, n 1, n2 . . . n,) l for agents A,, A, in A}, a
routing table in which agent A, is connected to agent
A, by the path through nodes n1 through 12%.
-‘ z = XI, X 2 .. . X,, the network state formed by tak-ing
the state of each node, X,.
T = Tl, T2 . . . Tn, the set of network transitions formed
by the transitions, T,, from p, at each node.
I, = I:, I; . . . I;, the jth initial network state formed
by taking the initial state of each node, I:.
The first three elements of a network, N, A, R, define the
global network structure. N and A define the interior and
exterior nodes of the network while R defines the connec-tions
between exterior nodes using paths of interior nodes.
The latter three elements, X , T, 13, define the state and
transition relation of the network in a per- process fashion.
Each of X , T, I3 are defined using the state, transitions and
initial state of each node. The state, transitions and ini-tial
state of each node are all parameterized definitions, as
given next.
Definztzon 2: Parameterized Protocol. A finite state pa-rameterized
protocol, p, is a triple ( X,, T,, I,) where
X , = xi : tl, xi : t 2 . . . xX : tk, a list of declarations in
which each variable xcj at node i has type t,.
T, = T;, ri . . . TL, a list of transitions for process I,
in which each 7;” has the form r; = g,( z, R, X) ct
asgn( i, R, X ) .
I,? = asgnXi, the jth initial state for process i in which
Both the guard and the assignment in each transition take
the routing table and network state as parameters. Includ-ing
the network state and routing tables as parameters al-lows
the guard and assignment to access the states of other
nodes. For example, the guard in transition rj can use the
state of an adjacent node to determine if 7; is enabled. Sim-ilarly,
the presence of the routing table and network work
state in the update expression allows the transition at a
node to modify the states of other nodes in the network.
Transitions need to modify the state of adjacent nodes if
the transition moves a message between two nodes.
We now define the semantics of a network of processes
over a state graph.
Definition 3: Parameterized State Graph. Given a net-work
of processes: and a routing table R, the parameterized
state graph, S“ is a three- tuple, ( QR, PR, IR) where
each variable in Xi is assigned a value.
. .
QR = x:, xi.. . xi, x :, X; . . . xi... xi, x i.. . X :
PR= u~=,( u~= lrf( qw) h ere
if g:( q, R , X ) = F
‘ f( q) = { las gn;( q, R, X ) otherwise
0 IR = { qlinit( q)}
In the definition of SR, QR is a graph node representing
a global network state, PR represents the transitions en-abled
for a graph node and IR is the set of initial states.
The entire state graph, S, for a protocol defined over a
network of processes is created by taking the union of all
state graphs over all routing tables. For networks with un-boundedly
large network topologies, S contains a finite but
unbounded number of states. Since the unboundedness of
S stems from the unbounded number of unique valid rout-ing
tables, the crux of the abstraction is creating a model
which contains a bounded number of network topologies
and using predicate abstraction to model the unbounded
number of states in each topology. Each topology has an
unbounded number of states because there may be an un-bounded
number of nodes in each edge of a given network
We now define the abstraction of a state graph given the
abstraction of a routing table. This part of the abstrac-tion
uses predicate abstraction to represent the unbounded
number of states in a topology. The abstraction of routing
tables will be discussed later. We begin with preliminary
definitions and results for predicate transformers.
Definition 4: Strongest Postcondition. For a parameter-ized
transition rr and a set of states characterized by a
predicate cp, the strongest postcondition of cp by rp is de-fined
as:
topology.
POSt[ 7inl( P) = 37’. rin( q‘, 4) A d 4 ’ )
Definition 5: Weakest Precondition. For a parameter-ized
transition r? and a set of states characterized by a
predicate cp, the weakest precondition of cp by 7: is defined
as:
Intuitively, post[ rF](( pi) s the smallest set of successors of cp
reachable by rp and jKG[ rp]( cp) is the largest set of states
F[ 7inI(( P) = Vq’. qYq, 9’) * ( P( 4’)
148
that map to cp by r,". As reported in [ GS97], we can rewrite
Eb3 ( 9) an d POSt[ T," I( cp) as
E[. r, nl( P) =
post[ CI( cp) * P'iff cp * E[ 7, nI( cp')
( g:( 4 =+ cF:[ wn:( n, R, Wl( n, R , X ) l)
Definztzon 6: Abstract State Graph. Given a state graph
SR = ( QR, U;. In) for a network of nodes and routing
table R with abstracted routing table RI ( as will be defined
later), let QZ' be a lattice of abstract states with 5' 2' =
( Q ~ ' , U ~ , I " a'n) d ( a : 2QR cs QZ', yQf' c) 2QR). T hen
Sf is an abstraction of SR iff
IR C y( If), and
Vn. Vi. VqA E QZ'.
Post[ T," l(?'( qA)) y(. fp, ath( n) ( q A ) )
R G y( R')
Intuitively, 5' 2' is an abstraction of SR if for every transi-tion
at every node in SR, the strongest postcondition of the
concrete states in ' y( qA) is a subset of the concrete states in
' y(, i, p" th'n'( qA)). In short, for every move T at every node
in SR, there is a move ? in Sz' that does as much or more
than 7.
Next we identify an abstraction scheme for SR. We con-sider
the abstract state lattice 0,"' in duced by the pred-icates
cp;, cp;, . . . cp: parameterized by each node n. For
each predicate in 9% a nd abstract path j in R' we define
two abstract state variables ai@:.
Given the set of
monomials over 19: and 8 for an abstract routing table
R' and glb operator A ( boolean conjunction) with lub op-erator
( weakened form of disjuction), the abstract state
lattice 6fR' is defined to be ( fi, A , U)
Each monomial in MR' represents a set of concrete states
described by a conjunction of quantified predicates as given
in Figure 1. As shown in the figure, an abstract mono-mial
represents the set of concrete states which contain
sequences of nodes that may contain a node that satisfies
a predicates ( P, depending on the values of i$ i and I9; in
the monomial.
We now define the abstract transition relations parame-terized
by paths using monomials over abstract state vari-ables.
For a given abstract state 7F1 we compute the ab-stract
transition ?," corresponding to transition 7," for some
n E IC using the equation shown in Figure 2. The equation
states that the next state of ?: ( fi) is F if ' y( 7jz) always fails
to satisfy the guard for transition r: for any n E k; but that +: ( m) includes any disjunction over a!@!, 8f-+!, ~ 8 f @ f
and - a!-@: for next states that may or may not have
nodes in path k that may or may not satisfy cp;. Note
that each ( y( 7E1) A 9:) + ~ cp,"[ asgn:( 3?)/ 3?] is simply the
quantifier free form of p o s t [ r ; ] ( y ( h ) ) + p,".
As mentioned before, the crux of the abstraction is re-ducing
the potentially unbounded number of routing tables
over an unbounded set of terminal and non- terminal nodes
to a bounded number of small abstract routing tables that
Definztzon 7: Abstract state lattice.
represent all possible network configurations. If we restrict
the set of invariants to safety properties over a constant
number of terminal nodes, then we can enumerate all pos-sible
( up to path length) acyclic configurations, R,, on
n terminal nodes. The class R, of networks corresponds
to the class of unique Steiner topologies over n terminals
where each terminal has degree one ( see [ HRS%' 92] for a dis-cussion
of Steiner topologies). This correspondence gives
an upper- bound on the number of unique acyclic network
configurations over n nodes.
Given a concrete routing table R, we construct a corre-sponding
abstract routing table R' by first labeling n of the
terminal nodes ( as required to check a property on n termi-nal
nodes). The abstract routing table R' is then created
by projecting only the n labeled nodes and the paths be-tween
them. The final step is to replace the nodes in each
unique path segment between the n labeled nodes with a
single path variable. An example of creating an abstract
routing table can be found in Section 111. An important
property of the routing table abstraction is that all net-works
with the same topology on the n labeled nodes are
reduced to the same abstract routing table.
Given an abstract routing table R' E R, we construct
the concretization of RI, y( R'), as follows. The set R, =
r( R') is thc set of concrete routing tables such that:
Every terminal node t, in R' also appears in every R,.
If R'( i, j) = pl ... p,, then R( i, j) = y( p1) ... y( p,)
where y( p) is the smallest set of nodes that appears in
every entry of R which corresponds to an entry in R'
containing p.
More formally, we define y( R') as
concretization of a routing table R' is
Definztzon 8: Concretization of a Routing Table. The
{ R I t, E R' + t, E RA
R'( i, j)= ~ i . . . ~ r* n R( i, j)= y ( ~ ~ ) . . . y ( ~ m ) }
where y ( p ) = { ni ... nmlVk, Z. p E R'( k, l) + n1 ... nm E
R( k 0)
111. TUTORIAELX AMPLE
We give a simple example of checking a property on a
simplified version of the PCI protocol [ PC195], called PCI,,
including only posted messages. In PCI, a posted message
is an unacknowledged message which can be neither deleted
nor reordered. The property we wish to check is: " if two
agents send a posted message to a single destination, then
one of the messages always reaches the destination first."
The property is not true for PCI, so we expect to find a
violation.
There is only one topologically unique way to connect
three nodes in an acyclic network, so there is only one ab-stract
routing table to consider in the construction of the
abstract state graph. Although all networks over three ter-minal
nodes have the same abstraction, we provide an ex-ample
of constructing the abstract routing table. Suppose
we have a PCI, network containing three terminal nodes
with the following routing table:
149
. ii" ( m) =
Fig. 1. Sets of concrete states represented by a monomial over the abstract state variables.
Fig. 2. Computing the abstract transition relation for a concrete transition T:
9,8,12,11
We chose to mark nodes 1,2 and 3 as the terminal nodes
in the property being checked; that means that node 10 will
be eliminated in the abstraction. After eliminating termi-nal
node 10, we replace the nodes in each non- branching
sub- path in the remaining network with a single path. For
example, all paths to and from node 1 include nodes 4 and
5. This means that nodes 4 and 5 form a non- branching
sub- path, which we represent as path A in the abstract
routing table. Note that the abstract routing table RI is
defined such that R C y( R'):
A PCI, message is written as a tuple ( s, d) which indi-cates
a message from agent s to agent d. We begin with
the definition of the state and transitions at a PCI, node,
parameterized by node address i.
X, = q: Array[ 2] of PCI, message, opposite- q: Array[ 2]
of PCI, message.
Transition r: with
g; = X,. q[ O] = ( 1,3) A next( i, 3) # 3A
asgn; = delete( 0, i); append(( l, 3), next( i, 3))
g; = Xz. q[ O] = ( 2,3) A next( i, 3) # 3A
asgn; = delete( 0, i); append(( l, 3), next( i, 3))
lf~ 11( Xnext~ a. q, 3) )
Transition 7- l with
+ WXnext(,, 3) . q)
1; with d. q[ O] = ( 1,3), s2. q[ O] = ( 2,3) and sJ. q[ k] =
Each node contains two arrays which each contain a max-imum
of two messages. Transition 7- i moves message ( 1,3)
from node a to the next node on the path from i to agent
3- if the queue in the next node is not full. Similarly, tran-sition
r: moves message ( 2,3) to the next node on the path
from i to agent 3.
empty for every other j , k.
The property we want to check asserts that the message
from agent 1 to agent 3 arrives at agent 3 first. This is
property is expressed by the following predicate:
cph = ( i = 3) 3 a2. q[ O=] (( 1,3) V empty)
We use cpb and the additional predicates
cp; = g; = X,. q[ O] =
cp; = g; = X,. q[ O] =
( 123) A next( i, 3) # 3 A lfull( xnext(,, a)
( 273) A next( i, 3) # 3 A lf~ ll( Xnext( a, 3~
to define the abstract state space. Given the initial state 11
and the predicates yb, cp;, 9; we have the following initial
abstract state:
il = -+@," 18fl@ Af 4F1@,"
l^ Y1 1 Y1 lflP@ P
17Y;+; 6f@? ' 6g@
' A - A -, dB - B
The initial abstract state represents all concrete states
which contain message ( 1,3) in path A and message ( 2,3)
in path B.
We compute the next states for f1 under the transitions
7- i and r;. We begin with . i;'. First, we check
y( f1) + Vn E A. lgF
that the concretization of the abstract initial state does not
satisfy gr for every node n in ?( A). We check the negated
form of the previous equation:
~ ( f i )=+ 3n E A. g r
Since fl includes 8t@ f we have that 3n E A. pT and from
the definition of cp? we have
3n E A. gF =+ 3n E A. g;
which is trivially true. This gives us tha t:+ # F and
we compute the values of the state variables for the other
predicates and network paths. We compute the effects of +! by considering the effects of applying rr to any node
n in the concretization of A. We present in detail how the
values of 8f@ f are computed and summarize the values
150
for the other state var! ables.
state of ?:( fl). We add 8f@ fif
First, we check if Sf@ should be added to the next
3n E A. 3m E A. ( y( f1) A 9:) + cpy[ asgn;( Z)/%]
It is possible to pick a node n in ?( A) such that p;". Sup-pose
n is not the last node in y( A) and m is the next node
after n in y( A), then asgnF( 5) moves PI from node n to
node m. In this case, if node m is empty before appending
PI then cp? is true of m after asgnF( Z)/%.
Next, we check if 8f- yf should be added to the next
state of ? f( il) W. e add 19f+ f if
377. E A. 3m E A.( y( f~ A) g: + - p;"[ asgn;(%)/%]
Which is also true. If we pick n and m to be the same node
in ?.( A), then after [ asyn?( Z)/%] P I is no longer in m so
3m E A.~( p;"[ asgn;( 3!/% a] n d we add 8f+ f to . i,"( fl).
Now we check if - 8f@ q should be added to the next
state of ? f( fl). W e add + f@;' if
37~ E .4.- 3m E A.( y( Il) A 9: + ~ ~ ? [ U S ~ T L ; ( % ) / % ]
Which is true if we pick n to be the last node in ?( A).
In this case, [ asgnF(%)/% m] oves PI out of the last node in
y( A) so that 4 m E A. cp;"[ asgn;(%)/ Z]. So we add 18f+ f
Finally, we check if 18fl@ f should be added to the next
3n E - 4.13m E A.( y( il) Agy + - yy[ asgn;(%)/%]
Which is not true because PI is in at most one node in ?( A)
before and after [ asgnF(%)/% a] n d PI is in different nodes
before and after the transition. Consequently, PI can not
be in all nodes of ?( A) after the transition.
We now have that 8f@ f', @+ f and - 8pp;" are in
?:( il). We have now computed the values of 81 and $ 1
for path A. We next perform a similar analysis for paths B
and C
to ? f( il).
state of f,"( fl). We add i8fi$ f if
For path B, only - 8F@ F is in ? t( fl). This is because
[ asgn;(%)/% c] a n not move message ( 1,3) to a bridge
in path B sirice riext( i, 3) is never a bridge in B for all
bridges i in path ,4.
For path C, we find that the following terms for 7- 1" are
in Ft( f1): 8f'@ f8', f'l@ fa nd 18FGf. These terms
are included because [ asgn;(%)/% c] a n, but is not re-quired
to, move message ( 1,3) to a bridge in path C
from a bridge in path A.
Next, we need to determine which state variables for pred-icates
po and p2 fo, r bridges in paths A, B and C need to
be included in ??( Il).
For predicate cpo, F e ( f 1 ) has no effect on cpo because
[ asgn;(%)/% c] a n not violate the invariant. Suppose
[ asgn;( Z)/ s] moves ( 1,3) into the head of agent 3.
Then if pi was true before [ asgn?(%)/% th] en cp; is still
true after [ asgn;(%)/ Z]. Suppose [ asgnF(%)/% d] o es
not move ( 1.3) into the head of agent 3. Similarly, if
pz was true before [ asgnF( 3)/% t] h en pz is still true
after [ asgny(%)/% J.
For predicate 9 2 , ?,"( f1) has no effect on cp2 either.
This is because [ asgnF( Z)/% d] oes not affect message
( 2,3). While [ asgn;(%)/% d] oes move message ( 1,3),
the location of message ( 2,3) has no bearing on the
value of p2.
This concludes the computation of ff( f1). We have that ? e ( f1) includes the following boolean expression over the
abstract state variables:
ff( f1) = ~ d t ~ A$ - 8tfi @ f A T~~ T@~ ( 8t@ f V 8fi@ f V - 8fGf) A
idF@ fA
( 8F@ f V 8p-@ f V 18fGf') A
~ 8,"@ A, " a $@$ A i8$&
Next, we perform the same analysis for ? y( fl) and
? f( fl). We begin by checking that
y( f1) 3 Vn E B.- g; and y( f1) * Vn E C. ig:
Both of these implications are true because i@ and @?
~ 8?@ arfe in 11. For + y( fl), w e then have that
- 3m E B. qY A y( f1) + Vn E C. lgr
and cp? = 9;". Because no nodes in paths B and C satisfy
the guard on T~ in state il, both ?,"( fl) and ? f( j1) equal
F.
Having determined the abstraction of all possible effects
of qAo n all network nodes of all concrete states represented
by 11, we now analyze the effects of r2 on all nodes in
all states represented by 11. The effects of 7- 2 are similar
to the effects of 71 except r2 moves message ( 2,3) rather
than message ( 1,3). We will compute the next state set
for ??( fl) and find a violation of the invariant. To make
the example complete, we first check that the transition in
enabled by attempting to disprove
$ 12) + Vn E B.- g;
Since 8,"@," is in f1, we have that
3m E B.& Ay(&) 3 Vn E B. lg,"
which is false since cp2 = g2. Since ?,"( ilis) e nabled, we
next computeAwhich abstract state variables are in the next
state for ??( I1),
We will start with 8$&' because it will yield a violation
of the form 8: 7@ g. To include dg-~@ itn the next state
of f. f( il) we need to prove that
3n E B. 3m E C.( y( Ii) A g; =+ ~ c p ~ [ ~ ~ g $ ( % ) / P ]
If we pick n to be the last bridge in B and let m be bridge 3
in path C ( implying that C has only one bridge, which is an
acceptable assumption) then [ asgna(%)/% m] o ves message
( 2,3) into the head of the queue in m. Bridge m now
violates
x3. q[ o] = ( 2,3) A ( i = 3) + xz. q[ O] = (( 1,3) V empty)
so we add 8$-@ g to ? F( il) and find that a node exists in
path C which violates 90.
151
Predicate abstraction is conservative, rather than exact,
so this violation does not necessarily imply that a violation
exists in the concrete model. However, in this case, the
violation can be translated into a violating trace. The vi-olating
PCI, trace allows the message ( 2,3) to reach agent
3 before the message ( 1,3).
IV. CONCLUDINRGEM ARKS
By restricting the class of properties that can be checked
and using a representation based on predicate abstraction,
we have created an abstraction method which is intended to
extend parameterized system verification to complex pro-tocols
over branching networks. At present, our predicate
abstraction technique for networks exists only as “ paper-ware.”
That is, predicate abstraction for networks has been
worked out on paper and pencil, and paper examples have
been completed; but that we have not yet built a tool which
incorporates these techniques and applies them systemati-cally.
Before building a tool based on these ideas, we plan to
extend the paper- ware version to include other network
classes, apply to distributed shared memory systems and
provide conservative support for reasoning about VCTL*
properties. We anticipate that the most difficult aspect
of the implementation will be providing reasoning support
for deciding if the set of concrete states represented by a
monomial
transition
[ AK86]
[ BJNTOO]
[ CGJ95]
[ DDPSS]
[ ESOO]
[ Gru97]
[ GS97]
[ HP991
[ HRW92]
[ JGOO]
[ KMILlf97]
of abstract state variables satisfies a guard to a
REFERENCES
Krzysztof R. Apt and Dexter C. Kozen. Limits for auto-matic
verification of finite- state concurrent systems. In-formation
Processing Letters, 22( 6): 307- 309, May 1986.
Ahmed Bouajjani, Bengt Johnsson, Marcus Nilsson, and
Tayssir Touilli. Regular model checking. In Emerson and
Sistla [ ESOO], pages 403- 418.
E. M. Clarke, 0. Grumberg, and S. Jha. Verifying pa-rameterized
networks using abstraction and regular lan-guages.
In 6th International Conference on Concurrency
Theory ( CONCUR’ 95), Philadelphia, PA, August 1995.
Satyaki Das, David L. Dill, and Seungioori Park. Ex-perience
with predicate abstraction. In Halbwachs and
Peled [ HP99].
E. Allen Emerson and A. Prasad Sistla, editors.
Computer- Aided Verification, CAV ‘ 00, volume 1855 of
Lecture Notes in Computer Science, Chicago, IL, July
2000. Springer- Verlag.
Orna Grumburg, editor. Computer- Aided Verification,
CAV ’ 97, volume 1254 of Lecture Notes in Computer
Science, Haifa, Israel, June 1997. Springer- Verlag.
Susanne Graf and Hassen Saidi. Construction of abstract
state graphs with PVS. In Grumburg [ Gru97].
Nicolas Halbwachs and Doron Peled, editors. Computer-
Aided Verification, CAV ’ 99, volume 1633 of Lecture
Notes an Computer Science, Trento, Italy, July 1999.
Springer- Verlag.
F. K. Hwang, D. S. Richards, and P. Winter. The Steiner
% e Problem, volume 53 of Annals of Discrete Mathe-matics.
North- Holland, Amsterdam, Netherlands, 1992.
h4ichael Jones and Ganesh Gopalakrishnan. Verifying
transaction ordering properties in unbounded bus net-works
through combined deductive/ algorithmic meth-ods.
In Formal Methods in Computer- Aided Design:
FMCAD’OU, November 2000. To appear.
Y. Kesten, 0. Maler, M. Marcus, A Pnueli, and E. Sha-har.
Symbolic model checking with rich assertional lan-guages.
In Grumburg [ Gru97].
[ LS97]
[ MHJGOO]
[ PC1951
[ PSOO]
[ SG89]
[ SS991
David Lesens and Hassen Saidi. Automatic verification
of parameterized networks of processes by abstraction.
In 2nd International Workshop on the Vemfication of
Infinite State Systems: INFINITY’ 97, July 1997.
Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones,
and Ganesh Gopalakrishnan. Formalization and proof
of a solution to the PCI 2.1 bus transaction ordering
problem. Formal Methods in Systems Design, 16( 1): 93-
119, January 2000.
PCISIG. PCI Special Interest Group- PCI Local Bus
Specification, Revision 2.1, June 1995.
Amir l‘ nueli and Elad Shahar. Liveness and accelera-tion
in parameterized verification. In Emerson and Sistla
[ ESOO], pages 328- 343.
Z. Shtadler and 0. Grumberg. Network grammars,
communication behaviors and automatic verification.
In Workshop on Automatic Verification Methods for
Fmzte- State Systems, volume 407 of Lecture Notes
in Computer Science, Grenoble, France, June 1989.
Springer- Verlag.
Hassen Sddi and N. Shankar. Abstract and model check
while you prove. In Halbwachs and Peled [ HP99].
152