Strategic Ability Updating in Concurrent Games by Coalitional Commitment

Area of Science:

• Formal Methods and Logic
• Artificial Intelligence
• Multi-Agent Systems

Background:

• Strategic ability updating is crucial for multicomponent reactive systems.
• Existing models like Alternating-time Temporal Logic (ATL) provide a semantic foundation but may lack mechanisms for dynamic ability modification.
• Research in social law and planning via model checking requires robust methods for reasoning about system behavior and achieving desired properties.

Purpose of the Study:

• To propose a novel mechanism, coalitional commitment, for strategic ability updating in reactive systems.
• To introduce coordinated ATL (co-ATL) for reasoning about these updated strategic abilities.
• To analyze the computational complexity of co-ATL model checking and coalitional commitment problems.

Main Methods:

• Modeling reactive systems as concurrent game structures (CGS), the semantic basis of ATL.
• Defining coalitional commitment by extending CGS with context functions and coalitional normative systems (CNS).
• Developing coordinated ATL (co-ATL) for reasoning about systems modified by CNS and analyzing its model-checking complexity.
• Characterizing the limitations of coalitional commitment power.
• Investigating the complexity of effectiveness, feasibility, and synthesis problems for coalitional commitment.
• Presenting an algorithm for coalitional commitment synthesis based on the planning as model checking paradigm.

Main Results:

• The model-checking problem for co-ATL is PTIME-complete, indicating tractability.
• Characterizations of the limitations of coalitional commitment power are provided.
• The effectiveness, feasibility, and synthesis problems for coalitional commitment are shown to be PTIME-complete, NP-complete, and FNP-complete, respectively.
• An algorithm for coalitional commitment synthesis is proposed.

Conclusions:

• Coalitional commitment offers an effective tool for strategic ability updating in reactive systems.
• Coordinated ATL (co-ATL) provides a tractable framework for reasoning about these updated abilities.
• The proposed approach enhances both social law research and planning via model checking.