DocumentCode
626288
Title
Decidability of Weak Simulation on One-Counter Nets
Author
Hofman, Piotr ; Mayr, Richard ; Totzke, Patrick
Author_Institution
Univ. of Warsaw, Warsaw, Poland
fYear
2013
fDate
25-28 June 2013
Firstpage
203
Lastpage
212
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 ω, but only at ω2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN [1], and so are weak (and strong) trace inclusion (Sec. VII).
Keywords
Petri nets; automata theory; bisimulation equivalence; decidability; OCN; Petri nets; one-counter automata; one-counter nets; semantic relations; weak bisimulation; weak simulation decidability; weak simulation preorder; weak test; weak trace inclusion; Automata; Computational modeling; Educational institutions; Games; Model checking; Radiation detectors; Semantics; Automata theory; One-counter machines;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
Conference_Location
New Orleans, LA
ISSN
1043-6871
Print_ISBN
978-1-4799-0413-6
Type
conf
DOI
10.1109/LICS.2013.26
Filename
6571552
Link To Document