Model checking BDI logics over finite-state worlds