Evènement pour le groupe Modélisation et Verification


Date 2013-11-14  11:00-12:00
TitreInclusion problems for One-Counter Nets 
RésuméA fundamental question in formal verification is the inclusion problem, that asks if the behaviour of one process can be reproduced by another. Just as equivalence and model checking problems, inclusion has been extensively studied for various notions of behavioural preorders and for many computational models. This talk will focus on One-Counter Nets (OCN), which consist of a finite control and a single integer counter that cannot be fully tested for zero. OCN form a natural subclass of both One-Counter Automata and thus Pushdown Systems, which allow explicit zero-tests and Petri Nets/VASS, which allow multiple such weak counters. They are arguably the simplest model of discrete infinite-state systems but make an interesting case study for different settings of the inclusion problem. I will highlight recent results on trace/language inclusion for OCN. This problem is NL-complete if only one of the given processes is deterministic. At the same time, trace universality for (nondeterministic) OCN is already Ackermanian. 
Lieu205, bât A29 
OrateurPatrick Totzke 
Emailp.totzke@ed.ac.uk 
UrlUniv. Edinburgh 



Aucun document lié à cet événement.

Retour
Retour à l'index