Linear process algebra as an expressive denotational model of concurrency
Vaughan Pratt (Stanford University)
LOGIC AND COMPUTATION SEMINARDATE: 2011-06-22
TIME: 15:30:00 - 17:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
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 three event states or scalars, *ready*, *ongoing*, or *terminated*. These permit the expression of run time, mutual exclusion, and event independence. A fourth scalar, *cancelled*, 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.
BIO:
Vaughan Pratt is an emeritus professor of Computer Science at Stanford University and historically interested in a large number of areas of the subject - architecture, algorithms, languages, systems and particularly the application of mathematics.
More details of his achievements are available though Wikipedia.
He will be visiting CECS for the week of 20-24 June.
