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. © 2014 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Courtois, J. B., & Schmitz, S. (2014). Alternating vector addition systems with states. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8634 LNCS, pp. 220–231). Springer Verlag. https://doi.org/10.1007/978-3-662-44522-8_19
Mendeley helps you to discover research relevant for your work.