Abstracts of Publications

This page is no longer updated. A somewhat less out-of-date version can be found here. More recent information is available on our homepages:

Precongruence Formats for Decorated Trace Semantics

Well-behaved Flow Event Structures for Parallel Composition and Action Refinement

First, suitable subclasses are characterised. Then two specific subclasses are proposed. The larger class generalises the one from [CZ], which is not suitable for action refinement. The smaller one is still sufficiently expressive for dealing with all standard process algebras and action refinement.

Software Geography: Physical and Economic Aspects

Orthocurrence as both Interaction and Observation

Transition and Cancellation in Concurrency and Branching Time

Precongruence Formats for Decorated Trace Preorders

The Linear Time -- Branching Time Spectrum {I}; The Semantics of Concrete, Sequential Processes

Higher dimensional automata revisited

The continuum as a final coalgebra

Petri Nets, Configuration Structures and Higher Dimensional Automata

Full completeness of the multiplicative linear logic of Chu spaces

Chu spaces as a semantic bridge between linear logic and mathematics

The motivating role of linear logic is as a ``logic behind logic.'' We propose a sibling role for it as a logic of transformational mathematics via the self-dual category of Chu spaces, a generalization of topological spaces. These create a bridge between linear logic and mathematics by soundly interpreting linear logic while fully and concretely embedding a comprehensive range of concrete categories of mathematics. Our main goal is to treat each end of this bridge in expository detail. In addition we introduce the dialectic lambda-calculus, and show that dinaturality semantics is not fully complete for the Chu interpretation of linear logic.

Refinement of Actions and Equivalence Notions for Concurrent Systems

On the Representation of Abelian Groups as Chu Spaces

Types as Processes, via Chu spaces

Chu spaces from the representational viewpoint

Towards Full Completeness for the Linear Logic of Chu Spaces

Bisimulation and Propositional Intuitionistic Logic

Using this insight, we are able to characterize validity in a Kripke structure in terms of bisimilarity.

Theorem 1: Let K be a finite Kripke structure for propositional intuitionistic logic, then two worlds in K are bisimilar if and only if they satisfy the same set of formulas.

This theorem lifts to structures in the following manner.

Theorem 2: Two finite Kripke structures K and K' are bisimilar if and only if they have the same set of valid formulas.

We generalize these results to a variety of infinite structures; finite principal filter structures and saturated structures.

Axiomatizing Flat Iteration Scheduling Algebra

Branching Bisimulation as a Tool in the Analysis of Weak Bisimulation

Axiomatizing Prefix Iteration with Silent Steps

Reconciling Event Structures and Higher Dimensional Automata

Broadening the denotational semantics of linear logic

Linear Logic complements Classical Logic

Chu realizes all small concrete categories

Chu Spaces and their Interpretation as Concurrent Objects

The Stone Gamut: A Coordinatization of Mathematics

The Meaning of Negative Premises in Transition System Specifications II

Ntyft/ntyxt Rules Reduce to Ntree Rules

These rates assume randomly distributed data. The distribution of the faulty pairs themselves however is far from random, with the effect that if the data is so nonrandom as to be just the constant 1, then random calculations started from that constant produce a division error once every few minutes, and these errors will sometimes propagate many more steps. A much higher rate yet is obtained when dividing small (<100) integers ``bruised'' by subtracting one millionth, where every 400 divisions will see a relative error of at least one in a million.

The software engineering implications of the bug include the observations that the method of exercising reachable components cannot detect reachable components mistakenly believed unreachable, and that handchecked proofs build false confidence.

Rational Mechanics and Natural Mathematics

This paper addresses the chief stumbling block for Descartes' 17th-century philosophy of mind-body dualism, how can the fundamentally dissimilar mental and physical planes causally interact with each other? We apply Cartesian logic to reject not only divine intervention, preordained synchronization, and the eventual mass retreat to monism, but also an assumption Descartes himself somehow neglected to reject, that causal interaction within these planes is an easier problem than between. We use Chu spaces and residuation to derive all causal interaction, both between and within the two planes, from a uniform and algebraically rich theory of between-plane interaction alone. Lifting the two-valued Boolean logic of binary relations to the complex-valued fuzzy logic of quantum mechanics transforms residuation into a natural generalization of the inner product operation of a Hilbert space and demonstrates that this account of causal interaction is of essentially the same form as the Heisenberg-Schr"odinger quantum-mechanical solution to analogous problems of causal interaction in physics.

Time and Information in Sequential and Concurrent Computation

Shorter proof of universality of Chu spaces

Chu Spaces: A Model of Concurrency

We provide several equivalent definitions of Chu spaces, including two pictorial representations. Chu spaces represent processes as automata or schedules, and Chu duality gives a simple way of converting between schedules and automata. We show that Chu spaces can represent various concurrency concepts like conflict, temporal precedence and internal and external choice, and they distinguish between causing and enabling events.

We present a process algebra for Chu spaces including the standard combinators like parallel composition, sequential composition, choice, interaction, restriction, and show that the various operational identities between these hold for Chu spaces. The solution of recursive domain equations is possible for most of these operations, giving us an expressive specification and programming language. We define a history preserving equivalence between Chu spaces, and show that it preserves the causal structure of a process.

Chu Spaces: Automata with Quantum Aspects

Chu Spaces: Complementarity and Uncertainty in Rational Mechanics

Reactive, Generative and Stratified Models of Probabilistic Processes

Vaandrager established that both results crucially depend on the use of unguarded recursion, and its noncomputable consequences. Effective versions of CCS, SCCS, Meije and ACP, not using unguarded recursion, are incapable of expressing all effective De Simone languages. And no effective language can denote all computable process graphs.

In this paper I recreate De Simone's results in aprACP without using unguarded recursion. The price to be payed for this is the use of a partial recursive communication function and---for the second result---a single constant denoting a simple infinitely branching process. Due to the noncomputable communication function, the version of aprACP employed is still not effective.

However, I also define a wide class of De Simone languages that are expressible in an effective version of aprACP. This class includes the effective versions of CCS, SCCS, ACP, Meije and most other languages proposed in the literature, but not CSP. An even wider class, including CSP, turns out to be expressible in an effective version of aprACP to which an effective relational renaming operator has been added.

Notes on the Chu construction and Recursion

Notes on Event Structures and Chu

Axiomatising ST-Bisimulation Equivalence

Full Abstraction in Structural Operational Semantics

Gates Accept Concurrent Behavior

We define a process algebra of event Kripke structures, showing how to combine them in the usual ways---parallel composition, sequential composition, choice, interaction and iteration. Various properties of these connectives like associativity and distributivity are proved. We then show that Winskel's event structures can be embedded in the class of event Kripke structures, and define partial synchronous composition, the primary connective for event structures, for event Kripke structures, and show its equivalence to Winskel's definition.

What is branching time semantics and why use it?

The Second Calculus of Binary Relations

The linear time -- branching time spectrum II

A complete axiomatization for branching bisimulation congruence of finite-state behaviours

Linear Logic for Generalized Quantum Mechanics

The Duality of Time and Information

To accommodate flexible distributed computing systems we then bring in choice and concurrency and pass to partially ordered time and information, the formal basis for this extension being Birkhoff-Stone dualtiy. A degree of freedom in how this is done permits a perfectly symmetric logic of computation amounting to Girard's full linear logic, which we view as the natural logic of computation when equal importance is attached to choice and concurrency.

We conclude with an assessment of the prospects for extending the duality to other organizations of time and information besides partial orders in order to accommodate real time, nonmonotonic logic, and automata that can forget, and speculate on the philosophical significance of the duality.

Some Monoidal Closed Categories of Stable Domains and Event Structures

Disjunctive Systems and L-Domains

A Roadmap of Some Two-Dimensional Logics

Origins of the Calculus of Binary Relations

Dynamic Algebras: Examples, Constructions, Applications

Arithmetic + Logic + Geometry = Concurrency

Interleaving Semantics and Action Refinement with Atomic Choice

On the Specification of Concurrent Systems

In this dissertation the notion of partial order is replaced by that of a set with a metric which takes values in a given ordered monoid. Partial orders are the simple case of a monoid whose two elements represent the presence or absence of a constraint.

An ordered monoid can be seen as a monoidal category, and schedules based on it are categories enriched in the monoid. Algebraic operations on schedules can then be defined as constructions in the category of schedules.

These definitions rely on certain properties of a category of schedules, such as closure and completeness. To simplify proofs of these properties, two constructions are defined. The first creates a category of unlabeled schedules from a system of constraints. The second adds labels to unlabeled schedules. Many categories of interest can be constructed from simple categories using these two methods. The main results of the dissertation derive the required properties of categories so constructed from similar, more easily verified properties of the base categories.

Several notions of timing constraint can be viewed in a uniform way in this framework. An example is the Gaifman-Pratt system, essentially the partial order model with additional specification as to whether two events may occur simultaneously. It corresponds to a monoid whose three elements represent strict precedence, lax precedence (simultaneity is permitted), and absence of constraint. Real-valued timing constraints correspond to the additive monoid of the real numbers.

Event Spaces and Their Linear Logic

Here we achieve both via the notion of an event space as a poset with all nonempty joins representing concurrence and a top representing the unreachable event. The symmetry is with the dual notion of state space, a poset with all nonempty meets representing choice and a bottom representing the start state. The algebra is that of a parallel programming language expanded to the language of full linear logic, Girard's axiomatization of which is satisfied by the event space interpretation of this language.

Event spaces resemble finite-dimensional vector spaces in distinguishing tensor product from direct product and in being isomorphic to their double dual, but differ from them in distinguishing direct product from direct sum and tensor product from tensor sum.

Modeling Concurrency with Geometry

Action Logic and Pure Induction

Enriched Categories and the Floyd-Warshall Connection

Dynamic Algebras as a Well-behaved Fragment of Relation Algebras

Modeling Concurrency with Partial Orders

Two Easy Theories whose Combination is Hard