On the model-checking of branching-time temporal logic with BDI modalities