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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Stochastic Games with Lossy Channels
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
Manuscript (Other academic)
Identifiers
URN: urn:nbn:se:uu:diva-95522OAI: oai:DiVA.org:uu-95522DiVA: diva2:169770
Funder
Available from: 2007-03-02 Created: 2007-03-02 Last updated: 2011-01-17
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.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 277
Keyword
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
Identifiers
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
Opponent
Supervisors
Available from: 2007-03-02 Created: 2007-03-02 Last updated: 2011-02-17Bibliographically approved

Open Access in DiVA

No full text

Authority records BETA

Abdulla, Parosh Aziz

Search in DiVA

By author/editor
Abdulla, Parosh Aziz
By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 519 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf