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 Abstract Freely available
Right arrow Full Text (PDF)
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.

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.



References

  1. Abdulla PA, Cerans K, Jonsson B, Tsay Y-K. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation (2000) 160:109–127.[CrossRef][ISI]
  2. Alur R, Dill D. Automata for modelling real-time systems. In: Vol. 443 of Lecture Notes in Computer Science (1990) Proceedings of ICALP '90. Warwick: Springer. 322–335.
  3. Alur R, Henzinger T, Kupferman O. Alternating-time temporal logic. (1997) Proceedings of 38th Annual Symposium on Foundations of Computer Science. Miami Beach, Florida: IEEE Computer Society. 100–109.
  4. Abdulla PA, Jonsson B. Undecidable verification problems for programs with unreliable channels. Information and Computation (1996) 130:71–90.[CrossRef][ISI]
  5. Abdulla PA, Jonsson B. Verifying programs with unreliable channels. Information and Computation (1996) 127:91–101.[CrossRef][ISI]
  6. Abdulla PA, Nylén A. Timed Petri nets and BQOs. (2001) Proc. ICATPN'2001: 22nd International Conference on Application and Theory of Petri nets. Vol. 2075 of Lecture Notes in Computer Science. Newcastle, UK: Springer. 53–70.
  7. Barzdin JM, Bicevskis JJ, Kalninsh AA. Automatic construction of complete sample systems for program testing. In: IFIP Congress, 1977 (1977) Toronto, North-Holland.
  8. Bouajjani A, Mayr R. Model checking lossy vector addition systems. In: Symposium on Theoretical Aspects of Computer Science. Vol. 1563 of Lecture Notes in Computer Science (1999) Trier, Germany: Springer. 323–333.
  9. Cerans K. Deciding properties of integral relational automata. In: Proc. ICALP '94, 21st International Colloquium on Automata, Languages, and Programming, Vol. 820 of Lecture Notes in Computer Science—Abiteboul Serge, Shamir Eli, eds. (1994) Jerusalem: Springer Verlag. 35–46.
  10. de Alfaro L, Henzinger T, Majumdar R. Symbolic algorithms for infinite-state games. Larsen KG, Nielsen M, eds. (2001) Proc. CONCUR 2001, 12th International Conference on Concurrency Theory. Vol. 2154 of Lecture Notes in Computer Science. Aaalborg: Springer Verlag. 536–550.
  11. Delzanno G. Automatic verification of cache coherence protocols. Allen Emerson E, Prasad Sistla A, eds. (2000) Proceedings 12th International Conference on Computer Aided Verification.Vol. 1855 of Lecture Notes in Computer Science. Chicago: Springer Verlag. 53–68.
  12. Delzanno G, Esparza J, Podelski A. Constraint-based analysis of broadcast protocols. In: Proc. CSL'99 (1999) Madrid: Springer.
  13. Esparza J, Finkel A, Mayr R. On the verification of broadcast protocols. (1999) Proc. LICS '99, 14th IEEE International Symposium on Logic in Computer Science, IEEE Computer Society: Trento, Italy.
  14. Finkel A. Decidability of the termination problem for completely specified protocols. Distributed Computing (1994) 7:129–135.[CrossRef][ISI]
  15. Finkel A, Schnoebelen P. Well-structured transition systems everywhere! Theoretical Computer Science (2001) 256:63–92.[CrossRef][ISI]
  16. Grädel E, Thomas W, Wilke T. Automata, Logics, and Infinite Games: A Guide to Current Research. In: Vol. 2500 of Lecture Notes in Computer Science (2002) Dagstuhl, Germany: Springer.
  17. Higman G. Ordering by divisibility in abstract algebras. (1952) 2. Proceedings of London Mathematical Society. 326–336.
  18. JanCar P. Undecidability of bisimilarity for Petri nets and related problem. Theoretical Computer Science (1995) 148:281–301.[CrossRef][ISI]
  19. Mayr R. Undecidable problems in unreliable computations. In: Theoretical Informatics (LATIN'2000). Number 1776 in Lecture Notes in Computer Science (2000) Punta del Este, Uruguay: Springer.
  20. Raskin J-F, Samuelides M, Van Begin L. Games for counting abstractions. Electronic Notes in Theoretical Computer Science (2005) 128:69–85.[CrossRef]
  21. Thomas W. Infinite games and verification. (2002) In Proceedings of 14th International Conference on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science. Copenhagen, Denmark: Springer. 58–64.
  22. Zielonka W. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science (1998) 200:135–183.[CrossRef][ISI]

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



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
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?