Basser Seminar Series

Linear process algebra as an expressive denotational model of concurrency

Speaker: Professor Vaughan Pratt
Stanford University

Time: Friday 17 June 2011, 4:00-5:00pm
Refreshments will be available from 3:30pm
Location: The University of Sydney, School of IT Building, Lecture Theatre (Room 123), Level 1

Add seminar to my diary


Concurrent processes can be modeled inter alia as higher dimensional automata representing n concurrently ongoing events as an n-dimensional cell, and as Chu spaces representing relationships between events and states. Linear process algebra unifies these two models by defining a process (A,X) as a set X of state vectors indexed by a set A of events serving as coordinates. At each coordinate an event may be in one of four event states or scalars, *ready*, *ongoing*, *terminated*, or *cancelled*. The first three scalars permit the expression of run time, mutual exclusion, and event independence. The fourth scalar permits the expression of process termination, sequential composition, and a notion of branching time. The operations are those of linear logic together with sequential composition and choice. We give an alternative formulation of the model that replaces its set theoretic foundations with a category theoretic one by representing processes as primitive objects, events and states as process transformations, and the four scalars as all and only those transformations that are both events and states.

Speaker's biography

Vaughan Pratt wrote his thesis on shellsort under Donald Knuth and then taught at MIT from 1972 to 1981 and at Stanford since 1981, where he is now Professor Emeritus. His research interests include computational complexity, logics of programs, natural language, speech recognition, foundations of concurrency, universal algebra, category theory, and most recently climate change. He has participated in several startups including Sun Microsystems where he developed the Pixrect framebuffer abstraction and designed the Sun logo. His more theoretical contributions include dynamic logic, succinct certificates of primality and the Knuth-Morris-Pratt pattern matcher.