A modular Petri net is composed of individual Petri nets, the modules. Modules are composed by fusing their interface transitions. The behavior of internal transitions is unrelated to other modules and is recorded in local reachability graphs for each module. The behavior of interface transitions is recorded in a single synchronization graph. The local reachability graphs and the synchronization graph form the modular state space [18]. In this paper, we study the reachability problem in the composed Petri net using the modular state space instead of the state space of the composed Petri net. We analyze how the reachability of markings that satisfy a state predicate can be verified. Local reachability graphs are encoded as Binary Decision Diagrams [9, 23, 29]. We present algorithms to solve the mentioned reachability problem in this setting. Finally, we compare the implementation with traditional state space exploration in the non-modular state space.