Ross Casley's thesis is now available by anonymous ftp, in both .tex and .dvi forms. It should be of interest to those working in concurrency modeling, particularly if you have an interest in notions of time other than the two-valued one implicit in partial order and linear order models of concurrency. The thesis views concurrent processes in terms of an algebra of behaviors each defined as a set of events spread out in time and labeled or endowed with attributes, rather than as sequential processes connected by communication channels. Although a treatment of timed processes was the motivating concern of the thesis, there exist interesting parallels between the algebraic structure of behaviors as developed in the thesis and the structure of types. Both behaviors and types combine naturally via sum, product, and exponentiation, and both are amenable to very similar categorical treatments. While these are not drawn out in any detail in the thesis, those familiar with type theory should have little difficulty in seeing at least some of these connections. Types can be thought of as the dual of behaviors: a type is a disjunctive collection of values (a variable can take on only one value) while a behavior is a conjunctive collection of events (all events of the behavior must happen for the behavior itself to be considered to have happened). A set passed as a parameter or stored as a value lives on the behavior side of this duality inasmuch as it is a conjunctive aggregate: the elements of the set are all present simultaneously. The contravariant power object functor 2?X equips this duality with a natural and mathematically rich representation. One of the motivations behind our present interest in event spaces, concurrent automata, partial distributive lattices, etc., is a better understanding of this duality. Instructions for obtaining the thesis, along with other papers from the same source, appear below. Vaughan Pratt ===================================================================== Papers on Concurrency Modeling Available by Anonymous FTP from Boole.Stanford.EDU This file is README in the /pub directory of Boole.Stanford.EDU, 36.8.0.65, accessible by anonymous ftp. The /pub directory is for FTP distribution of recent publications of the Boole group. The Boole group is a subgroup of the Mathematical Theory of Computation group, Computer Science Department, Stanford University. The group consists of the following. Ross Casley casley@cs.stanford.edu (SYS) Roger Crew crew@cs.stanford.edu (SYS) Rob van Glabbeek rvg@cs.stanford.edu Vineet Gupta vgupta@cs.stanford.edu Vaughan Pratt (group leader) pratt@cs.stanford.edu (SYS) Pat Simmons (secretary) simmons@cs.stanford.edu Orli Waarts orli@cs.stanford.edu ==========================Instructions================================= FTP LOGIN. Give the following commands. ftp boole.stanford.edu Login: anonymous (if you don't have an account on boole) Paswd: yoursurname (though any string will work) bin (if you are retrieving a .dvi file) prompt off (if you want no ? prompts from mget) cd pub (change directory to ^ftp/pub ls -lt (see what's there, most recent first) mget filename-1 ... filename-n (e.g. mget cg.tex logic.bib) quit (exit from FTP) SOURCE. To retrieve the source to paper foo, get foo.tex and logic.bib. The source should be compiled using latex foo; bibtex foo; latex foo; latex foo DVI. If you wish to print paper foo without having to compile with latex, retrieve just foo.dvi. You must first give the bin command to ftp since .dvi files are not text files. Print foo.dvi on your host using lpr -d foo.dvi. PROBLEMS. If you have problems in either retrieving or compiling papers, please contact a systems person (flagged SYS on the list above). ===========================Available papers================================= TITLES casthes.tex On the Specification of Concurrent Systems es.tex Event Spaces and their Linear Logic (in preparation) catl.tex Concurrent Automata and Their Logic (old es.tex, temporary) cg.tex Modeling Concurrency with Geometry jelia.tex Action Logic and Pure Induction man.tex Temporal Structures pp2.tex Teams Can See Pomsets am4.tex Enriched Categories and the Floyd-Warshall Connection iowatr.tex Dynamic Algebras as a well-behaved fragment of Relation Algebras ijpp.tex Modelling Concurrency with Partial Orders ----------------------------------------------------------------------- ABSTRACTS casthes.tex On the Specification of Concurrent Systems Ross Casley Ph.D. Thesis, January, 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.tex Event Spaces and their Linear Logic V. Pratt Submitted to LICS-91 under its earlier title of "Concurrent Automata and Their Logic" (This paper is still being written. The paper to date is being made available for those wishing to follow closely or contribute to the development of event spaces. See catl.tex for a more stable but dated account.) An event space is a partially ordered set with a top element and all nonempty joins, including infinite ones. Whereas in a Boolean algebra OR and AND are interpreted extrinsically as respectively join and meet, in an event space they are both interpreted as join and distinguished intrinsically according to whether or not that join is the top element. In addition we take the order itself as the interpretation of AND-THEN, sequential AND. Event spaces subsume Winskel event structures, and are dual to state spaces in an unexpectedly simple way. We exhibit a calculus of event spaces whose primitive operations are direct product, tensor product, and free space, along with associated constants providing units for the two products. From these are derived by duality etc. several other operations constituting simultaneously a concurrent programming language and a linear logic of concurrency. While event spaces resemble vector spaces in many ways, they improve on them with respect to duality (restricted to finite dimensions for vector spaces), flexibility (vector spaces are more rigid), and nondegeneracy (product and sum coincide for vector spaces but not event spaces, and similarly for other dual pairs of operations). catl.tex Concurrent Automata and Their Logic V. Pratt Submitted to LICS-91 (This is the previous revision of es.tex, which will replace it when ready.) A concurrent automaton is a poset with a top (the global initial state) and all nonempty sups (the local initial states). A schedule is defined identically. These form dually isomorphic categories Aut and Sched admitting universally definable operations constituting a concurrent programming language, and additional operations constituting a linear logic of concurrency in which $!a$ and $?a$ are respectively a free choice automaton and a free concert schedule. The linear theory Th(CSLat) of complete semilattices strictly extends Th(Aut) with $\query a=\bang a$, an unwanted isomorphism of free and cofree semilattices (both being Boolean algebras) found only in CSLat. Both theories contain such howlers as 0=1. Intersection with classical logic (multiplication by 2) removes the howlers, but not usefully so for CSLat, and moreover $\query a=\bang a$ remains. The self-duality of these categories permits a non-categorical account requiring only elementary lattice theory. cg.tex Modeling Concurrency with Geometry V. Pratt To appear in POPL-91. Abstract: 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.tex Action Logic and Pure Induction V. Pratt To appear in Proceedings of JELIA-90, European Workshop on Logics in AI (ed. J. van Benthem and Jan Eijck), held Amsterdam, Sept. 1990 Abstract: 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.tex Temporal Structures R. Casley, R. Crew, J. Meseguer, V. Pratt To appear in Mathematical Structures in Computer Science, inaugural issue, 1990. Revision of proceedings version in Category Theory and Computer Science, LNCS 389, Manchester, 1989. Formerly called "Dynamic Types." Abstract: 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.tex Teams Can See Pomsets G. Plotkin and V. Pratt Draft in preparation Abstract: 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.tex Enriched Categories and the Floyd-Warshall Connection V. Pratt Proceedings, AMAST-88 Abstract: 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.tex Dynamic Algebras as a well-behaved fragment of Relation Algebras V. Pratt Algebraic Logic and Universal Algebra in Computer Science, LNCS 425, ed. C.H. Bergman, R.D. Maddux, D.L. Pigozzi, Springer-Verlag, 1990. Abstract: 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. ijpp.tex Modelling Concurrency with Partial Orders V. Pratt International Journal of Parallel Programming, 15:1, 33-71, Feb. 1986. Abstract: 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.