# Petri Nets

Record: `arch:petri-nets`
Kind: model
Layer: [Atomic Boundary](https://banes-lab.com/records/layer/atomic-boundary.md)
Severity: contextual
Scope: concurrency, workflow, verification
Canonical: https://banes-lab.com/ontology#arch-petri-nets

## Repair

- Refactored by: Model concurrent flow as a Petri net and analyze reachability
- Detected by: deadlocks or lost tokens found only at runtime
- Violated by: concurrent resource flows coordinated by hand-reasoned lock ordering
- Measured by: unreachable or deadlock-prone markings
- Enforced by: concurrency model review

## requires

- [Places and Transitions](https://banes-lab.com/records/lex/places-and-transitions.md)

## reinforces

- [Concurrency Correctness](https://banes-lab.com/records/lex/concurrency-correctness.md)
- [Deadlock Freedom](https://banes-lab.com/records/lex/deadlock-freedom.md)

## enables

- [Concurrent-Flow Modeling](https://banes-lab.com/records/lex/concurrent-flow-modeling.md)
- [Reachability and Deadlock Analysis](https://banes-lab.com/records/lex/reachability-and-deadlock-analysis.md)

## conflicts-with

- [Ad-Hoc Lock Ordering](https://banes-lab.com/records/lex/ad-hoc-lock-ordering.md)

## tensions-with

- [Modeling Overhead](https://banes-lab.com/records/lex/modeling-overhead.md)

## tensions

- [Petri Nets Modeling Overhead](https://banes-lab.com/records/tension/modeling-overhead-petri-nets.md)

## contracts

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