Simulation Over One-counter Nets is PSPACE-Complete

Piotr Hofman, Slawomir Lasota, Richard Mayr, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationIARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages12
ISBN (Print)978-3-939897-64-4
Publication statusPublished - 2013

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


Dive into the research topics of 'Simulation Over One-counter Nets is PSPACE-Complete'. Together they form a unique fingerprint.

Cite this