## 1 Introduction  
The use of mobile devices has grown exponentially in the past decade, driving demand for applications that provide users with personalized, real-time information [1, 2, 3]. One of the most rapidly advancing areas has been geolocation-based mobile applications [4, 5], which allow the delivery of relevant content to users based on their physical location [6]. These technologies have been widely adopted in the commercial sector, aiming to enhance user experience by delivering real-time promotions [7]. However, the efficiency and reliability of these applications rely heavily on the effective management of communication between mobile devices and the backend servers that supply necessary data and services [8]. To address these challenges, Petri nets offer a suitable formal modeling tool for systems that require the coordination of multiple asynchronous and concurrent processes [9], as in the case of mobile applications interacting with APIs (Application Programming Interfaces) [10]. Petri nets allow the accurate representation of interactions between network requests, message delivery, and user proximity detection, contributing to a smooth and optimized user experience [11]. This article presents the design and implementation of a mobile application developed in Kotlin, which leverages geolocation services to send its geographic position to an API. The API calculates the proximity between the user and registered shopping centers, such as Soriana, GranD, and HEB, using the Haversine formula [12]. If the user is detected within a radius of 600 m or less from a shopping center, the API, developed using the Laravel framework, sends real-time promotional offers. Additionally, the application features a share button, enabling users to distribute offers among their contacts, thereby extending the reach of the promotions [13]. By utilizing Petri nets to model the system's asynchronous behavior, communication between the mobile application and the API is optimized, ensuring fast response times and accurate delivery of promotions. The complexity of developing the mobile application and API lies in handling multiple simultaneous user requests in parallel without affecting response time. To address this challenge, Petri nets are introduced as an appropriate formal modeling tool, enabling the representation and analysis of the system's asynchronous and distributed behavior. This approach enhances user experience and prevents communication conflicts [14; 15]. The main contribution of this study lies in the application of Petri nets for formal modeling in real-time proximity systems, demonstrating their effectiveness not only in optimizing the delivery of relevant content but also as a scalable and robust methodology that can be applied in future mobile application developments in this field. The obtained results show that the proposed system achieves a reduction in response times and improves the accuracy of proximity detection using the Haversine formula, validating the effectiveness of modeling with Petri nets and concurrency management in real-time notification systems. To guide our research and provide a clear structure for the rest of the article, we pose the following research questions:  
1. How can an efficient real-time promotional advertisement delivery system be implemented based on the user's proximity to shopping centers? 2. What benefits does the integration of Petri nets offer in modeling mobile applications for managing asynchronous and concurrent behaviors? 3. What advantages does the use of Petri nets present for identifying and optimizing bottlenecks in the interaction flow between the mobile application and the API? These questions address the key aspects of our study, including technical implementation, Petri net modeling, system accuracy, and the advantages of the proposed methodology. Throughout the article, we will explore these issues in detail, presenting our methods, results, and conclusions.