Budget-Constrained Dynamics in Multiagent Systems

1 Introduction

Budget-Constrained Transition System. In this paper we propose a model of multiagent transition systems in which agents incur cost of performing transitions. For example, consider transition system depicted in Figure 1. This system has three states: w, u, and v and two agents that can perform the transitions: agent a and agent c. It costs agent a two dollars to transition the system from state w to state u. This is shown in the figure by labeling one of the transitions from state w to state u with agent a and the negative profit -$2 that the agent incurs if she chooses to make this transition. The cost of the same transition to agent c is $5. The same figure shows that agent a can recover her costs by making a loop transition from state u back to state u. This transition yields profit of $1. The loop transition can be potentially repeated by agent a multiple number of times for an additional profit.

Although in this paper we use financial terminology, in many cases the same model could be used to reason about other types of resources such as time, storage, network capacity, reputation.

So far, we have assumed that an agent can make any transition labeled with her name. In many real-life settings there are financial barriers on performing transitions. For example, in order to make a profit from an investment one needs to have money available to make the investment. In other situations, there might be various fees, fixed overhead costs, and other similar initial costs of doing business. We model

Pavel Naumov

Vassar College Poughkeepsie, New York, USA pnaumov@vassar.edu

such requirements by assuming that in addition to profit each transition is also labeled with the minimal budget needed to initiate the transition. For example, Figure 2 depicts a transition system in which agent a has two transitions from state w to state u. The first transition requires only the initial investment of $1. After taking this transition, the agent not only recovers this investment, but she makes an additional profit of $3. In other words, if she starts the transition with $100 in hands, she will have $103 after the transition is finished. The second transition has a larger initial budget requirement of $5, but it also brings a larger profit of $4. If the agent starts this transition with the same $100, she will have $104 after the transition is finished. Thus, the agent might prefer to make the second transition unless she has insufficient initial funds. The same figure also shows a transition from state u to state v. If this transition is taken, the agent not only will not recover her original investment, but she will lose additional $2, making her profit on this transition to be -$5.

a

Figure 2: System with Budget Requirements.

In this paper we adopt the described above approach of labeling each transition with the initial budget requirement and the profit. Alternatively, one can use transitions of the form given in Figure 1 and capture initial budget requirement through introduction of additional "ghost" states. Figure 3 uses this alternative approach to specify essentially the same transition system as the one depicted in Figure 2.

Budget-Constraint as a Modality. There are many different questions that can be asked about the described above budgetconstrained transition systems. The focus of this paper is on a modal logic for reasoning about agents' abilities in such systems. At the core of our logical system is modality [a]pb ϕ that stands for "statement ϕ is true after any sequence of transitions that agent a can perform on a budget at most b that results in a profit of at least p". For example, consider the transition system depicted in Figure 4.

This system has four states: u, v,w, and s. Although atomic proposition P is true only in state v of this model, statement w ⊩ [a]23 P is true in this system. In other words, the only states that can be reached from state w with budget 3 and profit 2 is state v. Indeed, state s is not reachable under these financial constraints because transition from state w to state s has initial budget requirement of 4, which is greater than our given budget 3. State u is reachable from state w given our constraints on budget, but the profit of 1 achieved after the transition from state w to state u would not satisfy our minimal profit requirement of 2. Finally, the state w can be reached from itself on a zero budget without any transitions, but it can not be reached with the minimal required profit of 2.

Modalities of the form [a]pb can be nested. For example, formula [a]20 [c]20 P states that after any sequence of transitions by agent a on budget 0 and with profit at least 2 followed by any sequence of transitions by agent c on budget 0 and with profit at least 2, statement P is satisfied. Formula

[a]20 [c]20 P , for example, holds in state w of the transition system depicted in Figure 5.

As it is common in modal logic, one can define a dual ("possibility") modality 〈a〉pb ϕ as an abbreviation for ¬[a]pb ¬ϕ. Informally, statement 〈a〉pb ϕ means that on a budget b and a minimal profit requirement p, agent a can transit the system into a state where statement ϕ is satisfied. For example, for the transition system depicted in Figure 6, with an initial budget of 1 agent a can reach a state where P is true, while making a profit of 300. Or, using our formal notations, w ⊩ 〈a〉300 1 P. Indeed, although with budget of just 1 agent a can not make a transition from state w to state u at first, she will be able to make this transition after 99 loop transitions from state w back to state w. The latter is true because each of the loop transitions increases her available funds by 1.

By combining modalities for different agents, we can express interaction between these agents. For example, formula w ⊩ 〈a〉00 〈c〉100 0 ⊤, where ⊤ is the Boolean truth constant, says that at zero expense to herself agent a can create and opportunity for agent c to make a profit of 100. This formula is true, for example, for the transition system depicted in Figure 7. To create such an opportunity, the agent a needs to first accumulate profit 100 by making 100 loop transitions from state w to state w. Second, agent a uses the accumulated profit to transition from state w to state u. From state u agent c can make 100 loop transitions to accumulate her own profit of 100. On the other hand, formula w ⊩ 〈a〉00 [c]100 0 ⊥, where ⊥ is the Boolean false constant, says that at zero expense agent a can "prevent" agent c from making a profit of 100.

We have stated earlier that we informally interpret modality 〈a〉pb ϕ to mean that on a budget b and a minimal profit requirement p agent a can transition the system into a state where statement ϕ is satisfied. The meaning of word "can" needs to be clarified in the situation when there are multiple transitions from the same states labeled with different agents. For example, in the transition system depicted in Figure 8

agent a "can" transition the system from state w to state u and agent c "can" transition the system from state w to state v, but of courses they can not do both. Informally, in this paper we interpret modality 〈a〉 as "agent a, if it acts fast enough, can

...". Thus, from the point of few of the formal semantics that we define later in this paper, in the transition system depicted in Figure 8 both of the following is true: w ⊩ 〈a〉10 P and w ⊩ 〈c〉10 Q.

Logical System. The discussed above modal formulas are satisfied in some states of some transition systems and are not satisfied in the others. In this paper we are interested in the properties of budget-constrained modality that are satisfied in all states of all transition systems. An example of such property is distributivity:

Informally, it states that if statement ϕ → ψ is satisfied in all states that agent a can reach with budget b at a profit of at least p and statement ϕ is also in all such states, then statement ψ is satisfied in the same states.

A more interesting example of such a property is the following form of transitivity:

Informally, it states that if statement ϕ is satisfied in all states that agent a can reach with budget b at a profit of at least p+q, then statement ϕ is satisfied in any state that agent a can reach by first making a sequence of moves on budget b bringing a profit of at least p and than making a sequence of moves on budget b+p bringing a profit of at least q. The reason why the budget for the second sequence of moves is b+p and not just b is that the agent's budget after the first sequences of moves is adjusted by the profit she makes during these moves.

In a formula of the form [a]pb ϕ, value of b represents the budget available to the agent. The budget represents the funds available to the agent before it starts the transitions and it is assumed that the balance never goes below zero. Because of this we only allow non-negative values of the budget b. Profit, on the other hand is different. A sequence of transitions can result in balance increase, which corresponds to a positive profit or a balance decrease, which corresponds to a negative profit. A special case of a sequence of transitions is the empty sequence. It has zero profit and can be accomplished on a zero budget. Thus, if p ≤ 0 and formula ϕ is satisfied in any state that agent a can reach from state w by making a sequence of moves on budget b bringing a profit of at least p, then formula ϕ must be satisfied in the state w as well:

There are two monotonicity principles for the modality [a]pb . The first of them says that anything that can be achieved on a smaller budget can also be achieved on a larger budget: 〈a〉pdϕ → 〈a〉pb ϕ, where d ≤ b. This principle could be rephrased in terms of modality [a]pb as

The other monotonicity principle states that anything that can be achieved with a profit at least q could also be achieved with profit at least p, where p ≤ q. That is 〈a〉qb ϕ → 〈a〉pb ϕ, where p ≤ q. Rephrased in terms of modality [a]pb ,

Perhaps surprisingly, in Lemma 1 we prove that principle (5) logically follows from principles (1), (2), and (3). Furthermore, in Theorem 2 we show that principles (1), (2), (3), and (4) form a complete logical system describing all universal properties of budget-constrained dynamics.

Literature Review. The logical system proposed in this paper could be viewed as a form of dynamic modal logic [Harel et al., 2000]. Instead of a specific program that transition system from one state to another we consider budget and profit associated with such a transition.

The axiomatic system proposed in this paper is also related to other logical systems for reasoning about bounded resources. The classical logical system for reasoning about resources is the linear logic [Girard, 1987; Ryu, 1998; Costantini and Formisano, 2013]. Alechina and Logan [2002] presented a family of logical systems for reasoning about beliefs of a perfect reasoner that can only derive consequences of her beliefs after some time delay. This approach has been further developed into the multi-agent Timed Reasoning Logic in [Alechina et al., 2004]. Bulling and Farwer [2010a] proposed Resource-Bounded Tree Logics for reasoning about resource-bounded computations and obtained preliminary results on the complexity and decidability of model checking for these logics. Their logical system dealing with agent's endowment [Bulling and Farwer, 2010b] is closely related to our current work, but their focus is on model checking rather than a complete axiomatization. Alechina, Logan, Nga, and Rakib [2011] incorporated resource requirements into Coalition logic and gave a sound and complete axiomatization of the resulting system.

Alechina, Logan, Nguyen, Raimondi and Mostarda [2015] implemented a model checking algorithm for the verification of properties expressed in Resource-Bounded Alternating Time Temporal Logic.

Naumov and Tao introduced sound and complete modal logics for reasoning about budget-constrained knowledge [2015] and cost of privacy [2016]. Balbiani, Fern´andezDuque, and Lorini [2016a; 2016b] introduced a logical system for belief dynamics of resource-bounded agents. Another logical system for reasoning about knowledge under bounded resources was proposed by [Jamroga and Tabatabaei, 2013]. Their paper focuses on the expressive power of the language of the system and the model checking algorithm.

Unlike the current paper, described above works consider neither profit and budget constraints nor their interplay.

Outline. This paper is organized as following. In Section 2 we define syntax and formal semantics of our logical system. In Section 3 state axioms and inference rules of this system as well as prove principle (5) from these axiom. We show soundness of the axioms in Section 4 and their completeness in Section 5. Section 6 concludes.

2 Syntax and Semantics

In this section we define syntax and formal semantics of our logical system. We assume a fixed set of agents A and a fixed set of propositional variables. As we have discussed in the introduction, value b in the expression [a]pb ϕ represents the budget available to agent a. Since we assume that the balance never goes below zero, we restrict the syntax of our system to subscript b being a non-negative real number.

At the same time, the value of superscript p could be negative if the agent looses money during a sequence of transitions. Since the losses can not be larger than initially available funds, we restrict the syntax by the assumption -b ≤ p.

Definition 1 Let Φ be the minimal set of formulas such that

1. P ∈ Φ for each propositional variable P,
2. ϕ→ψ ∈ Φ for each ϕ, ψ ∈ Φ,
3. ¬ϕ ∈ Φ for each ϕ ∈ Φ,
4. [a]pb ϕ ∈ Φ for each ϕ ∈ Φ, each p, b ∈ R, and each a ∈ A, where 0 ≤ b and -b ≤ p.

Let symbol R denote the set of all real numbers and symbol R+0 denote the set of all non-negative real numbers.

Definition 2 A transition system is triple 〈V, T, ⊩〉, such that 1. V is an arbitrary finite set of "states",

1. T ⊆ V ×R+0 ×A×R×V is a set of "transitions",
2. ⊩ is a satisfiability relation between states and propositional variables.

For example, for the transition system depicted in Figure 8, set of states V is the set {u, v,w}, set of transitions T is the set {(w, 0, a, 1, u), (w, 0, c, 1, v)}, and satisfiability relation ⊩ is the relation {(u, P ), (v, Q)}.

Definition 3 We extend satisfiability relation ⊩ to a relation between vertices in V and formulas in Φ as follows:

1. v ⊩ ¬ϕ if v ⊮ ϕ,
2. v ⊩ ϕ→ψ if v ⊮ ϕ or v ⊩ ψ,
3. v ⊩ [a]pb ϕ if vn ⊩ ϕ for all sequences (v0, b1, a, p1, v1), (v1, b2, a, p2, v2), . . . , (vn-1, bn, a, pn, vn) ∈ T such that
4. (a) n ≥ 0,
5. (b) v0 = v,
6. (c) ∑ni=1 pi ≥ p,
7. (d) b + ∑k-1 i=1 pi ≥ bk for each 1 ≤ k ≤ n.

The condition (c) in the above definition captures the assumption that the total profit along the computational path is at least p and the condition (d) states the requirement that at any point in the path the agent performs a transition only if she has accumulated sufficient funds for this transition.

3 Axioms

In addition to propositional tautologies in language Φ, our logical system consists of the following axioms:

1. Reflexivity: [a]pb ϕ→ϕ where p ≤ 0,
2. Transitivity: [a]p+q b ϕ→ [a]pb [a]qb+pϕ,
3. Distributivity: [a]pb (ϕ→ψ) → ([a]pb ϕ→ [a]pb ψ),
4. Monotonicity: [a]pb ϕ→ [a]pdϕ, where d ≤ b.

Formula ϕ is a theorem of our logical system and write ⊢ ϕ if formula ϕ is provable in our logical system using the above axioms and Necessitation and Modus Ponens inference rules:

We write X ⊢ ϕ if formula ϕ is provable from the theorems of our logical system and the set of additional axioms X using only Modus Ponens inference rule.

To conclude this section we prove principle (5) from the axioms of our logical system. This principle has been discussed in the introduction. The soundness of our logical system is established in Section 4.

Proof. Note that -b ≤ p by Definition 1. Hence, -b ≤ p ≤ q due to the assumption of the lemma. Thus, 0 ≤ b + q, -(b + q) ≤ p - q, and p - q ≤ 0. Hence, by Reflexivity axiom ⊢ [a]p-q b+q ϕ → ϕ. Then, ⊢ [a]qb ([a]p-q b+q ϕ → ϕ) by Necessitation inference rule. Thus, by Distributivity axiom and Modus Ponens inference rule,

On the other hand, inequality -b ≤ p ≤ q also implies that -b ≤ q + (p - q) and -(b + q) ≤ p - q. Hence, by Transitivity axiom, ⊢ [a]q+(p-q) b ϕ → [a]qb [a]p-q b+q ϕ. In other words, ⊢ [a]pb ϕ → [a]qb [a]p-q b+q ϕ. Thus, taking into account formula (6), by the laws of propositional reasoning, ⊢ [a]pb ϕ → [a]qb ϕ. ⊠

4 Soundness

In this section we prove soundness of our logical system with respect to the formal semantics given earlier. We state this result as Theorem 1 below.

Theorem 1 Let ϕ ∈ Φ. If ⊢ ϕ, then v ⊩ ϕ for every state v ∈ V of every model 〈V, T, ⊩〉.

Soundness of most of the axioms and inference rules is straightforward. Below we show the soundness of Transitivity axiom.

Suppose v ⊩ [a]p+q b ϕ. Consider any sequence of tuples (v0, b1, a, p1, v1), . . . , (vm-1, bm, a, pm, vm) ∈ T such that m ≥ 0, v0 = v,

and

By Definition 3, it suffices to prove that vm ⊩ [a]qb+pϕ. Indeed, consider any sequence of tuples (vm, bm+1, a, pm+1, vm+1), . . . , (vn-1, bn, a, pn, vn) ∈ T such that m ≤ n,

and

It suffices to show that vn ⊩ ϕ. To do this, first notice that, due to inequalities (7) and (9),

Second, we show that b + ∑k-1 i=1 pi ≥ bk for each 0 ≤ k ≤ n by considering cases 0 ≤ k ≤ m and m + 1 ≤ k ≤ n separately. In the first case, the required follows from statement (8). In the second case, due to inequalities (7) and (10),

Therefore, vn ⊩ ϕ by the assumption v ⊩ [a]p+q b ϕ and Definition 3. This concludes the proof of Theorem 1 .

5 Completeness

In this section we prove completeness of our logical system. This result is stated and proven in the end of the section as Theorem 2. We start by specifying a canonical model 〈V, T, ⊩〉 using "unraveling" technique [Sahlqvist, 1975].

Definition 4 Let set V be the set of all sequences

1. n ≥ 0,
2. Xi is a maximal consistent subset of Φ for each i ≥ 0,
3. ¬[ai]pi bi ψi ∈ Xi-1 for each i ≥ 1,
4. ¬ψi ∈ Xi for each i ≥ 1,
5. {χ | [ai]pi bi χ ∈ Xi-1} ⊆ Xi.

It is helpful to think about the sequences in set V as paths in an infinite collection of infinite trees, see Figure 9, whose nodes are maximal consistent sets of formulas and whose edges are labeled by tuples (a, b, p, ψ).

By hd(v) we mean the last element of any non-empty sequence v. In particular, hd(v) = Xn if

By α :: β we mean the concatenation of sequences α and β. In particular, if α is sequence

We are now ready to define the set of of transitions of the canonical model.

...

...

Definition 5 Let T be the set

For example, in the setting depicted in Figure 9, set T contains tuples

. . .

Definition 6 v ⊩ P if P ∈ hd(v).

This concludes the definition of the model 〈V, T,⊩〉. The next two lemmas are auxiliary statements that are used in the proof of the core Lemma 4.

Lemma 2 For any consistent set X, if ¬[c]qdσ ∈ X, then set {¬σ} ∪ {τ | [c]qd τ ∈ X} is consistent.

Proof. Suppose the opposite. Thus, τ1, . . . , τn ⊢ σ for some [c]qd τ1, . . . , [c]qd τn ∈ X. Hence, by the deduction theorem in the propositional logic, ⊢ τ1 → (τ2 → . . . (τn → σ) . . . ). Then, ⊢ [c]qd (τ1 → (τ2 → . . . (τn → σ) . . . )) by Necessitation rule. Thus, ⊢ [c]qd τ1 → [c]qd (τ2 → . . . (τn → σ) . . . ))

by Distributivity axiom and Modus Ponens inference rule. Hence, X ⊢ [c]qd (τ2 → . . . (τn → σ) . . . )) due to the assumption [c]qd τ1 ∈ X. Then, X ⊢ [c]qdσ by repeating the last two steps n - 1 times. The last statement implies inconsistency of the set X due to the assumption ¬[c]qdσ ∈ X of the lemma. ⊠

Lemma 3 For any sequence (v0, b1, c, p1, v1), (v1, b2, c, p2, v2), . . . , (vn-1, bn, c, pn, vn) ∈ T, any d ≥ 0, and any q ≥ -d such that

1. ∑ni=1 pi ≥ q,

if [c]qdσ ∈ hd(v0), then σ ∈ hd(vn).

Proof. We prove this statement by induction on n. If n = 0, then condition 2 of the lemma implies that 0 ≥ q. Thus, q ≤ 0. Hence ⊢ [c]qdσ → σ by Reflexivity axiom. Then, assumption [c]qdσ ∈ hd(v0) implies hd(v0) ⊢ σ by Modus Ponens inference rule. Therefore, σ ∈ hd(v0) due to maximality of the set hd(v0).

Suppose now that n > 0. Note that d + p1 + · · · + pn-1 ≥ bn ≥ 0 by the third assumption of the lemma and Definition 1. Hence, assumption [c]qdσ ∈ hd(v0) by Transitivity axiom implies that hd(v0) ⊢ [c]p1+···+pn-1 d [c]q-p1-···-pn-1 d+p1+···+pn-1 σ. Thus, [c]p1+···+pn-1 d [c]q-p1-···-pn-1 d+p1+···+pn-1 σ ∈ hd(v0) due to maximality of the set hd(v0). Then, by the induction hypothesis, [c]q-p1-···-pn-1 d+p1+···+pn-1 σ ∈ hd(vn-1). Condition 2 of the lemma implies q - p1 - · · · - pn-1 ≤ pn. Thus, by Lemma 1,

Condition 3 of the lemma implies that d+p1+· · ·+pn ≥ bn. Hence, by Monotonicity axiom, hd(vn-1) ⊢ [c]pn bn σ. Thus, [c]pn bn σ ∈ hd(vn-1) due to the maximality of the set hd(vn-1). Therefore, σ ∈ hd(vn) by condition 5 of Definition 4. ⊠

Proof. We prove this lemma by induction on structural complexity of formula ϕ. If formula ϕ is a propositional variable, then the required follows from Definition 6. The cases when formula ϕ is a negation or an implication follow from Definition 3 and the assumption of maximality and consistency of the set hd(v) in the standard way. Assume now that formula ϕ has the form [a]pb ψ.

(⇒) Suppose that [a]pb ψ /∈ hd(v). Thus, ¬[a]pb ψ ∈ hd(v) due to the maximality of the set hd(v). Hence, by Lemma 2, set {¬ψ} ∪ {χ | [a]pb χ ∈ hd(v)} is consistent. Let Y be any maximal consistent extension of this set. Thus, v :: 〈(a, b, p, ψ), Y 〉 ∈ S by Definition 4. Note that ¬ψ ∈ Y . Hence, ψ /∈ Y due to the consistency of set Y . Thus,

by the induction hypothesis. Finally, note that by Definition 5,

Therefore, v ⊮ [a]pb ψ by Definition 3.

(⇐) Let [a]pb ψ ∈ hd(v). By Definition 3, it suffices to show that vn ⊩ ψ for any sequence of tuples (v0, b1, c, p1, v1), (v1, b2, c, p2, v2), . . . , (vn-1, bn, c, pn, vn) ∈ T such that

1. n ≥ 0,
2. v0 = v,
3. ∑ni=1 pi ≥ q,

Indeed, ψ ∈ hd(vn) by Lemma 3. Therefore, vn ⊩ ψ by the induction hypothesis. ⊠

Note that to prove part (⇒) above we need to construct a state v′ reachable from state v such that ϕ /∈ hd(v′ ). Although Definition 3 only requires that such state v′ is reachable through a sequence of transitions in our case state v′ = v :: 〈(a, b, p, ψ), Y 〉 is reachable through a single move.

We are now ready to state and to prove the main result of this paper - a completeness theorem for our logical system.

Theorem 2 (completeness) Let ϕ ∈ Φ. If v ⊩ ϕ for every state v ∈ V of every model 〈V, T, ⊩〉, then ⊢ ϕ.

Proof. Suppose that ⊬ ϕ. Let X0 be a maximal consistent subset of Φ containing formula ¬ϕ. Let 〈V, T,⊩〉 be the defined above canonical model and v be the single-element sequence 〈X0〉. Thus, ¬ϕ ∈ X0 = hd(v). Hence, ϕ /∈ hd(v) due to X being a consistent set. Therefore, v ⊮ ϕ by Lemma 4. ⊠

6 Conclusion

In this paper we proposed a logical system for reasoning about budget-constrained transition systems. Our contribution here is twofold: on one hand we have proposed the notion of a budget-constrained transition system and a novel modal language that incorporates two types of budget constraints: profit constraint and budget constraint. On the other hand, we have described a sound and complete logical system that captures all universal principles expressible through this modality. The logical system, through its Transitivity axiom, captures a dependency between the two constraints.

Although throughout the paper we have assumed that the budget is constrained by a non-negative real number, we believe that our work could be modified to allow for infinite value of the budget subscript in the modality. In this extended language modality w ⊩ [a]p∞ϕ would mean that statement ϕ is true at any state reachable from state w by agent a with profit p and no restriction on the budget. In case when value of b is ∞, we can also allow the value of superscript p to be -∞ without violating our constraint -b ≤ p.

Another possible extension of this work is to consider modality [C]pb , where set C ⊆ A represents a coalition of agents working together. This extension would require a significant modification not only to the axiomatic system and the proof of its completeness, but also to the definition of the budget-constrained transition system. Such modifications could follow the approach of [Alechina et al., 2011].