On the (Un-)Decidability of Model Checking Resource-Bounded Agents

Abstract

The verification and modelling of multi-agent systems is an important topic that has attracted much attention in recent years. Resources, how-ever, have only recently been studied as simple extensions to well-known logics. Trying to find a set of useful features while retaining essential properties for practical use, we explore the question: Where are the lim-its of what can be verified about resource-bounded agents? We try to answer this question by considering several natural logic-based settings that may arise and prove that verification is usually undecidable apart from bounded or otherwise restrictive settings. Most interestingly, we identify various factors that influence the (un-)decidability and provide grounds for fu-