Department of Information Technology

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.

Updated  2012-11-12 13:47:21 by Frédéric Haziza.