MOVES Seminar 8 April 2010, 11:00 (seminar room of i7, Room 4116)
Stephane Demri, ENS Cachan, F
The covering and boundedness problems for branching vector addition systems
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.
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.
