Perelli, Giuseppe
(2015)
Logics for Multi-Agent Systems Verification.
[Tesi di dottorato]
| Tipologia del documento: |
Tesi di dottorato
|
| Lingua: |
English |
| Titolo: |
Logics for Multi-Agent Systems Verification |
| Autori: |
| Autore | Email |
|---|
| Perelli, Giuseppe | perelli.gi@gmail.com |
|
| Data: |
Marzo 2015 |
| Numero di pagine: |
101 |
| Istituzione: |
Università degli Studi di Napoli Federico II |
| Dipartimento: |
Matematica e Applicazioni "Renato Caccioppoli" |
| Scuola di dottorato: |
Scienze matematiche e informatiche |
| Dottorato: |
Scienze computazionali e informatiche |
| Ciclo di dottorato: |
27 |
| Coordinatore del Corso di dottorato: |
| nome | email |
|---|
| Moscariello, Gioconda | gmoscari@unina.it |
|
| Tutor: |
| nome | email |
|---|
| Murano, Aniello | [non definito] |
|
| Data: |
Marzo 2015 |
| Numero di pagine: |
101 |
| Parole chiave: |
Logiche, Metodi Formali, Verifica |
| Settori scientifico-disciplinari del MIUR: |
Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
[error in script]
[error in script]
| Depositato il: |
10 Apr 2015 11:52 |
| Ultima modifica: |
25 Set 2015 08:25 |
| URI: |
http://www.fedoa.unina.it/id/eprint/10094 |
| DOI: |
10.6092/UNINA/FEDOA/10094 |
Abstract
Nel Capitolo 1 si introduce la logica SL e se ne richiamano i principali risultati di complessità. In particolare, si ricorda che il problema del model-checking è NonElementary-Hard, mentre la soddisfacibilità è indecidibile.
Nel Capitolo 2, prendendo a spunto il divario computazionale tra SL e la logica ATL*, per cui model-checking e soddisfacibilità sono 2ExpTime-Complete, si cerca di stabilire quali siano le caratteristiche sintattiche che rendono la prima fortemente intrattabile. Si introducono dapprima alcuni frammenti sintattici di SL, rispettivamente chiamati Nested-Goal Strategy Logic SL[NG], Boolean-Goal Strategy Logic SL[BG] e One-Goal Strategy Logic SL[1G], ordinati per inclusione dal più grande al più piccolo. Successivamente, si analizza una proprietà modellare, chiamata behavioral, che risulta centrale per l'applicazione di procedure risolutive computazionalmente più convenienti. In particolare, si dimostra che SL[1G] possiede tale proprietà. Tramite la behavioral property, si dimostra che il model-checking e la soddisfacibilità di SL[1G] è 2ExpTime-Complete. Inoltre, si mostra che il model-checking per SL[NG] è già NonElementary-Complete, mentre la soddisfacibilità per SL[BG] è già indecidibile.
Nel Capitolo 3, si applicano alcuni risultati ottenuti al problema della Sintesi Razionale, mostrando che questa ha complessità 2ExpTime-Complete sia nel caso cooperativo, introdotto da Fisman, Kupferman e Loding nel 2010, sia nel caso non-cooperativo, introdotto da Kupferman, Perelli e Vardi nel 2014. Il problema della sintesi è studiato anche nel caso quantitativo, in cui i goal degli agenti sono specificati mediante la logica Objective LTL (OLTL). Anche in questo caso, tramite una riduzione dal caso qualitativo, si è provato che la complessità del problema è 2ExpTime-Complete.
Nel Capitolo 4, si introducono i Pushdown-Concurrent Game Systems (PGS) per la rappresentazione finita di modelli ricorsivi. Per questi modelli è stato studiato il problema del model checking con specifiche in ATL*, mostrando una soluzione in 3ExpTime e un lower-bound in 2ExpSpace.
Downloads per month over past year
Actions (login required)
 |
Modifica documento |
