Towards Encoding of the Transition Relation in Dialogue Games Model Checking

We can understand a protocol as a set of rules used by the communicating entities i.e. people or computers. These rules specify allowed interactions between them. Every day people use protocols unconsciously during their conversations since they help to achieve the goal of the conversation (e.g. a compromise, a persuasion). In the paper, we focus on argumentative dialogues in which players can perform actions representing speech acts like claim, question, scold etc. Since we consider dialogues which have an emotional undertow we want to design a system for semantic verification of properties of dialogue games with emotional reasoning. This framework is based on interpreted systems designed for a dialogue protocol in which participants have emotional skills. The GERDL language is used for a dialogue game specification. We present the idea of encoding rules describing the dialogue game given in this language. We want to verify some properties of dialogue games and we focus on the reachability property that can take into account emotions and commitments of players.