Completeness of two fragments of a logic for conditional strategic reasoning

TL;DR

This paper proves the completeness of two fragments of a new logic for conditional strategic reasoning, advancing formal understanding of agents' strategic abilities in multi-agent systems.

Contribution

It establishes the completeness of the liability and ability fragments of the Logic for Cooperating Conditional Strategic Reasoning (CCSR), a significant step forward in strategic logic theory.

Findings

Proved completeness of liability fragment

Proved completeness of ability fragment

Introduced a novel proof approach for strategic logics

Abstract

Classical logics for strategic reasoning, such as Coalition Logic and Alternating-time Temporal Logic, formalize absolute strategic reasoning about the unconditional strategic abilities of agents to achieve their goals. Goranko and Ju, in two recent papers, introduced a Logic for Conditional Strategic Reasoning (CSR). However, its completeness is still an open problem. CSR has three featured operators, and one of them has the following reading: For some action of A that guarantees the achievement of her goal, B has an action to guarantee the achievement of his goal. This operator makes good sense when A is cooperating with B. The logic about this operator is called Logic for Cooperating Conditional Strategic Reasoning (CCSR). In this paper, we prove the completeness of two fragments of CCSR: the liability fragment and the ability fragment. The key ingredients of our proof approach include standard disjunctions, the validity-reduction condition of standard disjunctions, abstract game forms, and their realization, and the derivability-reduction condition of standard disjunctions. The approach has good potential to be applied to the completeness of CSR and other strategic logics.