Simulation over one-counter nets is PSPACE-complete

DOI10.4230/LIPICS.FSTTCS.2013.515MaRDI QIDQ2963939zbMATH OpenOpenAlexFDO

Authors Piotr Hofman, Sławomir Lasota, Patrick Totzke, Richard M. Mayr

Publication date 21 February 2017

Full work available at URL https://arxiv.org/abs/1310.6303

zbMATH Keywords

complexityone-counter netssimulation preorder

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.

Recommendations

• Simulation problems over one-counter nets
• scientific article; zbMATH DE number 1304996
• Decidability of weak simulation on one-counter nets
• scientific article; zbMATH DE number 1500527
• EXPSPACE-complete variant of countdown games, and simulation on succinct one-counter nets

Cited in

(11)

• EXPSPACE-complete variant of countdown games, and simulation on succinct one-counter nets
• Trace inclusion for one-counter nets revisited
• Bisimulation equivalence and regularity for real-time one-counter automata
• scientific article; zbMATH DE number 1696434 (Why is no real title available?)
• Simulation problems over one-counter nets
• Trace inclusion for one-counter nets revisited
• scientific article; zbMATH DE number 1304996 (Why is no real title available?)
• scientific article; zbMATH DE number 1500527 (Why is no real title available?)
• Decidability of weak simulation on one-counter nets
• Countdown games, and simulation on (succinct) one-counter nets
• EXPSPACE lower bounds for the simulation preorder between a communication-free Petri net and a finite-state system

This page was built for publication: Simulation over one-counter nets is PSPACE-complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2963939)