Practical verification of multi-agent systems against Slk specifications.
Information and Computation(2018)
摘要
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 Image 1, 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.
更多查看译文
关键词
Model checking,Strategy Logic,Multi-agent systems,Formal verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络