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

Direct link
Limiting Behavior of Markov Chains with Eager Attractors
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology.
2006 In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST 2006), 2006, 253--262 p.Chapter in book (Other academic) Published
Place, publisher, year, edition, pages
2006. 253--262 p.
URN: urn:nbn:se:uu:diva-95521OAI: oai:DiVA.org:uu-95521DiVA: diva2:169769
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

Total: 215 hits
ReferencesLink to record
Permanent link

Direct link