Résumé | Petri nets, or equivalently vector addition systems (VAS),
are widely recognized as a central model for concurrent systems.
Many interesting properties are decidable for this class,
such as boundedness, reachability, regularity,
as well as context-freeness, which is the focus of this paper.
The context-freeness problem asks whether the trace language
of a given VAS is context-free.
This problem was shown to be decidable by Schwer in 1992,
but the proof is very complex and intricate.
The resulting decision procedure relies on five technical conditions over
a customized coverability graph.
These five conditions are shown to be necessary,
but the proof that they are sufficient is only sketched.
In this paper, we revisit the context-freeness problem for VAS,
and give a simpler proof of decidability.
Our approach is based on witnesses of non-context-freeness,
that are bounded regular languages satisfying a nesting condition.
As a corollary,
we obtain that the trace language of a VAS is context-free if,
and only if,
it has a context-free intersection with every bounded regular language. |