Paper available: Transition and Cancellation in Concurrency and Branching Time
This is to announce the availability of "Transition and Cancellation in Concurrency and Branching Time" on http://boole.stanford.edu/pub/seqconc.ps.gz to appear in the forthcoming special issue of MSCS on "The Difference Between Sequential and Concurrent Computation." The all-too-familiar notion of the cancelled event, whose picture appears on page 2, should appeal to anyone with an interest in simpler semantics for branching time (if the idea is not new I'd obviously very much appreciate hearing about it). The semantics makes both concurrent and sequential composition idempotent, which may come as a bit of a shock to those more accustomed to any of action-oriented semantics, labeled event structures, or coproduct-oriented composition of event structures, where neither operation is idempotent. (How could 1 + 1 not be 2?) This paper uses ordinary set union instead (less fuss than trying to do the same thing with pushouts), without which the techniques of this paper giving a simple treatment of concurrency and branching time in unlabeled event structures would not be possible. Abstract We review the conceptual development of (true) concurrency and branching time starting from Petri nets and proceeding via Mazurkiewicz traces, pomsets, bisimulation, and event structures up to higher dimensional automata (HDAs), whose acyclic case may be identified with triadic event structures and triadic Chu spaces. Acyclic HDAs may be understood as the extension of Boolean logic with a third truth value _- expressing transition. We prove the necessity of such a third value under mild assumptions about the nature of observable events, and show that the expansion of any complete Boolean basis L to L_T with a third literal trans(a) expressing a = _- forms an expressively complete basis for the representation of acyclic HDAs. The main contribution is a new event state X of cancellation, sibling to _- and serving to distinguish a(b+c) from ab+ac while simplifying the extensional definitions of termination v' A and sequence AB. We show that every HDAX (acyclic HDA with X) is representable in the expansion of L_T to L_{TX} with a fourth literal canc(a) expressing a=X. 18-Apr-2002 16:02:53 -0300,5121;000000000000-00000000
participants (1)
-
Vaughan Pratt