Perelli, Giuseppe (2015) Logics for Multi-Agent Systems Verification. [Tesi di dottorato]
Preview |
Text
Perelli_Giuseppe_27.pdf Download (987kB) | Preview |
| Item Type: | Tesi di dottorato |
|---|---|
| Resource language: | English |
| Title: | Logics for Multi-Agent Systems Verification |
| Creators: | Creators Email Perelli, Giuseppe perelli.gi@gmail.com |
| Date: | March 2015 |
| Number of Pages: | 101 |
| Institution: | Università degli Studi di Napoli Federico II |
| Department: | 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 UNSPECIFIED |
| Date: | March 2015 |
| Number of Pages: | 101 |
| Keywords: | Logiche, Metodi Formali, Verifica |
| Settori scientifico-disciplinari del MIUR: | Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
| Date Deposited: | 10 Apr 2015 11:52 |
| Last Modified: | 25 Sep 2015 08:25 |
| URI: | http://www.fedoa.unina.it/id/eprint/10094 |
| DOI: | 10.6092/UNINA/FEDOA/10094 |
Collection description
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
Downloads per month over past year
Actions (login required)
 |
View Item |
