Can I efficiently model check asynchronous agents with memory?
Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies
This paper tackles the challenge of verifying strategic abilities in multi-agent systems where agents have memory of past interactions, particularly focusing on asynchronous communication. It adapts and extends existing techniques like Knowledge-Based Subset Construction and Partial Order Reduction to handle imperfect information and memory. This allows for translating a complex problem (agents with memory) into a simpler one (memoryless agents in an expanded model) and shrinking the model size while preserving key properties. These advancements are relevant for verifying the correctness and security of complex multi-agent web applications where LLMs could act as reasoning engines for individual agents. The ability to verify strategic properties within these systems, especially for agents with recall (like LLMs which maintain conversation history), provides a powerful tool for ensuring dependable and secure application behavior.