# Petri Nets

> Model concurrent flow as places, tokens, and transitions, so reachability and deadlock are analyzable before runtime.

Record: `algo:petri-nets`
Kind: architecture
Canonical: https://banes-lab.com/ontology/algorithms#algo-petri-nets
Closure: https://banes-lab.com/json/records/algo/petri-nets/closure

## principle

- [Petri Nets](https://banes-lab.com/records/arch/petri-nets.md)

## composes

- [Concurrency Correctness](https://banes-lab.com/records/algo/concurrency-correctness.md)
- [Correctness Core](https://banes-lab.com/records/algo/correctness-core.md)