Using Strategic Logics to Reason about Agent Programs

摘要

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.In our logic,it is possible to refer to “rational” strategies for agents developed under the Belief-Desire-Intention agent paradigm.This allows us to express and verify properties of BDI systems using ATL-type logical frameworks.