Alternating-Time Temporal Logic with Default Actions
摘要
We introduce an extension of Alternating-Time Temporal Logic (ATL) that incorporates default actions to model communication failures in multi-agent systems. Our framework, ATL-kD, allows for a limited number of communication failures during which agents’ intended strategies may not be delivered. In the event of such a communication failure, a predefined default action is played. We analyse the computational complexity of model checking in this setting, showing NP-hardness and coNP-hardness in general, but polynomial-time solvability when default actions are restricted to a fixed subset of agents. We also study a variant with default preferences, which better handles cases where the default action might be unavailable in some states due to protocol constraints. Additionally, we introduce default action updates, allowing the default action to be revised during system execution. Together, these results provide a formal foundation for robust verification under unreliable communication.