Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information
Francesco Belardinelli, Alessio R. Lomuscio · 2017
We introduce a 3-valued abstraction technique for alternating-time temporal logic (ATL) in contexts of imperfect information. We introduce under- and over-approximations of an agent's strategic abilities in terms of must- and may-strategies and provide a 3-valued semantics for ATL based on agents in interpreted systems (IS). We define a relation of simulation between the agents and prove that it preserves defined truth values of ATL formulas. Finally, we introduce a notion of abstraction on IS and show that it simulates the concrete interpreted system. Under this setting we present a procedure that enables the direct construction of a finite abstraction from an infinite-state system.