A concise proof of Commoner's theorem

Petr Jancar

A concise proof of Commoner's theorem

Petr Jancar

TL;DR

The aim of this note is to give a concise self-contained proof of Commoner's theorem characterizing liveness in free-choice Petri nets.

Abstract

The textbook proofs of Commoner's theorem characterizing liveness in free-choice Petri nets are given in contexts of technical notions and claims that make the proofs look a bit long. The aim of this note is to give a concise self-contained proof.

A concise proof of Commoner's theorem

TL;DR

The aim of this note is to give a concise self-contained proof of Commoner's theorem characterizing liveness in free-choice Petri nets.

Abstract

Paper Structure (1 theorem)

This paper contains 1 theorem.

Key Result

Theorem 1

For any free-choice net $N=(P,T,F)$ with no isolated places (i.e., $P={}^\bullet{T}\cup{T}^\bullet$) and any $M_0\in\mathbb{N}^P$, the next two conditions are equivalent:

Theorems & Definitions (2)

Theorem : Commoner
proof