Petri net systems modelling distributed systems often provide a component structure, comprising individual components that collaborate occasionally. The modular state space [1, 6] method for Petri net systems embraces this structure in the exploration of the state space with the aim of completely representing the behavior of a Petri net system while minimizing time and memory resources. The efficient method currently considers bounded Petri net systems with a finite state space. For unbounded Petri net systems with an infinite state space, the coverability graph [7] is a finite representation of the state space that abstracts the infinite behavior on diverging places. As it is related with the state space by a simulation relation [2], the coverability graph is a valid base for verification for unbounded Petri net systems. This work presents a modular construction algorithm for unbounded Petri net systems, that generates a finite, modular representation of its state space, the covering modular state space. The covering modular state space simulates the state space as well and allows efficient modular verification for unbounded Petri net systems. Furthermore, this work examines how verification of standard Petri net system properties such as reachability, existence of deadlocks and liveness, can be performed in the covering modular state space.