Reasoning about resource-bounded multi-agent systems
Nguyen, Nguyen (2011) Reasoning about resource-bounded multi-agent systems. PhD thesis, University of Nottingham.
The thesis presents logic-based formalisms for modelling and reasoning about resource-bounded multi-agent systems. In the field of multi-agent system, it is well-known that temporal logics such as CTL and ATL are powerful tools for reasoning about multi-agent systems. However, there is no natural way to utilise these logics for expressing and reasoning about properties of multi-agent systems where actions of agents require resources to be able to perform. This thesis extends logics including Computational Tree Logic (CTL), Coalition Logic (CL) and Alternating-time Temporal Logic (ATL) which have been used to reasoning about multi-agent systems so that the extended ones have the power to specify and to reason about properties of resource-bounded multi-agent systems. While the extension of CTL is adapted for specifying and reasoning about properties of systems of resource-bounded reasoners where the resources are explicitly memory, communication and time, the extensions of CL and ATL are generalised so that any resource-bounded multi-agent system can be modelled, specified and reasoned about. For each of the logics, we describe the range of resource-bounded multi-agent systems they can account for and axiomatisation systems for reasoning which are proved to be sound and complete. Moreover, we also study the satisfiability problem of these logics.
Archive Staff Only: item control page