×

zbMATH — the first resource for mathematics

Alternating vector addition systems with states. (English) Zbl 1425.68290
Csuhaj-Varjú, Erzsébet (ed.) et al., Mathematical foundations of computer science 2014. 39th international symposium, MFCS 2014, Budapest, Hungary, August 25–29, 2014. Proceedings, Part I. Berlin: Springer. Lect. Notes Comput. Sci. 8634, 220-231 (2014).
Summary: 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.
For the entire collection see [Zbl 1294.68016].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q25 Analysis of algorithms and problem complexity
91A80 Applications of game theory
PDF BibTeX XML Cite
Full Text: DOI