Reasoning about Agent Programs using ATL-like Logics
This work addresses verification challenges for BDI agent systems, but it is incremental as it builds on existing ATL variants like ATLES.
The authors tackled the problem of verifying properties of Belief-Desire-Intention (BDI) agent systems by proposing a variant of Alternating-time Temporal Logic (ATL) grounded in agents' abstract plans, enabling explicit reference to rational strategies for verification.
We propose a variant of Alternating-time Temporal Logic (ATL) grounded in the agents' operational know-how, as defined by their libraries of abstract plans. Inspired by ATLES, a variant itself of ATL, it is possible in our logic to explicitly refer to "rational" strategies for agents developed under the Belief-Desire-Intention agent programming paradigm. This allows us to express and verify properties of BDI systems using ATL-type logical frameworks.