In an earlier work [ACJYK00] we presented a general frame-work for verification of infinite-state transition systems, where the transition relation is monotonic with respect to a well quasi-ordering on the set of states. In this paper, we investigate extending the framework for the context of transition systems to that of games. We show that monotonic games are in general undecidable. We identify a subclass of monotonic games, called downward closed games. We provide algorithms for analyzing downward closed games subject to winning conditions which are formulated as safety properties.
展开▼
