Strategy RV: A tool to approximate ATL model checking under imperfect information and perfect recall

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We present Strategy RV, a tool that allows to approximate the verification of Alternating-time Temporal Logic under imperfect information and perfect recall, which is known to be undecidable, by using Runtime Verification. The tool uses an interface to enter the game model and the specifications and to provide results. We test Strategy RV in a variant of the Curiosity rover scenario and provide some experimental results.

Original languageEnglish
Title of host publication20th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2021
PublisherInternational Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)
Pages1752-1754
Number of pages3
ISBN (Electronic)9781713832621
Publication statusPublished - 1 Jan 2021
Event20th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2021 - Virtual, Online
Duration: 3 May 20217 May 2021

Publication series

NameProceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
Volume3
ISSN (Print)1548-8403
ISSN (Electronic)1558-2914

Conference

Conference20th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2021
CityVirtual, Online
Period3/05/217/05/21

Keywords

  • ATL Model Checking
  • Imperfect Information
  • Perfect Recall Strategies
  • Runtime Verification

Fingerprint

Dive into the research topics of 'Strategy RV: A tool to approximate ATL model checking under imperfect information and perfect recall'. Together they form a unique fingerprint.

Cite this