=Paper=
{{Paper
|id=Vol-1113/paper7
|storemode=property
|title=Logics for Non-Cooperative Games with Expectations
|pdfUrl=https://ceur-ws.org/Vol-1113/paper7.pdf
|volume=Vol-1113
|dblpUrl=https://dblp.org/rec/conf/eumas/GodoM13
}}
==Logics for Non-Cooperative Games with Expectations==
https://ceur-ws.org/Vol-1113/paper7.pdf
Logics for Non-Cooperative Games with
Expectations
Lluı́s Godo1 , Enrico Marchioni2
1
IIIA, Artificial Intelligence Research Institute
CSIC, Spanish National Research Council
Campus de la Univ. Autònoma de Barcelona s/n
08193 Bellaterra, Spain
Email: godo@iiia.csic.es
2
Institut de Recherche en Informatique de Toulouse
Université Paul Sabatier, 118 Route de Narbonne
31062 Toulouse, France
Email: enrico.marchioni@irit.fr
Abstract. We introduce the logics E(G) for reasoning about probabilis-
tic expectation over classes G of games with discrete polynomial payoff
functions represented by finite-valued Lukasiewicz formulas and provide
completeness and complexity results. In addition, we introduce a new
class of games where players’ expected payoff functions are encoded by
E(G)-formulas. In these games each player’s aim is to randomise her
strategic choices in order to affect the other players’ expectations over
an outcome as well as their own. We offer a logical and computational
characterisation of this new class of games.
1 Introduction
In this work, we introduce the logics E(G) for reasoning about probabilistic
expectation over classes G of games with discrete polynomial payoff functions
represented by finite-valued Lukasiewicz formulas. This type of games, called
Lukasiewicz games [14], is a generalisation of Boolean games [1, 12] and involves a
finite set of players P = {P1 , . . . , Pn }, each controlling a finite set of propositional
variables Vi , so that the sets Vi are mutually disjoint. Being in control of a set
Vi of propositional variables means that Pi assigns to the variables in Vi values
from the scale
1 k−1
Lk = 0, , . . . , ,1 .
k k
A strategy for a player Pi is a function s : Vi → Lk that corresponds to a
valuation of the variables controlled by Pi . Strategies can be interpreted as efforts
or costs, and each player’s strategic choice can be seen as an assignment to each
controlled variable carrying an intrinsic cost.
Each player is assigned
Sn a finite-valued Lukasiewicz formula ϕi , with proposi-
tional variables from i Vi , whose valuation is interpreted as the payoff function
for Pi and corresponds to the restriction over Lk of a continuous piecewise linear
polynomial function with integer coefficients. Notice that not all variables in ϕi
might be under Pi ’s control and, consequently, Pi ’s payoff from playing a certain
strategy (i.e. choosing a certain variable assignment) also depends on the choices
made by (some of) the other players.
In this work, we expand Lukasiewicz games by providing an explicit definition
of a class G of games, and also defining suitable concepts of a mixed strategy, best
response and Nash Equilibrium, adapted to this framework. Then, we define a
probabilistic logic E(G) over many-valued formulas (of finite-valued Lukasiewicz
logic) to reason about expectations in a class G of Lukasiewicz games. This
might be in principle a bit surprising since probabilities are not the same as ex-
pectations, but the reason is simple. The generalisation of a classical probability
measure on Boolean algebras to the algebraic setting of MV-algebras [3] (the
algebraic counterpart of Lukasiewicz logics) corresponds to the so-called states
[16], which can be seen as averages of truth-values. Indeed, a state (or finitely-
additive probability) σ over the set of Lukasiewicz logic formulas L (built from
a given set of propositional variables V ) is a mapping σ : L → [0, 1] such that:
– σ(1) = 1,
– σ(ϕ ⊕ ψ) = σ(ϕ) + σ(ψ), if ¬(ϕ&ψ) is a Lukasiewicz tautology,
– σ(ϕ) = σ(ψ), if ϕ ↔ ψ is a Lukasiewicz tautology.
When we consider only finite-valued Lukasiewicz logics Lk , as proved in [18],
a mapping σ : L → [0, 1] is a state on formulas iff there exists a probability
distribution π : Ωk → [0, 1] on the set of Lk -valuations Ωk on L such that
X
σ(ϕ) = p(w) · w(ϕ).
w∈Ωk
The state σ(ϕ) corresponds to a weighted average of the truth-values of ϕ under
all possible valuations, and it can also be regarded as the expected value of the
function fϕ : Ωk → [0, 1], defined as fϕ (w) = w(ϕ) for all w ∈ Ωk . If we look
at Lukasiewicz formulas as a particular class of functions, to reason about the
probability of these formulas amounts to reasoning about the expectation of the
corresponding functions. This is the view we take in this paper.
Note that a logic, called F P (Ln , L), to reason about the probability of Lk -
formulas was defined and axiomatised in [6]. The logic E(G) introduced here is
a (partially) syntactical and semantic expansion of F P (Ln , L), and its expres-
sive power makes it possible to represent expectations in games where players’
payoffs are given by discrete polynomial functions with integer coefficients over
Lk (encoded by finite-valued Lukasiewicz formulas).
E(G) is built from a set of non-modal formulas ϕ, ψ, . . . that correspond
to formulas of the finite-valued Lukasiewicz logic Lck (with additional truth con-
stants for each element c ∈ Lk ), and a set of modal formulas Eϕ, Eψ, . . . to repre-
sent the expectation associated to each ϕ, ψ, . . . . Modal formulas are combined
with the connectives of the LΠ 21 -logic [5], which makes it possible to express
combinations of polynomial equalities and inequalities with rational coefficients.
Based on the logics E(G), we also introduce a new class of games, called
Lukasiewicz games with expectations, that generalise Lukasiewicz games. In the
situations of strategic interactions modelled in Game Theory, the goal of each
player is essentially the maximisation of her own expected payoff. Players, how-
ever, often care not only about maximising their own expectation, but also about
influencing other players’ expected outcomes. Lukasiewicz games with expecta-
tions offer a formalisation of these kinds of strategic interactions where each
player’s aim is to randomise her strategic choices in order to affect the other play-
ers’ expectations over an outcome as well as their own expectation. Lukasiewicz
games with expectations expand Lukasiewicz games by assigning to each player
Pi a modal formula Φi of E(G), whose interpretation corresponds to a piecewise
rational polynomial function whose variables are interpreted as expected val-
ues. The modal formula Φi assigned to each player is then meant to represent a
player’s goal concerning the relation between her and other players’ expectations.
This work is organised as follows.1 The next section introduces the basic
background notions about Lukasiewicz logics and the LΠ 12 -logic. In Section 3,
we present the main definition of a Lukasiewicz game, define the concept of a
class G of games and build the logics E(G) to represent expectations in each G.
We provide both completeness and complexity results for E(G). In Section 4,
we introduce games with expectations based on E(G) and offer some examples
along with a logical and computational characterisation. We end with some final
remarks.
2 Logical Background
The language of Lukasiewicz logic L (see [3]) is built from a countable set of
propositional variables {p1 , p2 , . . .}, the binary connective → and the truth con-
stant 0 (for falsity). Further connectives are defined as follows:
¬ϕ is ϕ → 0̄, ϕ ∧ ψ is ϕ&(ϕ → ψ),
ϕ&ψ is ¬(ϕ → ¬ψ), ϕ ∨ ψ is ((ϕ → ψ) → ψ),
ϕ ⊕ ψ is ¬(¬ϕ&¬ψ), ϕ ↔ ψ is (ϕ → ψ)&(ψ → ϕ),
ϕ ψ is ϕ&¬ψ, d(ϕ, ψ) is ¬(ϕ ↔ ψ).
Let Form denote the set of Lukasiewicz logic formulas. A valuation e from
Form into [0, 1] is a mapping e : Form → [0, 1] assigning to all propositional
variables a value from the real unit interval (with e(0) = 0) that can be extended
to complex formulas as follows:
e(ϕ → ψ) = min(1 − e(ϕ) + e(ψ), 1) e(¬ϕ) = 1 − e(ϕ)
e(ϕ&ψ) = max(0, e(ϕ) + e(ψ) − 1) e(ϕ ⊕ ψ) = min(1, e(ϕ) + e(ψ))
e(ϕ ψ) = max(0, e(ϕ) − e(ψ)) e(ϕ ∧ ψ) = min(e(ϕ), e(ψ))
e(ϕ ∨ ψ) = max(e(ϕ), e(ψ)) e(d(ϕ, ψ)) = |e(ϕ) − e(ψ)|
e(ϕ ↔ ψ) = 1 − |e(ϕ) − e(ψ)|
1
Notice that the proofs of the main results are either simply sketched or omitted due
to space constraints.
A valuation e satisfies a formula ϕ if e(ϕ) = 1. As usual, a set of formulas is
called a theory. A valuation e satisfies a theory T , if e(ψ) = 1, for every ψ ∈ T .
Infinite-valued Lukasiewicz logic has the following axiomatisation:
(L1) ϕ → (ψ → ϕ), (L2) (ϕ → ψ) → ((ψ → χ) → (ϕ → χ)),
(L3) (¬ϕ → ¬ψ) → (ψ → ϕ), (L4) ((ϕ → ψ) → ψ) → ((ψ → ϕ) → ϕ).
The only inference rule is modus ponens, i.e.: from ϕ → ψ and ϕ derive ψ.
A proof in L is a sequence ϕ1 , . . . , ϕn of formulas such that each ϕi either is
an axiom of L or follows from some preceding ϕj , ϕk (j, k < i) by modus ponens.
We say that a formula ϕ can be derived from a theory T , denoted as T ` ϕ, if
there is a proof of ϕ from a set T 0 ⊆ T . A theory T is said to be consistent if
T 6` 0.
Lukasiewicz logic is complete with respect to deductions from finite theories
for the given semantics, i.e.: for every finite theory T and every formula ϕ, T ` ϕ
iff every valuation e that satisfies T also satisfies ϕ.
For each k ∈ N, the finite-valued Lukasiewicz logic Lk is the schematic ex-
tension of L with the axiom schemas:
(L5) (n − 1)ϕ ↔ nϕ, (L6) (kϕk−1 )n ↔ nϕk ,
for each integer k = 2, . . . , n − 2 that does not divide n − 1, and where nϕ is an
abbreviation for ϕ ⊕ · · · ⊕ ϕ (n times) and ϕk is an abbreviation for ϕ& . . . &ϕ,
(k times). The notions of valuation and satisfiability for Lk are defined as above
just replacing [0, 1] by
1 k−1
Lk = 0, , . . . , ,1
k k
as set of truth values. Every Lk is complete with respect to deductions from
finite theories for the given semantics.
It is sometimes useful to introduce constants in addition to 0 that will denote
values in the domain Lk . Specifically, we will denote by Lck the Lukasiewicz logic
obtained by adding constants c for every value c ∈ Lk . We assume that valuation
functions e interpret such constants in the natural way: e(c) = c.
A McNaughton function [3] is a continuous piecewise linear polynomial func-
tions with integer coefficients over the nth-cube [0, 1]n . To each Lukasiewicz
formula ϕ(p1 , . . . , pn ) we can associate a McNaughton function fϕ so that, for
every valuation e
fϕ (e(p1 ), . . . , e(pn )) = e(ϕ(p1 , . . . , pn )).
Every L-formula is then said to define a McNaughton function. The converse is
also true, i.e. every continuous piecewise linear polynomial function with integer
coefficients over [0, 1]n is definable by a formula in Lukasiewicz logic. In the case
of finite-valued Lukasiewicz logics, the functions defined by formulas are just the
restrictions of McNaughton functions over (Lk )n . In this sense, we can associate
to every formula ϕ(p1 , . . . , pn ) from Lk a function fϕ : (Lk )n → Lk . As for
each Lck , the functions defined by a formula are combinations of restrictions of
McNaughton functions and, in addition, the constant functions for each c ∈ Lk .
The class of functions definable by Lck -formulas exactly coincides with the class
of all functions f : (Lk )n → Lk , for every n ≥ 0.
The expressive power of infinite-valued Lukasiewicz logic lies in, and is limited
to, the definability of piecewise linear polynomial functions. Expanding L with
the connectives , →Π of Product logic [10], interpreted as the product of reals
and as the truncated division, respectively, significantly augments the expressive
power of the logic. The LΠ 12 logic [5] is the result of this expansion, obtained by
adding the connectives , →Π , 12 , whose valuations e extend the valuations for
L as follows:
(
1 e(ϕ) ≤ e(ψ)
e(ϕ ψ) = e(ϕ) · e(ψ) e(ϕ →Π ψ) = e(ψ)
otherwise
eϕ
1 e(ϕ) = 1
1 1
e 2 = 2 e(∆ϕ) =
0 otherwise
Notice that the presence of the constant 12 makes it possible to define constants
for all rationals in [0, 1] (see [5]). LΠ 12 ’s axioms include the axioms of Lukasiewicz
and Product logics (see [10]) as well as the following additional axioms, where
∆ϕ is ¬ϕ →Π 0:
(LΠ1) (ϕ ψ) (ϕ χ) ↔ ϕ (ψ χ),
(LΠ2) ∆(ϕ → ψ) → (ϕ →Π ψ),
(LΠ3) ∆(ϕ →Π ψ) → (ϕ → ψ),
(LΠ4) 12 ↔ ¬ 12 .
The deduction rules are modus ponens for & and →, and the necessitation rule
for ∆, i.e.: from ϕ derive ∆ϕ. LΠ 12 is complete with respect to deductions from
finite theories for the given semantics [5].
While L is the logic of McNaughton functions, LΠ 21 is the logic of piecewise
rational functions with integer coefficients over [0, 1]n (see [15]). In fact, the
function defined by each LΠ 21 -formula corresponds to a supremum of rational
fractions
P (x1 , . . . , xn )
Q(x1 , . . . , xn )
over [0, 1]n , where P (x1 , . . . , xn ), Q(x1 , . . . , xn ) are polynomials with rational co-
efficients. Conversely, every piecewise rational function with rational coefficients
over the unit cube [0, 1]n can be defined by an LΠ 21 -formula.
3 Logics for Representing Expectation
In this section we first introduce the concept of a Lukasiewicz game on Lck along
with the notion of a class G of Lukasiewicz games. Then, we define the logic
E(G) to represent expected payoffs for games in G, and provide completeness
and complexity results.
3.1 Lukasiewicz Games
A Lukasiewicz game G on Lck [14] is a tuple
G = hP, V, {Vi }, {Si }, {ϕi }i
where:
1. P = {P1 , . . . , Pn } is a set of players;
2. V = {p1 , . . . , pm } is a finite set of propositional variables;
3. For each i ∈ {1, . . . , n}, Vi ⊆ V is the set of propositional variables under
control of player Pi , so that the sets Vi form a partition of V, |Vi | = mi , and
P n
i=1 mi = m.
4. For each i ∈ {1, . . . , n}, Si is the strategy set for player Pi that includes all
valuations s : Vi → Lk of the propositional variables in Vi , i.e.
Si = {s | s : Vi → Lk }.
5. For each i ∈ {1, . . . , n}, ϕi (p1 , . . . , pt ) is an Lck -formula, built from variables
in V, whose associated function
fϕi : (Lk )t → Lk
corresponds to the payoff function of Pi , and whose value is determined by
the valuations in {S1 , . . . , Sn }.
We denote by S = S1 × · · · × Sn the product of the strategy spaces. A
tuple s = (s1 , . . . , sn ) ∈ S of strategies is called a strategy combination. s−i
denotes the tuple of strategies (s1 , . . . , si−1 , si+1 , . . . , sn ) not including si . Aside
from s, we use the form (si , s−i ) do denote a strategy combination. With an
abuse of notation, we denote by fϕi (si , s−i ) (or, equivalently, fϕi (s)) the value
of the payoff function fϕi under the valuation corresponding to the strategy
combination (si , s−i ) [or, equivalently, s].2
Given a game G, let
δ : P → {1, . . . , m}
be a function assigning to each player Pi an integer from {1, . . . , m} that corre-
sponds to the number of variables in Vi : i.e.:
δ(Pi ) = mi .
δ is called a variable distribution function. Given a game G, the type of G is the
triple hn, m, δi, where n is the number of players, m is the number of variables
in V, and δ is the variable distribution function for G.
2
fϕi (si , s−i ) can be also seen as the value of e(ϕi ), when e coincides with the valuation
s.
Definition 1 (Class). Let G and G 0 be two Lukasiewicz games G and G 0 on Lck
of type hn, m, δi and hn, m, δ 0 i, respectively. We say that G and G 0 belong to the
same class G if there exists a permutation of the indices {1, . . . , n} such that,
for all Pi ,
δ(P(i) ) = δ 0 (Pi ).
Notice that what matters in the definition of a type is not which players are as-
signed certain variables, but rather their distribution. For instance, take two
games G and G 0 all having three players P1 , P2 , P3 and the same variables
p1 , . . . , p6 . Suppose that, in G, P1 controls p1 , P2 controls p2 , p3 , and P3 con-
trols p4 , p5 , p6 , while in G 0 , P2 controls p3 , P3 controls p4 , p5 , and P1 controls
p1 , p2 , p6 . G and G 0 have the same type, since they have the same number of
players, the same number of variables, and the permutation , where
1 7−→ 2 2 7−→ 3 3 7−→ 1,
is such that δ P(i) = δ 0 (Pi ) for all Pi .
Given the above definitions, we can adapt some well-known game-theoretic
concepts to this settings. We introduce the notion of mixed strategy in order to
define the concept of expected payoff along with the notions of best response
and equilibrium.
Let G = hP, V, {Vi }, {Si }, {ϕi }i be a Lukasiewicz game on Lck . A mixed strat-
egy πi for player Pi is a probability distribution on the strategy space Si . By
π−i , we denote the tuple of mixed strategies (π1 , . . . , πi−1 , πi+1 , . . . , πn ).
Given a tuple (π1 , . . . , πn ) of mixed strategies for P1 , . . . , Pn , respectively,
the expected payoff for Pi of playing πi , when P−i play π−i , is given by
X Yn
expϕi (πi , π−i ) = πj (sj ) · fϕi (s)
s=(s1 ,...,sn )∈S j=1
Let Σi denote the set of mixed strategies of Pi . Pi ’s best response to P−i ’s
mixed strategy combination π−i is a mixed strategy πi such that, for all strategies
πi0 ∈ Σi :
expϕi (πi , π−i ) ≥ expϕi (πi0 , π−i ).
Definition 2 (Nash Equilibrium). Let G be a Lukasiewicz game on Lck . We
call a tuple of mixed strategies (π1∗ , . . . , πn∗ ) a Nash Equilibrium for G if each
player’s mixed strategy πi∗ is a best response to the other players’ mixed strategy
∗
combination π−i .
Example: Matching Pennies. The following game is a generalisation of Match-
ing Pennies3 , a classic example of a zero-sum game without a pure strategy equi-
librium. In the original game, two players P1 and P2 both have a penny and must
secretly choose to turn it to head or tails and reveal their choice at the same
3
The idea behind this generalisation comes from [13].
time. If their choices agree, P1 takes both pennies, but if they do not match, P2
is the one winning both.
Now, imagine that both players have a dice with n + 1 faces, they both
choose one and reveal it at the same time. P1 ’s overall strategy is to be as
close as possible to P2 ’s choice, who, instead, wants to keep the greater possible
distance between the outcomes. Clearly, we can represent each player’s strategy
space with the set Lk . P1 ’s payoff function is given by the formula ¬d(p1 , p2 ),
whose associated function is 1−|e(p1 )−e(p2 )|, while P2 ’s payoff is defined by the
formula d(p1 , p2 ), which corresponds to the function |e(p1 ) − e(p2 )|. The game
is formally defined on Lck as follows:
G= {P1 , P2 }, {p1 , p2 }, {p1 }1 , {p2 }2 , {s1 : {p1 } → Lk }, {s2 : {p2 } → Lk }, {¬d(p1 , p2 ), d(p1 , p2 )} .
Table 1 shows the payoff matrix for this generalised version of Matching Pennies
with k = 5 (the values in each cell correspond to the first and second player
payoffs under the valuation to the variables p1 , p2 ).
By Nash’s Theorem [17], we know that an equilibrium with mixed strategies
always exists for the generalised version of Matching Pennies.
P2
0 1/5 2/5 3/5 4/5 1
0 1, 0 4/5, 1/5 3/5, 2/5 2/5, 3/5 1/5, 4/5 0, 1
1/5 4/5, 1/5 1, 0 4/5, 1/5 3/5, 2/5 2/5, 3/5 1/5, 4/5
2/5 3/5, 2/5 4/5, 1/5 1, 0 4/5, 1/5 3/5, 2/5 2/5, 3/5
P1
3/5 2/5, 3/5 3/5, 2/5 4/5, 1/5 1, 0 4/5, 1/5 3/5, 2/5
4/5 1/5, 4/5 2/5, 3/5 3/5, 2/5 4/5, 1/5 1, 0 4/5, 1/5
1 0, 1 1/5, 4/5 2/5, 3/5 3/5, 2/5 4/5, 1/5 1, 0
Table 1. Generalised Matching Pennies.
3.2 The Logic E(G)
The aim of this section is to introduce the logic E(G) for reasoning about ex-
pected utility in games with Lukasiewicz strategies. Notice that, while sometimes
we refer to E(G) as “a logic”, we are actually defining a whole family of logics,
one for each class G.
Syntax The construction of E(G) mimics the one provided for logics for reason-
ing about uncertainty in [7]. The syntax of E(G) is built by taking the m-variable
fragment mLck 4 of Lck as inner logic and LΠ 21 as outer logic. Its language is defined
as follows:
1. The set NModF of non-modal formulas corresponds to the set of mLck -
formulas built from the propositional variables p1 , . . . , pm .
2. The set ModF of modal formulas is built from the atomic modal formulas
Eϕ, with ϕ ∈ NModF, using the LΠ 12 connectives. Eϕ is meant to encode
a player’s expected payoff from playing a mixed strategy, given the payoff
function associated to ϕ. Nested modalities are not allowed.
Semantics Given a class of games G on mLck , a model M for E(G) is a tuple
hS, e, {πi }i, such that:
1. S is the set of all strategy combinations {s = (s1 , . . . , sn ) | (s1 , . . . , sn ) ∈
S1 × · · · × Sn }.
2. e : (NModF × S) → Lk is a valuation of non-modal formulas, such that, for
each ϕ ∈ NModF
e(ϕ, s) = fϕ (s),
where fϕ is the function associated to ϕ and s = (s1 , . . . , sn ).
3. πi : Si → [0, 1] is a probability distribution, for each Pi .
Given a formula Φ, the truth value of Φ in M at the combination s, denoted
kΦkM,s , is inductively defined as follows:
1. If Φ is a non-modal formula ϕ ∈ NModF, then
kϕkM,s = e(ϕ, s),
2. If Φ is an atomic modal formula Eϕ, then
X n
Y
kEϕkM,s = expϕ (π1 , . . . , πn ) = πj (sj ) · e(ϕ, s) .5
s=(s1 ,...,sn )∈S j=1
3. If Φ is a non-atomic modal formula, its truth value is computed by evalu-
ating its atomic modal subformulas and then by using the truth functions
associated to the LΠ 12 -connectives occurring in Φ.
4
Notice that the functions definable in mLck are exactly all the functions f : (Lk )t →
Lk , where t ≤ m.
5
Notice that the notation is slightly different from the one used above for the definition
of expected payoff but the meaning is the same.
Since the valuation of a modal formula Φ does not depend on a specific
strategy combination but only on the model M, we will often simply write kΦkM
to denote the valuation of Φ in M. As usual, we say that a formula Φ is satisfiable
if there exists a model M such that kΦkM = 1. Similarly, a modal theory Γ , i.e. a
set of modal formulas, is satisfiable if there exists a model that satisfies each and
every one of the formulas contained in Γ . Validity clearly means satisfiability in
all models.
Axiomatisation The axioms of E(G) are the following:
1. All the Lck -tautologies for mLck , i.e.: all the Lck -tautologies in the variables
p1 , . . . , pm , for non-modal formulas.
2. All the LΠ 12 -axioms and rules for modal formulas.
3. Probabilistic axioms for E, with ϕ, ψ, r ∈ NModF:
(a) E(¬ϕ) ↔ ¬Eϕ
(b) E(ϕ ⊕ ψ) ↔ [(Eϕ → E(ϕ&ψ)) → Eψ]
(c) Er ↔ r
4. Independence axioms for E, where p1i , . . . , pmi is the tuple of variables as-
signed to Pi , for all tuples r11 , . . . , rm1 , . . . , r1n , . . . , rmn ∈ (Lk )m :
V V Jn Vmi
n mi
(a) E i=1 ji =1i (∆ (p ji ↔ r ji )) ↔ i=1 E ji =1i ∆ (p ji ↔ r ji )
5. The following inference rules for E, with ϕ, ψ ∈ NModF:
(a) Necessitation: from ϕ derive Eϕ
(b) Monotonicity: from ϕ → ψ derive Eϕ → Eψ
Notice that each
mi
^
(†) (∆ (pji ↔ rji ))
ji =1i
encodes a particular strategy for player Pi . In fact, each ∆ (pji ↔ rji ) is satisfi-
able if and only if e(pji ) = rji . So, given a tuple r1i , . . . , rmi , (†) is satisfiable by
a strategy si if and only if si (pji ) 7−→ rji , for all pji .
The notion of proof in E(G) is defined as usual. For any modal theory Γ and
formula ϕ, we write
Γ `E(G) ϕ
to denote that ϕ is a consequence of Γ in E(G).
Completeness Before we prove completeness for E(G) we provide an axiomatic
characterisation for the expectation of mixed strategies over mLck -formulas.
Theorem 1. Let G be a class of Lukasiewicz games on Lck and let mLck be the
m-variable fragment of Lck . The following statements are equivalent:
1. There exists a state
σ : mLck → [0, 1].
such that for all tuples r11 , . . . , rm1 , . . . , r1n , . . . , rmn ∈ (Lk )m
n
^ mi
^ Yn mi
^
σ (∆ (pji ↔ rji )) = σ ∆ (pji ↔ rji ) ,
i=1 ji =1i i=1 ji =1i
where p1i , . . . , pmi is the tuple of variables assigned to Pi .
2. There exists a probability distribution
πi : Si → [0, 1]
for each Pi , such that, for all ϕ ∈ mLck , σ(ϕ) = expϕ (π1 , . . . , πn ), i.e.:
X Yn
σ(ϕ) = πj (sj ) · fϕ (s) ,
s=(s1 ,...,sn )∈S j=1
where fϕ is the function associated to ϕ.
Proof. It is easy to check that (2) implies (1).
To prove the converse, suppose that there exists a state
σ : mLck → [0, 1].
As shown by Paris in [18, Appendix 2] there exists a probability distribution
π : S1 × · · · × Sn → [0, 1] such that
X
σ(ϕ) = π(s) · fϕ (s),
s∈S
for all ϕ ∈ mLck .
Now, let mi Lck [pi ] be the mi -variable fragment of Lck in the variables pi =
{p1i , . . . , pmi }, i.e. the variables assigned to Pi . Let σ↓i be the restrictions of σ to
mi Lck [pi ]. It is clear that each σ↓i is still a probability measure. It follows, again,
from [18, Appendix 2] that, for each i, there exists a probability distribution
πi : Si → [0, 1]
such that, for all ψ ∈ mi Lck [pi ]
X
σ(ψ) = σ↓1 (ψ) = πi (si ) · fψ (si ).
si ∈Si
By assumption, σ satisfies
n
^ mi
^ n
Y mi
^
σ (∆ (pji ↔ rji )) = σ ∆ (pji ↔ rji ) ,
i=1 ji =1i i=1 ji =1i
for all tuples r11 , . . . , rm1 , . . . , r1n , . . . , rmn ∈ (Lk )m .
It is possible to check that the above condition guarantees the fact that all
probability distributions πi are independent, and so for all s ∈ S
n
Y
π(s) = πi (si ).
i=1
Therefore
X X n
Y
σ(ϕ) = π(s) · fϕ (s) = πj (sj ) · fϕ (s) .
s∈S s=(s1 ,...,sn )∈S j=1
We can now proceed to proving the Completeness Theorem.
Theorem 2 (Completeness). Let Γ and Φ be a finite modal theory and a
modal formula in E(G). Then, Γ `E(G) Φ if and only if for every model M such
that, for each Ψ ∈ Γ , kΨ kM = 1, also kΦkM = 1.
Proof. The proof follows from an adaptation of the strategy laid out in [10] and
generalised in [7].
We now study the computational complexity of certain kinds of satisfiability
problems for E(G). Let r ∈ Q ∩ [0, 1] and let [ ∈ {<, >, ≤, ≥, =}. We call an
E(G)-modal formula Φ [r-satisfiable if there is a model M such that
kΦkM [r.
Following a strategy similar to the one laid out by Hájek in [11] for probability
logics, satisfiability of an E(G)-formula Φ can be translated into an existential
formula in the theory of the reals whose size is exponential in the number of
non-modal propositional variables in Φ. Decidability for the existential theory
of the reals Th∃ (R) was shown by Canny to be in PSPACE [2]. Therefore, we
obtain the following result:
Theorem 3. Checking [r-satisfiability for E(G) is in EXPSPACE.
4 Games with Expectations
In this section we introduce a class of games with polynomial constraints over ex-
pectations. These games expand Lukasiewicz games by assigning to each player
a formula of E(G), which is a piecewise rational polynomial function whose vari-
ables correspond to expected values. The idea is that in a situation of strategic
interaction players might be interested not only in maximizing their own ex-
pectation, but also in influencing others’. The modal formula assigned to each
player is then meant to represent a player’s goal concerning the relation between
her and other players’ expectations.
A game with expectations EG on E(G) is a tuple
EG = hP, V, {Vi }, {Si }, {ϕi }, {Mi }, {Φi }i,
where:
1. G = hP, V, {Vi }, {Si }, {ϕi }i is a Lukasiewicz game on Lck , with G ∈ G,
2. for each i ∈ {1, . . . , n}, Mi is the set of all mixed strategies on Si of player
Pi ,
3. for each i ∈ {1, . . . , n}, Φi is an E(G)-formula such that every atomic modal
formula occurring in Φi has the form Eψ, with ψ ∈ {ϕ1 , . . . , ϕn }.
Let EG be a game with expectations on E(G). A model M = hS, e, {πi }i for
E(G) is called a best response model for a player Pi whenever, for all models
M0 = hS, e, {πi0 }i with π−i
0
= π−i ,
kΦi kM0 ≤ kΦi kM .
Definition 3 (Equilibrium). A game with expectations EG on E(G) is said
to have a Nash Equilibrium, whenever there exists a model M∗ that is a best
response model for each player Pi .
Example 1. Let EG be any game with expectations where each Pi is simply
assigned the formula Φi := Eϕi . This game corresponds to the the situation
where each player cares only about her own expectation and whose goal is its
maximisation. Clearly, by Nash’s Theorem [17], every EG of this form admits an
Equilibrium, since it offers a formalisation of the classical case where equilibria
are given by tuples of mixed strategies over valuations in a Lukasiewicz game.
Example 2. Not every game with expectations has an equilibrium. In fact,
consider the following game
EG = hP, V, {Vi }, {Si }, {ϕi }, {Mi }, {Φi }i,
with i ∈ {1, 2}, where:
1. ϕ1 := p1 and ϕ2 := p2 , and
2. Φ1 := ¬d(E(p1 ), E(p2 )) and Φ2 := d(E(p1 ), E(p2 )).
The above game can be regarded as a particular version of Matching Pennies
with expectations. In fact, while P1 aims at matching P2 ’s expectation, P2 ’s goal
is quite the opposite, since she wants their expectations to be as far as possible.
It is easy to see that there is no model M that gives an equilibrium for EG .
Proposition 1. There exist games with expectations on E(G) that do not admit
a Nash Equilibrum.
As mentioned above, the satisfiability of every E(G)-formula can be trans-
lated into the validity of an existential formula of the theory Th(R) of real closed
fields. In a similar way, we can express the existence of an equilibrium in a game
with expectations EG through a first-order sentence ξ of Th(R) having exponen-
tially many variables and a fixed alternation of quantifiers. By using the fact that
the general decidability problem for Th(R) is singly exponential in the number of
variables when the alternation of quantifiers is fixed [8], we obtain the following
result.
Theorem 4 (Complexity). Checking the existence of a Nash Equilibrium in
a game with expectations EG on E(G) is in 2-EXPTIME.
By exploiting the connection between LΠ 21 and real closed fields it is also
possible to express the existence of an equilibrium through an LΠ 12 -formula (see
[4]). Therefore, we obtain the following logical characterisation.
Theorem 5. For every game with expectations EG on E(G) there exists an LΠ 12 -
formula φ such that EG admits a Nash Equilibrium if and only if φ is satisfiable.
5 Final Remarks
In this work, we presented a logic E(G) for reasoning about expectations in a
class G of Lukasiewicz games. We have also introduced a new class of games
based on E(G) that expand Lukasiewicz games. These games capture strategic
interactions in which players randomise their choices in order to influence the
expectations of the other players as well as their own.
While our approach to representing expectation in games in a logical frame-
work is certainly novel, other works have dealt with similar topics. In [9], Halpern
and Pucella introduced a propositional logic for reasoning about probabilistic ex-
pectation. Their work, though, is mainly concerned with modelling expectation
in general and not in a game-theoretic setting. Certainly closer to our paper is
the work by Sack and van der Hoek [19], where the authors study a modal logic
to reason about mixed strategies in games. Although (each instance of) their
logic is based on a fixed game and a fixed set of mixed strategies, it makes it
possible to represent the concept of a Nash Equilibrium through logical formulas:
a feature that is not possible in our logic.
In our future work, we plan to extend the logical study of expectation for
Lukasiewicz games to those situations where payoff formulas are functions de-
fined over the whole unit cube [0, 1]n , and, consequently, players have an infinite
strategy space.
Acknowledgments
Godo acknowledges support from the Spanish projects EdeTRI (TIN2012-39348-
C02-01) and AT (CONSOLIDER CSD 2007-0022). Marchioni acknowledges sup-
port from the Marie Curie Project NAAMSI (FP7-PEOPLE-2011-IEF).
References
1. E. Bonzon, M.C. Lagasquie-Schiex, J. Lang, B. Zanuttini. Boolean games revisited.
In Proceedings of the Seventeenth European Conference on Artificial Intelligence
(ECAI-2006), Riva del Garda, Italy, 265–269, 2006.
2. J.F. Canny. Some algebraic and geometric computations in PSPACE. In Proceedings
of the 20th ACM Symposium on Theory of Computing, 460–467, 1988.
3. R. Cignoli, I. M. L. D’Ottaviano, D. Mundici. Algebraic Foundations of Many-alued
Reasoning, Volume 7 of Trends in Logic, Kluwer Academic Publishers, Dordrecht,
2000.
4. F. Esteva, L. Godo, E. Marchioni. Fuzzy logics with enriched language. In Handbook
of Mathematical Fuzzy Logic, Cintula P., Hájek P., and Noguera C. (Editors), College
Publications, 627–712, 2011.
5. F. Esteva, L. Godo, F. Montagna. The LΠ and LΠ 21 logics: two complete fuzzy
logics joining Lukasiewicz and product logic. Archive for Mathematical Logic, 40:
39–67, 2001.
6. T. Flaminio, L. Godo. A logic for reasoning about the probability of fuzzy events.
Fuzzy Sets and Systems, 158: 625–638, 2007.
7. T. Flaminio, L. Godo, E. Marchioni. Reasoning about uncertainty of fuzzy events:
an overview. In Reasoning under Vagueness - Logical, Philosophical, and Linguistic
Perspectives, Cintula P., Fermüller C., Godo L., Hájek P. (Editors), Studies in Logic,
College Publications, 367–400, 2011.
8. D. Y. Grigor’ev. Complexity of deciding Tarski algebra. Journal of Symbolic Com-
putation, 5: 65–108, 1988.
9. J.Y. Halpern, R. Pucella. Characterizing and reasoning about probabilistic and non-
probabilistic expectation. Journal of the ACM, Article No. 15, 54(3), 2007.
10. P. Hájek Metamathematics of Fuzzy Logic. Volume 4 of Trends in Logic, Kluwer
Academic Publishers, Dordrecht, 1998.
11. P. Hájek. Complexity of fuzzy probability logics II. Fuzzy Sets and Systems,
158(23): 2605–2611, 2007.
12. P. Harrenstein, W. van der Hoek, J.J.Ch. Meyer, C. Witteveen. Boolean games.
In Proceeding of the Eighth Conference on Theoretical Aspects of Rationality and
Knowledge (TARK VIII), J. van Benthem (Ed.), Siena, Italy, 287–298, 2001.
13. T. Kroupa, O. Majer. Nash Equilibria in a class of constant-sum games represented
by McNaughton functions. In Logic, Algebra and Truth Degrees 2012, Book of
Abstracts, K. Terui and N. Preining (Eds.), 2012.
14. E. Marchioni, M. Wooldridge. Lukasiewicz Games. Submitted.
15. F. Montagna, G. Panti. Adding structures to MV-algebras. Journal of Pure and
Applied Algebra, 164: 365–387, 2001.
16. D. Mundici, Averaging the truth-value in Lukasiewicz logic. Studia Logica 55(1):
113–127, 1995.
17. J. Nash. Non-cooperative games. The Annals of Mathematics, Second Series, 54(2):
286–295, 1951.
18. J. B. Paris. A note on the Dutch Book method (revised version). In Second Interna-
tional Symposium on Imprecise Probability and their Application, Cornell University,
Ithaca, NY (USA), 2001.
19. J. Sack, W. van der Hoek. A Modal Logic for Mixed Strategies. Studia Logica,
accepted.