Di Stasio, Antonio
(2018)
Reasoning about LTL Synthesis over finite and infinite games.
[Tesi di dottorato]
| Tipologia del documento: |
Tesi di dottorato
|
| Lingua: |
English |
| Titolo: |
Reasoning about LTL Synthesis over finite and infinite games |
| Autori: |
| Autore | Email |
|---|
| Di Stasio, Antonio | antonio.distasio@unina.it |
|
| Data: |
11 Dicembre 2018 |
| Numero di pagine: |
101 |
| Istituzione: |
Università degli Studi di Napoli Federico II |
| Dipartimento: |
Matematica e Applicazioni "Renato Caccioppoli" |
| Dottorato: |
Scienze matematiche e informatiche |
| Ciclo di dottorato: |
31 |
| Coordinatore del Corso di dottorato: |
| nome | email |
|---|
| de Giovanni, Francesco | francesco.degiovanni2@unina.it |
|
| Tutor: |
| nome | email |
|---|
| Murano, Aniello | [non definito] |
|
| Data: |
11 Dicembre 2018 |
| Numero di pagine: |
101 |
| Parole chiave: |
Parity Games; Planning; Synthesis |
| Settori scientifico-disciplinari del MIUR: |
Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
[error in script]
[error in script]
| Depositato il: |
19 Dic 2018 09:16 |
| Ultima modifica: |
18 Giu 2020 05:14 |
| URI: |
http://www.fedoa.unina.it/id/eprint/12639 |
Abstract
In the last few years, research formal methods for the analysis and the verification of properties of systems has increased greatly. A meaningful contribution in this area has been given by algorithmic methods developed in the context of synthesis. The basic idea is simple and appealing: instead of developing a system and verifying that it satisfies its specification, we look for an automated procedure that, given the specification returns a system that is correct by construction. Synthesis of reactive systems is one of the most popular variants of this problem, in which we want to synthesize a system characterized by an ongoing interaction with the environment. In this setting, large effort has been devoted to analyze specifications given as formulas of linear temporal logic, i.e., LTL synthesis.
Traditional approaches to LTL synthesis rely on transforming the LTL specification into parity deterministic automata, and then to parity games, for which a so-called winning region is computed. Computing such an automaton is, in the worst-case, double-exponential in the size of the LTL formula, and this becomes a computational bottleneck in using the synthesis process in practice.
The first part of this thesis is devoted to improve the solution of parity games as they are used in solving LTL synthesis, trying to give efficient techniques, in terms of running time and space consumption, for solving parity games. We start with the study and the implementation of an automata-theoretic technique to solve parity games. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games
where the number of priorities is relatively small. This makes the new algorithm quite useful in practice.
We then provide a broad investigation of the symbolic approach for solving parity games. Specifically, we implement in a fresh tool, called SPGSolver, four symbolic algorithms to solve parity games and compare their performances to the corresponding explicit versions for different classes of games. By means of benchmarks, we show that for random games, even for constrained random games, explicit algorithms actually perform better than symbolic algorithms. The situation changes, however, for structured games, where symbolic algorithms seem to have the advantage. This suggests that when evaluating algorithms for parity-game solving, it would be useful to have real benchmarks and not only random benchmarks, as the common practice has been.
LTL synthesis has been largely investigated also in artificial intelligence, and specifically in
automated planning. Indeed, LTL synthesis corresponds to fully observable nondeterministic planning in which the domain is given compactly and the goal is an LTL formula, that in turn is related to two-player games with LTL goals. Finding a strategy for these games means to synthesize a plan for the planning problem. The last part of this thesis is then dedicated to investigate LTL synthesis under this different view. In particular, we study a generalized form of planning under partial observability, in which we have multiple, possibly infinitely many, planning domains with the same actions and observations, and goals expressed over observations, which are possibly temporally extended. By building on work on two-player games with imperfect information in the Formal Methods literature, we devise a general technique, generalizing the belief-state construction, to remove partial observability. This reduces the planning problem to a game of perfect information with a tight correspondence between plans and strategies. Then we instantiate the technique and solve some generalized planning problems.
Downloads per month over past year
Actions (login required)
 |
Modifica documento |
