Parameterised model checking for alternating-time temporal logic
File(s)FAIA285-0725.pdf (361.54 KB)
Published version
Author(s)
Kouvaros, Panagiotis
Lomuscio, Alessio
Type
Conference Paper
Abstract
We investigate the parameterised model checking problem for specifications expressed in alternating-time temporal logic. We introduce parameterised concurrent game structures representing infinitely many games with different number of agents. We introduce a parametric variant of ATL to express properties of the system irrespectively of the number of agents present in the system. While the parameterised model checking problem is undecidable, we define a special class of systems on which we develop a sound and complete counter abstraction technique. We illustrate the methodology here devised on the prioritised version of the train-gate-controller.
Editor(s)
Kaminka, GA
Fox, M
Bouquet, P
Hullermeier, E
Dignum, V
Dignum, F
VanHarmelen, F
Date Issued
2016-08-01
Date Acceptance
2016-06-07
Citation
Frontiers in Artificial Intelligence and Applications, 2016, 285, pp.1230-1238
ISBN
978-1-61499-671-2
ISSN
0922-6389
Publisher
IOS Press
Start Page
1230
End Page
1238
Journal / Book Title
Frontiers in Artificial Intelligence and Applications
Volume
285
Copyright Statement
© 2016 The Authors and IOS Press.This article is published online with Open Access by IOS Press and distributed under the termsof the Creative Commons Attribution Non-Commercial License 4.0 (CC BY-NC 4.0).
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Identifier
http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000385793700143&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=1ba7043ffcc86c417c072aa74d649202
Grant Number
EP/I00520X/1
COLAR_P60375
Source
22nd European Conference on Artificial Intelligence (ECAI)
Subjects
Science & Technology
Technology
Computer Science, Artificial Intelligence
Computer Science
CONCURRENT SYSTEMS
VERIFICATION
Publication Status
Published
Start Date
2016-08-29
Finish Date
2016-09-02
Coverage Spatial
Hague, NETHERLANDS