Relating State-Based and Process-Based Concurrency through Linear Logic

This paper has the purpose of reviewing some of the established relationships between logic and concurrency, and of exploring new ones.Concurrent and distributed systems are notoriously hard to get right. Therefore, following an approach that has proved highly beneficial for sequential programs, much effort has been invested in tracing the foundations of concurrency in logic. The starting points of such investigations have been various idealized languages of concurrent and distributed programming, in particular the well-established state-transformation model inspired to Petri nets and multiset rewriting, and the prolific process-based models such as the π-calculus and other process algebras. In nearly all cases, the target of these investigations has been linear logic, a formal language that supports a view of formulas as consumable resources. In the first part of this paper, we review some of these interpretations of concurrent languages into linear logic.In the second part of the paper, we propose a completely new approach to understanding concurrent and distributed programming as a manifestation of logic, which yields a language that merges those two main paradigms of concurrency. Specifically, we present a new semantics for multiset rewriting founded on an alternative view of linear logic. The resulting interpretation is extended with a majority of linear connectives into the language of ω-multisets. This interpretation drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication, and more. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. For example, a simple translation maps process constructors of the asynchronous π-calculus to rewrite operators, while the structural equivalence corresponds directly to logically-motivated structural properties of ω-multisets (with one exception).