Large Foundation Models (LFMs) have unlocked new possibilities in human-computer interaction, particularly with the rise of mobile Graphical User Interface (GUI) Agents capable of interacting with mobile GUIs. These agents allow users to automate complex mobile tasks through simple natural language instructions. However, the inherent probabilistic nature of LFMs, coupled with the ambiguity and context-dependence of mobile tasks, makes LFM-based automation unreliable and prone to errors. To address this critical challenge, we introduce VeriSafe Agent (VSA)1: a formal verification system that serves as a logically grounded safeguard for Mobile GUI Agents. VSA deterministically ensures that an agent's actions strictly align with user intent before executing the action. At its core, VSA introduces a novel autoformalization technique that translates natural language user instructions into a formally verifiable specification. This enables runtime, rule-based verification of agent's actions, detecting erroneous actions even before they take effect. To the best of our knowledge, VSA is the first attempt to bring the rigor of formal verification to GUI agents, bridging the gap between LFM-driven actions and formal software verification. We implement VSA using off-the-shelf LFM services (GPT-4o) and evaluate its performance on 300 user instructions across 18 widely used mobile apps. The results demonstrate that VSA achieves 94.33%–98.33% accuracy in verifying agent actions, outperforming existing LFM-based verification methods by 30.00%–16.33%, and increases the GUI agent's task completion rate by 90%–130%.

The advent of large language models (LLMs) has opened up new opportunities in the field of mobile task automation. Their superior language understanding and reasoning capabilities allow users to automate complex and repetitive tasks. However, due to the inherent unreliability and high operational cost of LLMs, their practical applicability is quite limited. To address these issues, this paper introduces MobileGPT1, an innovative LLM-based mobile task automator equipped with a human-like app memory. MobileGPT emulates the cognitive process of humans interacting with a mobile app---explore, select, derive, and recall. This approach allows for a more precise and efficient learning of a task's procedure by breaking it down into smaller, modular sub-tasks that can be re-used, re-arranged, and adapted for various objectives. We implement MobileGPT using online LLMs services (GPT-3.5 and GPT-4) and evaluate its performance on a dataset of 185 tasks across 18 mobile apps. The results indicate that MobileGPT can automate and learn new tasks with 82.7% accuracy, and is able to adapt them to different contexts with near perfect (98.75%) accuracy while reducing both latency and cost by 62.5% and 68.8%, respectively, compared to the GPT-4 powered baseline.

We present a relay path determination scheme that maximizes the network lifetime and guarantees the end-to-end reliability in the wireless sensor networks with mobile sink. The simple flooding algorithm may render an easy means for the determination but the resulting frequent collisions and profuse relay hops disable determining energy-efficient and reliable paths. To resolve this problem, we present a transmission backoff (TB)- based broadcasting algorithm that uses a transmission deferring approach to reduce the number of collisions and the number of the relay hops, while guaranteeing the end-to-end reliability. It is a distributed and stateless approach in which the relay path is determined by each node without any global and/or local exchange of network information. Each node decides whether or not to rebroadcast based on its own transmission backoff time, which is calculated using its residual battery energy and the target end-to-end reliability. Simulation results reveal that the proposed algorithm can achieve a longer network lifetime and a higher end-to-end reliability performance than other existing schemes.