Alternating Vector Addition Systems with States

Jean-Baptiste Courtois 1 Sylvain Schmitz 1, 2, *
* Corresponding author
2 DAHU - Verification in databases
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
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

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00980878
Contributor : Sylvain Schmitz <>
Submitted on : Monday, June 30, 2014 - 11:46:38 AM
Last modification on : Thursday, February 7, 2019 - 5:29:23 PM
Long-term archiving on : Tuesday, April 11, 2017 - 9:23:36 AM

File

article.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jean-Baptiste Courtois, Sylvain Schmitz. Alternating Vector Addition Systems with States. 39th International Symposium on Mathematical Foundations of Computer Science, Aug 2014, Budapest, Bulgaria. pp.220--231, ⟨10.1007/978-3-662-44522-8_19⟩. ⟨hal-00980878v2⟩

Share

Metrics

Record views

561

Files downloads

329