Reduction Using Induced Subnets To Systematically Prove Properties For Free-Choice Nets

TL;DR

This paper introduces a systematic method using induced subnets to transform free-choice nets into T-nets and P-nets, enabling easier property verification while preserving key characteristics like liveness and safety.

Contribution

It presents a general approach for converting free-choice nets into simpler net classes, facilitating property proofs by preserving essential properties.

Findings

Preserves well-formedness, liveness, lucency, pc-safety, and perpetuality during transformation.

Enables systematic proofs by peeling off non-trivial parts of nets.

Applicable to various properties across different net classes.

Abstract

We use sequences of t-induced T-nets and p-induced P-nets to convert free-choice nets into T-nets and P-nets while preserving properties such as well-formedness, liveness, lucency, pc-safety, and perpetuality. The approach is general and can be applied to different properties. This allows for more systematic proofs that "peel off" non-trivial parts while retaining the essence of the problem (e.g., lifting properties from T-net and P-net to free-choice nets).