A Truthful Multiunit Profit-Optimal Mechanism for Synthesizing Social Laws
For researchers in multi-agent systems and mechanism design, this work provides a computationally feasible solution for social law synthesis under strategic behavior, though it is incremental as it applies known mechanism design principles to a new domain.
This paper tackles the problem of synthesizing optimal social laws in strategic multi-agent environments, proposing a truthful, individually rational, and profit-optimal mechanism called PO-ASL. The mechanism achieves incentive compatibility and profit optimality while reducing payment determination to allocation determination in polynomial time.
This paper studies Social Law Synthesis (SLS) in strategic multi-agent environments as a new multi-unit mechanism design problem. We model SLS as a Bayesian single-parameter procurement auction based on Alternating-time Temporal Logic (ATL) and aim to design a truthful, individually rational, and profit-optimal mechanism. We first prove a representation lemma showing that any valuation respecting alternating bisimulation can be compactly expressed as a feature set of ATL formulae. We then reduce payment determination to allocation determination in polynomial time, resolving the irregular payment issue inherent in multi-unit settings. We further show that allocation determination is \(FP^{NP}\)-complete and encode ATL semantics into integer linear programming (ILP) constraints to make the problem tractable with standard solvers. Based on these results, we present the $\mathcal{PO\text{-}ASL}$ mechanism, which is incentive-compatible, individually rational, and maximizes expected profit. Theoretical guarantees and examples confirm that our approach provides an effective and computationally feasible solution for synthesizing optimal social laws under strategic agent behavior.