Decidability of Weak Simulation on One-Counter Nets

P. Hofman, R. Mayr, P. 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 only a weak test for zero. We show that weak simulation preorder is decidable for OCN and that weak simulation approximants do not converge at level ω, but only at ω2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN [1], and so are weak (and strong) trace inclusion (Sec. VII).

Original languageEnglish
Title of host publicationLogic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages10
ISBN (Print)978-1-4799-0413-6
Publication statusPublished - 2013


  • Petri nets
  • automata theory
  • bisimulation equivalence
  • decidability
  • OCN
  • one-counter automata
  • one-counter nets
  • semantic relations
  • weak bisimulation
  • weak simulation decidability
  • weak simulation preorder
  • weak test
  • weak trace inclusion
  • Automata
  • Computational modeling
  • Educational institutions
  • Games
  • Model checking
  • Radiation detectors
  • Semantics
  • Automata theory
  • One-counter machines


Dive into the research topics of 'Decidability of Weak Simulation on One-Counter Nets'. Together they form a unique fingerprint.

Cite this