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 EMAIL@cs.stanford.edu
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)
ABSTRACTS
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 http://boole.stanford.edu/\-pub/\-winter.ps.gz}")
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
http://boole.stanford.edu/\-pub/\-delta.ps.gz}")
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.
Bisimulation
@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 http://boole.stanford.edu/\-pub/\-bis.ps.gz}", 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 http://boole.stanford.edu/pub/lics2000.ps.gz}")
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 http://boole.stanford.edu/\-pub/\-spectrum1.ps.gz}")
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 http://boole.stanford.edu/\-pub/\-concur99.ps.gz}")
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 http://boole.stanford.edu/pub/fullchu.ps.gz}")
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 ftp://boole.stanford.edu/\-pub/\-bisimpi.ps.gz}")
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 ftp://boole.stanford.edu/\-pub/\-flat.ps.gz}")
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 ftp://boole.stanford.edu/pub/tool.ps.gz}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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 Boole.stanford.edu}")
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.