The Monadic Second Order Theory of Grid-Free 1-Safe Petri Nets is Decidable

TL;DR

This paper proves that monadic second order logic is decidable for grid-free finite 1-safe Petri nets, confirming Thiagarajan's conjecture and advancing the understanding of their behavioral properties.

Contribution

The paper establishes the decidability of MSO logic for grid-free 1-safe Petri nets, confirming a long-standing conjecture.

Findings

MSO logic is decidable for grid-free 1-safe Petri nets.

Confirms Thiagarajan's conjecture on the characterization of decidability.

Enhances understanding of behavioral properties of net systems.

Abstract

Finite 1-safe Petri nets, also called \emph{net systems}, are natural models of asynchronous concurrency. The event structure of a net system describes all its possible executions and their concurrent nature: two events may be causally ordered, occur in parallel or be conflicting. Monadic second order logic (MSO) can be used to specify behavioural properties of net systems. Thiagarajan's conjecture states that MSO is decidable if and only if the net system is grid-free. The present paper gives a positive answer to this conjecture.