Stanford Concurrency Group
Abstracts of Publications

This page contains the abstracts of papers written by current and former members of the Concurrency Group, a subgroup of the Mathematical Theory of Computation Group, Computer Science Department, Stanford University. Current members of the Concurrency Group are as follows. MEMBER Rob van Glabbeek rvg Dominic Hughes dominic Gordon Plotkin (summers) gdp Vaughan Pratt (group leader) pratt Wendy Cardamone (secretary) wendyc To retrieve a paper, click on its title. If you have problems in either retrieving or compiling papers, please email Vaughan Pratt as above.

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:

Rob van Glabbeek (papers, abstracts, references in bibtex and pdf) Dominic Hughes (selected papers) Gordon Plotkin (papers available online) Vaughan Pratt (papers; references.pdf)


Precongruence Formats for Decorated Trace Semantics

@Techreport( BFG02, Author="B. Bloom and W.J. Fokkink and Glabbeek, R.J. van", Title ="Precongruence Formats for Decorated Trace Semantics", Year = 2002, month = {April}. Note="Available at {\tt\-pub/\}") This paper explores the connection between semantic equivalences and preorders for concrete sequential processes, represented by means of labelled transition systems, and formats of transition system specifications using Plotkin's structural approach. For several preorders in the linear time - branching time spectrum a format is given, as general as possible, such that this preorder is a precongruence for all operators specifiable in that format. The formats are derived using the modal characterizations of the corresponding preorders.

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

@Techreport( GG02, author = {Glabbeek, R.J. van and U. Goltz}, title = {Well-behaved Flow Event Structures for Parallel Composition and Action Refinement}, year = 2002, month = {March}, Type = {Braunschweiger Informatik-Berichte}, Institution="Institut f{\"u}r Software, Technische Universit{\"a}t Braunschweig", Address={Germany}, Note="Available at {\tt\-pub/\}") Flow event structures were introduced as a model for giving semantics to process algebras. However it turned out that certain restrictions have to be made to make them suitable for this purpose. In this paper, we investigate subclasses of flow event structures which are both suited for the process algebraic composition operators, and for action refinement as a means of regarding processes on different levels of abstraction.

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

@InProceedings( Pr01c, Author="Pratt, V.R.", Title="Software Geography: Physical and Economic Aspects", BookTitle="Proc. SOFSEM'01", Series=LNCS, Volume=2234, Pages="336-346", Address="Bratislava", Month=Nov, Year=2001) To the metaphors of software engineering and software physics can be added that of software geography. We examine the physical and economic aspects of the Software Glacier (once an innocent bubbling brook, now a vast frozen mass of applications imperceptibly shaping both the Hardware Shelf below and User City above), Quantum Planet (colonization of which could be fruitful if and when it becomes practical), and Concurrency Frontier (an inaccessible land with rich resources that we project will be exploited to profound economic effect during the next half-century).

Orthocurrence as both Interaction and Observation

@Misc( Pr01b, Author="Pratt, V.R.", Title="Orthocurrence as both Interaction and Observation", Howpublished="Proc. Workshop on Spatial and Temporal Reasoning (ed. R.~Rodriguez and F.~Anger), IJCAI'01", Address=Seattle, Month=August, Year=2001) Orthocurrence or tensor product A*B of systems A and B can be understood symmetrically as an interaction operator expressing a form of conjunction of state predicates, or asymmetrically as one of two information channels: either A -o B' as a system consisting of A observing states of B (equivalently, conveying information about the states of B to A), or B -o A' for the same thing in the other direction. We show how the notion of Chu space or couple arises as a natural corollary of this point of view. We conclude with a history of orthocurrence.

Transition and Cancellation in Concurrency and Branching Time

@Article( Pr02a, Author="Pratt, V.R.", Title="Transition and Cancellation in Concurrency and Branching Time", Journal="Math. Structures in Comp. Sci.", Year=2002, Note="To appear") We review the conceptual development of (true) concurrency and branching time starting from Petri nets and proceeding via Mazurkiewicz traces, pomsets, bisimulation, and event structures up to higher dimensional automata (HDAs), whose acyclic case may be identified with triadic event structures and triadic Chu spaces. Acyclic HDAs may be understood as the extension of Boolean logic with a third truth value _|- expressing _transition_. We prove the necessity of such a third value under mild assumptions about the nature of observable events, and show that the expansion of any complete Boolean basis L to L_T with a third literal hat(a) expressing a = _|- forms an expressively complete basis for the representation of acyclic HDAs. The main contribution is a new event state X of _cancellation_, sibling to _|-, serving to distinguish a(b+c) from ab+ac while simplifying the extensional definitions of termination v' A and sequence AB. We show that every HDAX (acyclic HDA with X) is representable in the expansion of L_T to L_{TX} with a fourth literal /a expressing a=X.


@Misc( vG00b, Author="Glabbeek, R.J. van", Title="Bisimulation", Howpublished="To appear in the Encyclopedia of Distributed Computing (J.E. Urban \& P. Dasgupta, eds.), Kluwer. Available at {\tt\-pub/\}", Year=2000) Bisimulation equivalence is a semantic equivalence relation on labelled transition systems, which are used to represent distributed systems. It identifies systems with the same branching structure.

Precongruence Formats for Decorated Trace Preorders

@InProceedings( BFG00, Author="B. Bloom and W.J. Fokkink and Glabbeek, R.J. van", Title ="Precongruence Formats for Decorated Trace Preorders", Booktitle="{\rm Proceedings $15^{th}$ Annual IEEE Symposium on} Logic in Computer Science {\rm (LICS 2000), Santa Barbara, USA, June 2000}", Publisher="IEEE Computer Society Press", Year="2000", Pages="107-118", Note="Available at {\tt}") This paper explores the connection between semantic equivalences and preorders for concrete sequential processes, represented by means of labelled transition systems, and formats of transition system specifications using Plotkin's structural approach. For several preorders in the linear time - branching time spectrum a format is given, as general as possible, such that this preorder is a precongruence for all operators specifiable in that format. The formats are derived using the modal characterizations of the corresponding preorders.

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

@InCollection( vG00a, Author="Glabbeek, R.J. van", Title ="The Linear Time -- Branching Time Spectrum {I}; The Semantics of Concrete, Sequential Processes", Booktitle="Handbook of Process Algebra", Publisher="Elsevier", Chapter=1, Editor="J.A. Bergstra and A. Ponse and S.A. Smolka", Year=2000, Note="Available at {\tt\-pub/\}") In this paper various semantics in the linear time -- branching time spectrum are presented in a uniform, model-independent way. Restricted to the class of finitely branching, concrete, sequential processes, only fifteen of them turn out to be different, and most semantics found in the literature that can be defined uniformly in terms of action relations coincide with one of these fifteen. Several testing scenarios, motivating these semantics, are presented, phrased in terms of `button pushing experiments' on generative and reactive machines. Finally twelve of these semantics are applied to a simple language for finite, concrete, sequential, nondeterministic processes, and for each of them a complete axiomatization is provided.

Higher dimensional automata revisited

@Article( Pr00a, Author="Pratt, V.R.", Title="Higher dimensional automata revisited", Journal="Math. Structures in Comp. Sci.", Volume=10, Pages="525--548", Year=2000) The dual of a true concurrency schedule appears to be a false concurrency automaton, a paradox we resolved in a previous paper by extending the latter to higher dimensions. This extension may be formalized via such discrete geometries as n-categories, simplicial complexes, cubical complexes, and Chu spaces. We advocate the last as having a clear notion of event, a well-defined process algebra uniformly extending that for event structures, and ease of extension beyond the basic before-during-after analysis.

The continuum as a final coalgebra

@Article( PP00, Author="Pavlovic, D. and Pratt, V.R.", Title="The continuum as a final coalgebra", Journal=TCS, Note="Accepted for publication", Year=2002) We define the continuum up to order isomorphism, and hence up to homeomorphism via the order topology, in terms of the final coalgebra of either the functor NxX, product with the set of natural numbers, or the functor 1 + NxX. This makes an attractive analogy with the definition of N itself as the initial algebra of the functor 1 + X, disjoint union with a singleton. We similarly specify Baire space and Cantor space in terms of these final coalgebras. We identify two variants of this approach, a coinductive definition based on final coalgebraic structure in the category of sets, and a direct definition as a final coalgebra in the category of posets. We conclude with some paradoxical discrepancies between continuity and constructiveness in this setting.

Chu Spaces

@Misc( Pr99a, Author="Pratt, V.R.", Title="Chu Spaces", Comment="Course notes for the School in Category Theory and Applications", Address="Coimbra, Portugal", Month=July, Year=1999) These are the notes for the course on Chu Spaces for the School in Category Theory and Applications, Coimbra, Portugal, July 13-17, 1999. Chapter 1 introduces the basic notions, gives examples of use of Chu spaces, points out some interference properties, and proves that functions between Chu spaces are continuous if and only if they are homomorphisms. Chapter 2 realizes a variety of mathematical objects as Chu spaces, including posets, topological spaces, semilattices, distributive lattices, and vector spaces. Chapter 3 gives several senses in which Chu spaces are universal objects of mathematics. Chapter 4 interprets operations of linear logic and process algebra over Chu spaces. Chapter 5 studies linear logic from an axiomatic viewpoint, with emphasis on the multiplicative fragment. Chapter 6 develops several notions of naturality as a semantic criterion for canonical transformations. Chapter 7 proves full completeness of the multiplicative linear logic of Chu spaces

Petri Nets, Configuration Structures and Higher Dimensional Automata

@InProceedings( vG99, aAuthor="Glabbeek, R.J. van", Title ="Petri Nets, Configuration Structures and Higher Dimensional Automata", Booktitle="{\rm Proceedings} CONCUR '99, {\rm 10$^{\it th}$ International Conference on} Concurrency Theory, {\rm Eindhoven, The Netherlands, August 1999}", Year=1999, Editor="J.C.M. Baeten and S. Mauw", Publisher="Springer", Series="LNCS", Volume =1664, Pages="21-27", Note= "Available at {\tt\-pub/\}") In this talk, translations between several models of concurrent systems are reviewed c.q. proposed. The models considered capture causality, branching time, and their interplay, and these features are preserved by the translations. To the extent that the models are intertranslatable, this yields support for the point of view that they are all different representations of the same phenomena. The translations can then be applied to reformulate any issue that arises in the context of one model into one expressed in another model, which might be more suitable for analysing that issue. To the extent that the models are not intertranslatable, my investigations are aimed at classifying them w.r.t. their expressiveness in modelling phenomena in concurrency.

Full completeness of the multiplicative linear logic of Chu spaces

@InProceedings( DHPP, Author="Devarajan, H. and Hughes, D. and Plotkin, G. and Pratt, V.", Title="Full completeness of the multiplicative linear logic of Chu spaces", Booktitle="{\rm Proceedings $14^{th}$ Annual IEEE Symposium on} Logic in Computer Science, {\rm LICS'99, Trento, Italy, July 1999}", Editor="G. Longo", Month="July", Publisher="IEEE Computer Society Press", Year="1999", Note="Available at {\tt}") We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection with the binary logical transformations of the corresponding operations on the category of Chu spaces on a two-letter alphabet.}

Chu spaces as a semantic bridge between linear logic and mathematics

@Article( Pr98b, Author=Pratt, V.R.", Title="Chu spaces as a semantic bridge between linear logic and mathematics", Journal="TCS, to appear", Year=2002) (Note: this supersedes "Broadening the Denotational Semantics of Linear Logic", doubling its length and adding much new material.)

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

@Techreport( GG98, author = {Glabbeek, R.J. van and U. Goltz}, title = {Refinement of Actions and Equivalence Notions for Concurrent Systems}, year = 1998, month = {April}, Type = {Hildesheimer Informatik-Berichte}, Organization={University of Hildesheim}, Address={Germany}) We study an operator for refinement of actions to be used in the design of concurrent systems. Actions on a given level of abstraction are replaced by more complicated processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We recall that interleaving models of concurrent systems are not suited for defining such an operator in its general form. Instead, we define this operator on several causality based, event oriented models, taking into account the distinction between deadlock and successful termination. Then we investigate the interplay of action refinement with abstraction in terms of equivalence notions for concurrent systems, considering both linear time and branching time approaches. We show that besides the interleaving equivalences, also the equivalences based on steps are not preserved under refinement of actions. We prove that linear time partial order semantics are invariant under refinement. Finally we consider various bisimulation equivalences based on partial orders and show that the finest two of them are preserved under refinement whereas the others are not. Termination sensitive versions of these equivalences are even congruences for action refinement.

Scheduling Algebra

@TechReport{ GR98, Author={Glabbeek, R.J. van and P. Rittgen}, Title ={Scheduling Algebra}, Type ={Arbeitsberichte des Instituts f\"ur Wirtschaftsinformatik}, Number=12, Institution={Universit\"at Koblenz-Landau}, Address ={Germany}, Month = {March}, Year = 1998} The goal of this paper is to develop an algebraic theory of process scheduling. We specify a syntax for denoting processes composed of actions with given durations. Subsequently, we propose axioms for transforming any specification term of a scheduling problem into a term of all valid schedules. In particular, we axiomatize an operator that restricts attention to the efficient schedules. These schedules turn out to be representable as trees, because in an efficient schedule actions can only start at time zero or when a resource is released, i.e. upon termination of the action binding a required resource. All further delay would be useless. Nevertheless, we do not consider resource constraints explicitly at the time being. We show that a normal form exists for every closed term of the algebra and establish soundness of our axiom system with respect to a schedule semantics, as well as completeness for efficient processes.

On the Representation of Abelian Groups as Chu Spaces

@Unpublished( Pr97d, Author="Pratt, V.R.", Title="On the Representation of Abelian Groups as Chu Spaces", Comment="Draft Report", Month=Oct, Year=1997) We compare two representations of finite Abelian groups as Chu spaces. The first represents the elements of any ternary relational structure as words on an 8-letter alphabet. The second is based on the group characters of abelian groups as the elements of the dual group.

Types as Processes, via Chu spaces

@InProceedings( Pr97c, Author="Pratt, V.R.", Title="Types as Processes, via Chu spaces", Booktitle="EXPRESS'97 Proceedings", Year=1997) We match up types and processes by putting values in correspondence with events, coproduct with (noninteracting) parallel composition, and tensor product with orthocurrence. We then bring types and processes into closer correspondence by broadening and unifying the semantics of both using Chu spaces and their transformational logic. Beyond this point the connection appears to break down; we pose the question of whether the failures of the correspondence are intrinsic or cultural.

Chu spaces from the representational viewpoint

@InCollection( Pr97b, Author="Pratt, V.R.", Title="Chu spaces from the representational viewpoint", Booktitle="Parikh Festschrift", Year=1997) We give an elementary introduction to Chu spaces. The perspective taken views their elements as represented by words of a fixed length over some alphabet. This perspective dualizes the alternative view of Chu spaces as generalized topological spaces, and has the advantage of substituting the intuitions of formal language theory for those of topology.

Towards Full Completeness for the Linear Logic of Chu Spaces

@InProceedings( Pr97a, Author="Pratt, V.R.", Title={Towards Full Completeness for the Linear Logic of Chu spaces}, Booktitle="Proc. Math. Foundations of Programming Semantics (MFPS'97)", Series="ENTCS (Electronic Notes of Theoretical Computer Science)", Address="Pittsburgh", Year=1997) We prove full completeness for a fragment of the linear logic of the self-dual monoidal category of Chu spaces over 2, namely that the proofs between semisimple (conjunctive normal form) formulas of multiplicative linear logic without constants having two occurrences of each variable are in bijection with the dinatural transformations between the corresponding functors. The proof assigns to variables domains having at most four elements, demonstrating a uniform finite model property for this fragment. We define a notion of proof function analogous to the notion of truth function, determining a transformation between functors, and show that the transformation denoted by a proof net is dinatural if and only if the proof net is sound, namely acyclic and connected. Proof functions are of independent interest as a 2-valued model of MLL with MIX.

Bisimulation and Propositional Intuitionistic Logic

@InProceedings( Pa97, Author = "Patterson, A", Title = "Bisimulation and Propositional Intuitionistic Logic", Booktitle="{\rm Proceedings} CONCUR '97, {\rm 8$^{\it th}$ International Conference on} Concurrency Theory, {\rm Warsaw, Poland, July 1997}", Editor="A. Mazurkiewicz and J. Winkowski", Series = "LNCS", Volume=1243, Publisher="Springer", Month=may, Year=1997, Note="Available by ftp at {\tt\-pub/\}") The Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic suggests that p implies q can be interpreted as a computation that given a proof of p constructs a proof of q. Dually, we show that every finite canonical model of q contains a finite canonical model of p. If q and p are interderivable, their canonical models contain each other.

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

@InProceedings( vG97a, Author = "Glabbeek, R.J. van", Title = "Axiomatizing Flat Iteration", Booktitle="{\rm Proceedings} CONCUR '97, {\rm 8$^{\it th}$ International Conference on} Concurrency Theory, {\rm Warsaw, Poland, July 1997}", Editor="A. Mazurkiewicz and J. Winkowski", Series = "LNCS", Volume=1243, Publisher="Springer", Month=may, Year=1997, Pages="228--242", Note="Available by ftp at {\tt\-pub/\}") Flat iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be a sum of atomic actions. It generalizes prefix iteration, in which the first argument is a single action. Complete finite equational axiomatizations are given for five notions of bisimulation congruence over basic CCS with flat iteration, viz. strong congruence, branching congruence, eta-congruence, delay congruence and weak congruence. Such axiomatizations were already known for prefix iteration and are known not to exist for general iteration. The use of flat iteration has two main advantages over prefix iteration: 1. The current axiomatizations generalize to full CCS, whereas the prefix iteration approach does not allow an elimination theorem for an asynchronous parallel composition operator. 2. The greater expressiveness of flat iteration allows for much shorter completeness proofs. In the setting of prefix iteration, the most convenient way to obtain the completeness theorems for eta-, delay, and weak congruence was by reduction to the completeness theorem for branching congruence. In the case of weak congruence this turned out to be much simpler than the only direct proof found. In the setting of flat iteration on the other hand, the completeness theorems for delay and weak (but not eta-) congruence can equally well be obtained by reduction to the one for strong congruence, without using branching congruence as an intermediate step. Moreover, the completeness results for prefix iteration can be retrieved from those for flat iteration, thus obtaining a second indirect approach for proving completeness for delay and weak congruence in the setting of prefix iteration.

Branching Bisimulation as a Tool in the Analysis of Weak Bisimulation

@Misc( vG95a, Author="Glabbeek, R.J. van", Title ="Branching Bisimulation as a Tool in the Analysis of Weak Bisimulation", Month=Sep, Year ="1995", Howpublished = "Available at {\tt}") It is shown that the analysis of weak congruence can sometimes be simplified by means of a similar analysis of branching congruence as an intermediate step. This point is made through a completeness proof for an equational axiomatization of basic CCS with prefix iteration.

Axiomatizing Prefix Iteration with Silent Steps

@Article( AFGI96, Author="L. Aceto and W.J. Fokkink and Glabbeek, R.J. van and A. Ing\'olfsd\'ottir", Journal="Information and Computation", Title ="Axiomatizing Prefix Iteration with Silent Steps", Volume=127, Number=1, Pages="26-40", Year=1996) Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. branching congruence, eta-congruence, delay congruence and weak congruence. The completeness proofs for eta-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e., terms that may contain process variables. As a byproduct, the omega-completeness of the axiomatizations is obtained as well as their completeness for closed terms.

Reconciling Event Structures and Higher Dimensional Automata

Reconciling Event Structures and Higher Dimensional Automata V.R. Pratt Submitted to a conference Addressing the problem in the title, we diagnose the essential difficulty as the implicit assumption of two-valued logic in the event structure view of event occurrence as a true-or-false proposition. Taking the 3-valued logic of before-during-after as the common underlying logic of both event structures and higher dimensional automata (HDA's) unifies them into a single model having the same process algebra, linear logic, and schedule-automaton duality as had previously been achieved for event structures, but not previously for HDA's. The crucial tool is Chu spaces, whose application to concurrency has previously limited itself to Chu spaces over 2, and which here is taken over 3.

Broadening the denotational semantics of linear logic

Broadening the denotational semantics of linear logic V.R. Pratt To appear in ENTCS proceedings of Linear Logic '96, Tokyo The proof-theoretic origins and specialized models of linear logic make it primarily operational in orientation. In contrast first-order logic treats the operational and denotational aspects of general mathematics quite evenhandedly. Here we show that linear logic has models of even broader denotational scope than those of first order logic, namely Chu spaces, the category of which Barr has observed to form a model of linear logic. We have previously argued that every category of n-ary relational structures embeds fully and concretely in the category of Chu spaces over 2^n. The main contributions of this paper are improvements to that argument, and an embedding of every small category in the category of Chu spaces via a symmetric variant of the Yoneda embedding.

Linear Logic complements Classical Logic

Linear Logic complements Classical Logic V.R. Pratt Preliminary proceedings, Linear Logic '96, Tokyo Classical logic enforces the separation of individuals and predicates, linear logic draws them together via interaction; these are not right-or-wrong alternatives but dual or complementary logics. Linear logic is an incomplete realization of this duality. While its completion is not essential for the development and maintenance of logic, it is crucial for its application. We outline the ``four-square'' program for completing the connection, whose corners are set, function, number, and arithmetic, and define ordinal Set, a bicomplete *equational* topos, meaning its canonical isomorphisms are identities, including associativity of product.

Chu realizes all small concrete categories

V.R. Pratt Draft in preparation The category Chu is concretely universal for much of concrete mathematics; in particular it concretely represents or realizes all categories of relational structures and their homomorphisms, as well as all topological such. This note extends these results to all small concrete categories, equivalently all small subcategories of Set. The category C is realized in Chu(Set,K) where K is the disjoint union of the underlying sets of objects of C. Each object is realized as the normal Chu space (A,X) where X consists of all functions from A in C astricted to K.

Chu Spaces and their Interpretation as Concurrent Objects

@InCollection( Pr95d, Author= "Pratt, V.R.", Title= "Chu Spaces and their Interpretation as Concurrent Objects", Booktitle="Computer Science Today: Recent Trends and Developments", Series=LNCS, Volume=1000, Pages="392-405", Editor="van Leeuwen, J.", Publisher="Springer-Verlag", Year="1995") A Chu space is a binary relation =| from a set A to an antiset X defined as a set which transforms via converse functions. Chu spaces admit a great many interpretations by virtue of realizing all small concrete categories and most large ones arising in mathematical and computational practice. Of particular interest for computer science is their interpretation as computational processes, which takes A to be a schedule of events distributed in time, X to be an automaton of states forming an information system in the sense of Scott, and the pairs (a,x) in the =| relation to be the individual transcriptions of the making of history. The traditional homogeneous binary relations of transition on X and precedence on A are recovered as respectively the right and left residuals of the heterogeneous binary relation =| with itself. The natural algebra of Chu spaces is that of linear logic, made a process algebra by the process interpretation.

Configuration Structures

@InProceedings( vGP, Author="Van Glabbeek, R. and Plotkin, G.", Title="Configuration Structures", Booktitle="Logic in Computer Science", Pages="199-209", Month="June", Publisher="IEEE Computer Society", Year="1995") Configuration structures provide a model of concurrency generalising the families of configurations of event structures. They can be considered logically, as classes of propositional models; then sub-classes can be axiomatised by formulae of simple prescribed forms. Several equivalence relations for event structures are generalised to configuration structures, and also to general Petri nets. Every configuration structure is shown to be ST-bisimulation equivalent to a prime event structure with binary conflict; this fails for the tighter history preserving bisimulation. Finally, Petri nets without self-loops under the collective token interpretation are shown behaviourally equivalent to configuration structures, in the sense that there are translations in both directions respecting history preserving bisimulation. This fails for nets with self-loops.

The Stone Gamut: A Coordinatization of Mathematics

@InProceedings( Pr95c, Author="Pratt, V.R.", Title="The {S}tone Gamut: A Coordinatization of Mathematics", Booktitle="Logic in Computer Science", Pages="444-454", Month="June", Publisher="IEEE Computer Society", Year="1995") We give a uniform representation of the objects of mathematical practice as Chu spaces, forming a concrete self-dual bicomplete closed category and hence a constructive model of linear logic. This representation distributes mathematics over a two-dimensional space we call the Stone gamut. The Stone gamut is coordinatized horizontally by coherence, ranging {from} -1 for sets to 1 for complete atomic Boolean algebras (CABA's), and vertically by complexity of language. Complexity 0 contains only sets, CABA's, and the inconsistent empty set. Complexity 1 admits noninteracting set-CABA pairs. The entire Stone duality menagerie of partial distributive lattices enters at complexity 2. Groups, rings, fields, graphs, and categories have all entered by level 16, and every category of relational structures and their homomorphisms eventually appears. The key is the identification of continuous functions and homomorphisms, which puts Stone-Pontrjagin duality on a uniform basis by merging algebra and topology into a simple common framework.

The Meaning of Negative Premises in Transition System Specifications II

@Techreport( vG95a, Author= "Glabbeek, R.J. van", Title= "The Meaning of Negative Premises in Transition System Specifications {II}", Institution="Stanford University", Year=1995, Note= "Available by anonymous ftp from {\tt}") This paper reviews several methods to associate transition relations to transition system specifications with negative premises in Plotkin's structural operational style. Besides a formal comparison on generality and relative consistency, the methods are also evaluated on their taste in determining which specifications are meaningful and which are not.

Ntyft/ntyxt Rules Reduce to Ntree Rules

@Techreport( FG95, Author= "Fokkink, W.J. and Glabbeek, R.J. van", Title= "Ntyft/ntyxt Rules Reduce to Ntree Rules", Institution="Stanford University", Year=1995, Note= "Available by anonymous ftp from {\tt}") Groote and Vaandrager introduced the tyft/tyxt format for Transition System Specifications (TSSs), and established that for each TSS in this format that is well-founded, the bisimulation equivalence it induces is a congruence. In this paper, we construct for each TSS in tyft/tyxt format an equivalent TSS that consists of tree rules only. As a corollary we can give an affirmative answer to an open question, namely whether the well-foundedness condition in the congruence theorem for tyft/tyxt can be dropped. These results extend to tyft/tyxt with negative premises and predicates.

Anatomy of the Pentium Bug

@InProceedings( Pr95b, Author="Pratt, V.R.", Title="Anatomy of the Pentium Bug", Booktitle="TAPSOFT'95", Series=LNCS, Volume=915, Address="Aarhus, Denmark", Pages="97-107", Publisher="Springer-Verlag", Year=1995) The Pentium computer chip's division algorithm relies on a table from which five entries were inadvertently omitted, with the result that 1738 single precision dividend-divisor pairs yield relative errors whose most significant bit is uniformly distributed from the 14th to the 23rd (least significant) bit. This corresponds to a rate of one error every 40 billion random single precision divisions. The same general pattern appears at double precision, with an error rate of one in every 9 billion divisions or 75 minutes of division time.

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

@InProceedings( Pr95a, Author="Pratt, V.R.", Title="Rational Mechanics and Natural Mathematics", Booktitle="TAPSOFT'95", Series=LNCS, Volume=915, Address="Aarhus, Denmark", Pages="108-122", Publisher="Springer-Verlag", Year=1995) Chu spaces have found applications in computer science, mathematics, and physics. They enjoy a useful categorical duality analogous to that of lattice theory and projective geometry. As natural mathematics Chu spaces borrow ideas from the natural sciences, particularly physics, while as rational mechanics they cast Hamiltonian mechanics in terms of the interaction of body and mind.

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

@InProceedings( Pr94c, Author="Pratt, V.R.", Title="Time and Information in Sequential and Concurrent Computation", Booktitle="Proc. Theory and Practice of Parallel Programming (TPPP'94)", Address="Sendai, Japan", Month=Nov, Pages="1-24". Year=1994) Time can be understood as dual to information in extant models of both sequential and concurrent computation. The basis for this duality is phase space, coordinatized by time and information, whose axes are oriented respectively horizontally and vertically. We fit various basic phenomena of computation, and of behavior in general, to the phase space perspective. The extant two-dimensional logics of sequential behavior, the van Glabbeek map of branching time and true concurrency, event-state duality and schedule-automaton duality, and Chu spaces, all fit the phase space perspective well, in every case confirming our choice of orientation.

Shorter proof of universality of Chu spaces

@Note( Pr94b, Author="Vaughan Pratt", Title="Shorter proof of universality of Chu spaces", School="Stanford University", Month=Aug, Year=1994) We give a shorter proof of the result in section 5 of our MFPS'93 paper (scbr), that every k-ary relational structure is realizable as a Chu space.

Chu Spaces: A Model of Concurrency

@PhDThesis( Gup94, Author="Vineet Gupta", Title="Chu Spaces: A Model of Concurrency", School="Stanford University", Month=Sep, Year=1994) A Chu space is a binary relation between two sets. In this thesis we show that Chu spaces form a non-interleaving model of concurrency which extends event structures while endowing them with an algebraic structure whose natural logic is linear logic.

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

@InProceedings( Pr94b, Author="Pratt, V.R.", Title="Chu Spaces: Automata with Quantum Aspects", Booktitle="Proc. Workshop on Physics and Computation (PhysComp'94)", Pages="186-195", Address="Dallas", Publisher="{IEEE}", Year=1994) Chu spaces are a recently developed model of concurrent computation extending automata theory to express branching time and true concurrency. They exhibit in a primitive form the quantum mechanical phenomena of complementarity and uncertainty. The complementarity arises as the duality of information and time, automata and schedules, and states and events. Uncertainty arises when we define a measurement to be a morphism and notice that increasing structure in the observed object reduces clarity of observation. For Chu spaces this uncertainty can be calculated in an attractively simple way directly from its dimensions.

Chu Spaces: Complementarity and Uncertainty in Rational Mechanics

@TechReport( Pr94, Author="Pratt, V.R.", Title="Chu Spaces: Complementarity and Uncertainty in Rational Mechanics", Note="Course notes, TEMPUS summer school, 35pp", Address="Budapest", Year=1994) Notes for five lectures given at the Tempus summer school, Budapest, July 1994. Topics covered: Introduction to Chu spaces. Behavior: from event structures to rational mechanics. Algebra: from linear logic to process algebra. Relational structures. Heisenberg uncertainty in Chu spaces.

Reactive, Generative and Stratified Models of Probabilistic Processes

@TechReport( GSS, Author= "Glabbeek, R.J. van and Smolka, S.A. and Steffen, B.", Title= "Reactive, Generative and Stratified Models of Probabilistic Processes", Institution="Stanford University", Type="Report", Year=1994, Note= "To appear in {\em Information and Computation}. Available by ftp from {\tt}") We introduce three models of probabilistic processes, namely, reactive, generative and stratified. These models are investigated within the context of PCCS, an extension of Milner's SCCS in which each summand of a process summation expression is guarded by a probability and the sum of these probabilities is 1. For each model we present a structural operational semantics of PCCS and a notion of bisimulation equivalence which we prove to be a congruence. We also show that the models form a hierarchy: the reactive model is derivable from the generative model by abstraction from the relative probabilities of different actions, and the generative model is derivable from the stratified model by abstraction from the purely probabilistic branching structure. Moreover the classical nonprobabilistic model is derivable from each of these models by abstraction from all probabilities.

On the Expressiveness of ACP

@InProceedings( vG94, Author= "Glabbeek, R.J. van", Title= "On the Expressiveness of {ACP} (extended abstract)", Booktitle="ACP94, Workshop on Algebra of Communicating Processes {\rm Utrecht, The Netherlands, May 1994}", Editor= "A. Ponse and C. Verhoef and S.F.M. van Vlijmen", Series= "{\em Workshops in Computing}", Publisher="Springer-Verlag", Year=1994, Pages="188-218", Note= "Available by anonymous ftp from {\tt}") De Simone showed that a wide class of languages, including CCS, SCCS, CSP and ACP, are expressible up to strong bisimulation equivalence in Meije. He also showed that every recursively enumerable process graph is representable by a Meije expression. Meije in turn is expressible in aprACP (ACP with action prefixing instead of sequential composition).

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

@Unpublished( Plo93a, Author="Plotkin, G.D.", Title="Notes on the Chu construction and Recursion", Comment="Draft Report", Month=Aug, Year=1993) We consider two kinds of recursive equations in categories of the form Chu(K,x): type equations and value equations. Throughout it is assumed that K is monoidal closed, complete and co-complete.

Notes on Event Structures and Chu

@Unpublished( Plo93a, Author="Plotkin, G.D.", Title="Notes on Event Structures and Chu", Comment="Draft Report", Month=Aug, Year=1993) We consider the relation between event structures and Chu(Set,2), particularly the full subcategory Sys of set systems.

Axiomatising ST-Bisimulation Equivalence

@InProceedings( BGG93, Author= "Busi, N. and Glabbeek, R.J. van and Gorrieri, R.", Title= "Axiomatising {ST}-Bisimulation Equivalence", Booktitle="{\rm Proceedings IFIP TC2 Working Conference on} Programming Concepts, Methods and Calculi, {\rm June 1994, San Miniato, Italy}", Editor= "E.-R. Olderog", Publisher= "North-Holland", Year= 1994, Note= "Available by anonymous ftp from {\tt}") A simple ST operational semantics for a process algebra is provided, by defining a set of operational rules in Plotkin's style. This algebra comprises TCSP parallel composition, ACP sequential composition and a refinement operator, which is used for replacing an action with an entire process, thus permitting hierarchical specification of systems. We prove that ST-bisimulation equivalence is a congruence, resorting to standard techniques on rule formats. Moreover, we provide a set of axioms that is sound and complete with respect to ST-bisimulation. The intriguing case of the forgetful refinement (i.e., when an action is refined into the properly terminated process) is dealt with in a new, improved manner.

Full Abstraction in Structural Operational Semantics

@InProceedings( vG93d, Author="Glabbeek, R.J. van", Title="Full Abstraction in Structural Operational Semantics (extended abstract)", Booktitle="{\rm Proceedings of the Third International Conference on} Algebraic Methodology and Software Technology (AMAST'93), {\rm Twente, The Netherlands, June 1993}", Editor="M. Nivat and C. Rattray and T. Rus and G. Scollo", Publisher="Springer-Verlag", Series="Workshops in Computing", Pages="77-84", Year=1993, Note="Available by anonymous ftp from {\tt}") This paper explores the connection between semantic equivalences for concrete sequential processes, represented by means of transition systems, and formats of transition system specifications using Plotkin's structural approach. For several equivalences in the linear time - branching time spectrum a format is given, as general as possible, such that this equivalence is a congruence for all operators specifiable in that format. And for several formats it is determined what is the coarsest congruence with respect to all operators in this format that is finer than partial or completed trace equivalence.

Gates Accept Concurrent Behavior

@InProceedings( GP93, Author="Gupta, V. and Pratt, V.R.", Title="Gates Accept Concurrent Behavior", Booktitle="Proc. 34th Ann. IEEE Symp. on Foundations of Comp. Sci.", Pages="62-71", Month=Nov, Year=1993) We represent concurrent processes as Boolean propositions or gates, cast in the role of acceptors of concurrent behavior. This properly extends other mainstream representations of concurrent behavior such as event structures, yet is defined more simply. It admits an intrinsic notion of duality that permits processes to be viewed as either schedules or automata. Its algebraic structure is essentially that of linear logic, with its morphisms being consequence-preserving renamings of propositions, and with its operations forming the core of a natural concurrent programming language.

Concurrent Kripke Structures

@InProceedings( Gup93, Author="Gupta, V.", Title="Concurrent Kripke Structures", Booktitle="Proceedings of the North American Process Algebra Workshop, Cornell CS-TR-93-1369", Month=Aug, Year=1993) We consider a class of Kripke Structures in which the atomic propositions are events. This enables us to represent worlds as sets of events and the transition and satisfaction relations of Kripke structures as the subset and membership relations on sets. We use this class, called event Kripke structures, to model concurrency. The obvious semantics for these structures is a true concurrency semantics. We show how several aspects of concurrency can be easily defined, and in addition get distinctions between causality and enabling, and choice and nondeterminism. We define a duality for event Kripke structures, and show how this duality enables us to convert between imperative and declarative views of programs, by treating states and events on the same footing. We provide pictorial representations of both these views, each encoding all the information to convert to the other.

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?

@InCollection( vG93c, Author= "Glabbeek, R.J. van", Title= "What is branching time semantics and why use it?", Booktitle="The Concurrency Column", Editor= "M. Nielsen", Series= "Bulletin of the EATCS", Year= 1994, Pages= "190-198", Note= "Also available as Report STAN-CS-93-1486, Stanford University, 1993, and by ftp from {\tt}") The concept of branching time in the semantics of concurrent systems is well known and well understood. Still a formal definition of what it means for a model or equivalence to respect branching time has never explicitly been given. This note proposes such a definition. Additionally the opportunity is taken to voice an old but poorly understood argument for using branching time semantics instead of models or equivalences that are fully abstract with respect to some notion of observability.

The Second Calculus of Binary Relations

@InProceedings( Pr93b, Author="Pratt, V.R.", Title="The Second Calculus of Binary Relations", Booktitle="MFCS'93, Gda{\'{n}}sk", Pages="142-155", Address="Poland", Year=1993) We view the Chu space interpretation of linear logic as an alternative interpretation of the language of the Peirce calculus of binary relations. Chu spaces amount to K-valued binary relations, which for K=2^n we show generalize n-ary relational structures. We also exhibit a four-stage unique factorization system for Chu transforms that illuminates their operation.

The linear time -- branching time spectrum II

@TechReport( vG93b, Author= "Glabbeek, R.J. van", Title= "The linear time -- branching time spectrum {II}; the semantics of sequential systems with silent moves", Institution="Stanford University", Year=1993, Note= "Extended abstract in E. Best, editor: Proceedings {\em CONCUR'93}, Hildesheim, Germany, August 1993, LNCS 715, Springer-Verlag, 1993, pp. 66--81. Preliminary version available from {\tt}") This paper studies semantic equivalences and preorders for sequential systems with silent moves, restricting attention to the ones that abstract from successful termination, stochastic and real-time aspects of the investigated systems, and the structure of the visible actions systems can perform. It provides a parameterized definition of a such a preorder, such that most such preorders and equivalences found in the literature are obtained by a suitable instantiation of the parameters. Other instantiations yield preorders that combine properties from various semantics. Moreover, the approach shows several ways in which preorders that were originally only considered for systems without silent moves, most notably the ready simulation, can be generalized to an abstract setting. All preorders come with---or rather as---a modal characterization, and when possible also a relational characterization. Moreover they are motivated by means of an (also parameterized) testing scenario, phrased in terms of `button pushing experiments' on generative and reactive machines. The testing scenarios for branching bisimulation, eta-bisimulation and coupled simulation and the corresponding modal characterizations are especially new.

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

@InProceedings( vG93a, Author= "Glabbeek, R.J. van", Title= "A complete axiomatization for branching bisimulation congruence of finite-state behaviours", Booktitle="{\rm Proceedings} Mathematical Foundations of Computer Science 1993 (MFCS), {\rm Gdansk, Poland, August/September 1993}", Editor= "A.M. Borzyszkowski and S. Soko\l owski", Pages="473-484", Series= "LNCS", Volume=711, Publisher="Springer-Verlag", Year=1993, Note="Available by anonymous ftp from {\tt}") This paper offers a complete inference system for branching bisimulation congruence on a basic sublanguage of CCS for representing regular processes with silent moves. Moreover, complete axiomatizations are provided for the guarded expressions in this language, representing the divergence- free processes, and for the recursion-free expressions, representing the finite processes. Furthermore it is argued that in abstract interleaving semantics (at least for finite processes) branching bisimulation congruence is the finest reasonable congruence possible.

Linear Logic for Generalized Quantum Mechanics

@InProceedings( Pr93a, Author="Pratt, V.R.", Title="Linear Logic for Generalized Quantum Mechanics", Booktitle="Proc. Workshop on Physics and Computation (PhysComp'92)", Address="Dallas", Publisher="{IEEE}", Pages="166-180", Year=1993) Quantum logic is static, describing automata having uncertain states but no state transitions and no Heisenberg uncertainty tradeoff. We cast Girard's linear logic in the role of a dynamic quantum logic, regarded as an extension of quantum logic with time nonstandardly interpreted over a domain of linear automata and their dual linear schedules. In this extension the uncertainty tradeoff emerges via the ``structure veil.'' When VLSI shrinks to where quantum effects are felt, their computer-aided design systems may benefit from such logics of computational behavior having a strong connection to quantum mechanics.

The Duality of Time and Information

@InProceedings( Pr92e, Author="Pratt, V.R.", Title="The Duality of Time and Information", Booktitle="Proc. of CONCUR'92", Pages="237-253", Publisher="Springer-Verlag", Address="Stonybrook, New York", Month=Aug, Year=1992) The states of a computing system bear information and change time, while its events bear time and change information. We develop a primitive algebraic model of this duality of time and information for rigid local computation, or straightline code, in the absence of choice and concurrency, where time and information are linearly ordered. This shows the duality of computation to be more fundamental than the logic of computation for which choice is disjunction and concurrency conjunction.

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

@Article( Zh92a, Author="Zhang, Guo-Qiang", Title="Some Monoidal Closed Categories of Stable Domains and Event Structures", Journal="Mathematical Structures in Computer Science", Year=1992(to appear)) This paper introduces the following new constructions on stable domains and event structures: the tensor product, the linear function space, and the exponential. It results in a monoidal closed category of dI-domains as well as one of stable event structures which can be used to interpret intuitionistic linear logic. Finally, the usefulness of the category of stable event structures for modeling concurrency and its relation to other models is discussed.

Disjunctive Systems and L-Domains

@InProceedings( Zh92b, Author="Zhang, Guo-Qiang", Title="Disjunctive Systems and L-Domains", Booktitle="International Colloquium on Automata, Languages, and Programming", Address="Wien, Austria", Year=1992) Disjunctive systems are a representation of L-domains. They use sequents of the form X|-Y, with X finite and Y pairwise disjoint. We show that for any disjunctive system, its elements ordered by inclusion form an L-domain. On the other hand, via the notion of stable neighborhoods, every L-domain can be represented as a disjunctive system. More generally, we have a categorical equivalence between the category of disjunctive systems and the category of L-domains. A natural classification of domains is obtained in terms of the style of the entailment: when |X| = 2 and |Y| = 0, disjunctive systems determine coherent spaces; when |Y| <= 1 they represent Scott domains; when either |X| = 1 or |Y| = 0 the associated cpos are distributive Scott domains; and finally, without any restriction, disjunctive systems give rise to L-domains.

A Roadmap of Some Two-Dimensional Logics

@InProceedings( Pr92c, Author="Pratt, V.R.", Title="A Roadmap of Some Two-Dimensional Logics", Booktitle="Logic and Information Flow (Amsterdam 1992)", Editor="Van Eijck, J. and Visser, A.", Pages="149-162", Publisher="MIT Press", Address="Cambridge, MA", Year="1994") We define the notion of two-dimensional logic and diagram the relative locations of a number of such.

Origins of the Calculus of Binary Relations

@InProceedings( Pr92b, Author="Pratt, V.R.", Title="Origins of the Calculus of Binary Relations", Booktitle="Proc. 7th Annual IEEE Symp. on Logic in Computer Science", Address="Santa Cruz, CA", Month=Jun, Pages="248-254", Year=1992) The calculus of binary relations was introduced by De Morgan in 1860, and was subsequently greatly developed by Peirce and Schroeder. Half a century later Tarski, J'onsson, Lyndon, and Monk further developed the calculus from the perspective of modern model theory.

Dynamic Algebras: Examples, Constructions, Applications

@Article( Pr92d, Author="Pratt, V.R.", Title="Dynamic Algebras: Examples, Constructions, Applications", Journal="Studia Logica", Volume=50, Number="3/4", Pages="571-605", Year=1992) Dynamic algebras combine the classes of Boolean (B + ' 0) and regular (R U ; *) algebras into a single finitely axiomatized variety (B R <>) resembling an R-module with ``scalar'' multiplication <>. The basic result is that * is reflexive transitive closure, contrary to the intuition that this concept should require quantifiers for its definition. Using this result we give several examples of dynamic algebras arising naturally in connection with additive functions, binary relations, state trajectories, languages, and flowcharts. The main result is that free dynamic algebras are residually finite (i.e. factor as a subdirect product of finite dynamic algebras), important because finite separable dynamic algebras are isomorphic to Kripke structures. Applications include a new completeness proof for the Segerberg axiomatization of propositional dynamic logic, and yet another notion of regular algebra. (This is the published version of an MIT Tech Report that appeared in July 1979. It saw the light of publication only at the insistence of Istvan Nemeti and Hajnal Andreka.)

Arithmetic + Logic + Geometry = Concurrency

@InProceedings( Pr92a, Author="Pratt, V.R.", Title="Arithmetic + Logic + Geometry = Concurrency", Booktitle="Proc. First Latin American Symposium on Theoretical Informatics, LNCS 583", Pages="430-447", Publisher="Springer-Verlag", Address="Sao Paulo, Brazil", Month=Apr, Year=1992) We relate the arithmetic of concurrent schedules to the higher-dimensional cellular geometry of concurrent automata using the logic of their Birkhoff-Stone duality. This collects and unifies ideas from several of the author's previous papers.

Metric Process Models

@PhDThesis( Cre91, Author="Roger Crew", Title="Metric Process Models", School="Stanford University", Month=Dec, Year=1991) Among the various formal models proposed to provide semantics for concurrency constructs in programming languages, partial orders have the advantages of conceptual simplicity, mathematical tractability, and economy of expression. We first observe that the theory of enriched categories supplies a natural abstraction of the notion of partial order, the D-schedule. Varying the choice of temporal domain D allows for other forms of temporal constraint beyond that available from simple ordering. For example, having the constraints on inter-event delays be numeric bounds produces a generalized metric-space structure suitable for the discussion of real-time computation. We then construct an algebra of processes parametrized by notion of time. Here a process is a structure based on schedules that also incorporates nondeterminism. Since the model is category-based, we can define operations on D-schedules and processes via universal constructions that depend little on the choice of D. Also, given a suitable choice of process structure and process morphism, the constructions used for process operations and schedule operations are remarkably similar.

Interleaving Semantics and Action Refinement with Atomic Choice

@InProceedings( CGG92, Author="Czaja, I. and Glabbeek, R.J. van and Goltz, U.", Year=1992, Title="Interleaving Semantics and Action Refinement with Atomic Choice", Booktitle="Advances in Petri Nets 1992", Editor="G. Rozenberg", Series="LNCS", Volume=609, Publisher="Springer-Verlag", Pages="89-107", Note="Available by anonymous ftp from {\tt}") We investigate how to restrict the concept of action refinement such that established interleaving equivalences for concurrent systems are preserved under these restricted refinements. We show that interleaving bisimulation is preserved under refinement if we do not allow to refine action occurrences deciding choices and action occurrences involved in autoconcurrency. On the other hand, interleaving trace equivalence is still not preserved under these restricted refinements.

On the Specification of Concurrent Systems

@PhDThesis( Cas91, Author="Ross Casley", Title="On the Specification of Concurrent Systems", School="Stanford University", Month=Jan, Year=1991) In models of concurrent processes constraints on the order of events are often represented by partial orders, and schedules of events are then defined using an algebra of standard operations such as sequential and parallel composition.

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

@InProceedings( Pr91b, Author="Pratt, V.R.", Title="Event Spaces and Their Linear Logic", Booktitle="AMAST'91: Algebraic Methodology and Software Technology", Publisher="Springer-Verlag", Series="Workshops in Computing", Pages="1-23", Address="Iowa City", Year=1992) Boolean logic treats disjunction and conjunction symmetrically and algebraically. The corresponding operations for computation are respectively nondeterminism (choice) and concurrency. Petri nets treat these symmetrically but not algebraically, while event structures treat them algebraically but not symmetrically.

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

@InProceedings( Pr91a, Author="Pratt, V.R.", Title="Modeling Concurrency with Geometry", Booktitle="Proc. 18th Ann. ACM Symposium on Principles of Programming Languages", Pages="311-322", Month=Jan, Year=1991) Branching time and causality find their respective homes in the Birkhoff-dual models of automata and schedules. This creates a puzzle: if the duality is supposed to make the models completely equivalent then why does each phenomenon have a preferred side? We identify dimension as the culprit: 1-dimensional automata are skeletons permitting only interleaving concurrency, true n-fold concurrency resides in transitions of dimension n. The Birkhoff dual of a poset then becomes a simply-connected space. We distinguish Birkhoff duality from Stone duality and treat the former in detail from a concurrency perspective. We introduce true nondeterminism and define it as monoidal homotopy; from this perspective nondeterminism in ordinary automata arises from forking and joining creating nontrivial homotopy. We propose a formal definition of higher dimensional automaton as an n-complex or n-category, whose two essential axioms are associativity of concatenation within dimension and an interchange principle between dimensions.

Action Logic and Pure Induction

@InProceedings( Pr90b, Author="Pratt, V.R.", Title="Action Logic and Pure Induction", Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478", Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120", Address="Amsterdam, NL", Month=Sep, Year=1990) In Floyd-Hoare logic programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a -> b (HAD a THEN b) and postimplication b <- a (b IF-EVER a). Unlike REG, ACT is finitely based, makes a* reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a -> a)* = a -> a.

Temporal Structures

@Article( CCMP, Author="Casley, R.T and Crew, R.F. and Meseguer, J. and Pratt, V.R.", Title="Temporal Structures", Journal="Math. Structures in Comp. Sci.", Volume=1, Number=2, Pages="179-213", Month=Jul, Year=1991) We combine the principles of the Floyd-Warshall-Kleene algorithm, enriched categories, and Birkhoff arithmetic, to yield a useful class of algebras of transitive vertex-labeled spaces. The motivating application is a uniform theory of abstract or parametrized time in which to any given notion of time there corresponds an algebra of concurrent behaviors and their operations, always the same operations but interpreted automatically and appropriately for that notion of time. An interesting side application is a language for succinctly naming a wide range of datatypes.

Teams Can See Pomsets

Teams Can See Pomsets G. Plotkin and V. Pratt Workshop on Partial Order Methods in Verification Amer. Math. Soc., DIMACS series Vol. 29, 1997. Strings may serve as both specifications and observations of behavior. However partial strings or pomsets, superior to strings in certain respects for the representation of concurrent behavior, are provably unobservable and hence apparently suitable only for specifying behavior. The proof however tacitly assumes that observers are isolated individuals. We show that observations by a cooperating team of sequential observers agreeing on *what* happened but not *when* can distinguish all pomsets. The resolving power of a finite team increases strictly with its size k, permitting it to distinguish all pomsets of dimension (not width) k but not all of k+1. These results extend to observation of augment closed processes. As expected we depend on the now standard technique of refinement of atomic events to complex events; what is not expected is that their complexity need be only that of nondeterminism, in that we refine one atomic event to a set of alternative atomic events, not to a set of sequences.

Enriched Categories and the Floyd-Warshall Connection

@InProceedings( Pr89a, Author="Pratt, V.R.", Title="Enriched Categories and the {Floyd-Warshall} Connection", Booktitle="Proc. First International Conference on Algebraic Methodology and Software Technology", Pages="177-180", Address="Iowa City", Month=May, Year=1989) We give a correspondence between enriched categories and the Gauss-Kleene-Floyd-Warshall connection familiar to computer scientists. This correspondence shows this generalization of categories to be a close cousin to the generalization of transitive closure algorithms. Via this connection we may bring categorical and 2-categorical constructions into an active but algebraically impoverished arena presently served only by semiring constructions. We illustrate these techniques by applying them to Birkoff's poset arithmetic, interpretable as an algebra of ``true concurrency.''

Dynamic Algebras as a Well-behaved Fragment of Relation Algebras

@InProceedings( Pr90a, Author="Pratt, V.R.", Title="Dynamic Algebras as a Well-behaved Fragment of Relation Algebras", Booktitle="Algebraic Logic and Universal Algebra in Computer Science, LNCS 425", Editors="C.H. Bergman, R.D. Maddux, D.L. Pigozzi", Address="Ames, Iowa, June 1988", Pages="77-110", Publisher="Springer-Verlag", Year=1990) The varieties RA of relation algebras and DA of dynamic algebras are similar with regard to definitional capacity, admitting essentially the same equational definitions of converse and star. They differ with regard to completeness and decidability. The RA definitions that are incomplete with respect to representable relation algebras, when expressed in their DA form are complete with respect to representable dynamic algebras. Moreover, whereas the theory of RA is undecidable, that of DA is decidable in exponential time. These results follow from representability of the free intensional dynamic algebras.

Modeling Concurrency with Partial Orders

@Article( Pr86, Author="Pratt, V.R.", Title="Modeling Concurrency with Partial Orders", Journal="Int. J. of Parallel Programming", Volume=15, Number=1, Pages="33-71", Month=Feb, Year=1986) Concurrency has been expressed variously in terms of formal languages (typically via the shuffle operator), partial orders, and temporal logic, inter alia. In this paper we extract from these three approaches a single hybrid approach having a rich language that mixes algebra and logic and having a natural class of models of concurrent processes. The heart of the approach is a notion of partial string derived from the view of a string as a linearly ordered multiset by relaxing the linearity constraint, thereby permitting partially ordered multisets or pomsets. Just as sets of strings form languages, so do sets of pomsets form processes. We introduce a number of operations useful for specifying concurrent processes and demonstrate their utility on some basic examples. Although none of the operations is particularly oriented to nets it is nevertheless possible to use them to express processes constructed as a net of subprocesses, and more generally as a system consisting of components. The general benefits of the approach are that it is conceptually straightforward, involves fewer artificial constructs than many competing models of concurrency, yet is applicable to a considerably wider range of types of systems, including systems with buses and ethernets, analog systems, and real-time systems.

Two Easy Theories whose Combination is Hard

@Unpublished( Pr77, Author="Pratt, V.R.", Title="Two Easy Theories whose Combination is Hard", Comment="Memo sent to Nelson and Oppen concerning a preprint of their paper", Month=Sep, Year=1977) We restrict attention to the validity problem for unquantified disjunctions of literals (possibly negated atomic formulae) over the domain of integers, or what is just as good, the satisfiability problem for unquantified conjunctions. When = is the only predicate symbol and all function symbols are left uninterpreted, or when <= is the only predicate symbol (taking its standard interpretation on the integers) and the only terms are variables and integers, then satisfiability is decidable in polynomial time. However when <= and uninterpreted function symbols are allowed to appear together, satisfiability becomes an NP-complete problem. This combination of the two theories can arise for example when reasoning about arrays (the uninterpreted function symbols) and subscript manipulation (where <= arises in considering subscript bounds). These results are unaffected by the presence of successor, which also arises commonly in reasoning about subscript manipulation.

A Decidable Mu-Calculus

@InProceedings( Pr81b, Author="Pratt, V.R.", Title="A Decidable Mu-Calculus", Booktitle="Proc. 22nd IEEE Conference on Foundations of Computer Science", Month=Oct, Year=1981, Pages="421-427") We describe a mu-calculus which amounts to modal logic plus a minimization operator, and show that its satisfiability problem is decidable in exponential time. This result subsumes corresponding results for propositional dynamic logic with test and converse, thus supplying a better setting for those results. It also encompasses @InProceedings( Pr76, Author="Pratt, V.R.", Title="Semantical Considerations on {Floyd}-{Hoare} Logic", BookTitle="Proc. 17th Ann. IEEE Symp. on Foundations of Comp. Sci.", Pages="109-121", Month=Oct, Year=1976) This paper deals with logics of programs. The objective is to formalize a notion of program description and to give both plausible (semantic) and effective (syntactic) criteria for the notion of truth of a description. A novel feature of this treatment is the development of the mathematics underlying Floyd-Hoare axiom systems independently of such systems. Other directions that such research might take are also considered. This paper grew out of, and is intended to be usable as, class notes for an introductory semantics course.