Logics for Multi-Agent Systems Verification

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.