Grande Salle de VERIMAG
29 October 2009 - 14h00
The covering and boundedness problems for branching vector addition systems
by Stephane Demri from ENS CACHAN
Abstract: Branching vector addition systems (BVAS) form a new computational model that is used for instance in computational linguistics and for the verification of cryptographical protocols. This model has also tight relationships with data logics intepreted over data trees and with linear logic MELL. Decidability status of the reachability problem for BVAS is still open and this problem is known to be equivalent to essential problems from the above-mentioned fields. Recently, Verma and Goubault-Larrecq have shown that the covering and boundedness problems for BVAS are decidable.
In this talk, we characterize the computational complexity of these two problems on BVAS, for instance by extending the standard proof for vector addition systems (equivalent to Petri nets) by Rackoff (TCS, 1978).
This is a joint work with Marcin Jurdzinski, Oded Lachish and Ranko Lazic (University of Warwick, UK).
