pith. sign in

arxiv: 2605.16853 · v1 · pith:665MZ7UYnew · submitted 2026-05-16 · 💻 cs.GT

A Truthful Multiunit Profit-Optimal Mechanism for Synthesizing Social Laws

Jun Wu , Jian Huang , Chongjun Wang This is my paper

Pith reviewed 2026-05-19 19:29 UTC · model grok-4.3

classification 💻 cs.GT
keywords Social Law SynthesisMechanism DesignATLProcurement AuctionIncentive CompatibilityProfit MaximizationInteger Linear Programming
0
0 comments X

The pith

The PO-ASL mechanism synthesizes social laws that maximize expected profit while remaining incentive-compatible and individually rational.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper models social law synthesis in strategic multi-agent settings as a Bayesian single-parameter procurement auction using Alternating-time Temporal Logic. It proves a representation lemma allowing valuations to be expressed compactly as ATL formula sets, reduces payment calculation to allocation in polynomial time, and encodes the NP-hard allocation task as integer linear programming solvable by standard tools. The resulting PO-ASL mechanism is incentive-compatible, individually rational, and profit-optimal. A reader would care because the work gives a concrete computational path to optimal rule design when agents can misreport their preferences over system behaviors.

Core claim

Social law synthesis is cast as a Bayesian procurement auction based on ATL. A representation lemma establishes that any valuation respecting alternating bisimulation equals a compact feature set of ATL formulae. This permits a polynomial-time reduction of payment determination to allocation determination. Allocation is shown to be FP^NP-complete yet tractable once ATL semantics are encoded as ILP constraints. The PO-ASL mechanism therefore computes allocations that maximize expected profit while satisfying incentive compatibility and individual rationality.

What carries the argument

The PO-ASL mechanism, which relies on the representation lemma to convert the mechanism-design task into an integer linear program whose solution yields both the profit-maximizing allocation and the corresponding payments.

If this is right

  • Agents report true valuations because the mechanism is incentive-compatible.
  • Agents willingly participate because the mechanism is individually rational.
  • Expected profit is maximized under the Bayesian prior over valuations.
  • The allocation can be computed in practice by feeding the ILP encoding to any standard solver.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same reduction from payments to allocations could be attempted in other temporal-logic mechanism-design problems.
  • Relaxing the alternating-bisimulation requirement would allow the approach to handle a broader class of agent preferences.
  • Automated synthesis of social laws could be tested in domains such as traffic coordination or shared-resource protocols.

Load-bearing premise

Any valuation that respects alternating bisimulation can be expressed compactly as a finite set of ATL formulae.

What would settle it

A concrete valuation that respects alternating bisimulation yet cannot be written as any finite ATL formula set, or an instance in which the ILP solution produces strictly lower expected profit than the true optimum.

Figures

Figures reproduced from arXiv: 2605.16853 by Chongjun Wang, Jian Huang, Jun Wu.

Figure 1
Figure 1. Figure 1: Turning points of agent i 5.2 Computational complexity Allocation determination is the basic building block of the proposed mechanism, however we can show it is intractable. Lemma 17. Both Dominant Social Law and Dominant (i, n)-Social Law are FPNP -complete. Theorem 18. Mechanism PO-ASL is FPNP -complete. Thus, we are unlikely to find efficient algorithms for directly computing PO-ASL. Methodologies for c… view at source ↗
Figure 2
Figure 2. Figure 2: The dependencies between the variables The solution to ILP-Dom-SL or ILP-Dom-IN-SL is actually an assignment ℓ, which assigns an 0 or 1 to each of the variables under all the constraints. We let ηℓ(i, q) be the social law corresponding to assignment ℓ, that is, ηℓ(i, q) = {a ∈ εi(q)∣ℓ(y q i∶a ) = 1} (61) Then, we can further prove the following results: Lemma 19. 1) ∀q, i, a: ℓ(y q i∶a ) = 1 iff a ∈ ηℓ(i, … view at source ↗
Figure 3
Figure 3. Figure 3: A cost-aware concurrent game structure (CCGS) [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Structures obtained by implementing social laws [PITH_FULL_IMAGE:figures/full_fig_p020_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The closure of a formula and its underlying tree-like structure [PITH_FULL_IMAGE:figures/full_fig_p020_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: A structure for the proof of lemma 17 maximizes ∑ (ψi,wi)∈F,v⊧ψi wi (93) Therefore, Dominant Social Law is FPNP -complete. 2) For Dominant (i, n)-Social Law, the associated decision problem is “whether there is an (i, n)- social law η ∈ SL(i,n) S achieves the value of g(η, x) at least l ∈ R + ”, and it is trivially in NP since we can guess an (i, n)-social law and verify it in polynomial time. Therefore, D… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper models social law synthesis (SLS) as a Bayesian single-parameter procurement auction using Alternating-time Temporal Logic (ATL). It proves a representation lemma asserting that any valuation respecting alternating bisimulation can be compactly expressed as a feature set of ATL formulae, reduces payment determination to allocation determination in polynomial time, shows that allocation determination is FP^NP-complete, encodes ATL semantics into ILP constraints, and presents the PO-ASL mechanism claimed to be incentive-compatible, individually rational, and expected-profit maximizing.

Significance. If the representation lemma establishes a polynomial-size feature set and the reduction is polynomial, the work offers a novel integration of ATL-based multi-agent modeling with mechanism design, yielding a computationally feasible profit-optimal mechanism for strategic social law synthesis. The ILP encoding for tractability and the explicit handling of irregular payments in the multi-unit setting are constructive contributions that could enable practical deployment with standard solvers.

major comments (2)
  1. [Representation lemma and reduction section] Representation lemma (invoked to enable the payment-to-allocation reduction): the compactness claim is load-bearing for both the single-parameter domain and the polynomial-time reduction. The lemma states that valuations respecting alternating bisimulation can be compactly expressed as ATL formulae features, but the provided argument does not explicitly bound the size of the resulting feature set (or the number of independent ATL atoms) by a polynomial in the size of the ATL model or the number of agents; an exponential blow-up would render the subsequent reduction non-polynomial and the ILP encoding infeasible for profit maximization.
  2. [Complexity analysis] FP^NP-completeness claim for allocation determination: while the reduction from payment to allocation is asserted to be polynomial, the completeness result is stated without a self-contained hardness proof or explicit reference to the source problem (e.g., which NP oracle is used). This step is central to justifying the ILP encoding as a practical solution rather than a theoretical reformulation.
minor comments (2)
  1. [Abstract] The abstract refers to 'theoretical guarantees and examples' confirming effectiveness, but does not indicate the specific sections or theorems where these are presented.
  2. [Preliminaries and mechanism definition] Notation for the PO-ASL mechanism and the ATL feature sets could be introduced earlier with a clear table or definition list to aid readability across the reduction and ILP encoding.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the insightful comments on our paper. We address the major comments point by point below, indicating where revisions will be made to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Representation lemma and reduction section] Representation lemma (invoked to enable the payment-to-allocation reduction): the compactness claim is load-bearing for both the single-parameter domain and the polynomial-time reduction. The lemma states that valuations respecting alternating bisimulation can be compactly expressed as ATL formulae features, but the provided argument does not explicitly bound the size of the resulting feature set (or the number of independent ATL atoms) by a polynomial in the size of the ATL model or the number of agents; an exponential blow-up would render the subsequent reduction non-polynomial and the ILP encoding infeasible for profit maximization.

    Authors: We appreciate the referee highlighting the need for an explicit polynomial bound. In the full proof of the representation lemma (Lemma 3.1), the feature set is constructed from the quotient model under alternating bisimulation, and the number of independent ATL atoms is bounded by the number of distinct equivalence classes, which is at most the number of states in the model times the number of agents. Thus, the size is O(|S| * n), which is polynomial. We will add a new corollary (Corollary 3.2) explicitly stating this bound and its implication for the polynomial-time reduction. This addresses the concern directly. revision: yes

  2. Referee: [Complexity analysis] FP^NP-completeness claim for allocation determination: while the reduction from payment to allocation is asserted to be polynomial, the completeness result is stated without a self-contained hardness proof or explicit reference to the source problem (e.g., which NP oracle is used). This step is central to justifying the ILP encoding as a practical solution rather than a theoretical reformulation.

    Authors: We agree that a more detailed hardness proof would improve clarity. The FP^NP-completeness of allocation determination is shown via a reduction from the NP-hard winner determination problem in multi-unit auctions (using an NP oracle for verifying optimal sub-allocations). We will revise Section 4 to include a self-contained proof sketch, explicitly referencing the source as the 'multi-unit auction profit maximization' problem known to be FP^NP-complete, and clarify that the oracle solves the NP-complete subproblem of checking feasible allocations under ATL constraints. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation relies on proved representation lemma and standard reductions

full rationale

The paper explicitly states it proves the representation lemma showing compact ATL feature-set expression for valuations respecting alternating bisimulation. This lemma is used to justify modeling as a single-parameter domain, enabling the polynomial-time reduction from payment to allocation determination via standard mechanism-design techniques. No step reduces a claimed prediction or result to a fitted parameter or self-citation by construction; the central claims (IC/IR/profit-maximization of PO-ASL) follow from the ILP encoding of ATL semantics after the reduction. The derivation chain is self-contained against external benchmarks once the lemma is accepted as proved within the paper.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard ATL semantics and mechanism-design axioms; no free parameters or invented entities are introduced beyond the new mechanism itself.

axioms (2)
  • domain assumption Valuations respect alternating bisimulation and can be represented by ATL feature sets
    Invoked in the representation lemma to compactly express agent valuations.
  • domain assumption The procurement setting is single-parameter and Bayesian
    Used to model SLS as a multi-unit auction.

pith-pipeline@v0.9.0 · 5707 in / 1346 out tokens · 37867 ms · 2026-05-19T19:29:05.187029+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

79 extracted references · 79 canonical work pages

  1. [1]

    ˚Agotnes, W

    T. ˚Agotnes, W. van der Hoek, M. Tennenholtz, and M. Wooldridge. Power in normative systems. InProceedings of AAMAS-09, pages 145–152, 2009

    work page 2009

  2. [2]

    ˚Agotnes, W

    T. ˚Agotnes, W. van der Hoek, and M. Wooldridge. Robust normative systems. InProceedings of AAMAS-08, pages 747–754, 2008

    work page 2008

  3. [3]

    ˚Agotnes and M

    T. ˚Agotnes and M. Wooldridge. Optimal social laws. InProceedings of AAMAS-10, pages 667–674, 2010

    work page 2010

  4. [4]

    Rodriguez-Aguilar, Carles Sierra, and Michael Wooldridge

    Thomas ˚Agotnes, Wiebe van der Hoek, Juan A. Rodriguez-Aguilar, Carles Sierra, and Michael Wooldridge. On the logic of normative systems. InProceedings of IJCAI-07, pages 1175–1180, 2007

    work page 2007

  5. [5]

    Normative system games

    Thomas ˚Agotnes, Michael Wooldridge, and Wiebe van der Hoek. Normative system games. In Proceedings of AAMAS-07, pages 876–883, 2007

    work page 2007

  6. [6]

    R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic.JACM, 49(5):672– 713, 2002. 14

    work page 2002

  7. [7]

    R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. InProc. of 1998 Int. Conf. on Concurrency Theory, pages 163–178, 1998

    work page 1998

  8. [8]

    Truthful mechanisms for one-parameter agents

    Aaron Archer and ´Eva Tardos. Truthful mechanisms for one-parameter agents. InProc. 42nd IEEE Symposium on Foundations of Computer Science (FOCS-01), pages 482–491, 2001

    work page 2001

  9. [9]

    Frugal path mechanisms

    Aaron Archer and ´Eva Tardos. Frugal path mechanisms. InProc. of SODA-02, pages 991–999, 2002

    work page 2002

  10. [10]

    Frugal path mechanisms.ACM Transactions on Algorithms, 3(1):1– 19, 2004

    Aaron Archer and ´Eva Tardos. Frugal path mechanisms.ACM Transactions on Algorithms, 3(1):1– 19, 2004

    work page 2004

  11. [11]

    Bhattacharya, E

    S. Bhattacharya, E. Koutsoupias, J. Kulkarni, S. Leonardi, and X. Xu. Prior-free multi-unit auctions with ordered bidders.Theoretical Computer Science, 846(8):160–171, 2020

    work page 2020

  12. [12]

    Sushil Bikhchandani, Sven Vries, James Schummer, and Rakesh V. Vohra. Linear programming and vickrey auctions. InMathematics of the Internet: E-Auction and Markets. Springer, 2002

    work page 2002

  13. [13]

    Binmore.Game Theory and the Social Contract, vol

    K. Binmore.Game Theory and the Social Contract, vol. 1: Playing Fair. The MIT Press, Cambridge, Massachusetts, 1994

    work page 1994

  14. [14]

    Binmore.Game Theory and the Social Contract, vol

    K. Binmore.Game Theory and the Social Contract, vol. 2: Just Playing. The MIT Press, Cambridge, Massachusetts, 1998

    work page 1998

  15. [15]

    Revenue effects of ambiguity in multi-unit auctions

    Daniel Bougt, Gagan Ghosh, and Heng Liu. Revenue effects of ambiguity in multi-unit auctions. Journal of Economic Theory, 225:105996, 2025

    work page 2025

  16. [16]

    Walrasian pricing in multi-unit auctions.Artificial Intelligence, 322:103961, 2023

    Simina Brˆ anzei, Aris Filos-Ratsikas, Peter Bro Miltersen, and Yulong Zeng. Walrasian pricing in multi-unit auctions.Artificial Intelligence, 322:103961, 2023

    work page 2023

  17. [17]

    Bulling and M

    N. Bulling and M. Dastani. Verifying normative behaviour via normative mechanism design. In Proc. IJCAI-11, pages 103–108, 2011

    work page 2011

  18. [18]

    Bulling and M

    N. Bulling and M. Dastani. Norm-based mechanism design.Artificial Intelligence, 239:97–142, 2016

    work page 2016

  19. [19]

    Bounding the payment of approximate truthful mechanisms.Theoretical Computer Science, 562:419–435, 2015

    Gruia Calinescu. Bounding the payment of approximate truthful mechanisms.Theoretical Computer Science, 562:419–435, 2015

    work page 2015

  20. [20]

    Cary, Abraham D

    Matthew C. Cary, Abraham D. Flaxman, Jason D. Hartline, and Anna R. Karlin. Auctions for structured procurement. InProc. of SODA-08, pages 304–313, 2008

    work page 2008

  21. [21]

    Truthful multi-unit procurements with budgets

    Hau Chan and Jing Chen. Truthful multi-unit procurements with budgets. InProc. of Workshop on Internet and Network Economics, pages 89–105, 2014

    work page 2014

  22. [22]

    Bayesian auctions with efficient queries.Artificial Intelligence, 303:103630, 2022

    Jing Chen, Bo Li, Yingkai Li, and Pinyan Lu. Bayesian auctions with efficient queries.Artificial Intelligence, 303:103630, 2022

    work page 2022

  23. [23]

    Optimal competitive auctions

    Ning Chen, Nick Gravin, and Pinyan Lu. Optimal competitive auctions. InProceedings of STOC-14, pages 253–262, 2014

    work page 2014

  24. [24]

    E. M. Clarke, O. Grumberg, and D. A. Peled.Model Checking. MIT Press, Cambridge, Mas- sachusetts, 2000

    work page 2000

  25. [25]

    Edward H. Clarke. Multipart pricing of public goods.Public Choice, 11:17–33, 1971

    work page 1971

  26. [26]

    Dell’Anna, M

    D. Dell’Anna, M. Dastani, and F. Dalpiaz. Reasoning about norms revision. InProc. of BNAIC-17, pages 281–290, 2017

    work page 2017

  27. [27]

    Dobzinski and N

    S. Dobzinski and N. Nisan. Limitations of vcg-based mechanisms. InProc. of STOC-07, pages 338–344, 2007

    work page 2007

  28. [28]

    Frugality in path auctions

    Edith Elkind, Amit Sahai, and Ken Steiglitz. Frugality in path auctions. InProc. of SODA-04, pages 701–709, 2004

    work page 2004

  29. [29]

    Allen Emerson

    E. Allen Emerson. Handbook of theoretical computer science. chapter Temporal and modal logic, pages 997–1072. Elsevier, 1990. 15

    work page 1990

  30. [30]

    Quantifying the inefficiency of multi-unit auctions for normal goods.Journal of Economic Theory, 230:106094, 2025

    Simon Essig Aberg and Brian Baisa. Quantifying the inefficiency of multi-unit auctions for normal goods.Journal of Economic Theory, 230:106094, 2025

    work page 2025

  31. [31]

    Choosing social laws for multi-agent systems: Minimality and simplicity.Artificial Intelligence, 119:61–101, 2000

    David Fitoussi and Moshe Tennenholtz. Choosing social laws for multi-agent systems: Minimality and simplicity.Artificial Intelligence, 119:61–101, 2000

    work page 2000

  32. [32]

    Coalitional games on graphs: core structure, substitutes and frugality

    Rahul Garg, Vijay Kumar, Atri Rudra, and Akshat Verma. Coalitional games on graphs: core structure, substitutes and frugality. Technical Report TR-02-60, University of Texas at Austin, 2002

    work page 2002

  33. [33]

    Multi-unit auctions for allocat- ing chance-constrained resources

    Anna Gautier, Bruno Lacerda, Nick Hawes, and Michael Wooldridge. Multi-unit auctions for allocat- ing chance-constrained resources. InProceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 11560–11568, 2023

    work page 2023

  34. [34]

    Goldberg, Jason D

    Andrew V. Goldberg, Jason D. Hartline, Anna R. Karlin, Michael Saks, and Andrew Wright. Com- petitive auctions.Games and Economic Behavior, 55(2):242–269, 2006

    work page 2006

  35. [35]

    Goldberg, Jason D

    Andrew V. Goldberg, Jason D. Hartline, and Andrew Wright. Competitive auctions and digital goods. InProceedings of SODA-01, pages 735–744, 2001

    work page 2001

  36. [36]

    T. Groves. Incentives in teams.Econometrica, 41:617–631, 1973

    work page 1973

  37. [37]

    Collusion-proof mechanisms for multi-unit procurement.Games and Economic Behavior, 138:281–298, 2023

    Martin Hagen. Collusion-proof mechanisms for multi-unit procurement.Games and Economic Behavior, 138:281–298, 2023

    work page 2023

  38. [38]

    Hartline

    J. Hartline. Lectures on optimal mechanism design. Technical report, 2006

    work page 2006

  39. [39]

    Diffusion auction design.Artificial Intelligence, 303:103631, 2022

    Bin Li, Dong Hao, Hui Gao, and Dengji Zhao. Diffusion auction design.Artificial Intelligence, 303:103631, 2022

    work page 2022

  40. [40]

    Diffusion mechanism design in social networks

    Bin Li, Dong Hao, Dengji Zhao, and Tao Zhou. Diffusion mechanism design in social networks. In Proc. of AAAI-17, pages 586–592, 2017

    work page 2017

  41. [41]

    E. S. Maskin and J. G. Riley. Optimal multi-unit auctions. InThe Economics of Missing Markets, Information and Games, pages 312–335. 1989

    work page 1989

  42. [42]

    Dynamic mechanism design on social networks.Games and Economic Behavior, 131:84–120, 2022

    Dawen Meng, Lei Sun, and Guoqiang Tian. Dynamic mechanism design on social networks.Games and Economic Behavior, 131:84–120, 2022

    work page 2022

  43. [43]

    Roger B. Myerson. Optimal auction design.Mathematics of Operations Research, 6(1):58–73, 1981

    work page 1981

  44. [44]

    Algorithmic mechanism design

    Noam Nisan and Amir Ronen. Algorithmic mechanism design. InProceedings of the 31st Annual ACM Symposium on Theory of Computing, pages 129–140. ACM, 1999

    work page 1999

  45. [45]

    Algorithmic mechanism design.Games and Economic Behavior, 35:166–196, 2001

    Noam Nisan and Amir Ronen. Algorithmic mechanism design.Games and Economic Behavior, 35:166–196, 2001

    work page 2001

  46. [46]

    Computationally feasible vcg mechanisms.Journal of Artificial Intelligence Research, 29:19–47, 2003

    Noam Nisan and Amir Ronen. Computationally feasible vcg mechanisms.Journal of Artificial Intelligence Research, 29:19–47, 2003

    work page 2003

  47. [47]

    Cambridge University Press, 2007

    Noam Nisan, Tim Roughgarden, Eva Tardos, and Vijay V Vazirani.Algorithmic Game Theory, volume 1. Cambridge University Press, 2007

    work page 2007

  48. [48]

    Improved learning rates in multi-unit uniform price auctions

    Marius Potfer, Dorian Baudry, Hugo Richard, Vianney Perchet, and Cheng Wan. Improved learning rates in multi-unit uniform price auctions. InAdvances in Neural Information Processing Systems 37, 2024

    work page 2024

  49. [49]

    Sandholm

    T. Sandholm. Algorithm for optimal winner determination in combinatorial auctions.Artificial Intelligence, 135(1–2):1–54, 2002

    work page 2002

  50. [50]

    Shoham and M

    Y. Shoham and M. Tennenholtz. On the synthesis of useful social laws for artificial agent societies. InProceedings of AAAI-92, pages 276–281, 1992

    work page 1992

  51. [51]

    On social laws for artificial agent societies: off-line design

    Yoav Shoham and Moshe Tennenholtz. On social laws for artificial agent societies: off-line design. Artificial Intelligence, 73(1):231–252, 1995. 16

    work page 1995

  52. [52]

    The price of truth: Frugality in truthful mechanisms

    Kunal Talwar. The price of truth: Frugality in truthful mechanisms. InProc. of STACS-03, pages 608–619, 2003

    work page 2003

  53. [53]

    van der Hoek, M

    W. van der Hoek, M. Roberts, and M. Wooldridge. Knowledge and social laws. InProceedings of AAMAS-05, pages 674–681, Utrecht, Netherlands, 2005

    work page 2005

  54. [54]

    van der Hoek, M

    W. van der Hoek, M. Roberts, and M. Wooldridge. Social laws in alternating time: Effectiveness, feasibility, and synthesis.Synthese, 156:1–19, 2007

    work page 2007

  55. [55]

    Counterspeculation, auctions, and competitive sealed tenders.Journal of Finance, 16(1):8–37, 1961

    William Vickrey. Counterspeculation, auctions, and competitive sealed tenders.Journal of Finance, 16(1):8–37, 1961

    work page 1961

  56. [56]

    Strategic ability updating in con- current games by coalitional commitment.IEEE Transactions on Systems, Man, and Cybernetics, Part B, 41(6):1442–1457, 2011

    Chongjun Wang, Jun Wu, Zhong-Cun Wang, and Junyuan Xie. Strategic ability updating in con- current games by coalitional commitment.IEEE Transactions on Systems, Man, and Cybernetics, Part B, 41(6):1442–1457, 2011

    work page 2011

  57. [57]

    J. Wu, Y. Qiao, L. Zhang, C. Wang, and M. Liu. A multi-unit profit competitive mechanism for cellular traffic offloading. InProc. of AAAI-20, pages 2294–2301, 2020

    work page 2020

  58. [58]

    J. Wu, L. Zhang, C. Wang, and J. Xie. Synthesizing optimal social laws for strategical agents via bayesian mechanism design. InProc. of AAMAS-17, pages 1214–1222, 2017

    work page 2017

  59. [59]

    J. Wu, Y. Zhang, Y. Qiao, L. Zhang, C. Wang, and J. Xie. Multi-unit budget feasible mechanisms for cellular traffic offloading. InProc. of AAMAS-19, 2019

    work page 2019

  60. [60]

    A bayesian optimal social law synthesizing mechanism for strategical agents.Autonomous Agents and Multi-Agent Systems, 36(2):1–39, 2022

    Jun Wu, Jie Cao, Hongliang Sun, and Chongjun Wang. A bayesian optimal social law synthesizing mechanism for strategical agents.Autonomous Agents and Multi-Agent Systems, 36(2):1–39, 2022

    work page 2022

  61. [61]

    A framework for coalitional normative systems

    Jun Wu, Chongjun Wang, and Junyuan Xie. A framework for coalitional normative systems. In Proceedings of AAMAS-11, 2011

    work page 2011

  62. [62]

    +”) and unsatisfied formulas (with “-

    Lei Zhang, Haibin Chen, Jun Wu, Chongjun Wang, and Junyuan Xie. False-name-proof mechanisms for path auctions in social networks. InProceedings of ECAI-16, pages 1485–1492, 2016. A Examples for the Problem Setting The following example shows that coordinating a system consisting of some rational agents, can be modeled as a Social Law Synthesizing (SLS) pr...

    work page 2016

  63. [63]

    whether there is a social lawη∈SL S achieves the value ofg(η, x)at leastl∈R +

    the expected payment to each agent satisfy: pi(xi)=p i(0)+x iri(xi)−∫ xi 0 ri(ti)dti (14) . 21 Proof.First of all, the following equivalence relations follow trivially from the definition of BNIC and equations (9) and (10): Mechanism⟨H, P⟩is BNIC iff∀i∈A, xi, γi ∈Xi∶¯ui(xi, xi)≥¯ui(xi, γi) iff∀i∈A, xi, γi ∈Xi∶ˆui(xi)≥pi(γi)−ri(γi)xi iff∀i∈A, xi, γi ∈Xi∶ˆu...

    work page 2001

  64. [64]

    whether there is an(i, n)- social lawη∈SL (i,n) S achieves the value ofg(η, x)at leastl∈R +

    ForDominant(i, n)-Social Law, the associated decision problem is “whether there is an(i, n)- social lawη∈SL (i,n) S achieves the value ofg(η, x)at leastl∈R +”, and it is trivially inN Psince we can guess an(i, n)-social law and verify it in polynomial time. Therefore,Dominant(i, n)-Social Lawis in FP N P; Moreover, we can show that it is FP N P-hard by re...

    work page

  65. [65]

    Ifℓ(y q A∶⃗mA )=1, then by constraint (30),ℓ(y q A∶⃗mA )≥1, so∃i∈A∶ℓ(yq i∶⃗mA[i])=1; if∃i∈A∶ℓ(yq i∶⃗mA[i])=1, then by constraint (29),ℓ(y q A∶⃗mA )≥1, soℓ(y q A∶⃗mA )=1

    work page

  66. [66]

    Ifℓ(s q,φ A∶⃗mA,⃗m ¯A )=1, then by constraint (34), we have ℓ(y q ¯A∶⃗m ¯A )+ℓ(x δ(q,( ⃗mA,⃗m ¯A)) φ )≥1, thereforeℓ(y q ¯A∶⃗m ¯A )=1 orℓ(x δ(q,( ⃗mA,⃗m ¯A)) φ )=1; 28 Ifℓ(y q ¯A∶⃗m ¯A )=1 orℓ(x δ(q,( ⃗mA,⃗m ¯A)) φ )=1, then by constraints (32)(33), we haveℓ(s q,φ A∶⃗mA,⃗m ¯A )≥1, so ℓ(sq,φ A∶⃗mA,⃗m ¯A )=1

    work page

  67. [67]

    Ifℓ(z q,φ A∶⃗mA )=1, then by constraint (36), we have ∀⃗m ¯A ∈D¯A(q)∶ℓ(sq,φ A∶⃗mA,⃗m ¯A )≥1, therefore∀⃗m ¯A ∈D¯A(q)∶ℓ(sq,φ A∶⃗mA,⃗m ¯A )=1; If∀⃗m ¯A ∈D¯A(q)∶ℓ(sq,φ A∶⃗mA,⃗m ¯A )=1, then by constraint (37),ℓ(z q,φ A∶⃗mA )≥1, soℓ(z q,φ A∶⃗mA )=1

    work page

  68. [68]

    Ifℓ(e q,φ A∶⃗mA )=1, then by constraint (46),ℓ(z q,φ A∶⃗mA )≥1, so we haveℓ(z q,φ A∶⃗mA )=1; Moreover, by constraint (47),ℓ(y q A∶⃗mA )≤0, so we haveℓ(y q A∶⃗mA )=0; Ifℓ(y q A∶⃗mA )=0 andℓ(z q,φ A∶⃗mA )=1, then by constraint (45), we haveℓ(e q,φ A∶⃗mA )≥1, soℓ(e q,φ A∶⃗mA )=1

    work page

  69. [69]

    Ifℓ(r q ⟪A⟫ψUχ)=1, then by constraint (51), we haveℓ(x q ψ)≥1, thereforeℓ(x q ψ)=1 and by con- straint (52), we have ∑⃗mA∈DA(q) ℓ(eq,⟪A⟫ψUχ A∶⃗mA )≥1. It implies∃ ⃗mA ∈DA(q)∶ℓ(eq,⟪A⟫ψUχ A∶⃗mA )=1, so by lemma 19.5, we can obtainℓ(x q ψ)=1 and∃ ⃗mA ∈DA(q)∶ℓ(eq,⟪A⟫ψUχ A∶⃗mA )=1, and further by constraint (53), we can deduceℓ(r q ⟪A⟫ψUχ)≥1, soℓ(r q ⟪A⟫ψUχ)=1...

    work page

  70. [70]

    Caseφ∈cl(F),p∈Π: by constraints (38)(39), we can obtainℓ(x q p)=1 iffp∈(Π∩cl(F))∩π(q) iffp∈π(q)iffS†η ℓ, q⊧φ

    work page

  71. [71]

    Caseφ=¬ψ: by constraint (40) we can obtainℓ(x q ¬ψ)=1 iffℓ(x q ψ)=0 (by inductive hypothesis) iffS†η ℓ, q⊭φ(by the ATL semantics) iffS†η ℓ, q⊧¬φ

    work page

  72. [72]

    Caseφ=ψ∨χ: by constraints (41) (43), we can obtainℓ(x q ψ∨χ)=1, iffℓ(x q ψ)=1 orℓ(x q χ)=1 (by inductive hypothesis) iffS†η ℓ, q⊧ψorS†ηℓ, q⊧χ(by the ATL semantics) iffS†ηℓ, q⊧ψ∨χ

    work page

  73. [73]

    Caseφ=⟪A⟫◯ψ: Ifℓ(x q ⟪A⟫◯φ)=1, then by constraint (49) we can obtain ∑⃗mA∈DA(q) ℓ(eq,φ A∶⃗mA )≥1, therefore∃⃗mA ∈DA(q)∶ℓ(eq,φ A∶⃗mA )=1, by lemma 19.5, we have∃ ⃗mA ∈DA(q)∶ℓ(eq,φ A∶⃗mA )=1, and further by constraint (48), we can obtainℓ(x q ⟪A⟫◯φ)≥1, and thereforeℓ(x q ⟪A⟫◯φ)=1. So, now we have ℓ(xq ⟪A⟫◯φ)=1 iff∃⃗mA ∈DA(q)∶(ℓ(yq A∶⃗mA )=0 andℓ(z q,φ A∶⃗mA...

    work page

  74. [74]

    (by lemma 19.1, lemma 19.2) ; iff∃⃗mA ∈DA(q)∶(∀i∈A∶⃗mA[i]∉ηℓ(i, q)and∀⃗m ¯A ∈D¯A(q)∶∃i∈¯A∶ℓ(yq i∶⃗m ¯A[i])=1 orS†η ℓ, δ(q,( ⃗mA, ⃗m ¯A))⊧ φ) (by inductive hypothesis) iffS†η ℓ, q⊧⟪A⟫◯ψ(by the ATL semantics)

    work page

  75. [75]

    Caseφ=⟪A⟫ψUχ: Ifℓ(x q ⟪A⟫ψUχ)=1, then by constraint (56) we can obtainℓ(x q χ)+ℓ(r q ⟪A⟫ψUχ)≥1, thereforeℓ(x q χ)=1 orℓ(r q ⟪A⟫ψUχ)=1; Ifℓ(x q χ)=1 orℓ(r q ⟪A⟫ψUχ)=1, then by constraints (54)(55), we can obtainℓ(x q ⟪A⟫ψUχ)=1; 29 The above facts meansℓ(x q ⟪A⟫ψUχ)=1 iffℓ(x q χ)=1 orℓ(r q ⟪A⟫ψUχ)=1, iffℓ(x q χ)=1 or (ℓ(x q χ)=1 and∃ ⃗mA ∈DA(q)∶(ℓ(yq A∶⃗mA ...

    work page

  76. [76]

    Finally, the following result follows from the above two lemmas

    Caseφ=⟪A⟫◻ψ: Ifℓ(x q ⟪A⟫◻ψ)=1, then by constraint (57) we can obtainℓ(x q ψ)≥1, so we haveℓ(x q ψ)=1, moreover by constraint (58) we have ∑⃗mA∈DA(q) ℓ(eq,⟪A⟫◻ψ A∶⃗mA )≥1, therefore∃ ⃗mA ∈ DA(q)∶ℓ(eq,⟪A⟫◻ψ A∶⃗mA )=1; Ifℓ(x q ψ)=1 and∃ ⃗mA ∈DA(q)∶ℓ(eq,⟪A⟫◻ψ A∶⃗mA )=1, then by constraint (59) we haveℓ(x q ⟪A⟫◻ψ)≥1, soℓ(x q ⟪A⟫◻ψ)=1; The above facts meansℓ(x ...

    work page

  77. [77]

    Ifℓis a solution toILP-Dom-SL, thenη ℓ is a dominant social law under the bid profilex

    work page

  78. [78]

    Ifℓis a solution toILP-Dom-IN-SL, thenη ℓ is a dominant(i, n)-social law under the bid profile x. Proof.1) Sinceℓassigns binary values to eachy q i∶a, and ifℓis a solution toILP-Dom-SL(S,F, f 1, ..., fk, x), then it must satisfy constraint (27) which guarantees there is at least one available actions for each agent in each state, therefore there is a one-...

    work page

  79. [79]

    φis satisfied in the stateqofS

    Ifℓis a solution toILP-Dominant-IN-SL(S,F, f 1, ..., fk, x, i, n), then the additional constraint (60) guarantees that there is a one-to-one correspondence between{η ℓ}and possible(i, n)-social laws, i.e., SL(i,n) S . So, now this ILP basically tries to search inSL (i,n) S for the(i, n)-social law that maximizes g(η, x). Therefore,η ℓ is a dominant(i, n)-...

    work page 2002