Perelli, Giuseppe (2015) Logics for Multi-Agent Systems Verification. [Tesi di dottorato]

[img]
Preview
Text
Perelli_Giuseppe_27.pdf

Download (987kB) | Preview
[error in script] [error in script]
Item Type: Tesi di dottorato
Lingua: English
Title: Logics for Multi-Agent Systems Verification
Creators:
CreatorsEmail
Perelli, Giuseppeperelli.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:
nomeemail
Moscariello, Giocondagmoscari@unina.it
Tutor:
nomeemail
Murano, AnielloUNSPECIFIED
Date: March 2015
Number of Pages: 101
Uncontrolled 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

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.

Actions (login required)

View Item View Item