Conference Paper/Proceeding/Abstract 605 views
Symbolic model-checking for resource-bounded ATL
Natasha Alechina,
Brian Logan,
Hoang Nguyen 
,
Franco Raimondi,
Leonardo Mostarda
,
Franco Raimondi,
Leonardo Mostarda
AAMAS'15: International Conference on Autonomous Agents and Multiagent Systems
Swansea University Author:
Hoang Nguyen
Abstract
In this paper we present a symbolic implementation of a model checking algorithm for the verification of properties expressed in Resource-Bounded Alternating Time Temporal Logic (RB-ATL). The implementation is based on the model checker MCMAS. We evaluate the performance of our implementation using...
| Published in: | AAMAS'15: International Conference on Autonomous Agents and Multiagent Systems |
|---|---|
| Published: |
ACM Digital Library
2015
|
| Online Access: |
https://dl.acm.org/doi/10.5555/2772879.2773448 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa61991 |
| Abstract: |
In this paper we present a symbolic implementation of a model checking algorithm for the verification of properties expressed in Resource-Bounded Alternating Time Temporal Logic (RB-ATL). The implementation is based on the model checker MCMAS. We evaluate the performance of our implementation using simple multi-agent model checking problems of increasing complexity. |
|---|---|
| Item Description: |
https://dl.acm.org/doi/10.5555/2772879.2773448 |
| College: |
Faculty of Science and Engineering |