Cellular networks have been widely deployed and are under ever-growing communication pressure. Detecting traffic hotspots or other essential characteristics of network traffic distributions can help to adjust the base station control strategies of networks to save energy. Generally, existing approaches detect these characteristics by data analysis techniques, making the detection process generally inefficient and not automatic. Moreover, those approaches are also difficult to describe the dynamic spatio-temporal evolution characteristics of network traffics. In this paper, we propose a novel modeling and analysis approach by applying the spatio-temporal model checking technique to the detection of network traffic characteristics. First, we model the spatio-temporal evolution process of cellular network traffic by closure space model. Second, we give the logical characterizations of detection requirements by suitable Spatio-Temporal Logic of Closure Space (STLCS) formulas. Third, we verify the spatio-temporal properties in the closure space model by model checking algorithms. The experiments are illustrated on the Milan network traffic dataset and indicate that our approach can automatically and effectively detect desirable spatio-temporal properties of cellular network traffic.
