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.
![]() |
Text
1304.4104v2.pdf - Published version Download (514kB) |
![]() |
Text
HMT2013.pdf - Author Accepted Manuscript Download (473kB) |
Abstract
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: | 07 Dec 2024 05:06 |
DOI: | 10.1109/LICS.2013.26 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3031036 |