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.

	Text 1304.4104v2.pdf - Published version Download (514kB)
	Text HMT2013.pdf - Author Accepted Manuscript Download (473kB)

Official URL: http://dx.doi.org/10.1109/lics.2013.26

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:	19 Jan 2023 01:07
DOI:	10.1109/LICS.2013.26
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3031036