Inclusion Problems for One-Counter Systems

LaBRI , Bordeaux, France

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.