Decidability of Weak Simulation on One-counter Nets

Hofman, Piotr, Mayr, Richard and Totzke, Patrick ORCID: 0000-0001-5274-8190
(2013) Decidability of Weak Simulation on One-counter Nets. In: 2013 Twenty-Eighth Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2013), 2013-6-25 - 2013-6-28, New Orleans, LA, USA.

[img] Text
1304.4104v2.pdf - Published version

Download (514kB)
[img] Text
HMT2013.pdf - Author Accepted Manuscript

Download (473kB)


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 omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.

Item Type: Conference or Workshop Item (Unspecified)
Additional Information: 24 pages
Uncontrolled Keywords: Automata theory, One-counter machines
Depositing User: Symplectic Admin
Date Deposited: 21 Jan 2019 15:28
Last Modified: 19 Jan 2023 01:07
DOI: 10.1109/LICS.2013.26
Related URLs: