Don't worry too much about Tex 3.1, all the systems I'm aware of are only up to 3.0 (Paul's included, he confesses!). If you want to upgrade to 3.0, here are some places to look. Except for the first I found these by sending mail to archie@quiche.cs.mcgill.ca (a program) with subject "prog tex" and picking out those that referred to tex3.0. (I should have said "prog tex3.0"). Many more don't so identify themselves with the 3.0 suffix but may well carry tex3.0. For those not used to using anonymous ftp to fetch things with I include a copy of the README from Boole.Stanford.EDU, whose "Instructions" section explains the procedure. Vaughan Pratt Host labrea.stanford.edu (36.8.0.47) Location: /pub/tex Host ccadfa.cc.adfa.oz.au (131.236.1.2) Location: /tex/tex-3.0 Host emx.utexas.edu (128.83.1.33) Location: /pub/mnt/source/tex/tex-3.0 Host freja.diku.dk (129.142.96.1) Location: /TeX/TeX-3.0 Host psuvax1.cs.psu.edu (130.203.1.6) Location: /pub/src/TeX3.0/TeX3.0 Host ugle.unit.no (129.241.1.97) Location: /pub/tex/tex-3.0 Host uxc.cso.uiuc.edu (128.174.5.50) Location: /text/TeX3.0/TeX3.0 Host walhalla.informatik.uni-dortmund.de (129.217.64.63) Location: /pub/comp/msdos/emtex3.0 The Sun Garage Cache Prepublication Medium Papers on Parallel Software Theory 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 prepublications in the area of parallel software theory. It is run by the Boole group, a subgroup of the Mathematical Theory of Computation group, Computer Science Department, Stanford University. The group consists of the following people. 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 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 concurrences and a top representing the unreachable event. The symmetry is with the dual notion of state space, a poset with all nonempty meets representing choices and a bottom representing the start state. The algebra is that of a parallel programming language expanded to the language of linear logic, Girard's axiomatization of which is satisfied by the event space interpretation of this language. Event spaces resemble 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. catl.tex Concurrent Automata and Their Logic V. Pratt Superseded by es.tex 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. 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 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." 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 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 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. 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. 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.