uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Memoryless Determinacy of Parity and Mean Payoff Games: A Simple Proof
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology.
2004 In: Theoretical Computer Science, ISSN 0304-3975, Vol. 310, no 1-3, 365-378 p.Article in journal (Refereed) Published
Place, publisher, year, edition, pages
2004. Vol. 310, no 1-3, 365-378 p.
URN: urn:nbn:se:uu:diva-95518OAI: oai:DiVA.org:uu-95518DiVA: diva2:169766
Available from: 2007-03-02 Created: 2007-03-02Bibliographically approved
In thesis
1. Games and Probabilistic Infinite-State Systems
Open this publication in new window or tab >>Games and Probabilistic Infinite-State Systems
2007 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Computer programs keep finding their ways into new safety-critical applications, while at the same time growing more complex. This calls for new and better methods to verify the correctness of software. We focus on one approach to verifying systems, namely that of model checking. At first, we investigate two categories of problems related to model checking: games and stochastic infinite-state systems. In the end, we join these two lines of research, by studying stochastic infinite-state games.

Game theory has been used in verification for a long time. We focus on finite-state 2-player parity and limit-average (mean payoff) games. These problems have applications in model checking for the μ-calculus, one of the most expressive logics for programs. We give a simplified proof of memoryless determinacy. The proof applies both to parity and limit-average games. Moreover, we suggest a strategy improvement algorithm for limit-average games. The algorithm is discrete and strongly subexponential.

We also consider probabilistic infinite-state systems (Markov chains) induced by three types of models. Lossy channel systems (LCS) have been used to model processes that communicate over an unreliable medium. Petri nets model systems with unboundedly many parallel processes. Noisy Turing machines can model computers where the memory may be corrupted in a stochastic manner. We introduce the notion of eagerness and prove that all these systems are eager. We give a scheme to approximate the value of a reward function defined on paths. Eagerness allows us to prove that the scheme terminates. For probabilistic LCS, we also give an algorithm that approximates the limit-average reward. This quantity describes the long-run behavior of the system.

Finally, we investigate Büchi games on probabilistic LCS. Such games can be used to model a malicious cracker trying to break a network protocol. We give an algorithm to solve these games.

Place, publisher, year, edition, pages
Uppsala: Universitetsbiblioteket, 2007. 230 p.
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 277
program verification, model checking, determinacy, strategy improvement, infinite games, parity games, mean payoff games, stochastic games, Büchi games, reachability games, limiting average, limiting behavior, Markov chains, infinite-state systems, lossy channel systems, vector addition systems, noisy Turing machines
National Category
Computer Science
urn:nbn:se:uu:diva-7607 (URN)978-91-554-6813-2 (ISBN)
Public defence
2007-03-23, Polhemsalen, Ångström laboratory, Lägerhyddsvägen 1, 10:15
Available from: 2007-03-02 Created: 2007-03-02 Last updated: 2011-02-17Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 200 hits
ReferencesLink to record
Permanent link

Direct link