Conference Paper/Proceeding/Abstract 486 views
Symbolic model-checking for resource-bounded ATL
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 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
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 |