On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts

Technical Summary: On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts

Author: Dimitar P. Guelev
Date: February 12, 2026

1. Problem Statement

The paper addresses a fundamental limitation in existing temporal logics of strategic ability, specifically Alternating-time Temporal Logic with Strategy Contexts ($\text{ATL}^*_{sc}$). While $\text{ATL}^*_{sc}$ is powerful enough to express complex solution concepts like Nash equilibrium, it lacks a native mechanism to reason about qualitative preference between different outcomes (plays).

In rational game theory, players do not merely seek to satisfy a single objective; they often have multiple objectives with varying degrees of desirability. Current methods for expressing these preferences require non-trivial reasoning outside the logic itself. The core problem is: How can we extend $\text{ATL}^*_{sc}$ to include a preference operator and second-order path quantification without making the logic undecidable or requiring entirely new, complex model-checking algorithms?

2. Methodology

The author employs a translation-based approach. Instead of developing a new model-checking engine for an extended logic, the paper proposes adding expressive features to $\text{ATL}^*_{sc}$ and then providing a systematic way to "eliminate" them, translating the resulting formulas into the well-established Quantified Computation Tree Logic ($\text{QCTL}^*$).

Key methodological components include:

• Preference Modeling: A binary preference operator ($<$) is introduced on plays. To ensure algorithmic tractability, the author assumes that preference-indiscernibility (the property where two plays are treated identically by a player's preference relation) is an equivalence relation of finite index. This means the set of all possible plays can be partitioned into a finite number of equivalence classes, each definable by an LTL formula.
• Strategy Encoding: Strategies are encoded using quantified state variables within the $\text{QCTL}^*$ framework.
• Stability Assumption: The author assumes preferences are "stable," meaning they evolve predictably as players progress toward their objectives but do not change their underlying structure.
• Second-Order Path Quantification: A specialized quantifier ($\exists_{\sim}$) is introduced. Unlike standard path quantifiers that range over individual paths, $\exists_{\sim}$ forces path variables to range over sets of plays that are closed under preference-indiscernibility.

3. Key Contributions

1. Extension of $\text{ATL}^*_{sc}$: The paper introduces $\text{ATL}^*_{sc,<}$, an extension of $\text{ATL}^*_{sc}$ featuring a binary preference operator ($<$) and specialized second-order path quantifiers ($\exists_{\sim}$ and $\exists_{1}$).
2. Elimination Techniques:
   • A method to eliminate the preference operator ($<$) by replacing it with a finite combination of LTL formulas that define the preference equivalence classes.
   • A method to eliminate the specialized second-order quantifiers by expanding them into parameterized disjunctions over the finite set of preference-indiscernible classes.
3. Novel Translation to $\text{QCTL}^*$: The author provides a new, more efficient translation from $\text{ATL}^*_{sc}$ to $\text{QCTL}^*$ compared to previous literature, specifically optimizing the number of required propositional quantifications.
4. Axiomatization: The paper provides a set of axioms for the preference operator in $\text{QCTL}^*_{<}$, facilitating formal reasoning.

4. Results

• Expressivity of Solution Concepts: The author demonstrates that complex game-theoretic concepts, such as Nash equilibrium and secure equilibrium, can be expressed almost literally in the proposed logic. For example, a Nash equilibrium can be formulated as a single $\text{ATL}^*_{sc,<}$ formula that accounts for the relative desirability of objectives.
• Algorithmic Feasibility: The paper proves that any formula in the extended $\text{ATL}^*_{sc,<}$ can be translated into a $\text{QCTL}^*$ formula. This ensures that the problem of model checking in the new logic is reducible to the known decidable problem of model checking in $\text{QCTL}^*$.
• Complexity Management: By using the "Guarded Normal Form" (GNF) of LTL formulas and optimizing the encoding of actions, the author shows that the translation remains computationally manageable, avoiding the exponential blow-up typically associated with such extensions.

5. Significance

This work bridges the gap between qualitative preference theory and strategic temporal logic. Its significance lies in three areas:

• Theoretical: It provides a formal, logical framework for "rational synthesis," where agents are not just programmed to reach a goal, but to reach the best possible goal among several options.
• Practical: By relying on translations to $\text{QCTL}^*$, the author provides a "plug-and-play" solution for researchers. One can use existing $\text{QCTL}^*$ solvers to reason about complex, preference-aware multiplayer games.
• Unified Reasoning: The approach allows for a uniform way to handle various solution concepts (Nash, secure, dominant strategies) by treating the specific algebraic properties of the preference relation as "data" rather than hard-coded logic.