LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 13th January 1998

Title: Unique Fixed Points for Unguarded Recursion

Speaker: Rob van Glabbeek (Stanford University, USA)

In concurrency theory it is common practice to specify processes as solutions of recursive equations, or sets of mutually recursive equations. Such an equation or set is called a recursive specification. In most models of concurrency every recursive specification has at least one solution. A syntactic criterion of guardedness for recursive specifications has been developed, ensuring that their solutions are moreover unique. The meaning of an unguarded recursive specification is usually taken to be a special element of its set of solutions, selected either by operational or denotational means.

This talk is concerned with the question whether the solution provided with either denotational or operational methods is in some sense indeed the `right' one, or a rather arbitrary choice. As an example, consider the recursive CSP equation X = a || X in which || denotes a parallel composition that enforces synchronization over the action a. The standard denotational and operational approaches agree that this equation determines the totally inactive process STOP or 0. However, intuitively the solution X=a appears an equally plausible choice.

In this talk I provide denotational semantics of a simple language for concurrent processes in terms of process graphs (i.e. transition systems with an initial state), event structures and Petri nets. In all cases I consider process interpretations on the most concrete level, without dividing out isomorphism. It turns out that, except in the most trivial cases, the solutions of recursive specifications are in fact unique, and hence not subject to choice. The non-uniqueness observed elsewhere in the literature arises merely from identifying isomorphic processes.

The uniqueness results above follow by application of a general theorem that also allows to infer that certain functions are continuous based on the syntactic form of their definition.

The standard denotational and operational process graph, event structure and Petri nets semantics all agree with the unique fixed point semantics provided here. Therefore they are indeed canonical.