Approximating Strategic Abilities under Imperfect Information: a Naive Approach

TL;DR

This paper explores a naive approach to approximate the complex problem of verifying strategic abilities under imperfect information in multi-agent systems by translating it into a simpler logic and applying a fixpoint algorithm.

Contribution

It investigates the effectiveness of using a naive translation of ATL into alternating epistemic mu-calculus for approximate verification under imperfect information.

Findings

Naive translation provides a computationally simpler verification method.

Approximate results can be obtained despite the translation being incorrect.

The approach offers insights into the trade-offs between accuracy and complexity.

Abstract

Alternating-time temporal logic (ATL) allows to specify requirements on abilities that different agents should (or should not) possess in a multi-agent system. However, model checking ATL specifications in realistic systems is computationally hard. In particular, if the agents have imperfect information about the global state of the system, the complexity ranges from Delta2P to undecidable, depending on the syntactic and semantic details. The problem is also hard in practice, as evidenced by several recent attempts to tackle it. On the other hand, model checking of alternating epistemic mu-calculus can have a distinctly lower computational complexity. In this work, we look at the idea of approximating the former problem by the verification of its "naive" translations to the latter. In other words, we look at what happens when one uses the (incorrect) fixpoint algorithm to verify formulae of ATL with imperfect information.