Decidability of Weak Simulation on One-counter Nets
Formal Languages and Automata Theory
2014-06-17 v2
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.
Keywords
Cite
@article{arxiv.1304.4104,
title = {Decidability of Weak Simulation on One-counter Nets},
author = {Piotr Hofman and Richard Mayr and Patrick Totzke},
journal= {arXiv preprint arXiv:1304.4104},
year = {2014}
}
Comments
24 pages