Reasoning about Strategies under Partial Observability and Fairness Constraints

TL;DR

This paper introduces ATLK^F_po, a unified logical framework that combines strategies, partial observability, and fairness constraints, along with a model checking algorithm for it.

Contribution

It presents the first unified logic integrating strategies, partial observability, and fairness constraints, and provides a model checking algorithm for this logic.

Findings

Developed ATLK^F_po, a new logic for strategies under partial observability with fairness.

Provided a model checking algorithm for ATLK^F_po.

Demonstrated the applicability of the logic through theoretical analysis.

Abstract

A number of extensions exist for Alternating-time Temporal Logic; some of these mix strategies and partial observability but, to the best of our knowledge, no work provides a unified framework for strategies, partial observability and fairness constraints. In this paper we propose ATLK^F_po, a logic mixing strategies under partial observability and epistemic properties of agents in a system with fairness constraints on states, and we provide a model checking algorithm for it.