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

Abstract / Description of output

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
Pages515-526
Number of pages12
ISBN (Print)978-3-939897-64-4
DOIs
Publication statusPublished - 2013

Publication series

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

Fingerprint

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

Cite this