On the Model-Checking of Branching-Time Temporal Logic with BDI Modalities

BDI logics, i.e., logics with belief, desire and intention attitudes, are one of the most widely studied formal languages for modelling rational agents. In this paper, we consider the logic CTL*BDI that augments the branching-time logic CTL with the BDI modalities and adopt the possible-world semantics by Rao and Georgeff. We recall that in this semantics BDI relations vary over time according to a branching-time structure. We study the related model-checking question for finite-state structures, and in particular, we focus on models that are described as tuples of Kripke structures (one for each world) and where the BDI relations are captured by finite-state relations. Note that for formulas that do not contain BDI modalities this corresponds to standard CTL model-checking that is known to be PSPACE-complete. We show that by adding the BDI modalities the computational complexity of model-checking remains PSPACE-complete. The problem is still PSPACE-hard even if we disallow the nesting of temporal operators in the path formulas, i.e., we restrict to the temporal modalities of CTL. Finally, we give a fixed-point formulation of our algorithm for CTLBDI that implements it on the top of existing symbolic fixed-point solvers