Synthesis of Cost-Optimal Multi-Agent Systems
for Resource Allocation

Hence, the resource costs of a path $\pi$ is the sum of prices of the resources that are ever allocated by some agent in the states along $\pi$. Conversely, resources that are never allocated do not contribute to the costs. We consider MRAs that run until all goals have been achieved where each goal has a deadline. Thus, in the calculation of the costs of a path it is sufficient to only take the $k$-prefix of the path into account where $k$ is the latest deadline. Based on path costs we can now define what a resource cost-optimal winning strategy is.

Hence, a winning strategy $\sigma_{Agt}$ is cost-optimal with regard to resources if following this strategy results in a path whose costs are less or equal to the costs of the paths resulting from any other winning strategy $\sigma^{\prime}_{Agt}$. We denote the corresponding cost-optimal strategy synthesis problem by $[M,s\models\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,\Phi]_{Opt}^{Res}$.

Assuming that our example MRA models a resource allocation problem in distributed computing, the resource cost-optimal strategy gives us an indication which types and amounts of resources actually need to be purchased for an agent-based solution that guarantees the achievement of all resource goals. So far, we assumed that the number of agents in the system is fixed and that goals are pre-assigned to agents. In the following we will relax this condition and introduce a generalised cost-optimal strategy synthesis that also considers costs for agents.

Hence, the agent costs of a path is the sum of the prices of the agents that ever allocate some resources along the path. We can now straightforwardly define the overall costs of paths with regard to resources and agents.

This allows us to consider a generalised scenario where the goals to be achieved are not assigned to particular agents.

Thus, model checking of general goal properties searches for a strategy that ensures that each goal will be achieved by some agent. In this context, a cost-optimal winning strategy is one that minimises the combined costs of required resources and agents.

Hence, a winning strategy $\sigma_{Agt}$ is MRA cost-optimal if following this strategy results in a path whose combined resource and agent costs are less or equal to the costs of the paths resulting from any other winning strategy $\sigma^{\prime}_{Agt}$. We denote the corresponding cost-optimal strategy synthesis problem by $[M,s\models\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,\Phi]_{Opt}^{M}$.

For CNF formulas the satisfiability problem is defined as follows:

Weighted conjunctive normal form extends CNF by assigning non-negative weights to each clause of a formula.

For the sake of simplicity we typically just write $\mathcal{C}$ for hard clauses $(\mathcal{C},\infty)$. Each WCNF formula $\mathcal{F}$ can be written as a conjunction $\mathcal{H}\wedge\mathcal{S}$ where $\mathcal{H}$ are the hard clauses and $\mathcal{S}$ are the soft clauses of $\mathcal{F}$. For WCNF formulas the following optimisation problem has been defined:

Hence, the solution of the weighted maximum satisfiability problem with regard to $\mathcal{F}$ is a truth assignment $\alpha$ that maximises the sum of weights of the satisfied soft clauses, under the condition that all hard clauses are satisfied. If no such assignment exists, then the weighted maximum satisfiability problem has no solution. We will now show how cost-optimal strategy synthesis problems can be encoded as weighted Max-SAT problems.

The definition of the sub encoding $[r=a]_{t}$ can be found in [24].

If we conjunctively add the auxiliary encoding $[Aux_{Res}]$ to the overall encoding of a strategy synthesis problem, this will not affect the satisfiability. But now we have that a truth assignment $\alpha$ will set an auxiliary variable $nu_{r}$ to true if and only if $\alpha$ characterises a strategy $\sigma_{Agt}^{\alpha}$ and the resource $r$ will be never used when the strategy $\sigma_{Agt}^{\alpha}$ is followed. Hence, $nu_{r}$ is a single-variable encoding of $r$ never being used. We can now utilise each $nu_{r}$ as a unit clause in the optimisation extension of our encoding:

Hence, $[Opt_{Res}]$ consists of soft clauses $(nu_{r},\$(r))$, one for each $r\in Res$, where $nu_{r}$ encodes that $r$ is never used and $\$(r)$ (the price of the resource $r$) is the weight of the clause. The overall encoding of the problem of synthesising a resource cost-optimal strategy is $\mathcal{F}_{Opt}^{Res}=[\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi]\wedge[Aux_{Res}]\wedge[Opt_{Res}]$ where the sub formula $[\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi]\wedge[Aux_{Res}]$ consists of hard clauses only. Solving max-sat$(\mathcal{F}_{Opt}^{Res})$ will return a truth assignment that satisfies all hard clauses and maximises the sum of weights of satisfied soft clauses, if such an assignment exists. Such an assignment characterises a winning strategy that is resource cost-optimal.

Proof.  
We have that $\mathcal{F}^{Res}_{Opt}=\mathcal{H}^{Res}_{Opt}\wedge\mathcal{S}^{Res}_{Opt}$ where $\mathcal{H}^{Res}_{Opt}=[\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi]\wedge[Aux_{Res}]$ are the hard clauses and $\mathcal{S}^{Res}_{Opt}=[Opt_{Res}]$ are the soft clauses of the encoding. Moreover, the WCNF formula $\mathcal{F}^{Res}_{Opt}$ is defined over a set of Boolean variables $Var$, and $\mathcal{A}(Var)$ is the set of all possible truth assignments over $Var$.

Proof of Property 1:  
max-sat$(\mathcal{F}^{Res}_{Opt})=nil$ implies that sat$([\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi]\wedge[Aux_{Res}])=$ 0 (Definition 19). The sub formula $[Aux_{Res}]$ only introduces auxiliary variables and sets them equivalent to resource properties (Definition 21). Hence, $[Aux_{Res}]$ cannot be the cause of unsatisfiability and we can conclude that sat$([\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi])=$ 0. This implies that $[M,s_{0}\models\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,\Phi]$ does not hold (shown in [24]). We can now immediately conclude that there does not exist a joint winning strategy to achieve $\Phi$.

Proof of Property 2:  
max-sat$(\mathcal{F}^{Res}_{Opt})=\alpha$ implies that $\alpha=\underset{\alpha\in\mathcal{A}({Var})}{\operatorname{\textbf{arg max}}}\bigg{(}\alpha(\mathcal{H}^{Res}_{Opt})\cdot\big{(}\sum\limits_{(\mathcal{C},w_{\mathcal{C}})\in\mathcal{S}^{Res}_{Opt}}\alpha(\mathcal{C})\cdot w_{\mathcal{C}}\big{)}\bigg{)}$ (Definition 19). Hence, the assignment $\alpha$ satisfies all hard clauses of $\mathcal{F}^{Res}_{Opt}$. In particular, $\alpha([\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi])=$ 1. We can conclude that $[M,s_{0}\models\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,\Phi]$ holds, and that $\alpha$ characterises a corresponding winning strategy $\sigma_{Agt}^{\alpha}$ (shown in [24]). Now we still need to prove that $\sigma_{Agt}^{\alpha}$ is cost-optimal with regard to the use of resources. According to the definition of max-sat, out of all truth assignments that satisfy all hard clauses, $\alpha$ is the assignment that maximises the sum of weights of the satisfied soft clauses. Let $w^{s}_{\alpha}$ be the sum of weights of the soft clauses satisfied by $\alpha$. Then for all other truth assignments $\alpha^{\prime}$ that satisfy all hard clauses we have that $w^{s}_{\alpha}\geq w^{s}_{\alpha^{\prime}}$ (Definition 19). Conversely, let $w^{u}_{\alpha}$ be the sum of weights of the soft clauses not satisfied by $\alpha$. Then for all other truth assignments $\alpha^{\prime}$ that satisfy all hard clauses we have that $w^{u}_{\alpha}\leq w^{u}_{\alpha^{\prime}}$. Each soft clause is of the form $(nu_{r},\$(r))$. For a resource $r\in Res$, $\alpha(nu_{r})=$ 1 implies that $\alpha(\bigwedge_{t=0}^{k}[r=a_{0}]_{t})=$ 1 (Definition 21). The hard clauses of the encoding, $[\langle\!\langle{Agt}\rangle\!\rangle_{{}_{\!\mathit{}}}\,]\wedge[M]\wedge[\Phi]$, ensure that $\alpha(\bigwedge_{t=0}^{k}[r=a_{0}]_{t})=$ 1 if and only if $\alpha$ characterises a joint strategy $\sigma^{\alpha}_{Agt}$ that results in a path $\pi(s_{0},\sigma^{\alpha}_{Agt})$ where resource $r$ is never allocated by any agent at all time steps until $k$ where $k$ is the latest deadline (shown in [24]). We can conclude that $\alpha$ characterises a strategy that results in a $k$-bounded path where $w^{s}_{\alpha}$ are the cumulative costs of the resources that are never used, and $w^{u}_{\alpha}$ are the cumulative costs of the resources that are actually used. Thus, $c_{Res}(\pi(s_{0},\sigma^{\alpha}_{Agt}))=w^{u}_{\alpha}$ (Definition 10). Based on a similar argumentation, we can show that each alternative truth assignment $\alpha^{\prime}$ that satisfies all hard clauses characterises a path $\pi(s_{0},\sigma^{\alpha^{\prime}}_{Agt})$ with cumulative costs of resources $c_{Res}(\pi(s_{0},\sigma^{\alpha^{\prime}}_{Agt}))=w^{u}_{\alpha^{\prime}}$. We already argued that $w^{u}_{\alpha}\leq w^{u}_{\alpha^{\prime}}$ for all alternative assignments $\alpha^{\prime}$. Hence, we can conclude that $\alpha$ characterises a joint winning strategy $\sigma^{\alpha}_{Agt}$ that is resource cost-optimal (Definition 11).