We introduce Strategy Logic with Knowledge, a novel formalism to reason about knowledge and strategic ability in memoryless multi-agent systems with incomplete information. We exemplify its expressive power; we define the model checking problem for the logic and show that it is PSPACE-COMPLETE. We propose a labelling algorithm for solving the verification problem that we show is amenable to symbolic implementation. We introduce [Figure presented], an extension of the open-source model checker MCMAS, implementing the proposed algorithm. We report the benchmarks obtained on a number of scenarios from the literature, including the dining cryptographers protocol. © 2017

Practical verification of multi-agent systems against Slk specifications / Cermak, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 261:3(2018), pp. 588-614. [10.1016/j.ic.2017.09.011]

Practical verification of multi-agent systems against Slk specifications

Mogavero, Fabio;Murano, Aniello
2018

Abstract

We introduce Strategy Logic with Knowledge, a novel formalism to reason about knowledge and strategic ability in memoryless multi-agent systems with incomplete information. We exemplify its expressive power; we define the model checking problem for the logic and show that it is PSPACE-COMPLETE. We propose a labelling algorithm for solving the verification problem that we show is amenable to symbolic implementation. We introduce [Figure presented], an extension of the open-source model checker MCMAS, implementing the proposed algorithm. We report the benchmarks obtained on a number of scenarios from the literature, including the dining cryptographers protocol. © 2017
2018
Practical verification of multi-agent systems against Slk specifications / Cermak, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 261:3(2018), pp. 588-614. [10.1016/j.ic.2017.09.011]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11588/693916
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 33
  • ???jsp.display-item.citation.isi??? 17
social impact