Model checking coalitional games in shortage resource scenarios
Dario Della Monica, Margherita Napoli, Mimmo Parente

TL;DR
This paper introduces PRBATL, a novel logic for verifying multi-agent systems with shared, dynamically priced resources, providing a semantic approach to model resource evolution and market dynamics.
Contribution
It formalizes resource availability and pricing in MAS verification, proves EXPTIME-hardness of model checking, and compares the approach with previous resource logics.
Findings
PRBATL effectively models resource dynamics in MAS.
Model checking for PRBATL is EXPTIME-hard.
The formalism captures shared and priced resources in real-world scenarios.
Abstract
Verification of multi-agents systems (MAS) has been recently studied taking into account the need of expressing resource bounds. Several logics for specifying properties of MAS have been presented in quite a variety of scenarios with bounded resources. In this paper, we study a different formalism, called Priced Resource-Bounded Alternating-time Temporal Logic (PRBATL), whose main novelty consists in moving the notion of resources from a syntactic level (part of the formula) to a semantic one (part of the model). This allows us to track the evolution of the resource availability along the computations and provides us with a formalisms capable to model a number of real-world scenarios. Two relevant aspects are the notion of global availability of the resources on the market, that are shared by the agents, and the notion of price of resources, depending on their availability. In a…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
