Saved in:
Bibliographic Details
Main Authors: Wu, Jun, Huang, Jian, Wang, Chongjun
Format: Preprint
Published: 2026
Subjects:
Online Access:https://arxiv.org/abs/2605.16853
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866911690914791424
author Wu, Jun
Huang, Jian
Wang, Chongjun
author_facet Wu, Jun
Huang, Jian
Wang, Chongjun
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2605_16853
institution arXiv
publishDate 2026
record_format arxiv
spellingShingle A Truthful Multiunit Profit-Optimal Mechanism for Synthesizing Social Laws
Wu, Jun
Huang, Jian
Wang, Chongjun
Computer Science and Game Theory
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.
title A Truthful Multiunit Profit-Optimal Mechanism for Synthesizing Social Laws
topic Computer Science and Game Theory
url https://arxiv.org/abs/2605.16853