Evènement pour le groupe Modélisation et Verification
|Date|| 2013-11-14 11:00-12:00|
|Titre||Inclusion 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
|Lieu||205, bât A29 |
|Orateur||Patrick Totzke |
|Url||Univ. Edinburgh |
Aucun document lié à cet événement.RetourRetour à l'index