Specifications for decidable hybrid games

We introduce STORMED hybrid games (SHG), a generalization of STORMED hybrid systems, Vladimerou et al. (2008) [33], which have natural specifications that allow rich continuous dynamics and various decidable properties. We solve the control problem for SHG using a reduction to bisimulation on finite game graphs. This generalizes to a greater family of games, which includes o-minimal hybrid games, Bouyer et al. (2006)161. We also solve the optimal-cost reachability problem for Weighted SHG and prove decidability of WCTL for Weighted STORMED hybrid systems. (C) 2011 Elsevier B.V. All rights reserved