The aim of the paper is to consider a game-theoretic properties of strategies available to players in dialogue games. We treat speech acts formulated in a dialogue as moves in a dialogue game and rules for their appropriateness as rules of this game. We would like to analyze dialogical systems as a Nash-style games, and explore verification possibilities for some properties of such games e.g. dominant strategies and Nash equilibrium. Since automatic verification of such games could be of high complexity, we consider a model checking approach, which is commonly applied method allowing for verification of different systems and their properties. This method is based on solutions, which are trying to deal with the state explosion problem.
Formal dialogue systems study players’ decisions during the communication process.
To specify such a system, we typically use such elements as protocol, locution and
commitment rules, which allow us to define legal moves in a particular type of
dialogue game. Some of these systems examine dialogue types that satisfy certain
constraints, e.g. prohibition of fallacies (see e.g. [
The application of the game-theoretic approach to dialogue system modelling consists of three steps: the selected dialogue system needs to be expressed in game-theoretic notions, it must then be supplemented with the specification of the system’s properties, such as players’ preferences or payoffs, which are necessary for exploiting gametheoretic tools (DC needed to be expanded to include the following elements: (1) a goal for the dialogue, (2) termination and outcome rules; and (3) players’ preferences), and finally system must be studied in solutions for the DC system in view of players goals.
We shall assume that the reader is familiar with the basic concepts of the game
theory like dominant strategy, Nash equilibrium, sets of strategies, etc. (these notions
were presented in a more detailed way in [
The purpose of our current research is to propose a model checking technique to
verify communication protocols used by autonomous agents interacting using dialogue
games. For modelling strategies we are going to use a variant of the logic of actions and
graded beliefs A G n [
The model is a game in extensive form, formalizing the DC argumentation system
created by Mackenzie [
Given a set S , the set of all finite sequences over S is denoted by S and the set of all infinite sequences over S is denoted by S w . The empty sequence is denoted by e and the operation of concatenation is denoted by . Given sets A and B, C A, D B, and a function f : A ! B, symbols !f (C), !f 1(D) will denote the image and inverse image of f . The preliminary step of defining the game is to specify the following parameters of the game: the set of statements, the set of locutions and the relation of immediate consequence on the set of statements.
Let S0 be a non-empty and countable set called the set of atomic statements. The set of statements, S[S0], is a minimal set such that: – S0 S. – If s 2 S, then :s 2 S. (Negation) – If T S, then V T 2 S. (Conjunction) – If s; t 2 S, then s ! t 2 S. (Conditional)
The set of locutions, L[S0], is then defined as follows: L[S0] = S[S0] [ fQs : s 2 S[S0]g [ fWs : s 2 S[S0]g [ fYs : s 2 S[S0]g [ fRs : s 2 S[S0]g; where Q (question), W (withdrawal), Y (challenge), and R (resolution demand) are operators used for locution construction.
A relation of immediate consequence, 7! 2S[S0] 2S[S0] is a binary relation on the set of statements such that for all s; t 2 S, fs; s ! tg 7! ftg.
Given a set of atomic statements, S0, and a relation of immediate consequence, 7!, the (argumentation) game is a tuple G[S0;7!] = hP; p; H; T; (-i)i2P; (Ai)i2P; (ai)i2Pi where – P = fW; Bg is the set of players. – H L[S0] [ L[S0]w is the set of histories. A history is a (finite or infinite) sequence of locutions from L[S0]. The set of finite histories in H is denoted by H¯ . – p : H¯ ! P [ f?g is the player function assigning to each finite history the player who moves after it, or ?, if no player is to move. The set of histories at which player i 2 P is to move is Hi = !p 1(i). – T = !p 1(?) [ (H \ L[S0]w ) is the set of terminal histories. A terminal history is a history after which no player is to move, hence it consists of the set of finite histories mapped to ? by the player function and the set of all infinite histories. – -i T T is the preference relation of player i defined on the set of terminal histories.6 – Ai = L[S0] is the set of actions of player i 2 P. – ai : Hi ! 2Ai is the admissible actions function of player i 2 P, determining the set of actions that i can choose from after history h 2 Hi.
In what follows, we will assume that the set of atomic statements S0 is fixed and omit it, writing S rather than S[S0] and L rather than L[S0]. We are defining the properties of the player function for DC system: p(h) 2 fW?g if jhj is even and p(h) 2 fB; ?g if jhj is odd. Additionally, the rules of dialogue place restrictions on when the game can terminate: if p(h l) = ?, then l 2= fQs; Ys; Rsg. The remaining specification of game termination depends on the context in which the dialogue system is used, as discussed below.
The admissible actions function of the players is determined by the rules of
dialogue. In the case of the DC system, the rules of dialogue are defined using the notion
of players’ commitment sets. The commitment set function of player i is a function
Ci : L ! L, assigning to each finite sequence of locutions h 2 L the commitment set
Ci(h) of i at h. The commitment set function of i 2 P is defined inductively at follows
(where, given i 2 P, f ig = P n fig). The details of the definition of the commitment
set function are presented in [
The set of immediate consequence conditionals ICC = fV T ! s : T 7! fsgg. A set
of statements, T S, is immediately inconsistent if there exists a finite subset T 0 T
and a statement s such that :s 2 T 0 and T 0 7! fsg. For more details, see [
The details of the definition of the admissible actions function ai of player i 2 P are
presented in [
The set of histories, H, is the maximal set of sequences from L [ Lw satisfying the following: – e 2 H. – For any h1 h2 2 H with h1 2 L and h2 2 L [ Lw , h1 2 H.
– For any h1 s h2 2 H with h1 2 L , h2 2 L [ Lw and s 2 L, s 2 ap(h1)(h1). Two elements of the dialogue modelling game remain to define. These are player preferences and the termination rules that describe which finite histories are mapped to ?.
Note that every strategy profile S¯ = (SW; SB) determines a unique terminal history hS¯ such that for each strategy s 2 SW [ SB, finite history h0 2 H¯ and history h00 2 H with hS¯ = h0 a h00, a = Sp(h0)(h0). Player i 2 P prefers strategy profile S¯ to strategy profile S¯0, S¯0 -i S¯, if hS¯0 -i hS¯. Thus to define players’ preferences, we need to specify their preferences on terminal histories and the next section is intended to illustrate how this can be defined. 2.2
Persuasion dialogues are dialogues aimed at resolving conflicts of opinion between at
least two participants [21]. In this paper we restrict our attention to two participants
games. A conflict of opinion is with regard to a statement, t 2 S, called a topic. The
proponent holds a positive view on t, the opponent doubts t. According to [21], the
conflict is resolved if all players have the same point of view. If the dialogue ends,
either one of the players is the winner of the dialogue (in which case the other player is
the loser), or the dialogue ends in a tie, in which case neither of the players is a winner
or a loser. If the dialogue does not end, then neither of the players is a winner or a
loser. We consider a particular type of persuasion dialogue, called pure persuasion, as
described in [
By combining the DC system with pure persuasion we can complete the definition of the argumentation game G as follows. The first mover, player W, is the proponent and the second mover, player B, is the opponent. According to the description above, the game should end if one of the following happens: (i) The commitment sets of both players contain the topic t, or (ii) neither player’s commitment set contains the topic t. Since, according to the rules of DC system the most recent statements of any player are added to the commitment sets of both players, we adjust these rules of termination by allowing the next mover to respond and withdraw these statements from his set of commitments. If he is unable to do so, the game will terminate after his move. Similarly, if at any point in the game neither player’s commitment set contains t, the next mover has the opportunity to add t to at least one of the commitment sets. If he is unable to do so, the game terminates after his move. Formally, this amounts to a definition of finite terminal histories, which are defined as follows. A finite history h 2 H¯ is terminal, i.e. p (h) = ?, if one of the following conditions is satisfied:
Tprop : jhj is even and t 2 CW(h) \ CB(h), Topp : jhj is odd and t 2= CW(h) [ CB(h).
Note that in the DC system the set of admissible actions at each non-terminal history is non-empty. Therefore a finite history can be terminal only if one of the above conditions is satisfied.
Having defined finite terminal histories we will now define the preferences of the players. Let HWwin denote the set of finite histories for which condition Tprop is satisfied and let Hwin denote the set of finite histories for which condition Topp is satisfied. Set
B HWwin contains the terminal histories at which player W, the proponent, is the winner, and set Hwin contains the terminal histories at which player W, the opponent, is the
B winner.
We assume the following preference relation on terminal histories. Given h1; h2 2 T , h1 -W h2 if h2 2 HWwin or h2 2= Hwin and h1 2 Hwin; and
B B h1 -B h2 if h2 2 Hwin or h2 2= HWwin and h1 2 HWwin:
B
The above means that each player prefers a terminal history at which he wins to that at which he does not win, and each player prefers a history at which the opponent does not win to one at which the opponent wins.
These preferences of the players and termination rules imply that a rational proponent (player W) should start with an action that results in the topic t being added to the commitment set of at least one of the players.
The similar analysis can be done for the second type of persuasive dialogue, i.e.,
a conflict resolution dialogue, in which both participants attempt to reach an outcome
whereby either both of them have the topic t in their commitment sets or both have the
negation of the topic, :t, in their commitment sets [
A strategy of a player i is a function from player i’s histories to the set of actions Si : Hi ! L, such that for all h 2 Hi, Si(h) 2 ai(h). Thus a strategy is a contingent plan that determines a player’s move at each of his histories. The set of strategies of player i is denoted by Si. A strategy profile S¯ = (Si; S i) is a pair of strategies chosen by each of the players, S¯ 2 Si S i. Solution concepts define sets of strategy profiles which represent stable outcomes of the game. Below we define two basic solution concepts and illustrate them in the context of pure persuasion.
A strategy Si is dominant for player i if for all Si0 2 Si and all S j 2 S j with j = i, (Si0; S j) -i (Si; S j): A strategy is strictly dominant if the property above holds with strict inequality. A strategy profile S¯ = (Si; S i) is a solution in (strictly) dominant strategies iff Si is dominant for player i and S i is dominant for player i.7
A strategy profile S¯ = (Si; S i) is a Nash equilibrium if for all i 2 P and for all Si0 2 Si,
(Si0; S i) -i (Si; S i):
Note that if the game has a solution in dominant strategies, then it also has a Nash equilibrium (but the reverse is not necessarily true).
3.2
Consider a game G[S0;7!] defined for some set of atomic statements S0 and a relation of immediate consequence 7!. Suppose that players’ preferences and finite terminal histories are defined as for a persuasive dialogue.
Let us assume first that the topic, t, is an immediate consequence conditional, t 2 ICC. Consider a strategy s1 2 SW such that s1(e) = t. Note that after history h = t the commitment sets of both players contain t and the opponent cannot remove t from the commitment set of either of the players, because t 2 ICC, . The game ends in two rounds and the outcome most preferred by player W is achieved. Thus, any s1 as described above is a dominant strategy of the proponent. Moreover, for any s2 2 SB, the outcome of the game from strategy profile s¯ = (s1; s2) is the same: the commitment sets of proponent and opponent contain t. Changing a strategy does not guarantee to any player that he can obtain a strictly preferred outcome. Hence, s¯ is a Nash equilibrium of the game and leads to an outcome whereby the proponent wins.
Next, let us consider the case that the topic, t, is not an immediate consequence conditional, t 2= ICC. Let s2 2 SB be a strategy such that for any non-terminal history h with t 2 CW(h) \ CB(h) and jhj odd, s2(h) = Wt. In this case Wt 2 aB(h), because the last action of h must have been t. On the other hand, let s1 2 SW be a strategy such that for any non-terminal history h with t 2= CW(h) [CB(h), s1(h) = t. Note that the strategy profile s¯ = (s1; s2) is a Nash equilibrium of the game. This occurs because changing strategy does not give any of the players his most preferred outcome. Note that this equilibrium results in an infinite history.
The detailed solutions to conflict resolution dialogue with the DC system was
presented in [
In order to recall the illustration of the results from [
We assume the set of atomic statements to be such that fp; q; r; tg S0, where p means that they should go to the ballet, q means that they should go to the soccer match, r means that Wilma is too sick for the outdoors, and t means that Brian’s ex-wife will be at the ballet. Moreover, fq ! :p; p ! :q; r ! :q; t ! :pg 7!. This game has a topic p. Wilma is the proponent of p and Brian is the opponent of p.
Let us consider the strategy profile s0 = (s01; s02) where s01 is a strategy of Wilma’s in which she states p and r as soon as it is possible and s02 is a strategy of Brian’s in which he states q as soon as it is possible, never attacking Wilma’s statement by r stating t. More formally, s1 is a strategy such that (a) s1(e) = p and (b) for any nonterminal history h, if r 2 aW(h) then s1(h) = r, while s2 is a strategy such that for any non-terminal history h, (a) if q 2 aB(h) then s2(h) = q, and (b) if h = h0 r h00 then s2(h) 6= t. A play in line with this strategy profile is given in Table 1.
This play begins with the Wilma’s statement that they should go to the ballet. Brian withdraws this statement from his commitment set. Next, Wilma states that she is too sick for the outdoors. Brian replies that they should go to the soccer match. Then Wilma states that they cannot go to the soccer match since she is too sick. So, Brian asks for a resolution of the conflict. Wilma then withdraws her statement that they should go to the soccer match. Brian, not wanting to put his wife at risk, also gives up the idea of going to the soccer match. Then Wilma repeats her statement that they should go to the ballet and finally Brian agrees, i.e. he makes no move removing p from his commitment set. The strategy profile s0 = (s01; s02) described above is a Nash equilibrium of the game (i.e. no player wants to change his/her strategy, assuming that the other player does not) and it achieves Wilma’s most preferred outcome. 4
In this paper, we continue the study how existing dialogue systems can be formalized
in terms of game theory and we take Mackenzie’s DC argumentation system as a
representation of such a game. Furthermore, we analyze the obtained results how solutions
in dominant strategies and solutions in a Nash equilibrium can be used for the analysis
of dialogue games. We consider a model checking approach as a verification mean for
these properties, since automatic verification of these games is connected with excessive
complexity. Model checking is commonly applied method allowing for verification of
different systems and their properties and there are also some solutions applied within
model checking, which are trying to deal with the state explosion problem. The solution
in our case is software system using this approach which allows to examine selected
dialogue game systems with respect to game-theory properties, by semantically verifying
satisfaction of formulas of the A G n language which describe considered properties in a
given model. We will adopt A G n logic proposed by Budzynska and Kacprzak [