Timing via Pinwheel Double Categories

TL;DR

This work addresses the challenge of modeling timing in process descriptions by proposing a timing-aware diagrammatic calculus based on duoidally-graded symmetric monoidal categories built atop pinwheel double categories. The main approach combines timed polygraphs with a tilt construction that converts double-category cells into a 2-categorical setting, enabling pinwheel-augmented compositions that would otherwise be forbidden by traditional double-category formalisms. Key contributions include a semantics for timed string diagrams using two monoid operations ⊕ (addition) and ↑ (maximum) with a normal, commutative duoid constraint, a translation from timed polygraphs to double signatures, and a pathway to pinwheel double categories via the pinwheel monad and tilted 2-categories. The resulting framework provides a rigorous, timing-aware diagrammatic language for concurrent processes and suggests connections to time-graded coalgebras of monads and related notions like monoidal width, with potential impact on formal methods in timed process theories.

Abstract

We discuss string diagrams for timed process theories -- represented by duoidally-graded symmetric strict monoidal categories -- built upon the string diagrams of pinwheel double categories.

Figures (8)

• Figure 1: Process description of a preparation of crema di mascarpone, adapted from Sobocinski
• Figure 2: Timing of the "crema di mascarpone" process.
• Figure 3: Double signature from a timed polygraph.
• Figure 4: Equations for the double category from a timed polygraph.
• Figure 5: Two valid timings that form pinwheels.

Theorems & Definitions (24)

• Definition 1: Duoid
• Example 2: Natural numbers
• Definition 3: Duoidally-locally graded monoidal category
• Definition 4: Duoid-graded monoidal category
• Remark 5
• Definition 6: Double categories
• Definition 7: Double signature
• proposition 1: Double signature morphism
• proposition 2: Forgetful double signatures
• Definition 8: Timed polygraph