String Diagrammatic Trace Theory

TL;DR

This paper develops a graphical, monoidal category-based framework for formal languages and concurrency, connecting trace languages, automata, and string diagrams to unify and extend existing theories.

Contribution

It introduces symmetric monoidal automata, characterizes Mazurkiewicz trace languages within this framework, and relates Zielonka's automata to symmetric monoidal automata.

Findings

Mazurkiewicz trace languages are symmetric monoidal languages.

Symmetric monoidal automata define regular symmetric monoidal languages.

Zielonka's asynchronous automata coincide with symmetric monoidal automata.

Abstract

We extend the theory of formal languages in monoidal categories to the multi-sorted, symmetric case, and show how this theory permits a graphical treatment of topics in concurrency. In particular, we show that Mazurkiewicz trace languages are precisely symmetric monoidal languages over monoidal distributed alphabets. We introduce symmetric monoidal automata, which define the class of regular symmetric monoidal languages. Furthermore, we prove that Zielonka's asynchronous automata coincide with symmetric monoidal automata over monoidal distributed alphabets. Finally, we apply the string diagrams for symmetric premonoidal categories to derive serializations of traces.