Reasoning about Agent Programs using ATL-like Logics

TL;DR

This paper introduces a new ATL-like logic based on agents' operational know-how, enabling explicit reasoning about rational strategies in BDI systems for verifying properties of agent programs.

Contribution

It presents a novel logic grounded in agents' plan libraries, allowing explicit reasoning about rational strategies in BDI systems, extending ATL frameworks.

Findings

Enables explicit reasoning about rational strategies in agent systems

Allows verification of properties of BDI systems using ATL-like logic

Builds on and extends ATLES with a focus on agent know-how

Abstract

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.