Group synthesis for alternating-time temporal logic
File(s)DTR13-9.pdf (406.03 KB)
Published version
Author(s)
Jones, AV
Knapik, M
Lomuscio, Alessio
Penczek, W
Type
Report
Abstract
We present an extension of Alternating-time Temporal Logic
ATL, called ATLP (Parametric ATL), where parameters are allowed in
place of concrete groups of agents. We devise a procedure to nd all instantiations
for the parameters in a given formula of ATLP so that
is true in a given model. We propose a formalisation of the problem
and symbolic algorithms for its solution. We discuss an experimental implementation
of the approach on top of the open-source model checker
mcmas and demonstrate the bene ts of the technique through experimental
results.
ATL, called ATLP (Parametric ATL), where parameters are allowed in
place of concrete groups of agents. We devise a procedure to nd all instantiations
for the parameters in a given formula of ATLP so that
is true in a given model. We propose a formalisation of the problem
and symbolic algorithms for its solution. We discuss an experimental implementation
of the approach on top of the open-source model checker
mcmas and demonstrate the bene ts of the technique through experimental
results.
Date Issued
2013-01-01
Citation
Departmental Technical Report: 13/9, 2013, pp.1-16
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
16
Journal / Book Title
Departmental Technical Report: 13/9
Copyright Statement
© 2013 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
13/9