Decidable model-checking for a resource logic with production of resources

Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the m...

Full description

Bibliographic Details
Main Authors: Alechina, Natasha, Logan, Brian, Nguyen, Hoang Nga, Raimondi, Franco
Format: Conference or Workshop Item
Published: 2014
Online Access:https://eprints.nottingham.ac.uk/30179/
_version_ 1848793936777183232
author Alechina, Natasha
Logan, Brian
Nguyen, Hoang Nga
Raimondi, Franco
author_facet Alechina, Natasha
Logan, Brian
Nguyen, Hoang Nga
Raimondi, Franco
author_sort Alechina, Natasha
building Nottingham Research Data Repository
collection Online Access
description Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable.
first_indexed 2025-11-14T19:08:13Z
format Conference or Workshop Item
id nottingham-30179
institution University of Nottingham Malaysia Campus
institution_category Local University
last_indexed 2025-11-14T19:08:13Z
publishDate 2014
recordtype eprints
repository_type Digital Repository
spelling nottingham-301792020-05-04T16:52:20Z https://eprints.nottingham.ac.uk/30179/ Decidable model-checking for a resource logic with production of resources Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable. 2014-08-18 Conference or Workshop Item PeerReviewed Alechina, Natasha, Logan, Brian, Nguyen, Hoang Nga and Raimondi, Franco (2014) Decidable model-checking for a resource logic with production of resources. In: European Conference on Artificial Intelligence (ECAI 2014), 18-22 Aug 2014, Prague, Czech Republic. http://ebooks.iospress.nl/publication/36908
spellingShingle Alechina, Natasha
Logan, Brian
Nguyen, Hoang Nga
Raimondi, Franco
Decidable model-checking for a resource logic with production of resources
title Decidable model-checking for a resource logic with production of resources
title_full Decidable model-checking for a resource logic with production of resources
title_fullStr Decidable model-checking for a resource logic with production of resources
title_full_unstemmed Decidable model-checking for a resource logic with production of resources
title_short Decidable model-checking for a resource logic with production of resources
title_sort decidable model-checking for a resource logic with production of resources
url https://eprints.nottingham.ac.uk/30179/
https://eprints.nottingham.ac.uk/30179/