Decidability of weak simulation on one-counter nets

Hofman, P, Mayr, R and Totzke, P 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 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, and so are weak (and strong) trace inclusion. © 2013 IEEE.

Item Type:	Conference 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:	01 Mar 2026 04:27
DOI:	10.1109/LICS.2013.26
Related Websites:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3031036
Disclaimer:	The University of Liverpool is not responsible for content contained on other websites from links within repository metadata. Please contact us if you notice anything that appears incorrect or inappropriate.