State-of-the-art belief space planning (BSP) approaches assume data association to be solved or given. Some of the current authors have recently proposed a relaxation of this assumption, resulting in a more general framework of belief space planning where data association is incorporated within the belief (DA-BSP). Unfortunately, this can quickly become intractable under non-myopic planning. In this work, we seek to harness recent approaches in formal methods (specifically, linear temporal logic in the context of planning under uncertainty), to obtain formal-DA-BSP, an approach that incorporates high-level domain knowledge, to obtain more tractable planning. Thanks to generalised form of specification, the framework can also incorporate other complexities including explicit collision probability and determining planning horizon. The initial concepts are shown in an abstracted example of a robot janitor lost in one of the two floors.