Simulation Over One-counter Nets is PSPACE-Complete

Authors Piotr Hofman, Slawomir Lasota, Richard Mayr, Patrick Totzke



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2013.515.pdf
  • Filesize: 0.51 MB
  • 12 pages

Document Identifiers

Author Details

Piotr Hofman
Slawomir Lasota
Richard Mayr
Patrick Totzke

Cite As Get BibTex

Piotr Hofman, Slawomir Lasota, Richard Mayr, and Patrick Totzke. Simulation Over One-counter Nets is PSPACE-Complete. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 515-526, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/LIPIcs.FSTTCS.2013.515

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.

Subject Classification

Keywords
  • Simulation preorder; one-counter nets; complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail