We introduce the logics E(G) for reasoning about probabilistic expectation over classes G of games with discrete polynomial payo functions represented by nite-valued Lukasiewicz formulas and provide completeness and complexity results. In addition, we introduce a new class of games where players' expected payo functions are encoded by E(G)-formulas. In these games each player's aim is to randomise her strategic choices in order to a ect the other players' expectations over an outcome as well as their own. We o er a logical and computational characterisation of this new class of games.
In this work, we introduce the logics E(G) for reasoning about probabilistic
expectation over classes G of games with discrete polynomial payo functions
represented by nite-valued Lukasiewicz formulas. This type of games, called
Lukasiewicz games [
Lk =
1 0; ; : : : ; k k
1 k ; 1 : 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 e orts 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 a nite-valued Lukasiewicz formula 'i, with propositional variables from Sin Vi, whose valuation is interpreted as the payo function for Pi and corresponds to the restriction over Lk of a continuous piecewise linear polynomial function with integer coe cients. Notice that not all variables in 'i might be under Pi's control and, consequently, Pi's payo 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 de nition
of a class G of games, and also de ning suitable concepts of a mixed strategy, best
response and Nash Equilibrium, adapted to this framework. Then, we de ne a
probabilistic logic E(G) over many-valued formulas (of nite-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
expectations, but the reason is simple. The generalisation of a classical probability
measure on Boolean algebras to the algebraic setting of MV-algebras [
When we consider only nite-valued Lukasiewicz logics Lk, as proved in [
Note that a logic, called F P (Ln; L), to reason about the probability of
Lkformulas was de ned and axiomatised in [
E(G) is built from a set of non-modal formulas '; ; : : : that correspond
to formulas of the nite-valued Lukasiewicz logic Lck (with additional truth
constants for each element c 2 Lk), and a set of modal formulas E'; E ; : : : to
represent the expectation associated to each '; ; : : : . Modal formulas are combined
with the connectives of the L 21 -logic [
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 payo . Players, however, often care not only about maximising their own expectation, but also about in uencing other players' expected outcomes. Lukasiewicz games with expectations o er a formalisation of these kinds of strategic interactions where each player's aim is to randomise her strategic choices in order to a ect the other players' 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 values. 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 de nition of a Lukasiewicz game, de ne 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 o er some examples along with a logical and computational characterisation. We end with some nal remarks. 2
The language of Lukasiewicz logic L (see [
:' 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('& ) = max(0; e(') + e( ) 1) e(' ) = max(0; e(') e( )) e(' _ ) = max(e('); e( )) e(' $ ) = 1 je(') e( )j e(:') = 1 e(') e(' ) = min(1; e(') + e( )) e(' ^ ) = min(e('); e( )) e(d('; )) = je(') e( )j 1 Notice that the proofs of the main results are either simply sketched or omitted due to space constraints.
A valuation e satis es a formula ' if e(') = 1. As usual, a set of formulas is called a theory. A valuation e satis es a theory T , if e( ) = 1, for every 2 T .
In nite-valued Lukasiewicz logic has the following axiomatisation: (L1) ' ! ( ! '), (L3) (:' ! : ) ! (
(L2) (' ! ! '), (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 nite theories for the given semantics, i.e.: for every nite theory T and every formula ', T ` ' i every valuation e that satis es T also satis es '.
For each k 2 N, the nite-valued Lukasiewicz logic Lk is the schematic extension 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 satis ability for Lk are de ned as above just replacing [0; 1] by
Lk = as set of truth values. Every Lk is complete with respect to deductions from nite theories for the given semantics.
It is sometimes useful to introduce constants in addition to 0 that will denote values in the domain Lk. Speci cally, we will denote by Lck the Lukasiewicz logic obtained by adding constants c for every value c 2 Lk. We assume that valuation functions e interpret such constants in the natural way: e(c) = c.
A McNaughton function [
f'(e(p1); : : : ; e(pn)) = e('(p1; : : : ; pn)): Every L-formula is then said to de ne a McNaughton function. The converse is also true, i.e. every continuous piecewise linear polynomial function with integer coe cients over [0; 1]n is de nable by a formula in Lukasiewicz logic. In the case of nite-valued Lukasiewicz logics, the functions de ned by formulas are just the restrictions of McNaughton functions over (Lk)n. In this sense, we can associate adding the connectives ; ! L as follows: to every formula '(p1; : : : ; pn) from Lk a function f' : (Lk)n ! Lk. As for each Lck, the functions de ned by a formula are combinations of restrictions of McNaughton functions and, in addition, the constant functions for each c 2 Lk. The class of functions de nable by Lck-formulas exactly coincides with the class of all functions f : (Lk)n ! Lk, for every n 0.
The expressive power of in nite-valued Lukasiewicz logic lies in, and is limited
to, the de nability of piecewise linear polynomial functions. Expanding L with
the connectives ; ! of Product logic [
2 e(' ) = e(') e( ) e(' !
) =
The deduction rules are modus ponens for & and !, and the necessitation rule
for , i.e.: from ' derive '. L 21 is complete with respect to deductions from
nite theories for the given semantics [
While L is the logic of McNaughton functions, L 12 is the logic of piecewise
rational functions with integer coe cients over [0; 1]n (see [
P (x1; : : : ; xn)
Q(x1; : : : ; xn) over [0; 1]n, where P (x1; : : : ; xn); Q(x1; : : : ; xn) are polynomials with rational coe cients. Conversely, every piecewise rational function with rational coe cients over the unit cube [0; 1]n can be de ned by an L 12 -formula. 3
In this section we rst introduce the concept of a Lukasiewicz game on Lck along with the notion of a class G of Lukasiewicz games. Then, we de ne the logic E(G) to represent expected payo s for games in G, and provide completeness and complexity results. 3.1
Lukasiewicz Games
A Lukasiewicz game G on Lck [
G = hP; V; fVig; fSig; f'igi 1. P = fP1; : : : ; Png is a set of players; 2. V = fp1; : : : ; pmg is a nite set of propositional variables; 3. For each i 2 f1; : : : ; ng, Vi V is the set of propositional variables under control of player Pi, so that the sets Vi form a partition of V, jVij = mi, and Pn
i=1 mi = m. 4. For each i 2 f1; : : : ; ng, Si is the strategy set for player Pi that includes all valuations s : Vi ! Lk of the propositional variables in Vi, i.e.
Si = fs j s : Vi ! Lkg: 5. For each i 2 f1; : : : ; ng, 'i(p1; : : : ; pt) is an Lck-formula, built from variables in V, whose associated function
f'i : (Lk)t ! Lk corresponds to the payo function of Pi, and whose value is determined by the valuations in fS1; : : : ; Sng.
We denote by S = S1 Sn the product of the strategy spaces. A tuple s = (s1; : : : ; sn) 2 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 payo function f'i under the valuation corresponding to the strategy combination (si; s i) [or, equivalently, s].2
Given a game G, let be a function assigning to each player Pi an integer from f1; : : : ; mg that corresponds to the number of variables in Vi: i.e.: : P ! f1; : : : ; mg
(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.
De nition 1 (Class). Let G and G0 be two Lukasiewicz games G and G0 on Lck of type hn; m; i and hn; m; 0i, respectively. We say that G and G0 belong to the same class G if there exists a permutation | of the indices f1; : : : ; ng such that, for all Pi,
(P|(i)) = 0(Pi): Notice that what matters in the de nition of a type is not which players are assigned certain variables, but rather their distribution. For instance, take two games G and G0 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 controls p4; p5; p6, while in G0, P2 controls p3, P3 controls p4; p5, and P1 controls p1; p2; p6. G and G0 have the same type, since they have the same number of players, the same number of variables, and the permutation |, where is such that P|(i) = 0 (Pi) for all Pi.
Given the above de nitions, we can adapt some well-known game-theoretic concepts to this settings. We introduce the notion of mixed strategy in order to de ne the concept of expected payo along with the notions of best response and equilibrium.
Let G = hP; V; fVig; fSig; f'igi be a Lukasiewicz game on Lck. A mixed strategy 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 payo for Pi of playing i, when P i play i, is given by exp'i ( i; i) =
X
1 f'i (s)A De nition 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
Matching Pennies3, a classic example of a zero-sum game without a pure strategy
equilibrium. 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 [
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 payo function is given by the formula :d(p1; p2), whose associated function is 1 je(p1) e(p2)j, while P2's payo is de ned by the formula d(p1; p2), which corresponds to the function je(p1) e(p2)j. The game is formally de ned on Lck as follows: The aim of this section is to introduce the logic E(G) for reasoning about expected utility in games with Lukasiewicz strategies. Notice that, while sometimes we refer to E(G) as \a logic", we are actually de ning a whole family of logics, one for each class G.
Syntax The construction of E(G) mimics the one provided for logics for
reasoning about uncertainty in [
Semantics Given a class of games G on mLck, a model M for E(G) is a tuple hS; e; f igi, such that: 1. S is the set of all strategy combinations fs = (s1; : : : ; sn) j (s1; : : : ; sn) 2
S1 Sng. 2. e : (NModF S) ! Lk is a valuation of non-modal formulas, such that, for each ' 2 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 k kM;s, is inductively de ned as follows: 1. If
is a non-modal formula ' 2 NModF, then 2. If is an atomic modal formula E', then k'kM;s = e('; s);
in M at the combination s, denoted kE'kM;s = exp'( 1; : : : ; n) =
X
1 e('; s)A :5 3. If is a non-atomic modal formula, its truth value is computed by evaluating its atomic modal subformulas and then by using the truth functions associated to the L 21 -connectives occurring in . 4 Notice that the functions de nable in mLck are exactly all the functions f : (Lk)t !
Lk, where t m. 5 Notice that the notation is slightly di erent from the one used above for the de nition of expected payo but the meaning is the same.
Since the valuation of a modal formula does not depend on a speci c 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 satis able if there exists a model M such that k kM = 1. Similarly, a modal theory , i.e. a set of modal formulas, is satis able if there exists a model that satis es each and every one of the formulas contained in . Validity clearly means satis ability 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 2 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 assigned to Pi, for all tuples r11 ; : : : ; rm1 ; : : : ; r1n ; : : : ; rmn 2 (Lk)m: (a) E
Vin=1
Vmi ji=1i ( (pji $ rji )) $
Jn i=1 E
Vmi ji=1i (pji $ rji )
2 NModF: (a) Necessitation: from ' derive E' (b) Monotonicity: from ' ! derive E' ! E Notice that each mi ^ ji=1i (y)
( (pji $ rji )) encodes a particular strategy for player Pi. In fact, each (pji $ rji ) is satis able if and only if e(pji ) = rji . So, given a tuple r1i ; : : : ; rmi , (y) is satis able by a strategy si if and only if si(pji ) 7 ! rji , for all pji .
The notion of proof in E(G) is de ned as usual. For any modal theory formula ', we write and `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 c m-variable fragment of Lk. The following statements are equivalent: 1. There exists a state
: mLck ! [0; 1]: such that for all tuples r11 ; : : : ; rm1 ; : : : ; r1n ; : : : ; rmn 2 (Lk)m 0 n 0 mi 11 n 0 @ ^ ^ ( (pji $ rji ))AA = Y 0 mi
^ (pji $ rji )AA ; where p1i ; : : : ; pmi is the tuple of variables assigned to Pi. 2. There exists a probability distribution for each Pi, such that, for all ' 2 mLck, (') = exp'( 1; : : : ; n), i.e.: i : Si ! [0; 1] (') =
X
1 f'(s)A ; where f' is the function associated to '.
To prove the converse, suppose that there exists a state As shown by Paris in [18, Appendix 2] there exists a probability distribution : S1 Sn ! [0; 1] such that
: mLck ! [0; 1]: (') = X (s) f'(s);
s2S for all ' 2 mLck.
Now, let miLck[pi] be the mi-variable fragment of Lck in the variables pi = fp1i ; : : : ; pmi g, i.e. the variables assigned to Pi. Let #i be the restrictions of to miLck[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 such that, for all
2 miLck[pi] By assumption, satis es ( ) = #1( ) = X i(si) f (si): i : Si ! [0; 1] si2Si
i=1 (pji $ rji )AA ; for all tuples r11 ; : : : ; rm1 ; : : : ; r1n ; : : : ; rmn 2 (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 2 S n (s) = Y i(si):
i=1
(') = X (s) f'(s) =
X s2S s=(s1;:::;sn)2S j=1 We can now proceed to proving the Completeness Theorem.
1 f'(s)A : Theorem 2 (Completeness). Let and be a nite modal theory and a modal formula in E(G). Then, `E(G) if and only if for every model M such that, for each 2 , k kM = 1, also k kM = 1.
Proof. The proof follows from an adaptation of the strategy laid out in [
We now study the computational complexity of certain kinds of satis ability
problems for E(G). Let r 2 Q \ [0; 1] and let [ 2 f<; >; ; ; =g. We call an
E(G)-modal formula [r-satis able if there is a model M such that
k kM[r:
Following a strategy similar to the one laid out by Hajek in [
In this section we introduce a class of games with polynomial constraints over expectations. These games expand Lukasiewicz games by assigning to each player a formula of E(G), which is a piecewise rational polynomial function whose variables correspond to expected values. The idea is that in a situation of strategic interaction players might be interested not only in maximizing their own expectation, but also in in uencing 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; fVig; fSig; f'ig; fMig; f igi;
Let EG be a game with expectations on E(G). A model M = hS; e; f igi for E(G) is called a best response model for a player Pi whenever, for all models M0 = hS; e; f i0gi with 0 i = i, k ikM0 k ikM: De nition 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 [
EG = hP; V; fVig; fSig; f'ig; fMig; f igi; with i 2 f1; 2g, 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 satis ability of every E(G)-formula can be
translated into the validity of an existential formula of the theory Th(R) of real closed
elds. In a similar way, we can express the existence of an equilibrium in a game
with expectations EG through a rst-order sentence of Th(R) having
exponentially many variables and a xed alternation of quanti ers. By using the fact that
the general decidability problem for Th(R) is singly exponential in the number of
variables when the alternation of quanti ers is xed [
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 12 and real closed elds it is also
possible to express the existence of an equilibrium through an L 21 -formula (see
[
Theorem 5. For every game with expectations EG on E(G) there exists an L 21 formula such that EG admits a Nash Equilibrium if and only if is satis able. 5
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 in uence the expectations of the other players as well as their own.
While our approach to representing expectation in games in a logical
framework is certainly novel, other works have dealt with similar topics. In [
In our future work, we plan to extend the logical study of expectation for Lukasiewicz games to those situations where payo formulas are functions dened over the whole unit cube [0; 1]n, and, consequently, players have an in nite strategy space.
Godo acknowledges support from the Spanish projects EdeTRI (TIN2012-39348C02-01) and AT (CONSOLIDER CSD 2007-0022). Marchioni acknowledges support from the Marie Curie Project NAAMSI (FP7-PEOPLE-2011-IEF).