@Unpublished{     courtois:hal-00980878,
  Author        = "Courtois, Jean-Baptiste and Schmitz, Sylvain",
  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.}",
  affiliation   = "Laboratoire Sp{\'e}cification et V{\'e}rification [Cachan] - LSV , DAHU - INRIA Saclay - Ile de France",
  date-added    = "2014-07-01 06:15:27 +0000",
  date-modified = "2014-12-02 09:05:38 +0000",
  hal_id        = "hal-00980878",
  Keywords      = "readme",
  Language      = "Anglais",
  PDF           = "http://hal.inria.fr/hal-00980878/PDF/article.pdf",
  Title         = "{Alternating Vector Addition Systems with States}",
  URL           = "http://hal.inria.fr/hal-00980878",
  bdsk-url-1    = "http://hal.inria.fr/hal-00980878",
  File          = "Alternating Vector Addition Systems with States - Courtois, Schmitz (1) (0) - a - a - b.pdf",
  file-2        = "Alternating Vector Addition Systems with States - Courtois, Schmitz (0) (0) - a - a - b.pdf"
}

@Unpublished{ courtois:hal-00980878, Author = "Courtois, Jean-Baptiste and Schmitz, Sylvain", 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.}", affiliation = "Laboratoire Sp{\'e}cification et V{\'e}rification [Cachan] - LSV , DAHU - INRIA Saclay - Ile de France", date-added = "2014-07-01 06:15:27 +0000", date-modified = "2014-12-02 09:05:38 +0000", hal_id = "hal-00980878", Keywords = "readme", Language = "Anglais", PDF = "http://hal.inria.fr/hal-00980878/PDF/article.pdf", Title = "{Alternating Vector Addition Systems with States}", URL = "http://hal.inria.fr/hal-00980878", bdsk-url-1 = "http://hal.inria.fr/hal-00980878", File = "Alternating Vector Addition Systems with States - Courtois, Schmitz (1) (0) - a - a - b.pdf", file-2 = "Alternating Vector Addition Systems with States - Courtois, Schmitz (0) (0) - a - a - b.pdf" }