The Ordinal-Recursive Complexity of Timed-arc Petri Nets, Data Nets, and Other Enriched Nets

—We show how to reliably compute fast-growing functions with timed-arc Petri nets and data nets. This construction provides ordinal-recursive lower bounds on the complexity of the main decidable properties (safety, termination, regular simulation, etc.) of these models. Since these new lower bounds match the upper bounds that one can derive from wqo theory, they precisely characterise the computational power of these socalled “enriched” nets.

• Type: Journal
• Year: 2012
• Where: LICS
• Authors: Serge Haddad, Sylvain Schmitz, Philippe Schnoebelen
• Keywords: Automated Reasoning, Complexity, Computational Power, LICS 2012, Upper Bounds