UC Berkeley

Technologies pervasive today have enabled a plethora of diverse networked devices to proliferate in the market. Among these devices are sensors, wearables, mobile devices, and many other embedded systems, in addition to conventional computers. This diverse tapestry of networked devices, often termed the Internet of Things (IoT) and the Swarm, has the potential to serve as a platform for a new breed of sophisticated distributed applications that leverage the ubiquity, concurrency, and flexibility of these devices, often to integrate the similarly diverse information to which these devices have access. These kinds of applications, which we are calling Highly Dynamic Distributed Applications (HDDA), are particularly important in the domain of automated environments such as smart homes, buildings, and even cities.

In contrast with the kind of concurrent computation that can be represented with petri nets, synchronous systems, and other rigid models of concurrent computation, applications running on networks of devices such as the IoT demand models that are more dynamic, semantically heterogeneous, and composable. Because these devices are more than just peripherals to central servers, themselves capable of significant amounts of computation, HDDAs can involve the establishment of direct connections between these devices to share and process information. From the perspective of the platform this will look like an ever-evolving network of dynamic configuration and communication that may have no clear sense of a center, or even a central point of observation. Computation in this fashion begins to look less like a sequence of coherent states and more like a physical interaction in space.

Designing and reasoning about these kinds of applications in a rigorous and scalable fashion will require the development of new programming language semantics, specification logics, verification methods, and synthesis algorithms. At the core of all of these components of a robust programming model will be a need for an appropriate mathematical representation of behavior, specifying precisely what happens in these spaces of devices during the execution of a HDDA. This behavioral representation must characterize an application in as much detail as is necessary, without having to introduce details regarding the realization of the execution on a particular platform, bound to a specific architecture of concrete process and communication relationships. This representation must also be itself as scalable, modular, and composable as the distributed computations it describes.

The aim of this thesis is to identify the mathematical representation of behavior best fit to meet the challenges HDDAs pose to formal semantics and formal verification. To this end, this thesis proposes a new mathematical representation of concurrent computational behavior called an OEG, which generalizes, subsumes, or improves upon other representations of concurrent behavior such as Mazurkiewicz Traces, Event Structures, and Actor Event Diagrams. In contrast with many other representations of concurrent behavior, which are either graphs or partial orders, OEGs are, in essence, acyclic ported block diagrams. In these diagrams, each ported block represents an event and each connection between ports represents a direct dependency between events, while each port around a block represents the specific kind of information or influence consumed or produced in the event. OEGs have the advantage over other representations of concurrent behavior of being both modular and composable, as well as possessing a clear concept of hierarchy and abstraction.

The motivations and reasoning behind this choice of representation will be developed from two directions. The first will be an exploration of the context, consisting of networks of devices such as the IoT. The potential of these networks to serve as a distributed computational platform for HDDAs will be understood through the construction of a conceptual application model that will be called a Process Field. The demands of this application model and some concrete examples will be used to construct an intuitive picture of how the corresponding behavioral representation must look, and what it would need to serve the purposes of constructing semantics and performing verification in the context of HDDAs.

The second direction will reflect on the mathematical details of two classes of sequential representations of behavior, sequences and free monoids, and look at the ways these two classes generalize from the sequential case to the concurrent one. This will suggest, as potential generalizations of the two classes, generalized sequences and free monoidal categories. The former of these classes already has many instances prevalent in the literature. These existing representations based on generalized sequences, along with some other similar established means to represent concurrent behavior, will be reviewed in detail, and reasons will be given for why they do not meet the demands for modularity and composability needed for reasoning about HDDAs.

It will be concluded that the latter, far less investigated class of free monoidal categories offers a richer mathematical structure that is more appropriate for the demands of constructing formal models of HDDAs. In particular, free monoidal categories offer a very general form of composition involving both a parallel and a sequential product. These products, along with a collection of distinguished constants, form an algebra that can be used to construct semantics or to formulate specifications and prove properties of behaviors. Time will be taken to first review the concepts from category theory needed to define these structures, particularly focusing on monoidal categories and the concept of free structures and universal properties. The construction of free monoidal categories, and the particular variant of free symmetric monoidal categories, will then be detailed, and several important properties of these structures will be shown and discussed.

It will ultimately be established that spaces of OEGs defined in this thesis, along with their compositions, form free monoidal categories. Consequently, the study of OEGs can leverage all of the mathematical tools of monoidal category theory to study and better understand distributed behavior. A chapter will be devoted to showing specifically how the π-Calculus can be given a particularly elegant and powerful behavioral semantics using OEGs.