Formal Modelling and Verification of Probabilistic Resource Bounded Agents

Hoang Nga Nguyen, Abdur Rakib

Research output: Contribution to journalArticlepeer-review


Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity.
Original languageEnglish
Pages (from-to)(In-Press)
Number of pages32
JournalThe Journal of Logic, Language and Information
Publication statusAccepted/In press - 31 Aug 2023


  • Logic of Resources
  • Alternating-time Temporal Logic
  • Probabilistic Logic
  • Markov Decision Process
  • Multi-agent Systems


Dive into the research topics of 'Formal Modelling and Verification of Probabilistic Resource Bounded Agents'. Together they form a unique fingerprint.

Cite this