
Evènement pour le groupe Modélisation et Verification
Date  20131114 11:0012:00 
Titre  Inclusion problems for OneCounter 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 OneCounter 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 OneCounter Automata and thus Pushdown
Systems, which allow explicit zerotests and Petri Nets/VASS, which allow
multiple such weak counters. They are arguably the simplest model of discrete
infinitestate 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 NLcomplete if only one of the given processes is deterministic.
At the same time, trace universality for (nondeterministic) OCN is already
Ackermanian. 
Lieu  205, bât A29 
Orateur  Patrick Totzke 
Email  p.totzke@ed.ac.uk 
Url  Univ. Edinburgh 
Aucun document lié à cet événement. RetourRetour à l'index
 