|Résumé||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.
Keywords: counter-automata, reachability, simulation, energy games. |