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

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 C * that augments the branching-time logic C * with the modalities and adopt the possible-world semantics by Rao and George. We recall that in this semantics relations vary over time according to a branching-time structure. We study the related model-checking question for nite-state structures, and in particular, we focus on models that are described as tuples of Kripke structures (one for each world) and where the relations are captured by nite-state relations. Note that for formulas that do not contain modalities this corresponds to standard C * model-checking that is known to be P-complete. We show that by adding the modalities the computational complexity of model-checking remains P complete. The problem is still P-hard even if we disallow the nesting of temporal operators in the path formulas, i.e., we restrict to the temporal modalities of C. Finally, we give a xed-point formulation of our algorithm for C that implements it on the top of existing symbolic xed-point solvers.