pratt@cs.stanford.edu (Vaughan Pratt) (11/26/90)
Several papers on theoretical aspects of concurrency are available from the directory /pub on boole.stanford.edu (36.8.0.65) by anonymous ftp. The file pub/README, which follows, tells all. =================boole.stanford.edu:~ftp/pub/README============== This 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 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 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.