Conference item icon

Conference item

Probabilistic timed ATL

Abstract:
Weconsider strategic reasoning for multi-agent systems modelled as networks of continuous-time probabilistic timed automata (TA) with asynchronous execution (PCAMAS) in the setting of imperfect information. We define PTATL, a probabilistic extension of the alternating-time timed temporal logic TATL, which is interpreted over PCAMAS. Focusing on memoryless strategies of agents with imperfect information, both probabilistic (irP) and deterministic (irp), we establish theoretical results regarding the computational complexity of model checking for the proposed logic: between PSPACE and EXPTIME for PTATLirp, and in 2EXPTIME for PTATLirP. We demonstrate the practical feasibility of verification for PTATLirp formulas through a novel proof-of-concept combination of state-of-the-art tools IMITATOR and PRISM on a scalable benchmark, with encouraging results.
Publication status:
Published
Peer review status:
Peer reviewed

Actions

Access Document

Files:
Publication website:
https://dl.acm.org/doi/10.5555/3709347.3743625

Authors

More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Engineering Science
Role:
Author


More from this funder
Funder identifier:
https://ror.org/0472cxd90
Grant:
834115


Publisher:
Association for Computing Machinery
Host title:
AAMAS '25: Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems
Pages:
1051-1059
Publication date:
2025-06-05
Event title:
24th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2025)
Event location:
Detroit, Michigan, USA
Event website:
https://aamas2025.org/
Event start date:
2025-05-19
Event end date:
2025-05-23
EISSN:
1558-2914
ISSN:
1548-8403


Language:
English
Keywords:
Pubs id:
2247710
UUID:
uuid_f0673024-d8aa-46f0-b0fb-79ec2bc0a025
Local pid:
pubs:2247710
Deposit date:
2025-11-10
ARK identifier:

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP