Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
Accelerated Approximation for Stochastic Reachability Games: Extended version of paper New algorithms for solving simple stochastic games
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2010 (English)Other (Other academic)
Abstract [en]

In this paper new algorithms for finding optimal values and strategies inturn-based stochastic games with reachability objectives are presented,whose special case are the simple stochastic games considered elsewhere [4,11]. The general idea of these algorithms is to accelerate the successive approximation scheme for solving stochastic games [13] in which node values are updated in each iteration so that they converge to the optimal values of the game. This scheme is extended with a pair of positional strategies which are updated to remain greedy with respect to the current approximation. This way optimal strategies can be discovered before the current values get close to the optimal ones. The approximation process is accelerated, by predicting an approximate result of several updates of the current valuation and jumping directly to the predicted values.

New algorithms are based on three different acceleration techniques: iterative squaring, linear extrapolation, and linear programming; with different difficulty of performing single iteration and different acceleration level achieved by each of them. For each of these algorithms the complexity of a single iteration is polynomial. It is shown that accelerated algorithms will never perform worse than the basic, non-accelerated one and exponential upper bounds on the number of iterations required to solve a game in the worst case is given. It is also proven that new algorithms increase the frequency with which the greedy strategies are updated. The more often strategies are updated, the higher chances that the algorithm will terminate early. It is proven that the algorithm based on linear programming updates the greedy strategies in every iteration, which makes it similar to the strategy improvement method, where also a new strategy is found in each iteration and this also at the cost of solving linear constraint problems

Paper is concluded with presentation of results of experiments in which new algorithms were run on a sample of randomly generated games. It could be observed that the proposed acceleration techniques reduce the number of iterations of the basic algorithm by an order of magnitude and that they substantially increase frequency with which the greedy strategies are updated. The algorithms based on linear programming and linear extrapolation displayed similar efficiency as the ones based on strategy improvement. This makes the algorithm based on linear extrapolation especially attractive because it uses much simpler computations than linear constraint solving.

Place, publisher, year, pages
2010.
Keyword [en]
simple stochastic games, successive approximation, strategy improvement, complexity
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-179845OAI: oai:DiVA.org:uu-179845DiVA: diva2:546649
Note

The original paper was published in Proceedings of the Workshop on Games in Design and Verification (GDV 2004), volume 119 of Electronic Notes in Theoretical Computer Science, pages 51–65. Elsevier. http://dx.doi.org/10.1016/j.entcs.2004.07.008

Available from: 2012-08-24 Created: 2012-08-24 Last updated: 2013-01-22Bibliographically approved
In thesis
1. Logics and Algorithms for Verification of Concurrent Systems
Open this publication in new window or tab >>Logics and Algorithms for Verification of Concurrent Systems
2012 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In this thesis we investigate how the known framework of automatic formal verification by model checking can be extended in different directions. One extension is to go beyond the common limitation of the existing specification formalisms, that they can describe only regular properties of components. This can be achieved using logics capable of expressing non-regular properties, such as the Propositional Dynamic Logic of Context-free Programs (PDLCF), Fixpoint Logic with Chop (FLC) or the Higher-order Fixpoint Logic (HFL). Our main result in this area is proving that the problem of model checking HFL formulas of order bounded by k is k-EXPTIME complete. In the proofs we demonstrate two model checking algorithms for that logic. We also show that PDLCF is equivalent to a proper fragment of FLC.

The standard model checking algorithms, which are run on a single computer, are severely limited by the amount of available computing resources. A way to overcome this limitation is to develop distributed algorithms, which can be run on a cluster of computers and use their joint resources. In this thesis we show how a distributed model checking algorithm for the alternation-free fragment of the modal μ-calculus can be extended to handle formulas with one level of alternation. This is an important extension, since Lμ formulas with one level of alternation can express the same properties as logics LTL and CTL commonly used in formal verification.

Finally, we investigate stochastic games which can be used to model additional aspects of components, such as their interaction with environment and their quantitative properties. We describe new algorithms for finding optimal values and strategies in turn-based stochastic games with reachability winning conditions. We prove their correctness and report on experiments where we compare them against each other and against other known algorithms, such as value iteration and strategy improvement.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2012. 48 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 964
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-179847 (URN)978-91-554-8447-7 (ISBN)
Public defence
2012-10-01, Room 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2012-09-11 Created: 2012-08-24 Last updated: 2014-07-21Bibliographically approved

Open Access in DiVA

fulltext(212 kB)97 downloads
File information
File name FULLTEXT01.pdfFile size 212 kBChecksum SHA-512
a0f5ed06ccb872621bb45ea2abaf3a6a362a0f4ce90c3b0948e10ada5783838e33bb03d444866ba000039a2462b0f908fb4a9f13700486f1ca176a5d7393b334
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 97 downloads
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

urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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