Wireless Sensor Network (WSN) technology is now mature enough to be used in numerous application domains. However, due to the restricted amount of energy usually allocated to each node, a crucial property of interest for the users is the minimal lifetime of the network. In practice, this value strongly depends both on the design choices performed for each network element (hardware architecture, communication protocols, etc.) and on the whole execution environment (physical environment, execution platform, network topology, etc.). We propose here an original approach to evaluate this minimal network lifetime based on modelchecking techniques. It consists first in designing a timed model of the entire network behavior (taking into account its execution environment), and then to compute on the state space associated to this model the shortest execution sequences (from a temporal point of view) leading to some states considered as “terminal” (from the network lifetime point of view)....