@article{AbdullaBouajjaniDorso:JLC:2008,
    Abstract = {In an earlier work [Abdulla et al. (2000, Information and Computation, 160, 109--127)] we presented a general framework 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 article, we investigate extending the framework from the context of transition systems to that of games with infinite state spaces. We show that monotonic games with safety winning conditions are in general undecidable. In particular, we show this negative results for games which are defined over Petri nets. We identify a subclass of monotonic games, called downward closed games. We provide algorithms for analysing downward closed games subject to safety winning conditions. We apply the algorithm to games played on lossy channel systems. Finally, we show that weak parity games are undecidable for the above classes of games.},
    Author = {Abdulla, Parosh Aziz and Bouajjani, Ahmed and D'orso, Julien},
    EPrint = {http://logcom.oxfordjournals.org/content/18/1/153.full.pdf+html},
    File = {Monotonic and Downward Closed Games - Abdulla, Bouajjani, D'orso (0) (0) - a - a - s.pdf},
    Journal = {Journal of Logic and Computation},
    Keywords = {well-structured transition systems},
    Number = {1},
    Pages = {153-169},
    Title = {Monotonic and Downward Closed Games},
    URL = {http://logcom.oxfordjournals.org/content/18/1/153.abstract},
    Volume = {18},
    Year = {2008},
    bdsk-url-1 = {http://logcom.oxfordjournals.org/content/18/1/153.abstract},
    bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/exm062},
    date-added = {2013-03-27 16:58:36 +0000},
    date-modified = {2014-07-28 14:54:57 +0000},
    file-2 = {Monotonic and Downward Closed Games - Abdulla, Bouajjani, D'orso (1) (0) - a - a - s.pdf},
    doi = {10.1093/logcom/exm062}
}

@article{AbdullaBouajjaniDorso:JLC:2008, Abstract = {In an earlier work [Abdulla et al. (2000, Information and Computation, 160, 109--127)] we presented a general framework 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 article, we investigate extending the framework from the context of transition systems to that of games with infinite state spaces. We show that monotonic games with safety winning conditions are in general undecidable. In particular, we show this negative results for games which are defined over Petri nets. We identify a subclass of monotonic games, called downward closed games. We provide algorithms for analysing downward closed games subject to safety winning conditions. We apply the algorithm to games played on lossy channel systems. Finally, we show that weak parity games are undecidable for the above classes of games.}, Author = {Abdulla, Parosh Aziz and Bouajjani, Ahmed and D'orso, Julien}, EPrint = {http://logcom.oxfordjournals.org/content/18/1/153.full.pdf+html}, File = {Monotonic and Downward Closed Games - Abdulla, Bouajjani, D'orso (0) (0) - a - a - s.pdf}, Journal = {Journal of Logic and Computation}, Keywords = {well-structured transition systems}, Number = {1}, Pages = {153-169}, Title = {Monotonic and Downward Closed Games}, URL = {http://logcom.oxfordjournals.org/content/18/1/153.abstract}, Volume = {18}, Year = {2008}, bdsk-url-1 = {http://logcom.oxfordjournals.org/content/18/1/153.abstract}, bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/exm062}, date-added = {2013-03-27 16:58:36 +0000}, date-modified = {2014-07-28 14:54:57 +0000}, file-2 = {Monotonic and Downward Closed Games - Abdulla, Bouajjani, D'orso (1) (0) - a - a - s.pdf}, doi = {10.1093/logcom/exm062} }