...Abstraction
Partial support for this work was provided by the Office of Naval Research under contract N00014-89-J-1368, by the National Science Foundation under grant CCR-9023256, and by the Defense Advanced Research Projects Agency under DARPA project DAAL02-91-C-0051.

...Cuny,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003

...Forman,
Department of Computer Science and Engineering FR-35, University of Washington, Seattle, WA 98195

...Hough,
Amerinex Artificial Intelligence Inc., Amherst, MA 01002

...Ariadne.
= =1 .5 - =.9

In Greek mythology, Ariadne provided Theseus with the thread that enabled him to find his way through the Labyrinth to slay the Minotaur.

...programs.
Currently our traces are taken from a simulator or generated by hand.

...prototype.
The Ariadne prototype is only partially implemented. The matching faciltities and many of the query functions have been implemented but the syntax we use here is not yet available in the prototype. In addition, several recent modifications to the language including the use of WRT clauses as filters and the shuffle operator on the chain level have not yet been implemented. The examples in this paper, with the exception of the triangulation session, have been run on the prototype although in a few cases, we had to hand compute values returned by query functions.

...*).
Note that the shuffle operator is expensive to implement. We included it to model the behavior of guarded input commands; thus in practice, we would expect that only a few items will get shuffled at a time. We allow its use only on the chain level.

...events
The prefix e on precedes indicates that this is a predicate over a single abstract event, other versions of this same predicate operate over sequences of events.

...circumcircles
The circumcircle of a triangle is the circle that can be drawn through all of the vertices of that triangle.

...triangles:
Processes recompute the set of relevant triangles immediately before each lock attempt but that behavior is not modeled here.

Joydip Kundu kundu@neweng.enet.dec.com