Evènement pour le groupe Modélisation et Verification


Date 2014-04-17  11:00-12:00
TitreMonotonicity in One-Counter-Systems: what gives? 
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. 
Lieu076 
OrateurPatrick Totzke 
Emailpatrick.totzke@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index