Room 206 (Building IMAG)
20 April 2017 - 14h00
On the context-freeness problem for vector addition systems. (candidat MCF)
by Vincent Penelle from Universite de Varsovie
Abstract: 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 talk. 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.
We propose a new proof of this result, which relies on the notion of so-called witnesses of non-context-freeness, that are bounded regular languages satisfying a nesting condition. We obtain the result by the effective construction of a finite vector pushdown automaton which either recognises the same language as the VAS, or exhibits a witness of non-context-freeness whose intersection with the trace language is not context-free. 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.
This work is a joint work with Jérôme Leroux and Grégoire Sutre.
Further, this work has allowed to determine the complexity of this problem and to study that same problem on flat counter systems.
