Monotonicity for One-Counter Systems: What gives?

LaBRI , Bordeaux, France

I will discuss several basic problems involving one-counter automata (OCA) with special focus on the impact of monotonicity.

First we will recall a characterization of reachability based on Valiant's classic "hill cutting" argument, which leads to an NL decision procedure.

Not surprisingly, many problems involving two OCA are already undecidable: (Trace) inclusion and equivalence, simulation preorder, weak (and branching) bisimulation and so on. Forbidding zero-tests in OCA results in a model called one-counter nets (OCN) which corresponds to 1-dimensional VASS and lies in the intersection of VASS and pushdown systems. Due to the monotonicity of the step relation in OCN, some of the problems mentioned above become decidable.

I will discuss our technique for deciding strong simulation for OCN and mention some implications, generalizations and open problems.