Causal automata (Q1194329)

This paper begins the study of causality from a logical point of view. Causality has conventionally been studied --- at least in semantics --- through the use of partially ordered sets (posets). This paper points out that a poset, without additional structure, is only capable of expressing AND causality. From the logical perspective it is natural to extend this by incorporating the ``dual'' connective OR. The paper introduces the formalism of causal automata as a convenient model in which to do this. A causal automaton is a pair \((E,\rho)\) where \(E\) is a finite set of events and \(\rho: E\to BE\) is a function from \(E\) to the free Boolean algebra generated by \(E\). The paper concentrates on motivating this model by studying Milner's notion of confluence in CCS. Confluence in CCS is a strong, labelled form of the classical notion of confluence in transition systems. (It is discussed at length in Chapter 11 of \textit{R. Milner's} book [Communication and concurrency, Prentice Hall, New York (1989; Zbl 0683.68008)].) The main result in the paper is the following causal characterisation of confluence: \[ Confluence\;\equiv\;Determinism\;+\;\{AND,OR\} Causality. \] It follows that confluence is a two dimensional phenomenon, the dimensions being measured by the extent of AND and OR causality respectively. In earlier work the author has shown that (finite) confluent processes which use only AND causality can always be built up by compositional techniques in CCS. The problem of constructing all confluent processes in a compositional manner is still open. In a subsequent work the author has given a careful treatment of the principles underlying logics of causality and has discussed the logics which must be used when the number of events is infinite [Geometric logic, causality and event structures, Proc. 2nd int. Conf. concurrency theory, Amsterdam, Aug. 26-29 1991, Lect. Notes Comput. Sci. 527, 266-280 (1991)].