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

Direct link
Complexity of model checking by iterative improvement: the pseudo-Boolean framework
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology.
2003 In: Perspectives of Systems Informatics: 5th International Andrei Ershov Memorial Conference, 2003, 381-394 p.Chapter in book (Other academic) Published
Place, publisher, year, edition, pages
2003. 381-394 p.
URN: urn:nbn:se:uu:diva-92510ISBN: 3-540-20813-5OAI: oai:DiVA.org:uu-92510DiVA: diva2:165621
Available from: 2005-01-18 Created: 2005-01-18Bibliographically approved
In thesis
1. Combinatorial Optimization for Infinite Games on Graphs
Open this publication in new window or tab >>Combinatorial Optimization for Infinite Games on Graphs
2005 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Games on graphs have become an indispensable tool in modern computer science. They provide powerful and expressive models for numerous phenomena and are extensively used in computer- aided verification, automata theory, logic, complexity theory, computational biology, etc.

The infinite games on finite graphs we study in this thesis have their primary applications in verification, but are also of fundamental importance from the complexity-theoretic point of view. They include parity, mean payoff, and simple stochastic games.

We focus on solving graph games by using iterative strategy improvement and methods from linear programming and combinatorial optimization. To this end we consider old strategy evaluation functions, construct new ones, and show how all of them, due to their structural similarities, fit into a unifying combinatorial framework. This allows us to employ randomized optimization methods from combinatorial linear programming to solve the games in expected subexponential time.

We introduce and study the concept of a controlled optimization problem, capturing the essential features of many graph games, and provide sufficent conditions for solvability of such problems in expected subexponential time.

The discrete strategy evaluation function for mean payoff games we derive from the new controlled longest-shortest path problem, leads to improvement algorithms that are considerably more efficient than the previously known ones, and also improves the efficiency of algorithms for parity games.

We also define the controlled linear programming problem, and show how the games are translated into this setting. Subclasses of the problem, more general than the games considered, are shown to belong to NP intersection coNP, or even to be solvable by subexponential algorithms.

Finally, we take the first steps in investigating the fixed-parameter complexity of parity, Rabin, Streett, and Muller games.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2005. 51 p.
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 3
infinite games, combinatorial optimization, randomized algorithms, model checking, strategy evaluation functions, linear programming, iterative improvement, local search
National Category
Computer Science
urn:nbn:se:uu:diva-4751 (URN)91-554-6129-8 (ISBN)
Public defence
2005-02-18, 10132, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 14:15
Available from: 2005-01-18 Created: 2005-01-18 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: 68 hits
ReferencesLink to record
Permanent link

Direct link