Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Completeness of two fragments of a logic for conditional strategic reasoning

Yinfeng Li, Fengkui Ju

TL;DR

The paper addresses the open problem of completeness for CSR by focusing on two fragments of the cooperating conditional strategic reasoning logic: the liability and ability fragments. It introduces standard disjunctions and a four-step completeness strategy based on normal forms, downward validity, upward derivability, and induction, all facilitated by regular abstract game forms and their realizability. The main contributions are the formal completeness proofs for CL_LI, CL_AB, CCSR_LI, and CCSR_AB, each achieved via a uniform SD-based framework and reduction to lower-depth subformulas. The work advances the theoretical foundations of CSR and suggests a viable path toward the full completeness of CSR and other strategic logics, with potential implications for algorithmic reasoning in multi-agent systems.

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.

Completeness of two fragments of a logic for conditional strategic reasoning

TL;DR

The paper addresses the open problem of completeness for CSR by focusing on two fragments of the cooperating conditional strategic reasoning logic: the liability and ability fragments. It introduces standard disjunctions and a four-step completeness strategy based on normal forms, downward validity, upward derivability, and induction, all facilitated by regular abstract game forms and their realizability. The main contributions are the formal completeness proofs for CL_LI, CL_AB, CCSR_LI, and CCSR_AB, each achieved via a uniform SD-based framework and reduction to lower-depth subformulas. The work advances the theoretical foundations of CSR and suggests a viable path toward the full completeness of CSR and other strategic logics, with potential implications for algorithmic reasoning in multi-agent systems.

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.
Paper Structure (36 sections, 22 theorems, 38 equations, 1 figure)

This paper contains 36 sections, 22 theorems, 38 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Logic for Conditional Strategic Reasoning $\mathsf{CSR}$
  3. Some related work with $\mathsf{CSR}$
  4. Our work
  5. Preliminaries
  6. Concurrent game models
  7. Coalition Logic $\mathsf{CL}$ and its two fragments
  8. Logic for Cooperating Conditional Strategic Reasoning $\mathsf{CCSR}$ and its two fragments
  9. Our proof strategy
  10. Remarks
  11. Regular abstract game forms and their realization
  12. Completeness of the liability fragment ${\mathsf{CL_{LI}}}$ of $\mathsf{CL}$
  13. Remarks
  14. Standard disjunction and a normal form lemma for ${\mathsf{CL_{LI}}}$
  15. Remarks
  16. ...and 21 more sections

Key Result

Theorem 1

Every regular abstract game form and satisfiable elementary conjunction is realized by a pointed concurrent game model.

Figures (1)

  • Figure 1: This figure explains the pointed model $(\mathtt{M},s_0)$ constructed in the proof for Theorem \ref{['theorem:Realizability of abstract game forms']}. We assume $\mathtt{JA}^0_\mathtt{AG} = \{ \sigma^1_\mathtt{AG}, \dots, \sigma^n_\mathtt{AG} \}$ and $\gamma = \neg p \land q \land r$. Above the separation line, there are $n$ pointed models: $(\mathtt{M}_{\sigma_\mathtt{AG}^1},s_{\sigma_\mathtt{AG}^1}), \dots, (\mathtt{M}_{\sigma_\mathtt{AG}^n},s_{\sigma_\mathtt{AG}^n})$. For every $i$ such that $1 \leq i \leq n$, $\mathtt{M}_{\sigma_\mathtt{AG}^i},s_{\sigma_\mathtt{AG}^i} \Vdash \mathtt{force} (\sigma_\mathtt{AG}^i)$. The pointed model $(\mathtt{M},s_0)$ is depicted below the separation line. In the model $\mathtt{M}$: (1) available joint actions of a coalition $\mathrm{A}$ at the state $s_0$ is specified by $\mathtt{JA}^0_\mathrm{A}$; available joint actions of $\mathrm{A}$ at other states are as in the corresponding models; (2) for every $i$ such that $1 \leq i \leq n$, the outcome state of the available joint action $\sigma^i_\mathtt{AG}$ of $\mathtt{AG}$ at the state $s_0$ is $s_{\sigma^i_\mathtt{AG}}$; outcome states of available joint actions of $\mathtt{AG}$ at other states are as in the corresponding models; outcome states of available joint actions of other coalitions at a state are derived as usual; (3) at the state $s_0$, only $q$ and $r$ are true, which are conjuncts of $\neg p \land q \land r$; truth values of atomic propositions at other states are as in the corresponding models.

Theorems & Definitions (85)

  • Example 1
  • Definition 1: Concurrent game models
  • Definition 2: The language $\Phi_{\mathsf{CL}}$
  • Definition 3: Semantics of $\Phi_{\mathsf{CL}}$
  • Definition 4: The liability fragment $\Phi_{{\mathsf{CL_{LI}}}}$ of $\Phi_{\mathsf{CL}}$
  • Definition 5: The ability fragment $\Phi_{{\mathsf{CL_{AB}}}}$ of $\Phi_{\mathsf{CL}}$
  • Definition 6: The language $\Phi_{\mathsf{CCSR}}$
  • Definition 7: Semantics of $\Phi_{\mathsf{CCSR}}$
  • Definition 8: The liability fragment $\Phi_{\mathsf{CCSR_{LI}}}$ of $\Phi_{\mathsf{CCSR}}$
  • Definition 9: The ability fragment $\Phi_{\mathsf{CCSR_{AB}}}$ of $\Phi_{\mathsf{CCSR}}$
  • ...and 75 more