Coverability in a NonFunctional Extension of BVASS

We define Vector Addition with Sates and Split/Join Transitions, a new model that extends VASS and BVASS. We define a suitable notion of covering graph for the model, and prove its finiteness and effective constructibility, and prove a coverability theorem.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00947136
Author Jacobé de Naurois, Paulin
Maintainer CCSD
Last Updated May 6, 2026, 09:19 (UTC)
Created May 6, 2026, 09:19 (UTC)
Identifier hal-00947136
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Laboratoire d'Informatique de Paris-Nord (LIPN) ; Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)
creator Jacobé de Naurois, Paulin
date 2014-02-14T00:00:00
harvest_object_id 0cefac5d-5367-4036-a1d9-13efd4e74f7d
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2024-11-29T00:00:00
set_spec type:REPORT