A Truthful Multiunit Profit-Optimal Mechanism for Synthesizing Social Laws

1 Introduction

Social laws have proven to be a powerful and theoretically elegant approach to coordinating multi-agent systems. Based on modal logic, we can model a multi-agent system as a semantic structure, specify the system's properties as logical formulas, and then verify these formulas via model checking. A social law is a set of restrictions on the available actions of agents, altering the system's underlying structure in the hope that desirable properties (objectives) will emerge in the new structure [ ˚Agotnes et al., 2007]. By enabling the expression of valuations for potential social laws and accounting for the cost of implementing each action restriction, SLS can be modeled as an optimization problem [ ˚Agotnes and Wooldridge, 2010]. However, we find that information incompleteness and the self-interested nature of agents, common in typical strategic environments, can introduce unavoidable obstacles to solving this problem. For example, the costs of action restrictions, which are key optimization parameters, are known only privately to each agent; if we attempt to elicit these costs by "asking" the agents, they may strategically misreport them to maximize their own utility.

This challenge naturally falls into the domain of algorithmic mechanism design [Nisan et al., 2007]. We adopt the powerful Alternating-time Temporal Logic (ATL) [Alur et al., 2002] as our foundation, enabling us to model SLS as an auction design problem characterized by the following features:

∗ Jian Huang is the corresponding author.

1. Multi-unit Procurement: Each agent has multiple available actions, and the social law designer seeks to selectively restrict a subset of actions for each agent.
2. Bayesian single-parameter setting : Each agent holds private information about the unit cost of restricting each of its actions, while the prior probability distribution of these unit costs is common knowledge.
3. Profit-Optimality: The objective is to reliably output the social law that maximizes profit (defined as value minus payment), even when agents behave strategically.

The primary challenge stems from the "multi-unit" nature of the problem, which prevents us from deriving a clean solution directly from Myerson's framework [Myerson, 1981; Elkind et al., 2004]. Indeed, the interplay between the "multiunit" setting and the sophisticated semantics of ATL renders both the modeling and computation of the mechanism beyond the reach of current state-of-the-art techniques. We aim to develop a solution by carefully analyzing and leveraging ATL's syntax and semantics.

Our main contributions are summarized as follows:

1. We formally prove a representation lemma for ATLbased social laws: any valuation function that does not distinguish alternating bisimulation-equivalent structures [Alur et al., 1998] can be succinctly represented as a feature set, allowing us to formalize SLS as an auction design problem.
2. We identify that the critical obstacle from "multi-unit" settings is irregular payment calculation. We address this by designing an efficient polynomial-time reduction of payment determination to allocation determination, making allocation the key problem to solve.
3. We finally prove that allocation determination is FPNP - complete, and then reduce it to ILP in polynomial time by successfully encoding ATL semantics into a set of ILP constraints. This offloads the computational intractability to highly mature ILP solvers, which are widely used for large-scale industrial problems. Since payment determination reduces to allocation determination in polynomial time, we obtain a mechanism that is truthful, individually rational, profit-maximizing, and efficiently computable with ILP solvers.

Building on the above work, we propose a self-enforcing social law synthesis method that reliably optimizes expected profit in strategic environments.

2 Preliminaries

In this section, we introduce our problem setting.

2.1 Optimal social law synthesizing problem

Social laws can be formalized based on ATL, which adopts Concurrent Game Structures (CGS) as the semantic structure. Cost-aware concurrent game structure, CCGS: We define CCGS as an extended CGS where a marginal cost function which specifies each agent's unit cost is added. Formally, a CCGS is a tuple S = ⟨k, Q, qs, Π, π, ε, c, δ⟩ with:

• A set Ag = {1, ..., k} of agents, a finite set Q of states, an initial state qs ∈ Q, a finite set Π of propositions, a labeling function π specifying for each state q ∈ Q, a set π(q) ⊆ Π of true propositions, and an action function ε. For each agent a ∈ Ag and each state q ∈ Q, a nonempty set εa(q) of actions is available to agent a at state q. A joint action of all the agents at state q is a tuple ⟨j1, ..., jk⟩ such that ja ∈ εa(q) for each agent a. We write D(q) for the joint action space ε1(q) × ... × εk(q).
• A unit cost function c. For each agent i ∈ Ag, if n ∈ N of her actions are restricted, then the resulted cost to her is n ⋅ c(i). We assume c(i) to be agent i's private information, but as public information c(1), ..., c(k) are independent continuous random variables x1, ...,xk respectively, where each xi is drawn from the interval Xi = [0, ωi] subject to a probability density function fi.
• A transition function δ. For each state q ∈ Q and each joint action ⟨j1, ..., jk⟩ ∈ D(q), δ(q, j1, ..., jk) ∈ Q is the next state if every agent a ∈ Ag chooses action ja.

A CCGS intrinsically specifies the running of a multiagent system: each agent chooses an action simultaneously, and the actions chosen by all the agents determine the next state.

Note that, our cost model contains an assumption of constant marginal cost per action restriction. It actually tries to generalize the "minimality" objective in SLS proposed by [Fitoussi and Tennenholtz, 2000], which requires the social law to restrict as few actions as possible, and thus include least "side effects". Our cost model makes sense especially in cases when it is hard for the agents to determine the actual cost for restricting each individual action. Actually, it is easier for them to specify a rough or average cost per action restriction, and in this way we can well capture the agents' preference on fewer restrictions. We will study more general cost models in our future work.

Alternating-time Temporal logic, ATL: We can adopt ATL for specifying and verifying CCGSs. The language of ATL, denoted as LATL, is generated by the following grammar:

where p ∈ Π is a proposition, and A ⊆ Ag is a coalition.

The symbols ◯, ◻, U are the conventional linear-time temporal operators "next-time", "always", "until", respectively.

For a set A ⊆ Ag, the operator ⟪A⟫ is a path selection operator, with ⟪A⟫ψ aims to denote "coalition A can reliably enforce property ψ". Given a ATL formula φ, we use the notation S, q ⊧ φ to mean "φ is satisfied in the state q of S".

Social laws: A social law is an action constraint η for a CCGS S = ⟨k,Q, qs,Π,π, ε, c, δ⟩ defined as a function ∀i ∈ Ag, q ∈ Q ∶ ηi(q) ⊂ εi(q). The new structure obtained by implementing social law η on S, denoted S†η, is the structure S′ = ⟨k,Q, qs,Π, π, ε′ , c, δ′ ⟩ where ∀i ∈ Ag, q ∈ Q ∶ ε′i (q) = εi(q) ∖ ηi(q), and δ′ is obtained from δ by restricting the domain of definition according to ε′ . Intuitively, the implementing of a social law on a CGS is deleting from it all the actions restricted by this social law. We let SLS denote the set of all the possible social laws for S, and let WS denote the set of possible CCGSs that can be obtained from S by implementing a social law, that is, WS = {S′ ∣ ∃η ∈ SLS ∶ S†η = S′}.

Demand valuation function, DVF: Each of the structures in WS has a possibly different value, which can be specified as a DVF v ∶ WS → R+ . From the perspective of each agent i, implementing a social law η results in a cost Ci = c(i) ⋅ ∑q∈Q ∣ηi(q)∣. If the value of c(i) was known, we can pay exactly Ci units of money to agent i to compensate its cost. Therefore the overall payment to all the agent should be ∑i∈Ag Ci, and the profit of implementing social law η will be

Finally, profit optimal social law synthesizing can be modeled as the optimization problem of finding a social law that maximizes the function g(η).

2.2 Compactly represent the DVF

Based on the work in[Alur et al., 1998] and [ ˚Agotnes and Wooldridge, 2010], we can define a bisimulation relation between the state sets of two arbitrary structures in WS.

Alternating bisimulation relation: Given two CCGSs S = ⟨k,Q, qs,Π,π, ε, c, δ⟩ and S′ = ⟨k′ ,Q′ , q′s ,Π′ ,π′ , ε′ , c′ , δ′ ⟩ based on the same agent set Ag = {1, ..., k}, any binary relation Z ⊆ Q×Q′ is called an alternating bisimulation relation if qsZq′s and for any qZq′ , we have

1. π(q) = π′ (q′ );
2. For each A ⊆ Ag and every ⃗mA ∈ DA(q), there is a ⃗m′A ∈ D′A(q′ ) satisfying for all q′x ∈ out(q′ , ⃗m′A), there is a qx ∈ out(q, ⃗mA) satisfying qxZq′x ; and
3. For each A ⊆ Ag and every ⃗m′A ∈ D′A(q′ ), there is a ⃗mA ∈ DA(q) satisfying for all qx ∈ out(q, ⃗mA), there is a q′x ∈ out(q′ , ⃗m′A) satisfying qxZq′x .

Note that, according to ATL semantics, in any state q ∈ Q, DA(q) denotes the joint action space of coalition A, and out(q, ⃗mA) denotes the set of possible next states when coalition A chooses the joint action ⃗mA. The readers can consult the full version or [Alur et al., 2002] for more details about ATL syntax and semantics. We say two structures S and S′ are alternating bisimulation equivalent, denoted as S � S′ , if there is a bisimulation relation between S and S′ .

The representation lemma: Based on the following result, we can formally prove the subsequent representation lemma.

Theorem 1. [Alur et al., 1998] For two concurrent game structures S and S′ , if S � S′ and qZq′ , then for an arbitrary ATL function φ, we have S, q ⊧ φ iff S′ , q′ ⊧ φ.

Lemma 2 (Representation Lemma). The following two statements are equivalent:

Results show that DVFs that do not distinguish alternating bisimulation-equivalent structures admit compact feature-set representations. We focus on this class of DVFs for their mathematical soundness and broad applicability. Note that all proofs in this paper are deferred to the full version 1 .

3 MechanismDesign

3.1 Social law Synthesis via auctions

We select the social law by running a procurement auction: firstly we announce a mechanism consisting of an allocation function ˆR ∶ X → SLS and, for each agent i, a payment function Pi ∶ X → R+ . We then collect the bids (i.e., cost reports) from the agents to obtain the bid profile x, and finally select the social law η = ˆR(x) and pay Pi(x) to each agent i. Note that, the function ˆR can be equivalently specified as ∀i, q, a ∶ Rq i∶a (x) = 1 (indicating that agent i's action a in state q is selected) if a ∈ η(i, q), Rq i∶a (x) = 0 otherwise. Now, we let Ri(x) be the total number of agent i's restricted actions when the bid profile is x, i.e.,

Bayesian games: After a mechanism ⟨R,P⟩ is determined, it applies to any instances of agent set A where real costs are randomly drawn from X, the system intrinsically becomes a Bayesian game ⟨A, (Xi, fi, Bi, ui)i∈A⟩ where

• Xi now denotes not only the cost space but also the action space for agent i, i.e., each xi ∈ Xi also denote the action "bidding/reporting xi";
• Bi is the strategy space of agent i, consisting of all functions of the form b ∶ Xi → Xi, which allows agent i to report its cost strategically.
• ui ∶ Xi×X →R is agent i's utility function. When agent i's true cost is xi, a bid profile x yields the utility:

The expected utility achieved by agent i whose unit cost is xi ∈ Xi when submitting a bid x′i ∈ Xi is

Bayesian-Nash Equilibrium (BNE): A strategy profile (b1,⋯, bn) is a BNE if and only if

1 Available at https://arxiv.org/abs/2605.16853

A mechanism is called Bayesian-Nash Incentive Compatible (BNIC) if and only if truthful bidding(i.e., bi(xi) = xi for all i and xi) constitutes a BNE. According to the famous Revelation Principle [Nisan and Ronen, 2001], we can restrict the search space to BNIC mechanisms without loss of generality.

When agent i bids x′i , we let rq i∶a (x′i ), ri(x′i ) and pi(x′i ) be the probability of agent i's action a in state q being selected, the expected number of agent i's selected actions and the expected amount of payment to agent i, respectively, then

By equations (4)(3)(6) and (8) we can further obtain

Thus, the expected utility of agent i when bidding truthfully is:

Ensuring agents voluntarily comply with the restrictions (rather than via "hard constraints") is naturally captured by the game-theoretic concept of Individual Rationality (IR), which requires that each agent receives a non-negative expected utility after the social law is implemented. For BNIC mechanisms, IR is equivalent to:

Profit: For any cost profile x ∈ X, the selected social law and the payment to agent i will be ˆR(x) and Pi(x) respectively. For a designer with feature set F, the profit is

The expected profit of the designer over the cost profile space X is thus:

The aim of this paper is to find a BNIC and IR mechanism ⟨R∗ , P ∗ ⟩ that maximize the expected profit.

3.2 Truthful multiunit profit-optimal mechanisms

First, we prove that the allocation and payment of any BNIC mechanism can be characterized as follows:

Lemma 3. A mechanism ⟨R, P⟩ is BNIC iff ∀xi ∈ Xi:

1) ri(xi) is monotone nonincreasing; and

1. the expected payment to each agent satisfies:

.

We denote λi(xi) = xi + Fi(xi) fi(xi) and refer to it as the virtual unit cost of agent i. We focus on the regularity case of the space X, where λi is non-decreasing function of xi for every i. The above result leads to the following lemmas.

Algorithm 1 PO-ASL Mechanism

Input: structure S = ⟨k,Q, qs,Π, π, ε, c, δ⟩, feature set F, p.d.f. fi of each agent i's cost, and bid profile x Output: the allocation and payment (R∗ (x),P ∗ (x))

1. Find social law η = ˆR∗ (x) ∈ SLS maximizing

1. Compute the payment to each agent i as follows:

Lemma 4. A mechanism ⟨R, P⟩ is BNIC only if

Lemma 5. A mechanism ⟨H, P⟩ is BNIC and IR only if

Moreover, we further have:

where x ∈ X is the current bid profile and η is a selected social law. Based on the above results, we present the POASL mechanism, as outlined in Algorithm 1.

Dominant Social Law: An (i,n)-social law η∗ that maximizes g(η,x) over all (i,n)-social laws under bid profile x is called a dominant (i,n)-social law under x. The DOMINANT (i, n)-SOCIAL LAW problem refers to, given a structure S, a feature set F, a probability density function fi for each agent i's cost, and a bid profile x, finding the dominant (i,n)-social law.

The allocation step of the mechanism PO-ASL is to find the dominant social law under the bid profile x.

Lemma 6. The allocation function of PO-ASL is monotone nonincreasing.

Combining these lemmas, we can further prove:

Theorem 7. PO-ASL is BNIC, IR, and maximizes the expected profit among all BNIC and IR mechanisms.

It is well-known that for single-parameter procurement settings, truthful mechanisms (where truthful bidding is a dominant strategy) can be characterized as follows:

Theorem 8. [Archer and Tardos, 2001; Hartline, 2006] A single-parameter procurement auction is truthful if and only if for any agent i and bids of other agents x-i fixed,

• Ri(xi, x-i) is monotone non-increasing.

We prove that the mechanism PO-ASL satisfies exactly the above characterizations and is therefore truthful.

Corollary 9. PO-ASL is truthful.

4 Computation

The specification of PO-ASL defines the allocation determination and payment determination problems, but does not provide practical algorithms for solving them. We now address this gap by providing practical algorithms.

4.1 Reducing payment to allocation

In single-unit settings, P ∗ i (x) is simply the threshold bid of agent i and can be found by computing the allocation twice, once for ti = 0 and once for ti = +∞. However, when each agent may hold multiple units, this shortcut no longer applies. Whether an efficient method exists to compute payments in this setting is an open question.

Irregularity in payment calculation in multi-unit settings: Computing the payment P ∗ i (x) for each agent requires evaluating the integral of R∗ i (ti,x-i), a function that describes how the allocation to agent i changes as its bid ti varies from 0 to +∞ (with other agents' bids x-i fixed). A brute-force approach-computing the allocation for all ti ∈ [0,+∞]-is obviously infeasible. We must therefore find a more efficient approach.

Turning points in the allocation curve, TP: Our first observation is that R∗ i (ti, x-i) must be a monotone nonincreasing step function of ti. This follows from Lemma 6, where we proved that R∗ i (ti, x-i) is monotone nonincreasing, and from the fact that R∗ i (ti, x-i) represents the number of actions selected for agent i. To determine R∗ i (ti,x-i), it is sufficient to find its turning points, which form the sequence:

where n1, ...,nk are different natural numbers, (pj,nj) indicates ti = pj is the point where R∗ i (ti,x-i) changes to nj, and therefore k ∈ N ∖ {0}, ∀i ∈ [1, k] ∶ pi ∈ R+ and nk = 0. Moreover, we also let p0 = xi, n0 = R∗ i (xi,x-i), and ∀j > k ∶ pj = +∞, nj = 0, and so we have ∀j ∈ [0, k],∀p ∈ (pj, pj+1) ∶ R∗ i (p, x-i) = nj .

Deriving an efficient algorithm: We begin with the following lemma, which shows that if a social law η outperforms another law η′ (which restricts more of agent i's actions) at bid xi, η will continue to outperform η′ for all higher bids t ≥ xi.

For any i ∈ Ag and n ∈ N, We let

That is, SL(i,n) S refers to the set of all possible (i,n)-social laws, and moreover, we let

So, η(i,n,(xi,x-i)) and η(xi,x-i) refer to the dominant (i,n)- social law and the dominant social law respectively under the bid profile (xi,x-i). The following result shows that when agent i's bid varies from 0 to +∞, the dominant (i, n)-social law remains unchanged:

Thus, the dominant (i,n)-social law is independent of agent i's bid, so we may denote it as η(i,n,x-i) .

Lemma 12.

This result implies that the search space for the optimal social law can be greatly refined. As agent i's bid increases from xi to +∞, the social law that maximizes the objective function must lie in the set {η(i,R∗ i (xi,x-i),x-i) , ..., η(i,0,x-i) }, which contains only R∗ i (xi, x-i) + 1 social laws.

Letv(n, t) denote the objective function value of η(i,n,x-i) under bid profile (t,x-i), and let vn = v(n, 0). This yields the following result for the variation of v(n, t) as agent i's bid varies from 0 to +∞:

We now combine these results to prove the following theorem for determining the turning points, whose intuition is illustrated in Figure 1. The upper part of the figure shows the curves v(5, t), ..., v(0, t). By Lemma 11, each curve corresponds to a fixed social law. By Lemma 10, while all curves are monotone non-increasing, v(n, t) declines faster for larger n. At t = xi, the dominant social law is η(i,3,x-i) . By Lemma 12, as t increases from xi to +∞, the dominant social law will always be in {η(i,3,x-i) , η(i,2,x-i) , η(i,1,x-i) , η(i,0,x-i) } and will have the highest objective function value. Graphically, this corresponds to the curve that remains on the "top layer" of the stack, which successively includes the green curve (A′ ,B), yellow curve (B,C), purple curve (C,D), and blue curve (D,E). These curves correspond exactly to the allocation function R∗ (ti,x-i) shown in the lower part of the figure, with turning points at B, C and D. Theorem 14 identifies the first intersection point of the current top curve with any other curve as t increases:

Theorem 14. ∀j ≥ 1 ∶ If nj-1 > 0, then:

Otherwise, pj = +∞ and nj = 0.

With a precise representation of the curve R∗ i (ti, x-i), we can now determine the payments:

Theorem 15. Let k ∈ N be the smallest index such that nk = 0. Then the payment to agent i is

We now present algorithm 2 for payment computation, which uses the subfunctions Allocation(⋅) and AllocationFix(⋅) to find out the dominant social law and the dominant (i,n)-social law, respectively. The implementation of these subroutines is deferred to Algorithms 3 & 4 later in this paper.

Corollary 16. Algorithm 1 correctly computes the payment of mechanism PO-ASL.

4.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.

Thus, we are unlikely to find efficient algorithms for directly computing PO-ASL. Methodologies for countering intractability should therefore be considered.

4.3 An ILP-based algorithm

We propose an approach that, given an instance of DOMINANT ((i,n)-)SOCIAL LAW, automatically constructs an ILP such that solutions to the ILP correspond exactly to solutions of the original problem instance.

Closure: Let cl(φ) denote the closure of a formula φ, i.e.,

where

E.g., Example 2 (in the full version). The number of formulas in cl(φ) is called the size (or length) of formula φ.

For any feature set F = {(φ1, c1), ..., (φn, cn)}, we let

Algorithm 2 Payment

Input: structure S = ⟨k,Q, qs,Π, π, ε, c, δ⟩, feature set F, p.d.f. fi of each agent i's cost, and bid profile x

for all i ∈ Ag do

if n0 = 0 then

xi ← 0;

else

for 0 ≤ n ≤ n0 do

vn ← g(η′ , (0, x-i));

end for{determine all the (i,n)-social laws}

while nc > 0 do

end while{find the TPs by theorem 14}

{compute agent i's payment by theorem 15}

end if

end for

Actually, cl(F) is the set of all the formulas which can possibly influence the valuation of the objective function.

Variables: We can first of all introduce the following 4 classes of boolean variables:

where

1. yq i∶a = 1 iff at state q, agent i's action a is forbidden;
2. yqA∶ ⃗mA = 1 iff at state q, joint action ⃗mA is forbidden;
3. zq,φ A∶ ⃗mA = 1 iff at state q, coalition A adopting joint action ⃗mA can guarantee that φ is satisfied in the next state.

We now introduce additional intermediate variables and transform these constraints into an equivalent set of ILP constraints, yielding the following ILP for solving the DOMINANT SOCIAL LAW problem.

Note that, we focus on the state set Q, formula set cl(F), and agent set Ag, so for example we write ∀q, i,φ as an abbreviation for ∀q ∈ Q, i ∈ Ag,φ ∈ cl(F). When the state q is clear from the context, we also write ∀⃗mA as an abbreviation for ∀⃗mA ∈ DA(q), and write ∀⃗m¯ A as an abbreviation for ∀⃗m¯ A ∈ D¯ A(q). Moreover, ∀⟪A⟫ means for every operator ⟪A⟫ that appear in a formula in cl(F).

ILP-DOM-SL(S, F, f1, ..., fk, x): maximize

subject to:

We define ILP-DOM-IN-SL(S, F, f1, ..., fk, x, i, n) as the ILP obtained from ILP-DOM-SL(S,F, f1, ..., fk, x) by aiding the additional constraint:

The dependencies between the variables can be vividly depicted as figure 2.

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,

Then, we can further prove the following results:

Lemma 19.

1. ∀q, i, a: ℓ(yq i∶a ) = 1 iff a ∈ ηℓ(i, q);
2. ∀q,A, ⃗mA: ℓ(yqA∶ ⃗mA ) = 1 iff ∃i ∈ A ∶ ℓ(yq i∶ ⃗mA[i] ) = 1;
3. ∀q, ⟪A⟫, ⃗mA, ⃗m¯ A: ℓ(sq,φ A∶ ⃗mA, ⃗m¯A ) = 1 iff ℓ(yq¯ A∶ ⃗m¯A ) = 1 or ℓ(xδ(q,( ⃗mA, ⃗m ¯A)) φ ) = 1;
4. ℓ(zq,φ A∶ ⃗mA ) = 1 iff ∀ ⃗m ¯ A ∶ℓ(sq,φ A∶ ⃗mA, ⃗m ¯A ) = 1;
5. ∀q,φ,A, ⃗mA: ℓ(eq,φ A∶ ⃗mA ) = 1 iff ℓ(yqA∶ ⃗mA ) = 0 and ;

Lemma 20. For any φ ∈ cl(F), ℓ(xqφ) = 1 iff S†ηℓ, q ⊧ φ.

Finally, the following theorem follows from the above two lemmas. It shows that the proposed ILP correctly computes the allocation function.

Theorem 21.

1. If ℓ is a solution to ILP-DOM-SL, then ηℓ is a dominant social law under the bid profile x;

Algorithm 3 Allocation

Input: structure S = ⟨k,Q, qs,Π, π, ε, c, δ⟩, feature set F, p. d. f. fi of each agent i's cost, and bid profile x Generate ILP-DOM-SL(S, F, f1, . . . , fk, x); ℓ ← Solving ILP-DOM-SL (S, F, f1, . . . , fk, x); for all i ∈ Ag, q ∈ Q do ηℓ(i, q) ← {a ∈ εi(q) ∣ ℓ(yq i∶a ) = 1} end for return ηℓ

Algorithm 4 Allocation-Fix

Input: structure S = ⟨k,Q, qs,Π, π, ε, c, δ⟩, feature set F, p. d. f. fi of each agent i's cost, bid profile x, i ∈ Ag and

n ∈ N Generate ILP-DOM-IN-SL (S, F, f1, . . . , fk, x, i, n); ℓ ← Solving ILP-DOM-IN-SL(S, F, f1, . . . , fk, x, i, n); for all i ∈ Ag, q ∈ Q do ηℓ(i, q) ← {a ∈ εi(q) ∣ ℓ(yq i∶a ) = 1} end for return ηℓ

1. If ℓ is a solution to ILP-DOM-IN-SL, then ηℓ is a dominant (i, n)-social law under the bid profile x.

Theorem 22. Both ILP-DOM-SL and ILP-DOM-IN-SL can be generated in O(∣Q∣ ⋅ t ⋅ l2 ) time, where ∣Q∣, t are respectively the state number and state transition number of the given structure, and l is the total length of the formulas in the given feature set.

5 RelatedWork

The cost of implementing a social law was first studied by [Fitoussi and Tennenholtz, 2000]. [ ˚Agotnes and Wooldridge, 2010] later proposed the OPTIMAL SOCIAL LAW problem, which balances the cost and benefit of implementing a social law and models CTL-based social law synthesizing as a combinatorial optimization problem. [Wu et al., 2017; Wu et al., 2022] non-trivially extended the OPTIMAL SOCIAL LAW problem to the strategic case, developed solutions based on the framework of optimal auctions [Myerson, 1981; Elkind et al., 2004]. We consider more general ATL-based social laws, which leads to a new multiunit auction design problem [Maskin and Riley, 1989; Bhattacharya et al., 2020; Brˆanzei et al., 2023; Chan and Chen, 2014; Wu et al., 2019; Wu et al., 2020; Hagen, 2023; Gautier et al., 2023; Potfer et al., 2024; Bougt et al., 2025; Essig Aberg and Baisa, 2025] where payment determination is a major challenge.

6 Conclusion

ATL-based social law synthesis in strategic environments can be modeled as a novel multi-unit, profit-optimal mechanism design problem. By analyzing and encoding ATL semantics and integrating them into our mechanism design framework, we have developed a method to systematically address the modeling and computational challenges of this multi-unit setting and derived a practical profit-optimal mechanism.

Acknowledgments

The authors gratefully acknowledge the constructive comments and suggestions from the anonymous reviewers. This paper is supported by the National Social Science Fund of China (Grant No. 23BJL035).