Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Alternating Vector Addition Systems with States

Jean-Baptiste Courtois 1 Sylvain Schmitz 1, 2, *
* Corresponding author
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Alternating vector addition systems are obtained by equipping vector addition systems with states (VASS) with 'fork' rules, and provide a natural setting for infinite-arena games played over a VASS. Initially introduced in the study of propositional linear logic, they have more recently gathered attention in the guise of multi-dimensional energy games for quantitative verification and synthesis. We show that establishing who is the winner in such a game with a state reachability objective is 2-ExpTime-complete. As a further application, we show that the same complexity result applies to the problem of whether a VASS is simulated by a finite-state system.
Complete list of metadatas
Contributor : Sylvain Schmitz <>
Submitted on : Tuesday, April 22, 2014 - 9:19:05 AM
Last modification on : Thursday, July 2, 2020 - 5:26:03 PM
Document(s) archivé(s) le : Monday, April 10, 2017 - 3:32:45 PM


Files produced by the author(s)


  • HAL Id : hal-00980878, version 1


Jean-Baptiste Courtois, Sylvain Schmitz. Alternating Vector Addition Systems with States. 2014. ⟨hal-00980878v1⟩



Record views


Files downloads