Skip Navigation


Journal of Logic and Computation Advance Access originally published online on November 22, 2007
Journal of Logic and Computation 2008 18(1):153-169; doi:10.1093/logcom/exm062
This Article
Right arrow Full Text (PDF)
Right arrow All Versions of this Article:
18/1/153    most recent
exm062v1
Right arrow References
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Abdulla, P. A.
Right arrow Articles by D'orso, J.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2007. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Articles

Monotonic and Downward Closed Games*

Parosh Aziz Abdulla

Uppsala University, Sweden. E-mail: parosh{at}it.uu.se

Ahmed Bouajjani and Julien D'orso

University of Paris 7, France.

Received 19 September 2005.


  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.

Keywords: infinite-state games; lossy channel systems; Vector Addition Systems; Petri nets

* A preliminary version of this article appeared in Proc. CSL/KGC'03, Computer Science Logic and 8th Kurt Gödel Colloquium, 2003.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.