Skip to content
learn
Global menu

Petri nets — Mission

Why I’m learning this

Section titled “Why I’m learning this”

I can draw a state machine. I have written them in C# with an enum and a switch, and in Java with a state pattern, and they work as long as the system does one thing at a time. Then two things happen at once. Two threads take two locks in two orders. A Channel<T> fills up and the producer blocks for ever. A workflow has three branches and nobody can say whether all of them can finish.

A state machine cannot say any of that, because it has one current state, and the thing I am modelling has several. What I want is a model whose state is a distribution: so many requests in the queue, so many workers busy, one lock held. A Petri net is exactly that, and it comes with a small body of mathematics that answers questions I currently answer with load tests and hope:

  • can this queue overflow? Not “did it overflow last Tuesday” — can it, ever, under any interleaving;
  • can this system deadlock? And if it can, what is the shortest sequence that gets there;
  • is this workflow going to finish? From every state it can get into, not just the happy path.

Those three questions are decided by a program in this course, on nets that model real things: a bounded buffer, a mutual exclusion, two locks taken in opposite orders.

Who this course is for

Section titled “Who this course is for”

You are a C# or Java developer. You have written concurrent code and modelled processes with state machines. You do not need any mathematics beyond adding vectors and multiplying a matrix by one; the course introduces what it uses, and the first matrix appears in lesson 2 only because it makes something concrete easier.

The concurrency lessons lean on what you already know. Lesson 7 takes the backpressure of lessons 6 to 9 of the Advanced C# course — channels, TPL Dataflow, Rx — and models it instead of measuring it. Lesson 14 starts the repository dogfooding with one bounded C# lifecycle and an agent-lane lock; RabbitMQ and Kubernetes remain explicit follow-up experiments.

The running example

Section titled “The running example”

One producer, one consumer, and a buffer of two slots. Three places hold the state of the producer, the consumer and the buffer; four transitions are the events. Nothing is a “current state”: the marking says where every token is at once.

flowchart LR
    ready(("ready<br/>●"))
    produced(("produced"))
    free(("free<br/>● ●"))
    full(("full"))
    waiting(("waiting<br/>●"))
    taken(("taken"))
    produce["produce"]
    deposit["deposit"]
    take["take"]
    consume["consume"]
    ready --> produce
    produce --> produced
    produced --> deposit
    free --> deposit
    deposit --> full
    deposit --> ready
    full --> take
    waiting --> take
    take --> taken
    take --> free
    taken --> consume
    consume --> waiting

That net has twelve reachable markings, it never deadlocks, and the place free is the whole reason the buffer cannot overflow — remove it, and the set of reachable markings becomes infinite. Lessons 1 to 4 prove all three statements, and lesson 5 proves the first one again without looking at a single marking.

By the end of this course, I will be able to

Section titled “By the end of this course, I will be able to”
  • read and draw a Petri net, and say what its marking means in the system it models;
  • write the incidence matrix of a net, and know what the state equation does and does not decide;
  • build a reachability graph, and a coverability tree when the graph is infinite;
  • decide boundedness, safeness, liveness, deadlock-freedom, reversibility and persistence, and say which of them a given system actually needs;
  • compute place and transition invariants, and use one as a proof that holds for every reachable marking;
  • recognise state machines, marked graphs and free-choice nets, and use the theorems that come with them;
  • model mutual exclusion, producer/consumer, readers/writers and the dining philosophers, and compare the models with the C# and Java constructs they stand for;
  • use coloured, timed and stochastic nets, and know what each extension costs in analysis;
  • check a workflow for soundness, and translate between BPMN and workflow nets;
  • exchange nets with TINA, LoLA, CPN Tools, GreatSPN and TAPAAL through PNML;
  • model parts of the systems in this repository, and say honestly what the model found and what it missed;
  • know where the formalism stops: what is undecidable, what is decidable but hopeless, and what to reach for instead.

Outline

Section titled “Outline”
# Lesson You may already know
1 Why Petri nets state machines, enum plus switch, a bounded queue
2 The formal definition and the incidence matrix vectors, a matrix product
3 The reachability graph a breadth-first search, the state explosion of a test matrix
4 Properties deadlock, livelock, starvation
5 Invariants a loop invariant, a conserved count
6 Structural classes: state machines, marked graphs, free-choice nets
7 Modelling concurrency: mutual exclusion, producer/consumer, readers/writers, philosophers lock, SemaphoreSlim, Channel<T>, synchronized, ReentrantLock
8 Coloured nets generics, a typed message
9 Time and probability: timed nets, stochastic nets, GSPN percentiles, a queueing model
10 Workflows: workflow nets, soundness, BPMN, process mining BPMN, a workflow engine
11 Tools and interoperability: PNML, TINA, LoLA, Snoopy, PIPE, CPN Tools, GreatSPN, TAPAAL an XML exchange format
12 Industrial applications: manufacturing, protocols, hardware, biochemistry, security a public benchmark, a state space
13 Against other formalisms: TLA+, statecharts, process algebras, timed automata a second state space, computed elsewhere
14 On our own systems: C# pipelines and agent lanes Advanced C#; RabbitMQ and Kubernetes are follow-up experiments
15 Limits and what comes next: undecidability, unfoldings, partial order reduction, extensions a wrong answer from a correct algorithm
16 Interoperability: preserving behaviour, not just the drawing a round-trip test, a file that validates and still loses data

Journal: what I tried, what surprised me, what I still need to verify.

Resources

Section titled “Resources”