Introduction

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. [7,12,22]), the others concentrate on the requirements that dialogical communication must serve specific goals, such as persuasion, negotiation, information-seeking, inquiry, and so on (see e.g. [21,14,18,19,8,1]). Even though strategies in games get a lot of attention [5,6,11,17,24,1,4,9], only a few works try to combine a game-theoretic approach with dialogue games [15,20,13,16,10]. In these approaches is emphasized that we can investigate not only whether the participants behave correctly (according to the rules of the game) but also whether they behave successfully (according to the goals of the player). We continue the study presented in [10] in which strategy (consistent with given protocol) should be chosen so that the result of the dialogue will be most advantageous and rational for a given player. The method of such application using Mackenzie's DC system was presented in this paper.

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 [10]). The concept of solution defines sets of strategy profiles which represent stable outcomes of the game. We focus on two types of solutions which determine the rules for playing a specific game: dominant strategies and Nash equilibrium. Given a selected specification of DC (e.g. player preferences), if there exists a solution in dominant strategies, then it provides the rules of how to play a DC game in order to win regardless of the moves of the opponent. However, if such a solution does not exist, but there is a Nash equilibrium for this game, then the player's victory is not certain, but the Nash equilibrium gives rules on how to play rationally.

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 [2]. Whereas, for verification of properties of dialogue games we plan to apply methods and techniques explored in the software tool Perseus [3].

The game-theoretic framework 2.1 The model

The model is a game in extensive form, formalizing the DC argumentation system created by Mackenzie [12]. To define the model we use the following standard notation.

Given a set Σ , the set of all finite sequences over Σ is denoted by Σ * and the set of all infinite sequences over Σ is denoted by Σ ω . The empty sequence is denoted by ε 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 S 0 be a non-empty and countable set called the set of atomic statements. The set of statements, S[S 0 ], is a minimal set such that:

-S 0 ⊆ S. -If s ∈ S, then ¬s ∈ S. (Negation) -If T ⊆ S, then T ∈ S. (Conjunction) -If s,t ∈ S, then s → t ∈ S. (Conditional)

The set of locutions, L[S 0 ], is then defined as follows:

L[S 0 ] = S[S 0 ] ∪ {Qs : s ∈ S[S 0 ]} ∪ {Ws : s ∈ S[S 0 ]} ∪ {Ys : s ∈ S[S 0 ]} ∪ {Rs : s ∈ S[S 0 ]},

where Q (question), W (withdrawal), Y (challenge), and R (resolution demand) are operators used for locution construction.

A relation of immediate consequence, →⊆ 2 S[S 0 ] × 2 S[S 0 ] is a binary relation on the set of statements such that for all s,t ∈ S, {s, s → t} → {t}.

Given a set of atomic statements, S 0 , and a relation of immediate consequence, →, the (argumentation) game is a tuple Γ [S 0 , →] = P, π, H, T, ( i ) i∈P , (A i ) i∈P , (α i ) i∈P where

-P = {W, B} is the set of players. -H ⊆ L[S 0 ] * ∪ L[S 0 ] ω is the set of histories. AH i = − → π −1 (i). -T = − → π −1 (∅) ∪ (H ∩ L[S 0 ] ω )

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 -A i = L[S 0 ] is the set of actions of player i ∈ P. -α i : H i → 2 A i

is the admissible actions function of player i ∈ P, determining the set of actions that i can choose from after history h ∈ H i .

In what follows, we will assume that the set of atomic statements S 0 is fixed and omit it, writing S rather than S[S 0 ] and L rather than L[S 0 ]. We are defining the properties of the player function for DC system: π(h) ∈ {W∅} if |h| is even and π(h) ∈ {B, ∅} if |h| is odd. Additionally, the rules of dialogue place restrictions on when the game can terminate: if π(h • l) = ∅, then l / ∈ {Qs, Ys, Rs}. 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 C i : L * → L, assigning to each finite sequence of locutions h ∈ L * the commitment set C i (h) of i at h. The commitment set function of i ∈ P is defined inductively at follows (where, given i ∈ P, {−i} = P \ {i}). The details of the definition of the commitment set function are presented in [10].

The set of immediate consequence conditionals ICC = { T → s : T → {s}}. A set of statements, T ⊆ S, is immediately inconsistent if there exists a finite subset T ⊆ T and a statement s such that ¬s ∈ T and T → {s}. For more details, see [12].

The details of the definition of the admissible actions function α i of player i ∈ P are presented in [10].

The set of histories, H, is the maximal set of sequences from L * ∪ L ω satisfying the following:

-ε ∈ H. -For any h 1 • h 2 ∈ H with h 1 ∈ L * and h 2 ∈ L * ∪ L ω , h 1 ∈ H. -For any h 1 • s • h 2 ∈ H with h 1 ∈ L * , h 2 ∈ L * ∪ L ω and s ∈ L, s ∈ α π(h 1 ) (h 1 ).

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 = (S W , S B ) determines a unique terminal history h S such that for each strategy s ∈ S W ∪ S B , finite history h ∈ H and history h ∈ H with h S = h • a • h , a = S π(h ) (h ). Player i ∈ P prefers strategy profile S to strategy profile S , S i S, if h S i h S. 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.

Systems with pure persuasion

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 ∈ 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 [10].

By combining the DC system with pure persuasion we can complete the definition of the argumentation game Γ 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 ∈ H is terminal, i.e. π(h) = ∅, if one of the following conditions is satisfied:

T prop : |h| is even and t ∈ C W (h) ∩C B (h), T opp : |h| is odd and t / ∈ C W (h) ∪C B (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 H win W denote the set of finite histories for which condition T prop is satisfied and let H win B denote the set of finite histories for which condition T opp is satisfied. Set H win W contains the terminal histories at which player W, the proponent, is the winner, and set H win B contains the terminal histories at which player W, the opponent, is the winner.

We assume the following preference relation on terminal histories. Given h 1 , h 2 ∈ T , 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.

h 1 W h 2 if h 2 ∈

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 [10].

Strategies and solutions 3.1 Definitions

A strategy of a player i is a function from player i's histories to the set of actions S i : H i → L, such that for all h ∈ H i , S i (h) ∈ α i (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 S i . A strategy profile S = (S i , S −i ) is a pair of strategies chosen by each of the players, S ∈ S i × 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 S i is dominant for player i if for all S i ∈ S i and all S j ∈ S j with j = −i,

(S i , S j ) i (S i , S j ).

A strategy is strictly dominant if the property above holds with strict inequality. A strategy profile S = (S i , S −i ) is a solution in (strictly) dominant strategies iff S i is dominant for player i and S −i is dominant for player −i. 7A strategy profile S = (S i , S −i ) is a Nash equilibrium if for all i ∈ P and for all

S i ∈ S i , (S i , S −i ) i (S i , 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).

Solutions to pure persuasive dialogues

Consider a game Γ [S 0 , →] defined for some set of atomic statements S 0 and a relation of immediate consequence →. 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 ∈ ICC. Consider a strategy s 1 ∈ S W such that s 1 (ε) = 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 ∈ ICC, . The game ends in two rounds and the outcome most preferred by player W is achieved. Thus, any s 1 as described above is a dominant strategy of the proponent. Moreover, for any s 2 ∈ S B , the outcome of the game from strategy profile s = (s 1 , s 2 ) 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 / ∈ ICC. Let s 2 ∈ S B be a strategy such that for any non-terminal history h with t ∈ C W (h) ∩C B (h) and |h| odd, s 2 (h) = Wt. In this case Wt ∈ α B (h), because the last action of h must have been t. On the other hand, let s 1 ∈ S W be a strategy such that for any non-terminal history h with t / ∈ C W (h) ∪C B (h), s 1 (h) = t. Note that the strategy profile s = (s 1 , s 2 ) 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 [10].

Example

In order to recall the illustration of the results from [10], let us consider a version of the Battle of the Sexes game (cf. [16]) in which the couple -Wilma (W) and Brian (B)have to decide on their plans for the day. Brian thinks they should go to a soccer match, but Wilma thinks they should go to the ballet. Even though Wilma prefers the ballet to the soccer, she would still rather attend a soccer match than stay at home. Similarly, Brian likes the soccer match more than the ballet, but he prefers the ballet to staying home.

We assume the set of atomic statements to be such that {p, q, r,t} ⊆ S 0 , 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, {q → ¬p, p → ¬q, r → ¬q,t → ¬p} ⊆ →. 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 s = (s 1 , s 2 ) where s 1 is a strategy of Wilma's in which she states p and r as soon as it is possible and s 2 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, s 1 is a strategy such that (a) s 1 (ε) = p and (b) for any nonterminal history h, if r ∈ α W (h) then s 1 (h) = r, while s 2 is a strategy such that for any move number locution of W

locution of B C W C B 1 p - p p 2 - Wp p - 3 r - p, rr 4

q p, q, r q, r 5 r → ¬q -p, q, r, r → ¬q q, r, r → ¬q 6 -R(q ∧ r ∧ (r → ¬q)) p, q, r, r → ¬q q, r, r → ¬q 7

Wq -p, r, r → ¬q q, r, r → ¬q

∈ α B (h) then s 2 (h) = q, and (b) if h = h • r • h then s 2 (h) = 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 s = (s 1 , s 2 ) 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.

Verification of strategies

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 [2]. Currently, we are designing the application, which will expand the possibilities of earlier verification software tool Perseus [3]. We are planning to study functionality of existing model checking techniques, like Bounded Model Checking [23], for verification of agent communication modelled in terms of game semantics.