Verimag

Seminar details

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.





Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876201