The covering and boundedness problems for branching vector addition systems

Stéphane Demri (1, 2, 3) , Marcin Jurdziński (4) , Oded Lachish (4) , Ranko Lazić (4)

1 LSV - Laboratoire Spécification et Vérification
2 CNRS - Centre National de la Recherche Scientifique
3 DAHU - Verification in databases
4 University of Warwick [Coventry]

The covering and boundedness problems for branching vector addition systems are shown complete for doubly-exponential time.

Mots clés: Petri nets; branching vector addition systems (BVASS); covering; boundedness; complexity; vector addition system (VASS); 2EXPTIME

Domaines: Informatique [cs]; Théorie et langage formel [cs.FL]

Stéphane Demri, Marcin Jurdziński, Oded Lachish, Ranko Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, inPress, 79 (1), pp.23-38. ⟨10.1016/j.jcss.2012.04.002⟩. ⟨hal-03191875⟩