Model Checking in Federated Learning-Based Smart Advertising

As social networks continue to expand, smart advertising increasingly depends on machine learning to deliver personalized and effective advertisements. Federated Learning (FL) is a distributed learning paradigm that supports privacy-preserving advertising by training models locally while avoiding direct sharing of raw user data. However, ensuring the correctness, reliability, and operational robustness of FL-driven smart advertising systems remains a significant challenge, particularly in distributed and user-facing environments. In this study, we investigate the use of model checking as a formal verification technique for validating key properties of an FL-based smart advertising workflow in social networks. We combine a structured finite-state modeling approach with Linear Temporal Logic (LTL) specifications and model-checking tools to assess correctness, availability, and baseline privacy requirements. Using controlled simulation-based configurations, we show that, for a setup with 100 users and 20 edge servers, the system delivers advertisements to all users and the global model successfully processes 200 out of 200 requests. We further analyze verification overhead through detection-time measurements, observing an increase in average detection time from 10.05 s to 11.98 s as the number of users rises from 20 to 100. These results indicate that the proposed framework can provide practical assurance for FL-enabled smart advertising workflows, support more reliable deployment in distributed intelligent systems, and improve trustworthiness in real advertising applications.