In the paper, we show a formal model for a dialogue game in which players can perform actions representing locutions like claim, question, concede as well as locutions which have a greater emotional charge like scold or nod. We define a protocol for dialogues in which participants have emotional skills and then give an interpreted system for them. Finally, we propose an extension of CTL logic with commitment, emotion and goal modalities. All of this is a formal basis, which we use to perform semantic verification of properties of dialogue systems with emotional reasoning.
As members of society we have the need of collective work and protocols are an important part of our social skills. They help to facilitate structured conversations and are commonly used in everyday situations (sometimes unconsciously). Protocols should support dialogue, to help achieve the goal of the conversation. The first group of our interest are children who are known to have different cognitive abilities in comparison to adults. Usually, they are hard to convince and such a discourse is quite specific. For many people, it is hard to tell at first sight, from which argument we would benefit the most, and which one we should definitely avoid.
The aim of such an argumentation is a change in the emotional state of the interlocutor. The emotional state of our understanding consists of many factors, e.g. a sense of security, self-agency, self-satisfaction, self-confidence and so on. Some argument at the same time can increase one’s sense of self-agency, but decrease one’s sense of security (“if you find a job, you could move out, but you would have to rent your own flat”). We aim in designing an application which would be a support for people who have to convince somebody, but the more important factor is the emotional well-being of the interlocutor. We see such an application as a trainer of good practices in argumentation. We could consider possible reactions of potential interlocutor (e.g. a rebellious teenager, an expatriate) to specific arguments and monitor changes in the simplified representation of the emotional state. That is the reason we work on argumentative dialogue protocol, which is supposed to take into account change an emotional state of interlocutor in order to obtain the desired result (e.g. some kind of decision).
Usually, the aim of argumentation is figuring the agreement, the conviction of someone for their own reasons or even reaching a compromise [14, 32]. Persuasion dialogues are dialogues aimed at resolving conflicts of opinion between at least two participants. There are many types of such dialogues, e.g. conflict resolution dialogue begins with a conflict of opinion and ends when one of the participants convinces the other one. By the contrast, the argumentation under our consideration does not necessarily have to convince a child to do something, but it should help him become aware of his feelings. Certainly, we do not want to claim that there is an obvious argumentation that will convince everybody, but there are some argumentation strategies and mechanisms, which are quite known and considered as convincing ones.
Formal dialogue systems, which are growing field in the research on the process
of communication, can be used as a schema for such dialogues, both between artificial
agents or between the man and the machine. In our case, we need an argumentative
dialogue model designed for human-computer communication, which applies the
mentioned specific types of dialogues. There are other approaches which are focused rather
on the agent to agent communication [
In this paper, we present a continuation of our work on the mathematical model of dialogue inspired by dialogue games [16]. We would like to use this model as a semantic structure in verification of properties of dialogue protocols and enable automated analysis of dialogues. The model we base our current research on is founded on the tradition of argumentative dialogue games by Prakken and others [25].
There are many approaches that assume very strict rules of communications. Our
model, focusing on machine-man communication, is also based on such strict rules. On
one hand, it makes it a little trivial, but on the other hand we can extract and focus on
most important features of the dialogues. We can perceive dialogue games [
Each dialogue game should have three basic categories of rules. Locution rules define a set of actions (speech acts, locutions) the player is allowed to perform during the game. These actions express communication intentions of players. For example, rules of the dialogue game can assume that player can claim something, argue, justify, ask for justification, concede something etc. The second category of rules is responsible for the definition of possible answers for specific moves. For example, after one interlocutor claims something, the other one can concede it by performing concede or he can ask for justification by performing why. These rules are called structural rules. The third group of rules defines effects of actions. Due to performing some action (e.g. confirming or rejecting) a set of public declarations (commitments) of the interlocutor is changed. The result of an action is a change in the commitments set of the player, i.e. addition of some new statement to this set. These rules are called effect rules. We are specifying above rules which determine available moves for each player at every moment of the dialogue.
Even though every protocol must meet some general requirements, each one can be
quite unique and we are interested in verifying characteristic properties of the dialogue
defined by the specific protocol. In order to do that, we would like to use model
checking method applied in verification of multi-agent systems (MAS). Main solutions in
this matter combine bounded model checking (BMC) with symbolic verification using
translations to either ordered binary decision diagrams (BDDs) [13] or propositional
logic (SAT) [24]. Verified properties are expressed in logics which are combinations of
the epistemic logic with branching [27] or linear time temporal logic [30]. Such logics
can be interpreted either over interleaved interpreted systems (IIS) [19] or interpreted
systems themselves [
The work presents a sketch of a formal system, which is a base for designing model checking techniques for verification dialogue games. We are concerned with argumentative dialogues, in which players can perform actions affecting commitments as well as their emotions. As a result, they change the emotional state, mood and attitude of the players. The proposed model will be used to show what mechanisms occur in human argumentative dialogues. In particular, we focus on argumentations where rational arguments are less effective (or not as effective) as the arguments referring to the emotions. On this basis, we will build a tool for learning managing emotions. Since emotions play a major role in persuading children, this tool can be used for personal development training for teachers or parents, which are often confused about children’s feelings.
The study of emotions is part of various disciplines like Psychology, Economics, Cognitive Neuroscience, and, in recent years, also Artificial Intelligence and Computer Science. These studies aim to establish systems for emotional interaction. Nowadays, more and more artificial agents integrate emotional skills to achieve expressiveness, adaptability, and credibility. Such multiagent systems find application in the improvement of human-machine interaction, testing, refining and developing an emotional hypothesis or even the improvement of artificial intelligence techniques, once it optimizes decision-making mechanisms [28, 23].
We start out by defining a mathematical model for argumentation dialogue games. This model uses the concept of interpreted systems and Kripke structures. In this model formulas of a modal logic adequate to express properties that allow prediction of players’ behavior are interpreted. The obtained Kripke structure will be used to perform automatic verification of dialogue protocols via model checking techniques.
First, we assume that the set of players of a dialogue game consists of two players: White (W ) and Black (B), Pl = {W; B}: To each player p ∈ Pl, we assign a set of actions Actp and a set of possible local states Lp.
Every action from Actp can influence participant’s commitments. We assume that the set Actp contains also the special empty (null) action ε . Every action (except null action) is synonymous with locution expressed by the specific player. Results of locutions are determined by evolution function and are specified afterwards.
Player’s local state lp ∈ Lp consists of the player’s commitments, emotions, and goals, lp = (Cp; Ep; GOp): Player’s commitments and goals are elements of a fixed topic language, which allows expressing the content of locutions. Thus, Cp and GOp are sets of such expressions. These sets may be subject to change after a player’s action. More specifically, the player can add or delete the selected expression. Emotions which we consider are fear, disgust, joy, sadness, and anger. Their strength (intensity) is represented by natural numbers from the set {1; 2; : : : ; 10}. Thus, Ep is a 5-tuple consisting of five values, which may also change after a certain action. It is worth highlighting here that a change in the intensity of the emotions is dependent on the type of locution and, perhaps even more, on its content.
Next, Act denotes the Cartesian product of the players’ actions, i.e. Act = ActW × ActB: The global action a ∈ Act is a pair of actions a = (aW ; aB); where aW ∈ ActW , aB ∈ ActB and at least one of these actions is the empty action. This means that players cannot speak at the same time. Moreover, a player cannot reply to his own moves. Thus, the empty action is performed alternately by players W and B.
Also, we need to order performed global actions and indicate which actions correspond with which ones and therefore we define double-numbered global actions set Num2Act = N × N × Act: During the dialogue, we assign to each performed global action two numbers: the first one (ascending) indicates order (starting from the value 1). The second one points out to which earlier action this action is referring (0 at the beginning of the dialogue means that we are not referring to any move).
Furthermore, we define numbered global actions set Num1Act = N × Act. Each element of this set is a pair (n; a) consisting of an action a ∈ Act and the identifier of the action it refers to, n ∈ N. If we want to find out whether we can use some global action one more time, we should check if the possible move containing the same global action refers to the different earlier move. We define function Denum : Num2Act → Num1Act; which maps double-numbered global action to the numbered global action. We understand dialogue d as a sequence of moves and in particular, we denote d1::n = d1; :::; dn; where di ∈ Num2Act, di = (i; j; a); j ∈ N, j < i, a ∈ Act.
A global state g is a triple consisting of dialogue history and players’ local states corresponding to a snapshot of the system at a given time point g = (d(g); lW (g); lB(g)); g ∈ G where G is the set of global states. Given a global state g, we denote by d(g) a sequence of moves executed on a way to state g and by lp(g) - the local state of player p in g.
An interpreted system for a dialogue game is a tuple IS = (I; {Lp; Actp}p∈Pl ) where I ⊆ G is the set of initial global states.
Let α ;β ;φ ;ψ1; ::;ψn;γ1; ::;γn ∈ Form(PV ), i.e., be formulas defined over the set PV , which is a set of atomic propositions under which a content of speech acts is specified. Locutions used in players’ actions are the same for both players: ActW = ActB = {ε ; claim φ ; concede φ ; why φ ; scold φ ; nod φ ; φ since {ψ1; : : : ;ψn}; retract φ ; question φ }:
In argumentation dialogues, a player can claim some facts, concede with the opponent or change his mind performing action retract. To challenge the opponent’s statement, he may ask why, or ask whether the opponent commits to something, i.e., perform action question. For defense he can use the action since. It is the kind of reasoning and argumentation. Actions scold and nod express reprimand and approval, respectively. Note that all of these locutions refer to commitments, i.e., public announcements. We are not talking here about beliefs or knowledge, which may differ from the commitments.
Now we define legal answer function FLA : Num2Act → 2Num1Act ; which maps a double-numbered action to the set of possible numbered actions. This function is symmetrical for both players and determines for every action a set of legal actions which can be performed next.
– FLA(i; j; (ε ;ε )) = 0/, – FLA(i; j; (claim φ ;ε )) = {(i; act) : act ∈ {(ε ; why φ ); (ε ; concede φ ), (ε ; claim ¬φ ), (ε ; node ψ ), (ε ; scold ψ ) }, for some ψ ∈ Form(PV ), – FLA(i; j; (why φ ;ε )) = {(i; act) : act ∈ {(ε ;φ since {ψ1; : : : ;ψn}),(ε ; retract φ )}, – FLA(i; j; (φ since {ψ1; : : : ;ψn};ε )) = {(i; act) : act ∈ {(ε ; why α ), (ε ; concede β ); (ε ; ¬φ since {γ1; : : : ;γn}), (ε ; node ψ ), (ε ; scold ψ ) }, where α ∈ {ψ1; : : : ;ψn}, β ∈ {φ ;ψ1; : : : ;ψn}, and ψ ∈ Form(PV ), – FLA(i; j; (concede φ ;ε )) = {(i; act) : act ∈ {(ε ;ε ), (ε ; claim α ), (ε ; node α ), (ε ; scold α ), (ε ;α since {ψ1; : : : ;ψn}) }, for some α ;ψ1; : : : ;ψn ∈ Form(PV ), – FLA(i; j; (retract φ ;ε )) = {(i; act) : act ∈ {(ε ;ε ); (ε ; claim α ), (ε ; node α ), (ε ; scold α ), (ε ;α since {ψ1; : : : ;ψn})}, for some α ;ψ1; : : : ;ψn ∈ Form(PV ), – FLA(i; j; (question φ ;ε )) = {(i; act) : act ∈ {(ε ; retract φ ); (ε ; claim φ ), (ε ; claim ¬φ )}, – FLA(i; j; (scold φ ;ε )) = {(i; act) : act ∈ {(ε ; why φ ); (ε ; concede φ ), (ε ; claim ¬φ ), (ε ; node ψ ), (ε ; scold ψ ) }, for some ψ ∈ Form(PV ), – FLA(i; j; (nod φ ;ε )) = {(i; act) : act ∈ {(ε ;ε ), (ε ; claim α ), (ε ; node α ), (ε ; scold α ), (ε ;α since {ψ1; : : : ;ψn}) }, for some α ;ψ1; : : : ;ψn ∈ Form(PV ).
The actions executed by players are selected according to a protocol function Pr : G → 2Num2Act , which maps a global state g to the set of possible double-numbered global actions. The function Pr satisfies the following rules. (R1) For ι ∈ I Pr(ι ) =
{(1; 0; (claim φ , ε )), (1; 0; (question φ ,ε )), (1; 0; (φ since {ψ1; : : : ;ψn};ε ))}. (R2) Pr((d1::k−1; (k; l; (ε ;ε )); lW (g); lB(g))) = {(k +1; numact) : numact ∈ FLA(k; l; (ε ;ε )). (R3) Pr((d1::k−1; (k; l; (a;ε )); lW (g); lB(g))) = {(k +1; numact) : numact ∈ FLA(k; l; (a;ε ))}, for a ∈ {ε ; claim φ ; scold φ ; why φ ; φ since {ψ1; : : : ;ψn}}. (R4) Pr((d1::k−1; (k; l; (a;ε )); lW (g); lB(g))) = {(k + 1; numact) : numact ∈ ((∪i<=k FLA(di) ∩ {(n; (ε ;α )) : n < k;α ∈ ActB}) \{Denum(di) : i = 1; ::; k})}, for a ∈ {concede φ ; nod φ ; question φ }.
After opponent’s locutions concede, nod or question the player can use one from possible answers for all previous opponent’s moves, excluding these ones which he has already used. (R5) Pr((d1::k−1; (k; l; (retract φ ;ε )); lW (g); lB(g))) = {(k + 1; numact) : numact ∈ ((∪i<=k FLA(di) ∩ {(n; (ε ;α )) : n < k;α ∈ ActB})\{Denum(di) : i = 1; ::; k})} ∪ {(k + 1; x; (ε ; why β )) : ∃x<k dx = (x; y; (β since φ ;ε ))} for some φ ;β ∈ Form(PV ). After opponent’s locution retract φ the player can use one from possible answers for all previous opponent’s moves, excluding these ones which he has already used but also he can ask for the reason for β if φ was previously used to justify β . These rules for player B are analogous.
The protocol is a crucial element of the model since it gives strict rules which determine the behaviour of players. In other words, it formally describes who, when and which action can perform. Rules (R1) and (R2) refer to the beginning and end of the dialogue, respectively. Rule (R3) states that after locutions claim, scold, why, and since, only actions determined by the legal answer function can be used. According to rules (R4) and (R5), actions concede, nod and retract end one of the threads of dialogue. Therefore, the next action can start a new thread or return to one of the unfinished. Actions nod and scold act similarly to actions concede and claim, but what distinguishes these actions is their emotional charge.
To show how locutions and their contents affect players’ emotions and goals we define two functions. The first one determines the change of intensity of emotions:
possible 5-tuples for emotions, i.e., Emotionp = {(n1; : : : ; n5) : ni ∈ {1; : : : ; 10} ∧ i ∈ {1; : : : ; 5}}. The second one determines the change of goals: GOALp : Actw × Goalp → Goalp where p ∈ Pl and Goalp is a set of possible goals represented by expressions from the topic language, i.e. Goalp ⊂ Form(PV ).
Finally, we define global (partial) evolution function t : G × Num2Act → G; which determines results of actions. This function is symmetrical for both players. Let d(g) = d(g)1;:::;m, then:
Global evolution function defines results of actions. In particular, actions claim, concede, scold, nod and since add an expression to the commitments set while action retract deletes it. Actions why and question do not modify this set. 3
The mathematical model for argumentative dialogue games provides a basis for
applying the methods of model checking to verify the correctness of dialogue protocols
relative to the properties that the protocols should satisfy. Model checking [
The prerequisite inputs to model checking are a model of the system under consideration and a formal characterisation of the property to be checked. Therefore, we associate with the given interpreted system a Kripke structure, that is the basis for the application of model checking. A Kripke structure is defined as a tuple M = (G; Act; T; I) consisting of a set of global states G, a set of actions Act (in our approach Num2Act), a set of initial states I ⊆ G, a transition relation T ⊆ G × Act × G such that T is left-total. Relation T is defined as follows (g; a; g′) ∈ T iff g′ ∈ t(g; a): By T ∗ we will denote the reflexive and transitive closure of T .
To formulate properties of dialogue protocols suitable propositional temporal
logics are applied. The most commonly used, in general, are linear temporal logic (LTL),
computation temporal logic (CTL), a full branching time logic (CTL∗), the universal
and existential fragments of these logics, and other logics which are their modifications
and extensions. One of the most important practical problems in the model checking is
the exponential growth of the number of states of the Kripke structure. That is why in
future work we intend to focus on symbolic model checking of dialogue protocols.
Symbolic model checking avoids building a state graph; instead, sets and relations are
represented by Boolean formulae. One of the possible methods of symbolic model checking
is bounded model checking (BMC) [
The standard BMC algorithm, starting with k = 0, creates for a given Kripke structure M and a given formula φ , a formula [M;φ ]k: Then the formula [M;φ ]k is forwarded to either a SAT-solver or a SMT-solver. Note, that in the case of SAT-base BMC the propositional formula is converted to a satisfiability equivalent propositional formula in conjunctive normal form before forwarding it to a SAT-solver. If the tested formula is unsatisfiable, then k is increased (usually by 1) and the process is repeated. The BMC algorithm terminates if either the formula [M;φ ]k turns out to be satisfiable for some k, or k becomes greater than a certain, M-dependent, threshold (e.g. the number of states of M). Exceeding this threshold means that the formula φ is not true in the Kripke structure M. On the other hand, satisfiability of [M;φ ]k, for some k means that the formula φ is true in M.
Interpreted systems are traditionally used to give a semantics to an epistemic language
enriched with temporal connectives based on linear time [
Definition 1 (Syntax). Let Pl = {W; B} be a set of players. The set of formulas is defined inductively as follows: • true is a formula, • if φ ∈ Form(PV ) and p ∈ Pl then COMp(φ ) and Gp(φ ) are formulas, • Ep(e) is a formula for p ∈ Pl and e ∈ {fear, disgust, joy, sadness, anger}, • if α and β are formulas, then so are ¬α , α ∧ β and α ∨ β , • if a¯ ∈ ActW and α is a formula, then so are AX(W;a¯)α and AY(W;a¯)α , • if a¯ ∈ ActB and α is a formula, then so are AX(a¯;B)α and AY(a¯;B)α , • if α and β are formulas, then so are AXα , AGα and A(α Uβ ), • if α is a formula, then so are AYα and AHα . def def The remaining basic modalities are defined by derivation: EFα = ¬AG¬α , EPα = def def def ¬AH¬α , EZα = ¬AZ¬α , EZ(W;a¯)α = ¬AZ(W;a¯)¬α , EZ(a¯;B)α = ¬AZ(a¯;B)¬α , for def def def Z ∈ {X; Y}, Moreover, α ⇒ β = ¬α ∨ β , α ⇔ β = (α ⇒ β ) ∧ (β ⇒ α ), and f alse = ¬ true.
The formula true is used for technical reasons and helps to express that some action is possible to execute, i.e., an action can lead to a state in which true holds. Of course, true is satisfied in every state.
Formula COMp(φ ) describes the actual set of commitments of player p, more precisely, it expresses that φ is in this set. We should emphasize that φ is not a formula of the language defined herein, but a part of a separate structure in which it is possible to express the spoken sentences. In dialogue system, all actions are aimed at influencing the players’ commitments. Therefore, the modality COM is very important and often used in the protocol specification. Modalities Ep and Gp allow for expressing properties concerning emotions and goals of player p.
The temporal modalities X; G stand for “at the next step”, and “forever in the future”, respectively. Y; H are their past counterparts “at the previous step”, and “forever in the past”. The modality A is the universal quantifier - “for all”. Thus, AX means “for all next states” while AG means “for all states on all paths”.
We also introduce modality AX(W;a¯). It encodes an additional fact calling the action that led to the next state. Since we are talking about the implementation of a specific action, we must also indicate its executor. Hence, the subscript (W; a¯), expressing that the performer is a player White, is added. A similar modality is defined for Black: AX(a¯;B). As a result, the formula AX(a¯;B)α intuitively expresses that “at all next states reached after execution of action a¯ by Black, α is true”.
The operator U stands for Until; the formula α Uβ , expresses the fact that β eventually occurs and that α holds continuously until then.
As customary, the negation ¬A can be replaced by the existential quantifier E using the de Morgan’s laws. So, ¬AXα is equivalent with EX¬α - there exists a next state at which α holds. The interpretation of the other existential formulas is similar.
First, in order to give the semantics for the above formulas, we need to give a formal definition of a computation. A computation in a Kripke structure M = (G; Act; T; I) is a possibly infinite sequence of states π = (g0; g1; : : :) such that there exists an action am for which (gm; am; gm+1) ∈ T for each m ∈ N, i.e., gm+1 is the result of applying the transition relation T to the global state gm, and the action am.
Below we abstract from the transition relation, the actions, and the protocols, and simply use T , but it should be clear that this is uniquely determined by the interpreted system under consideration. In interpreted systems terminology, a computation is a part of a run. A k-computation is a computation of length k. For a computation π = (g0; g1; : : :), let π (k) = gk, and πk = (g0; : : : ; gk), for each k ∈ N. By Π (g) we denote the set of all the infinite computations starting at g in M, whereas by Πk(g) the set of all the k-computations starting at g.
Definition 2 (Semantics – Interpretation). Let M be a model (Kripke structure), g ∈ G be a state, π be a computation, and α ;β be formulas. M; g |= α denotes that α is true at the state g in the model M. M is omitted, if it is implicitly understood. The relation |= is defined inductively as follows: g |= true for all g ∈ G, g |= COMp(φ ) iff φ ∈ Cp(g), g |= Ep(e) iff ni > 5 in Ep(g) = (n1; ::; n5), where e is fear, disgust, joy, sadness, anger and i = 1; 2; 3; 4; 5, respectively, g |= Gp(φ ) iff φ ∈ GOp(g), g |= ¬α iff g ̸|= α , g |= α ∧ β iff g |= α and g |= β , g |= AX(W;a¯)α iff ∀a = (i; j; (a¯;ε )) ∈ Num2Act and ∀g′ ∈ G ( if (g; a¯; g′) ∈ T; then g′ |= α ), g |= AX(a¯;B)α iff ∀a = (i; j; (ε ; a¯)) ∈ Num2Act and ∀g′ ∈ G ( if (g; a¯; g′) ∈ T; then g′ |= α ), g |= AXα iff ∀g′ ∈ G ∀a ∈ Num2Act ( if (g; a; g′) ∈ T; then g′ |= α ), g |= AGα iff ∀π ∈ Π (g) (∀m≥0 π (m) |= α ); g |= A(α Uβ ) iff ∀π ∈ Π (g) (∃m≥0 [π (m) |= β and ∀ j<m π ( j) |= α ]), g |= AY(W;a¯)α iff ∀a = (i; j; (a¯;ε )) ∈ Num2Act and ∀g′ ∈ G ( if (g′; a; g) ∈ T; then g′ |= α ), g |= AY(a¯;B)α iff ∀a = (i; j; (ε ; a¯)) ∈ Num2Act and ∀g′ ∈ G ( if (g′; a; g) ∈ T; then g′ |= α ), g |= AYα iff ∀g′ ∈ G ∀a ∈ Num2Act ( if (g′; a; g) ∈ T; then g′ |= α ), g |= AHα iff ∀g′ ∈ G ( if (g′; g) ∈ T ∗; g′ |= α ).
The description of the semantics is finished by giving the definition of the validity in the model.
Definition 3. (Validity) A formula φ is valid in M (denoted M |= φ ) iff M;ι |= φ , i.e., φ is true at the initial state of the model M.
The formal language introduced in the previous section is used for giving the specification for dialogue protocols as well as for describing properties of these protocols. The properties can be divided into several classes [21]. Some of them are studied below.
Safety. Safety property usually expresses that something bad does not happen. However, it can also express that something good is always true. The best illustration here is the specification of locutions used in dialogues:
AG(AX(W;claim α ) COMW α ): This formula states that after locution claim α , the formula α is in the set of commitments of the performer.
The next formula expresses a similar property, i.e., before the execution of the locution retract α , the formula α must be in the commitments set of the player:
AG(AY(W;retract α ) COMW α ):
Nontermination. One of the most important safety properties is nontermination. It expresses that every legal dialogue, i.e., dialogue in accordance with rules of a dialogue game does not have a termination state:
This formula states that in every state of every computation there is an action which can be performed and after execution of this action a formula true is satisfied. As a consequence, every dialogue is infinite.
Guarantee. One of the guarantee properties, i.e., properties that ensure that some event eventually happens, is termination. In dialogue systems, we often assume that the end of a dialogue means the fulfillment of a certain condition. This condition may express that one of the players, e.g. W , is happy: If any dialogue should end with the termination condition and this condition means that White does not feel fear, then we can express this fact as follows:
E(true U EW ( joy)):
The formula claims that every computation contains a state at which the required condition holds.
Response. The response property expresses the fact that a property β is a guaranteed response to a condition α . An example of this is the formula
which states that if a player is committed to α , then during the dialogue he can change it. This property is very important since it states that it is possible to reject some commitment and at the same time it means the ability to change some opinion, what is crucial for argumentative dialogues. It makes no sense to provide and analyze arguments if the change of players’ commitments is not possible at all.
The aim of our research is to design and implement a framework to provide a communication between a user and a machine which allows to better understand emotions that appear during human dialogues. We plan to create a tool that will support the personal development in this matter, i.e., the acquisition of skills of identifying and naming emotions. This is particularly important for training teachers, educators, psychologists, and parents. This process can take place between a human, which plays a role of a student, and a software agent, which plays a role of a teacher. The challenge is to design a suitable interface for such communication. However, the implementation should be preceded by constructing a mathematical model and proposing a new dialogue protocol. In our work, we also propose formal language for protocol specification and expressing its properties. On this basis, we plan to design and implement a multimedia tool for educational purposes. Psychological aspects of the project are consulted with a group of psychologists. Our research does not deal with linguistic analysis, but we want to explore dialogues with the fixed base so that the user can learn to recognize these places and elements of dialogue which relate to emotions.
Acknowledgment. The research by Kacprzak have been carried out within the framework of the work S/W/1/2014 and funded by Ministry of Science and Higher Education. 13. A. V. Jones and A. Lomuscio. Distributed BDD-based BMC for the verification of multiagent systems. In W. van der Hoek, G. A. Kaminka, Y. Lespe´rance, M. Luck, and S. Sen, editors, Proc. of AAMAS, Volume 1-3, pages 675–682, 2010. 14. M. Kacprzak, M. Dziubinski, and K. Budzynska. Strategies in dialogues: A game-theoretic approach. In S. Parsons, N. Oren, C. Reed, and F. Cerutti, editors, Proc. of COMMA, volume 266 of Frontiers in Artificial Intelligence and Applications, pages 333–344. IOS Press, 2014. 15. M. Kacprzak and A. Sawicka. Identification of formal fallacies in a natural dialogue. Fundam. Inform., 135(4):403–417, 2014. 16. M. Kacprzak, A. Sawicka, and A. Zbrzezny. Dialogue systems: Modeling and prediction of their dynamics. In A. Abraham, K. Wegrzyn-Wolska, E. A. Hassanien, V. Snasel, and M. A.
Alimi, editors, Proc. of AECIA, pages 421–431. Springer International Publishing, 2016. 17. M. Kacprzak and O. Yaskorska. Dialogue protocols for formal fallacies. Argumentation, 28(3):349–369, 2014. 18. L. Keiff. Dialogical logic. In E. N. Zalta, editor, The Stanford Enc. of Philosophy. 2011. 19. A. Lomuscio, W. Penczek, and H. Qu. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In W. van der Hoek, G. A. Kaminka, Y. Lespe´rance, M. Luck, and S. Sen, editors, IFAAMAS, Volume 1-3, pages 659–666, 2010. 20. K. Lorenz and P. Lorenzen. Dialogische logik. WBG. Darmstadt, 1978. 21. Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems - specification. Springer, 1992. 22. A. Meski, W. Penczek, M. Szreter, B. Wozna-Szczesniak, and A. Zbrzezny. BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. AAMAS, 28(4):558–604, 2014. 23. F. S. Nawwab, P. E. Dunne, and T. Bench-Capon. Exploring the role of emotions in rational decision making. In Proc. of COMMA, 2010. 24. W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundam. Inform., 55(2):167–185, 2003. 25. H. Prakken. Models of persuasion dialogue. In Argumentation in AI, pages 281–300.
Springer, 2009. 26. S. Rahman and T. Tulenheimo. From games to dialogues and back: towards a general frame for validity. In O. Majer, A. Pietarinen, and T. Tulenheimo, editors, Games: Unifying Logic, Language, and Philosophy, volume 15 of LEUS, pages 153–208. Dordrecht: Springer, 2006. 27. F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic, 5(2):235 – 251, 2007. Logic-Based Agent Verification. 28. R. Silveira, G. K. da Silva Bitencourt, T. . Gelaim, J. Marchi, and F. de la Prieta. Towards a model of open and reliable cognitive multiagent systems: Dealing with trust and emotions.
ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal, 4(3), 2016. 29. C. Tinelli. SMT-based model checking. In NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, page 1, 2012. 30. W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In D. Bosnacki and S. Leue, editors, Proc. of SPIN, volume 2318 of LNCS, pages 95–111, 2002. 31. J. Visser, F. Bex, C. Reed, and B. Garssen. Correspondence between the pragma-dialectical discussion model and the argument interchange format. Studies in Logic, Grammar and Rhetoric, 23(36):189–224, 2011. 32. D. N. Walton and E. C. W. Krabbe. Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning. State University of N.Y. Press, 1995. 33. S. Wells and C. A. Reed. A domain specific language for describing diverse systems of dialogue. J. Applied Logic, 10(4):309–329, 2012. 34. O. Yaskorska, K. Budzynska, and M. Kacprzak. Proving propositional tautologies in a natural dialogue. Fundam. Inform., 128(1-2):239–253, 2013.