Checking Weak Simulation for One-Counter Nets
Patrick Totzke, University of Edinburgh
Date and Time
Thursday, November 15th, 2012 at 13:30
Polacksbacken, room 1113
I will talk about ongoing work on One-Counter Nets, particularly on our recent result that weak simulation preorder is decidable for this model. OCN are restricted variants of Petri nets and Pushdown automata. Each process maintains a single counter which cannot be tested for zero.
Our argument makes use of a symbolic representation of a systems ability to do infinite branching and is based on the original result that strong simulation is decidable. If time permits I will outline a few observations that allow us to derive meaningful upper bounds for strong and weak simulation.
One-Counter Systems, Monotonicity, Ordinal Approximants, Weak Simulation.