LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
11.00am, Friday 20th June 1997

*NOTE NONSTANDARD DAY AND TIME (S&LC Club Slot)*

Title: First-Order Axioms for Asynchrony

Speaker: Peter Selinger (University of Pennsylvania, USA)

The distinction between synchronous and asynchronous communication is an important issue in the design of concurrent networks. Informally, a communication channel is said to be {\em synchronous} if message transmission is instantaneous, such that sender and receiver must be available at the same time in order to communicate. It is {\em asynchronous} if messages are assumed to travel through a communication medium with possible delay, such that the sender cannot be certain when a message has been received. In the last few years, research on asynchronous communication has mostly focused on concurrent process calculi such as the asynchronous $\pi$-calculus or, more recently, the join calculus.

In this talk, we will study properties of asynchronous communication in general, independently of any particular process paradigm. We model processes by labeled transition systems with input and output. These transition systems are similar to the input/output automata by Lynch and Stark, but our presentation is more category-theoretic in a style that resembles Abramsky's interaction categories. First, we formalize the intuitive notion of asynchrony in elementary terms: we define a process to be asynchronous if its input and/or output is filtered through an explicitly modeled communication medium, such as a buffer or a queue, possibly with feedback. Then, we characterize the behavior of asynchronous agents abstractly by a series of first- and second-order axioms.