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.
In the paper we deal with a classic concurrency problem - a faulty train controller system (FTC). In particular, we formalize it by means of finite automata, and consider several properties of the problem, which can be expressed as formulae of a soft real-time branching time temporal logic, called RTECTL. Further, we verify the RTECTL properties of FTC by means of SAT-based bounded model checking (BMC) method, and present the performance evaluation of the BMC method with respect to the considered problem. The performance evaluation is given by means of the running time and the memory used.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.