Symbolic model checking for one-resource RB+-ATL

RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The modelchecking problem for RB+-ATL is known to be decidable. However the only available model checking algorithm for RB+-ATL uses a forward search of the state space, a...

Full description

Bibliographic Details
Main Authors: Alechina, Natasha, Logan, Brian, Nguyen, Hoang Nga, Raimondi, Franco
Format: Conference or Workshop Item
Language:English
Published: 2015
Online Access:https://eprints.nottingham.ac.uk/30173/