CatColab Petri Nets: Concurrent Systems Skill

CatColab Petri Nets: Concurrent Systems

Trit: +1 (PLUS - generator) Color: Magenta (#FF00FF)

Overview

Petri nets in CatColab model concurrent and distributed systems:

Places: States holding tokens (resources, conditions)
Transitions: Events that fire when enabled
Arcs: Flow of tokens between places and transitions
Tokens: Resources consumed/produced by transitions

Petri nets are the categorical foundation for process algebra, workflow modeling, and chemical reaction networks.

Mathematical Foundation

A Petri net is a bipartite graph:

┌─────────────────────────────────────────────────────┐
│                    PETRI NET                         │
├─────────────────────────────────────────────────────┤
│  Places (States):                                    │
│    (P1) Ready   (P2) Running   (P3) Done            │
│                                                      │
│  Transitions (Events):                               │
│    [T1] Start   [T2] Finish                          │
│                                                      │
│  Arcs (Token Flow):                                  │
│    P1 → T1 → P2 → T2 → P3                           │
│                                                      │
│  Diagram:                                            │
│    (P1)●──►[T1]──►(P2)──►[T2]──►(P3)                │
│     ●=token                                          │
└─────────────────────────────────────────────────────┘

Free Symmetric Monoidal Category

Petri nets are the free symmetric monoidal category on a signature:

Objects: P₁, P₂, ..., Pₙ (places)
Morphisms: Generated by transitions

Tensor: P₁ ⊗ P₂ (concurrent resources)
Composition: Sequential firing

Example:
  T: P₁ ⊗ P₂ → P₃ ⊗ P₄
  "Transition T consumes tokens from P₁, P₂
   and produces tokens in P₃, P₄"

Double Theory

// Petri net double theory
pub fn th_petri_net() -> DiscreteDblTheory {
    let mut cat = FpCategory::new();

    // Object type
    cat.add_ob_generator(name("Place"));

    // Morphism type (transitions as structured morphisms)
    cat.add_mor_generator(name("Transition"), name("Place"), name("Place"));

    // Monoidal structure (parallel composition)
    // P ⊗ Q represents "P and Q concurrently"

    cat.into()
}

CatColab Implementation

Place Declaration

{
  "type": "ObDecl",
  "name": "Idle",
  "theory_type": "Place",
  "description": "process waiting for input"
}

Transition Declaration

{
  "type": "MorDecl",
  "name": "activate",
  "inputs": ["Idle", "Resource"],
  "outputs": ["Active"],
  "theory_type": "Transition",
  "description": "process starts when resource available"
}

Practical Examples

Example 1: Producer-Consumer

Places: Buffer (capacity N), Produced, Consumed

Transitions:
  produce: Empty → Buffer + Produced
  consume: Buffer → Consumed

Tokens: Buffer starts empty, count items produced/consumed

Example 2: Dining Philosophers

Places: Thinking(i), Eating(i), Fork(i) for i=1..5

Transitions:
  pickup(i): Thinking(i) ⊗ Fork(i) ⊗ Fork(i+1) → Eating(i)
  putdown(i): Eating(i) → Thinking(i) ⊗ Fork(i) ⊗ Fork(i+1)

Deadlock possible when all pick up left fork simultaneously

Example 3: Chemical Reaction (A + B → C)

Places: A, B, C (species concentrations as token counts)

Transitions:
  react: A ⊗ B → C

Stochastic: Rate = k·[A]·[B] (mass action)

Connection to Stock-Flow

Petri nets and stock-flow diagrams are equivalent:

Petri Net           ≅   Stock-Flow
  Place             ↔   Stock
  Transition        ↔   Flow
  Token count       ↔   Population
  Firing rate       ↔   Mass-action rate

AlgebraicPetri.jl Integration

using AlgebraicPetri
using Catlab

# Define SIR as Petri net
sir_petri = @acset LabelledPetriNet begin
  S = 3  # places: S, I, R
  T = 2  # transitions: infect, recover

  tname = [:infect, :recover]
  sname = [:S, :I, :R]

  is = [1, 2]     # infect inputs: S, I
  os = [2, 2]     # infect outputs: I, I
  it = [1, 1]     # transition indices
  ot = [1, 1]
end

# Compose Petri nets
combined = sir_petri ⊕ vaccination_petri

GF(3) Triads

catcolab-regulatory-networks (-1) ⊗ topos-catcolab (0) ⊗ catcolab-petri-nets (+1) = 0 ✓
crn-topology (-1) ⊗ catcolab-stock-flow (0) ⊗ catcolab-petri-nets (+1) = 0 ✓

Commands

# Create Petri net
just catcolab-new petri-net "producer-consumer"

# Analyze reachability
just catcolab-analyze producer-consumer --reachability

# Check for deadlock
just catcolab-analyze producer-consumer --deadlock

# Export to PNML
just catcolab-export producer-consumer --format=pnml

# Simulate token dynamics
just catcolab-simulate producer-consumer --stochastic

References

Baez & Master (2020) "Open Petri nets"
Patterson et al. (2022) "Categorical data structures for technical computing"
AlgebraicPetri.jl
CatColab Petri Net Help (planned)

Skill Name: catcolab-petri-nets Type: Concurrent Systems / Process Algebra Trit: +1 (PLUS) GF(3): Balances the CatColab skill ecosystem

Agent Skills: CatColab Petri Nets: Concurrent Systems

Install this agent skill to your local

Skill Files