Papers on Foundations of Concurrency
	                Available for Download
	                from Boole.Stanford.EDU

===========================================================================
This ASCII file gives only the basic details: title, citation, and
abstract, in reverse chronological order.

For papers on Chu spaces, organized by topic instead of date, start
instead with

	http://boole.stanford.edu/chuguide.html

This is a web page that organizes those abstracts below that bear on
Chu spaces into four categories, Introductory, Applications, Technical
Notes, and Prehistory.  The abstracts in the present file are listed in
reverse chronological order, which is not the most convenient
organization for browsing.
===========================================================================

This file is ABSTRACTS in the /pub directory of Boole.Stanford.EDU,
36.8.0.65, accessible as

	http://boole.stanford.edu/pub/ABSTRACTS

The pub directory is for distribution of prepublications in the area of
foundations of concurrency.  It is run by the Stanford Concurrency
Group, whose home is the Theory Division, Computer Science Department,
Stanford University.  The group consists of the following people.

	Rob van Glabbeek		rvg@cs.stanford.edu
	Dominic Hughes			dominic@cs.stanford.edu
	Gordon Plotkin (summers)	gdp@cs.stanford.edu
	Vaughan Pratt (group leader)	pratt@cs.stanford.edu
	Maggie McLoughlin (secretary)	maggiemc@cs.stanford.edu

==========================Instructions=================================

The abstracts of papers on this site may be viewed at

	http://boole.stanford.edu/pub/ABSTRACTS  

Papers are retrieved by their one-word name, e.g. seqcon, by downloading

	http://boole.stanford.edu/pub/seqcon.ps.gz

To retrieve the DVI or TEX versions, which are available for almost all
papers on this site, download the appropriate one of

	http://boole.stanford.edu/pub/DVI/seqcon.dvi.gz
	http://boole.stanford.edu/pub/TEX/seqcon.tex.gz

These are gzipped (compressed) files and will normally need to be
"gunzipped" with the gunzip command.  (Caveat: under some circumstances
Netscape will gunzip the file automatically without notification and
without removing the .gz suffix, which can be confusing.)

PROBLEMS.  If you have problems in either retrieving or compiling
papers, please contact any group member listed above.

This page is no longer updated.
More recent information is available on our homepages:
<listing>
        <A HREF=http://theory.stanford.edu/~rvg/>Rob van Glabbeek</A> (<A HREF=http://theory.stanford.edu/~rvg/papers.html>papers</A>, <A HREF=http://theory.stanford.edu/~rvg/abstracts.html>abstracts</A>, references in <A HREF=http://theory.stanford.edu/~rvg/glabbeek.bib>bibtex</A> and <A HREF=http://theory.stanford.edu/~rvg/glabbeek.pdf>pdf</A>)
        <A HREF=http://boole.stanford.edu/~dominic/>Dominic Hughes</A> (<A HREF=http://boole.stanford.edu/~dominic/papers/>selected papers</A>)
        <A HREF=http://www.inf.ed.ac.uk/people/staff/Gordon_Plotkin.html>Gordon Plotkin</A> (<A HREF=http://homepages.inf.ed.ac.uk/gdp/publications/>papers available online</A>)
        <A HREF=http://boole.stanford.edu/pratt.html>Vaughan Pratt</A> (<A HREF=http://boole.stanford.edu/prattpubs.html>papers</A>; <A HREF=http://boole.stanford.edu/prattpubs.pdf>references.pdf</A>)
</listing>
===========================Available papers=================================

TITLES

resolv      Event Structures for Resolvable Conflict
nested	    Nested Semantics over Finite Trees are Equationally Hard
negative2   Meaning of Negative Premises in Transition System Specifications II
bundle	    Bundle Event Structures and CCSP
hml	    Compositionality of Hennessy-Milner Logic through SOS
mallnets-lics-with-proofs    Proof Nets for Unit-free Multiplicative-Additive Linear Logic (extended abstract)
query	    Query Nets: Interacting Workflow Modules for Global Termination
concur02    Event-State Duality: The Enriched Case
seqconc     Transition and Cancellation in Concurrency and Branching Time
winter	    Precongruence Formats for Decorated Trace Semantics
token       Token-controlled place refinement in hierarchical Petri nets
delta	    Well-behaved Flow Event Structs for Par'l Composition & Action Refinement
continuum   The continuum as a final coalgebra
bridge      Chu spaces as a semantic bridge between linear logic and mathematics
sg	    Software Geography: Physical and Economic Aspects
ortho       Orthocurrence as both Interaction and Observation
bis	    Bisimulation
lics2000    Precongruence Formats for Decorated Trace Preorders
spectrum1   The Linear Time--Branching Time Spectrum I
hda	    Higher dimensional automata revisited
concur99    Petri Nets, Config'n Structures and Higher Dimensional Automata
fullchu	    Full completeness of the multiplicative linear logic of Chu spaces
coimbra	    Chu Spaces (Coimbra notes)
refinement  Refinement of Actions and Equivalence Notions for Concurrent Systems
sa	    Scheduling Algebra
smallgp     On the Representation of Abelian Groups as Chu Spaces
tap	    Types as Processes, via Chu spaces
parikh	    Chu spaces from the representational viewpoint
fcllchu	    Towards Full Completeness for the Linear Logic of Chu Spaces
bisimpi     Bisimulation and Propositional Intuitionistic Logic
flat	    Axiomatizing Flat Iteration
tool	    Branching Bisimulation as a Tool in the Analysis of Weak Bisimul'n
prefix	    Axiomatizing Prefix Iteration with Silent Steps
reshda	    Reconciling Event Structures and Higher Dimensional Automata
broadll     Broadening the denotational semantics of linear logic
llcocl	    Linear Logic complements Classical Logic
embed       Chu realizes all small concrete categories
chuconc     Chu Spaces and their Interpretation as Concurrent Objects
conf	    Configuration Structures
gamut       The Stone Gamut: A Coordinatization of Mathematics
negative    The Meaning of Negative Premises in Transition System Spec'ns II
tree        Ntyft/ntyxt Rules Reduce to Ntree Rules
anapent     Anatomy of the Pentium Bug
ratmech     Rational Mechanics and Natural Mathematics
tppp        Time and Information in Sequential and Concurrent Computation
uni         Shorter proof of universality of Chu spaces
gupthes     Chu Spaces: A Model of Concurrency
ph94        Chu Spaces: Automata with Quantum Aspects
bud         Chu Spaces: Complementarity and Uncertainty in Rational Mechanics
prob        Reactive, Generative & Stratified Models of Probabilistic Processes
acp         On the Expressiveness of ACP
gdp.dvi     Notes on the Chu construction and Recursion
gdp2.dvi    Notes on Event Structures and Chu
axiomst     Axiomatising ST-Bisimulation Equivalence
sos         Full Abstraction in Structural Operational Semantics
gates       Gates Accept Concurrent Behavior
cks         Concurrent Kripke Structures
branch      What is branching time and why to use it
scbr        The Second Calculus of Binary Relations
spectrum    The linear time - branching time spectrum II
complete    A complete ax'n for branching bisim. cong. of fin.state behaviours
ql          Linear Logic for Generalized Quantum Mechanics
dti         The Duality of Time and Information
ldomain     Disjunctive Systems and L-Domains
monoidal    Some Monoidal Closed Categories of Stable Domains & Event Struct's
twod        A Roadmap of Some Two-Dimensional Logics
ocbr        Origins of the Calculus of Binary Relations
dalg        Dynamic Algebras: Examples, Constructions, Applications
algecon     Arithmetic + Logic + Geometry = Concurrency
crewthes    Metric Process Models
atch        Interleaving Semantics and Action Refinement with Atomic Choice
casthes     On the Specification of Concurrent Systems
es          Event Spaces and their Linear Logic
cg          Modeling Concurrency with Geometry
jelia       Action Logic and Pure Induction
man         Temporal Structures
pp2         Teams Can See Pomsets
am4         Enriched Categories and the Floyd-Warshall Connection
iowatr      Dynamic Algebras as a well-behaved fragment of Relation Algebras
lics87      Partial Order Models of Concurrency and the Computation of Functions
ijpp        Modelling Concurrency with Partial Orders
sefnp       Two Easy Theories whose Combination is Hard
modalmu81   A Decidable Mu-Calculus
amlp        Application of Modal Logic to Programming
pdmpdf      A Practical Decision Method for Propositional Dynamic Logic
semcon      Semantical Considerations on Floyd-Hoare Logic

-----------------------------------------------------------------------

ABSTRACTS

resolv

	@InProceedings(
GP04,	Author="Glabbeek, R.J. van and Plotkin, G.D.",
	Title ="Event Structures for Resolvable Conflict",
	Editor="Vaclav Koubek and Jan Kratochvil",
	Booktitle="{\rm Proceedings $29^{th}$ International Symposium on}
	Mathematical Foundations of Computer Science, {\rm MFCS 2004,
	Prague, Czech Republic, August 2004}",
	Series="LNCS", Publisher="Springer", Year=2004,
	Note="Available at {\tt http://boole.stanford.edu/\-pub/\-resolv.ps.gz}",)

We propose a generalisation of Winskel's event structures, matching
the expressive power of arbitrary Petri nets. In particular, our event
structures capture resolvable conflict, besides disjunctive and
conjunctive causality.


nested

        @TechReport(
AFGI03, Author="L. Aceto and W.J. Fokkink and Glabbeek, R.J. van and
                A. Ing{\'o}lfsd{\'o}ttir",
        Title ="Nested Semantics over Finite Trees are Equationally Hard",
        Institution="Department of Computer Science, University of Aarhus",
        Year=2003, Type="{BRICS} report", Number="RS-03-27", Address="Denmark",
        Month=Aug, Note="Available at {\tt
                http://boole.stanford.edu/\-pub/\-nested.ps.gz}")

This paper studies nested simulation and nested trace semantics over
the language BCCSP, a basic formalism to express finite process
behaviour. It is shown that none of these semantics affords finite
(in)equational axiomatizations over BCCSP. In particular, for each of
the nested semantics studied in this paper, the collection of sound,
closed (in)equations over a singleton action set is not finitely
based.


negative2

        @Article(
vG04,   Author="Glabbeek, R.J. van",
        Title ="The Meaning of Negative Premises in Transition System
                Specifications {II}",
        Journal="Journal of Logic and Algebraic Programming",
        Year=2004, Volume="to appear", Note="Available at {\tt
        http://boole.stanford.edu/\-pub/\-negative2.ps.gz}.
        Extended abstract in F. Meyer auf der Heide \& B. Monien, editors:
        Proceedings 23$^{\it th}$ International Colloquium on {\em Automata,
        Languages and Programming}, ICALP '96, Paderborn, Germany, July 1996,
        LNCS 1099, Springer, pp. 502--513")

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. Additionally, this paper contributes a proof theoretic
characterisation of the well-founded semantics for logic programs.


bundle

        @InProceedings(
GV03,   Author="Glabbeek, R.J. van and F.W. Vaandrager",
        Title ="Bundle Event Structures and {CCSP}",
        Booktitle="{\rm Proceedings} CONCUR 2003, {\rm 14$^{\it th}$
                  International Conference on} Concurrency Theory, {\rm
		  Marseille, France, September 2003}", Year=2003,
        Editor="R. Amadio and D. Lugiez",
        Publisher="Springer", Series="LNCS", Volume=2761, Pages="57--71",
        Note="Available at {\tt http://boole.stanford.edu/\-pub/\-bundle.ps.gz}")

We investigate which event structures can be denoted by means of
closed CCS + CSP expressions. Working up to isomorphism we find that
* all denotable event structures are bundle event structures, 
* upon adding an infinitary parallel composition all bundle event structures are denotable, 
* without it every finite bundle event structure can be denoted, 
* as well as every countable prime event structure with binary conflict. 
Up to hereditary history preserving bisimulation equivalence finitary
conflict can be expressed in terms of binary conflict. In this setting
all countable stable event structures are denotable.


hml

        @InProceedings(
FGW03,  Author="W.J. Fokkink and Glabbeek, R.J. van and Wind, P. de",
        Title ="Compositionality of {Hennessy-Milner} Logic through
		Structural Operational Semantics",
        Booktitle="{\rm Proceedings 14th International Symposium on}
		Fundamentals of Computation Theory, {\rm FCT 2003,
		Malm\"o, Sweden, August 2003}", Year=2003,
        Editor="A. Lingas and B.J. Nilsson",
        Publisher="Springer", Series="LNCS", Volume=2751, Pages="412--422",
        Note="Available at {\tt http://boole.stanford.edu/\-pub/\-hml.ps.gz}")

This paper presents a method for the decomposition of HML formulae. It
can be used to decide whether a process algebra term satisfies a HML
formula, by checking whether subterms satisfy certain formulae,
obtained by decomposing the original formula. The method uses the
structural operational semantics of the process algebra. The main
contribution of this paper is that an earlier decomposition method
from Larsen for the De Simone format is extended to the more general
ntyft/ntyxt format without lookahead.


mallnets-lics-with-proofs

        @InProceedings(
HG03,   Author="Hughes, D. and Glabbeek, R.J. van",
        Title ="Proof Nets for Unit-free Multiplicative-Additive Linear Logic
                (extended abstract)",
        Booktitle="{\rm Proceedings $18^{th}$ Annual IEEE Symposium on}
        Logic in Computer Science, {\rm LICS 2003, Ottawa, Canada, June 2003}",
        Year=2003, Publisher="IEEE Computer Society Press", Pages="1-10",
        Note="Available at {\tt
        http://boole.stanford.edu/\-pub/\-mallnets-lics-with-proofs.ps.gz}")

A cornerstone of the theory of proof nets for unit-free multiplicative
linear logic (MLL) is the abstract representation of cut-free proofs
modulo inessential commutations of rules. The only known extension to
additives, based on monomial weights, fails to preserve this key
feature: a host of cut-free monomial proof nets can correspond to the
same cut-free proof. Thus the problem of finding a satisfactory notion
of proof net for unit-free multiplicative-additive linear logic (MALL)
has remained open since the inception of linear logic in 1986. We
present a new definition of MALL proof net which remains faithful to
the cornerstone of the MLL theory.


query

        @InProceedings(
GS03,   Author="Glabbeek, R.J. van and D.G. Stork",
        Title ="Query Nets: Interacting Workflow Modules that Ensure
                Global Termination",
        Booktitle="{\rm Proceedings International Conference on} Business
                 Process Management, {\rm BPM 2003, Eindhoven, The
                 Netherlands, June 2003}",  Year=2003,
        Editor="Aalst, W.M.P. van der and Hofstede, A.H.M. ter and Weske, M.",
        Publisher="Springer", Series="LNCS", Volume=2678, Pages="184--199",
        Note="Available at {\tt http://boole.stanford.edu/\-pub/\-query.ps.gz}")

We address cross-organizational workflows, such as document workflows,
which consist of multiple workflow modules each of which can interact
with others by sending and receiving messages. Our goal is to
guarantee that the global workflow network has properties such as
termination while merely requiring properties that can be checked
locally in individual modules. The resulting query nets are based on
predicate/transition Petri nets and implement formal constructs for
business rules, thereby ensuring such global termination. Our method
does not require the notion of a global specification, as employed by
Kindler, Martens and Reisig.


concur02

        @InProceedings(
Pr02c,  Author="Pratt, V.R.",
        Title="Event-State Duality: the Enriched Case",
        Booktitle="Proc. CONCUR'02", Address="Brno", Month=Aug, Year=2002)

Enriched categories have been applied in the past to both
event-oriented true concurrency models and state-oriented information
systems, with no evident relationship between the two.  Ordinary Chu
spaces expose a natural duality between partially ordered temporal
spaces (pomsets, event structures), and partially ordered information
systems.  Barr and Chu's original definition of Chu spaces however was
for the general V-enriched case, with ordinary Chu spaces arising for
V = Set (equivalently V = Pos at least for biextensional Chu
spaces).  We extend time-information duality to the general enriched
case, and apply it to put on a common footing event structures,
higher-dimensional automata (HDAs), a cancellation-based approach to
branching time, and other models treatable by enriching either event
(temporal) space or state (information) space.


seqconc

	@Article(
Pr02a,  Author="Pratt, V.R.",
	Title="Transition and Cancellation in Concurrency and Branching Time",
	Journal="Math. Structures in Comp. Sci.",
	Volume=13, Number=4, Year=2003)

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.

        
winter

	@Article(
BFG04,  Author="B. Bloom and W.J. Fokkink and Glabbeek, R.J. van",
        Title ="Precongruence Formats for Decorated Trace Semantics",
	Journal="Transactions on Computational Logic", Publisher="ACM",
        Year = 2004, Volume = "to appear",
        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.


token

        @InProceedings(
SG02,   Author="D.G. Stork and Glabbeek, R.J. van",
        Title ="Token-controlled place refinement in hierarchical
	{Petri} nets with application to active document workflow",
        Editor="J. Esparza and C. Lakos",
        Booktitle="{\rm Proceedings $23^{rd}$ International Conference
	on} Application and Theory of Petri Nets, {\rm ICATPN 2002,
	Adelaide, Australia, June 2002}", Year=2002,
	Publisher="Springer", Series="LNCS", Volume =2360, Pages="394-413",
	Note="Available at {\tt http://boole.stanford.edu/\-pub/\-token.pdf}")

We propose extensions to predicate/transition nets to allow tokens to
carry both data and control information, where such control can refine
special "refinable place nodes" in the net. These formal extensions
find use in active document workflow, in which documents themselves
specify portions of the overall processing within a workflow net. Our
approach enables the workflow designer to specify which places of the
target predicate/transition net may be refined and enables the
document author to specify how these places will be refined (via
attachment of a token-generated "refinement net"). This apportionment
of the overall task allows the workflow designer to set general
constraints within which the document author can control the
processing; it prevents conflicts between them in foreseeable
practical cases. Refinable places are augmented with a permission
structure specifying which document authors can refine that place and
which document tokens can execute a node's refinement net. Our refined
nets have a hierarchical structure which can be represented by
bipartite trees.


delta

	@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 = {April},
	Type =	 {Braunschweiger Informatik-Berichte}, Number = {2002-01},
	Institution="Institut f{\"u}r Theoretische Informatik, Technische
	Universit{\"a}t Braunschweig", 	Address={Germany},
        Note="To appear in Theoretical Computer Science.
        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.


sg

        @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).


ortho   

	@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=Aug, 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.


bis

	@Misc(
vG00,	Author="Glabbeek, R.J. van",
	Title="Bisimulation", Year=2000,
	Howpublished="Scheduled to appear in the forgotten Encyclopedia of
        Distributed Computing (J.E. Urban \& P. Dasgupta, eds.), Kluwer.
        Available at {\tt http://boole.stanford.edu/\-pub/\-bis.ps.gz}")

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.


lics2000
 
        @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.


spectrum1

	@InCollection(
vG01,	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=2001,   pages="3--99", 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.


hda

        @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.


continuum

	@Article(
PP00,	Author="Pavlovic, D. and Pratt, V.R.",
	Title="The continuum as a final coalgebra",
	Journal=TCS, Note="Accepted for publication", Year=2000)

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.


coimbra

	@Misc(
Pr99a,	Author="Pratt, V.R.",
	Title="Chu Spaces",
	Comment="Course notes for the School in Category Theory and
	Applications",
	Address="Coimbra, Portugal", Month=Jul, 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


concur99

	@InProceedings(
vG99,	Author="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.


fullchu

	@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.}


bridge

        @Article(
Pr00,   Author="Pratt, V.R.",
        Title="Chu spaces as a semantic bridge between linear logic and
               mathematics",
        Journal="TCS", Note="Accepted for Publication", Year=2000)

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

	@Article(
GG01,	Author = "Glabbeek, R.J. van and U. Goltz",
	Title =	 "Refinement of Actions and Equivalence Notions for
	          Concurrent Systems", Note="Available at {\tt
        http://\-boole.\-stanford.edu/\-pub/\-refinement.ps.gz}",
        Journal= "Acta Informatica", Volume=37, Pages="229--327", Year=2001)

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.


sa

	@InProceedings(
GR99,	Author="Glabbeek, R.J. van and P. Rittgen",
	Title ="Scheduling Algebra",
	Booktitle="{\rm Proceedings of the $7^{th}$ International
                 Conference on} Algebraic Methodology and Software
                 Technology, {\rm AMAST'98, Amazonia, Brazil, January 1999}",
	Year=1999, Month="January", Editor="A.M. Haeberer",
	Series="LNCS", Volume=1548, Publisher="Springer", Pages="278--292")

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.


smallgp

	@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.


tap

	@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 corrrespondence are intrinsic or cultural.


parikh

        @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.


fcllchu

	@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.


bisimpi

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.


flat

	@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 at 
        {\tt http://\-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.


tool

	@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 http://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.


prefix

	@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, Note=
        "Available at {\tt http://boole.stanford.edu/\-pub/\-prefix.ps.gz}")

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.


reshda

	Reconciling Event Structures and Higher Dimensional Automata
	V.R. Pratt
	Technical Report, Stanford University, 1996

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.


broadll

	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.


llcocl

	Linear Logic complements Classical Logic
	V.R. Pratt
	To appear in preliminary proceedings of 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.


embed

	   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.


chuconc

	@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.


conf

	@InProceedings(
GP95,	Author="Glabbeek, R.J. van and Plotkin, G.D.",
	Title="Configuration Structures (extended abstract)",
	Booktitle="{\rm Proceedings $10^{th}$ Annual IEEE Symposium on}
	  Logic in Computer Science, {\rm LICS'95, San Diego, USA, June 1995}",
	Editor="D. Kozen", Month="June", Pages = "199-209",
	Publisher="IEEE Computer Society Press", Year="1995",
	Note="Available at {\tt http://boole.stanford.edu/pub/conf.ps.gz}")

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.


gamut

	@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.


negative

	@Techreport(
vG95,	Author=	"Glabbeek, R.J. van",
	Title=	"The Meaning of Negative Premises in Transition System
		 Specifications {II}", Month=Feb, Year=1995, 
	Institution="Stanford University", Number="STAN-CS-TN-95-16",
	Note="Available at {\tt http://boole.stanford.edu/pub/negative.ps.gz}.
	Extended abstract in F. Meyer auf der Heide \& B. Monien, editors:
	Proceedings 23$^{\it th}$ International Colloquium on {\em Automata,
	Languages and Programming}, ICALP '96, Paderborn, Germany, July 1996,
	LNCS 1099, Springer, pp. 502--513")

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.


tree

	@Article(
FG96,	Author=	"Fokkink, W.J. and Glabbeek, R.J. van",
	Title=	"Ntyft/ntyxt Rules Reduce to Ntree Rules", 
	Journal="Information and Computation",
	Volume=126, Number=1, Pages="1-10", Year=1996,
        Note="Available at {\tt http://boole.stanford.edu/\-pub/\-tree.ps.gz}")

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.


anapent

	@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. 


ratmech

	@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.


tppp

	@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.


uni

	@Note(
Pr94a,  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.


gupthes   

	@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.


ph94

	@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.


bud

	@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.


prob

	@Article(
GSS,	Author= "Glabbeek, R.J. van and Smolka, S.A. and Steffen, B.",
	Title=  "Reactive, Generative, and Stratified Models of
	Probabilistic Processes", Journal="Information and Computation",
	Volume=121, Number=1, Pages="59-80", Year=1995,
	Note=	"Available at {\tt http://boole.stanford.edu/pub/prob.ps.gz}")

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.


acp

	@InProceedings(
vG94,	Author=	"Glabbeek, R.J. van",
	Title=	"On the Expressiveness of {ACP} (extended abstract)",
        Booktitle="{\rm Proceedings First Workshop on the} Algebra of
                 Communicating Processes, {\rm ACP94, Utrecht, The
                 Netherlands, May 1994}",
	Editor= "A. Ponse and C. Verhoef and S.F.M. van Vlijmen",
	Series= "{\em Workshops in Computing}",
	Publisher="Springer", Year=1994, Pages="188-218",
	Note=	"Available at {\tt http://boole.stanford.edu/pub/acp.ps.gz}")

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.


gdp

	@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.


gdp2

	@Unpublished(
Plo93b,	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.


axiomst

	@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",
        Series="IFIP Transactions A-56", Publisher="North-Holland", Year= 1994,
	Note= "Available at {\tt http://boole.stanford.edu/pub/axiomst.ps.gz}")

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.


sos   

	@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", Series="Workshops in Computing",
	Pages="77-84", Year=1993, 
	Note=	"Available at {\tt http://boole.stanford.edu/pub/sos.ps.gz}")

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

	@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.


cks

	@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.


branch

	@InCollection(
vG01a,	Author=	"Glabbeek, R.J. van",
	Title=	"What is branching time semantics and why to use it?",
	Booktitle="Current Trends in Theoretical Computer Science;
                 Entering the 21st Century", Publisher="World Scientific",
        Editor= "G. Paun and G. Rozenberg and A. Salomaa", Year=2001,
        Note="Also available as Report STAN-CS-93-1486, Stanford
        University, 1993, at {\tt http://theory.stanford.edu/\-branching/},
        and in M.~Nielsen, editor: {\em The Concurrency Column},
        {\em Bulletin of the EATCS} 53, 1994, pp. 190--198",)

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.


scbr

	@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.


spectrum
spectrum.A4

	@Misc(
vG93b,	Author=	"Glabbeek, R.J. van",
	Title=	"The linear time -- branching time spectrum {II};
		 the semantics of sequential systems with silent moves",
        Howpublished="Manuscript. Preliminary version available at {\tt
                 http://boole.stanford.edu/\-pub/\-spectrum.ps.gz}",
	Year=1993, Note="Extended abstract in E. Best, editor: Proceedings
                 {\em CONCUR'93}, 4$^{\it th}$ International Conference on
                 {\em Concurrency Theory}, Hildesheim, Germany, August 1993,
                 LNCS 715, Springer, pp. 66--81")

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.


complete

	@InProceedings(
vG93a,	Author=	"Glabbeek, R.J. van",
	Title=	"A complete axiomatization for branching bisimulation
		 congruence of finite-state behaviours",
	Booktitle="{\rm Proceedings 18$^{\it th}$ International Symposium
                 on} Mathematical Foundations of Computer Science, {\rm
                 MFCS '93, Gdansk, Poland, August/September 1993}",
	Editor=	"A.M. Borzyszkowski and S. Soko\l owski",    Pages="473-484",
	Series=	"LNCS", Volume=711, Publisher="Springer", Year=1993,
	Note="Available at {\tt http://boole.stanford.edu/pub/complete.ps.gz}")

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.


ql

	@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.


dti

	@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.


monoidal

	@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.


ldomain

	@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.


twod

	@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.


ocbr

	@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.


dalg

	@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.


algecon

	@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.


crewthes

	@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.


atch

	@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", Pages="89-107",
	Note="Available at {\tt http://boole.stanford.edu/\-pub/\-atch.ps.gz}")

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.


casthes

	@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.


es

	@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.


cg

	@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.


jelia

	@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.


man

	Temporal Structures
	R. Casley, R. Crew, J. Meseguer, V. Pratt
	Mathematical Structures in Computer
	Science, 1:2.  Proceedings version in Category Theory
	and Computer Science, LNCS 389, Manchester, 1989.
	Formerly called "Dynamic Types."

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.


pp2    		Teams Can See Pomsets
		G. Plotkin and V. Pratt
		Draft in preparation

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.


am4

	@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.''


iowatr

	@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.

lics87

        @InProceedings(
GP,     Author="Gaifman, H. and Pratt, V.R.",
        Title="Partial Order Models of Concurrency and the Computation
                of Functions",
        BookTitle="Proc. 2nd Annual IEEE Symp. on Logic in Computer Science",
        Address="Ithaca, NY", Pages="72-85", Month=Jun, Year=1987)

We shall describe an abstract approach, based on structures of partially ordered events, for specifying and
analyzing concurrent processes. Within this approach, one framework is the pomset model. Another is based on
structures called "prossets" (preorder specification sets) which include, in addition to the < - relation, a
relation for denoting simultaneity of events. Some of the results apply to both, with almost identical proofs,
others necessitate the use of prossets. We show how within a framework of this kind general abstract definitions
can be given to concepts such as: fairness, input event, a location of the process (which can store members of
some given, arbitrary cpo), input-location, and the relation computed by the process in a given location.
Process composition and formation of loops are defined using a fusion operation, by which several locations are
fused into one. Kahn's network sematics turns out to be a rather particular case, derived from an abstract
theorem which etablishes a connection between operations on processes and the least fixpoint operator on the
functions defined by them.

ijpp

	@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.

modalmu81

        @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
similar results for a logic of flowgraphs.  This work provides and
intimate link between PDL as defined by the Segerberg axioms and the
mu-calculi of de Bakker and Park.

amlpd

        @Article(
Pr80c,  Author="Pratt, V.R.",
        Title="Application of Modal Logic to Programming",
        Journal="Studia Logica", Volume=34, Number="2/3", Pages="257-274",
        Year=1980)

The modal logician's notion of possible world and the computer
scientist's notion of state of a machine provide a point of commonality
which can form the foundation of a logic of action. Extending ordinary
modal logic with the calculus of binary relations leads to a very
natural logic for describing the behavior of computer programs.

pdmpdl

        @InProceedings(
Pr78,   Author="Pratt, V.R.",
        Title="A Practical Decision Method for Propositional Dynamic Logic",
        BookTitle="Proc. 10th Ann. ACM Symp. on Theory of Computing",
        Address="San Diego", Pages="326-337", Month=May, Year=1978)

We give a new characterization of the set of satisfiable formulae of
propositional dynamic logic (PDL) based on the method of tableaux. From
it we derive a heuristically efficient goal-directed proof procedure and
a complete axiom system for PDL. The proof procedure illustrates a
striking connection between natural deduction and symbolic execution.
The completeness proof for the axiom system incorporates a method for
the automatic synthesis of invariants. We also augment DL with new
modalities throughout, during, and preserves, supply a new semantic
foundation for DL programs, and show how to extend the satisfiability
characterizations for PDL to throughout. 

sefnp

	@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.

semcon

	@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.