Dell'Erba, Daniele (2019) Solving Infinite Games on Graphs via Quasi Dominions. [Tesi di dottorato]

Preview

Text Thesis.pdf Download (2MB) | Preview

[error in script] [error in script]

Item Type:	Tesi di dottorato
Lingua:	English
Title:	Solving Infinite Games on Graphs via Quasi Dominions
Creators:	Creators Email Dell'Erba, Daniele daniele.dellerba@unina.it
Date:	2019
Number of Pages:	183
Institution:	Università degli Studi di Napoli Federico II
Department:	Matematica e Applicazioni "Renato Caccioppoli"
Dottorato:	Scienze matematiche e informatiche
Ciclo di dottorato:	32
Coordinatore del Corso di dottorato:	nome email De Giovanni, Francesco francesco.degiovanni2@unina.it
Tutor:	nome email Benerecetti, Massimo UNSPECIFIED Mogavero, Fabio UNSPECIFIED
Date:	2019
Number of Pages:	183
Uncontrolled Keywords:	Games on graphs, parity games, mean payoff
Settori scientifico-disciplinari del MIUR:	Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica
Date Deposited:	13 Jan 2020 13:04
Last Modified:	17 Nov 2021 12:22
URI:	http://www.fedoa.unina.it/id/eprint/12951

Abstract

In this thesis we present a new approach to efficiently solve two types of infinite-duration games on graphs, namely parity games and mean-payoff games, which can be used, in the context of formal verification, for the model checking and synthesis of hardware and software systems. Our main aim is to improve the performances of the corresponding solution algorithms in order to support their effective use in practice. We start with the analysis of one of the principal algorithms for parity games developed by Zielonka, called the Recursive Algorithm. This study lead to the discovery of an infinite family of games whose structure makes them very difficult to solve even by improved versions of the considered algorithm. A more robust version of this family is proved to be challenging for most of other parity algorithms known in the literature as well. We then present a novel technique based on the notion of quasi dominions that is able to defeat all of worst case families that were known in the literature. This technique, called priority promotion (PP, for short), is the focal point of a divide et impera algorithm that solves a game by looking for subsets of the winning regions by exploiting a relaxed notion of dominion which is precisely a quasi dominion. The obtained procedure exhibits the best known space complexity up to date, a result in line with the purpose of this thesis, i.e., making a scalable solution algorithm in practice. The experiments we conducted show that the approach is extremely effective on both concrete and synthetic problems. Due to the subsequent discovery of an exponential-time worst case for the PP algorithm, we also revised the proposed approach as a framework general enough to be instantiated with different game-decomposition techniques and solution policies. The resulting refinements of PP method significantly mitigate the exponential behaviors exhibited by the vanilla approach. A first refinement consists in a finer policy promotion, called delayed promotion, that delays some of the promotions that are the cause of the recomputation of discarded results that were already computed before. A second one, instead, called region recovery, simply tries to recover these results that would, instead, be needlessly discarded. The effectiveness of each refinement is strongly supported by experimental results. Every presented algorithm, indeed, outperforms those previously proposed. We finally investigate, with success, the possible application of the quasi-dominion based technique to solve mean-payoff games, by presenting an algorithm that matches the best known time complexity of the problem. Also in this case, we significantly improve on the practical application of solution algorithms, by proving the existence of a family of games on which the new algorithm performs arbitrarily better than the classic approaches.

Downloads

Actions (login required)

View Item