Towards Encoding of the Transition Relation in Dialogue Games Model Checking

• Autorzy: Sawicka Anna , Kacprzak Magdalena , Zbrzezny Andrzej

Identyfikatory

DOI

10.3233/FI-2019-1789

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

description language; dialogue game; dialogue protocol; emotions

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 165, nr 3-4
• Strony: 345--361
• Opis fizyczny: Bibliogr. 27 poz.

Twórcy

autor

Sawicka Anna

• Faculty of Computer Science, Polish-Japanese Academy of Information Technology, Warsaw, Poland

autor

Kacprzak Magdalena

• Faculty of Computer Science, Bialystok University of Technology, Bialystok, Poland

autor

Zbrzezny Andrzej

• Faculty of Mathematics and Natural Sciences, Jan Długosz University, Czestochowa, Poland

Bibliografia

• [1] Budzyńska K, Kacprzak M, Sawicka A, Yaskorska O. Dialogue Dynamics: Formal Approach. IFS PAS, 2015.
• [2] Visser J, Bex F, Reed C, Garssen B. Correspondence between the Pragma-Dialectical Discussion Model and the Argument Interchange Format. Studies in Logic, Grammar and Rhetoric, 2011;23(36):189-224. URL http://hdl.handle.net/11245/1.363108.
• [3] Kacprzak M, Yaskorska O. Dialogue Protocols for Formal Fallacies. Argumentation, 2014;28(3):349-369. doi:10.1007/s10503-014-9324-4.
• [4] Kacprzak M, Sawicka A. Identification of Formal Fallacies in a Natural Dialogue. Fundam. Inform., 2014. 135(4):403-417. doi:10.3233/FI-2014-1131.
• [5] Yaskorska O, Budzyńska K, Kacprzak M. Proving Propositional Tautologies in a Natural Dialogue. Fundam. Inform., 2013;128(1-2):239-253. doi:10.3233/FI-2013-944.
• [6] Kacprzak M, Sawicka A, Zbrzezny A. Towards Model Checking Argumentative Dialogues with Emotional Reasoning (extended abstract). In: Proceedings of the 25th International Workshop on Concurrency, Specification and Programming. 2016 pp. 257-268.
• [7] Baier C, Katoen J. Principles of Model Checking. MIT Press, 2008. ISBN: 9780262026499.
• [8] Clarke EM, Grumberg O, Peled DA. Model checking. MIT Press, 2001. ISBN: 9780262032704.
• [9] Męski A, Penczek W, Szreter M, Woźna-Szcześniak B, Zbrzezny A. BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Autonomous Agents and Multi-Agent Systems, 2014;28(4):558-604. doi:10.1007/s10458-013-9232-2.
• [10] Zbrzezny AM, Zbrzezny A, Raimondi F. Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers. In: Agent and Multi-Agent Systems: Technology and Applications, 10th KES International Conference, KES-AMSTA 2016, Puerto de la Cruz, Tenerife, Spain, 2016, Proceedings. 2016 pp. 45-55. doi:10.1007/978-3-319-39883-9_4.
• [11] Penczek W, Woźna-Szcześniak B, Zbrzezny A. Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems. Fundam. Inform., 2012;119(3-4):373-392. doi:10.3233/FI-2012-743.
• [12] Zbrzezny AM, Woźna-Szcześniak B, Zbrzezny A. SMT-Based Bounded Model Checking for Weighted Epistemic ECTL. In: Pereira FC, Machado P, Costa E, Cardoso A (eds.), Progress in Artificial Intelligence - 17th EPIA 2015, Coimbra, Portugal, 2015. Proc., volume 9273 of Lecture Notes in Computer Science. Springer, 2015 pp. 651-657. doi:10.1007/978-3-319-23485-4_65.
• [13] Sawicka A, Kacprzak M, Zbrzezny A. A Novel Description Language for Two-Agent Dialogue Games. In: Polkowski L, Yao Y, Artiemjew P, Ciucci D, Liu D, Slezak D, Zielosko B (eds.), Rough Sets – International Joint Conference, IJCRS 2017, Olsztyn, Poland, July 3-7, 2017, Proceedings, Part II, volume 10314 of Lecture Notes in Computer Science. Springer, 2017 pp. 466-486. doi:10.1007/978-3-319-60840-2_34. URL https://doi.org/10.1007/978-3-319-60840-2_34.
• [14] Kacprzak M, Dziubiński M, Budzyńska K. Strategies in Dialogues: A Game-Theoretic Approach. In: Parsons S, Oren N, Reed C, Cerutti F (eds.), Computational Models of Argument - Proc. of COMMA 2014, Scottish Highlands, UK, 2014, volume 266 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2014 pp. 333-344. doi:10.3233/978-1-61499-436-7-333.
• [15] Kacprzak M, Sawicka A, Zbrzezny A. Dialogue Systems: Modeling and Prediction of their Dynamics. In: Abraham A, Wegrzyn-Wolska K, Hassanien AE, Snásel V, Alimi AM (eds.), Proc. of AECIA 2015, Villejuif (Paris-sud), France, 2015, volume 427 of Advances in Intelligent Systems and Computing. Springer, 2015 pp. 421-431. doi:10.1007/978-3-319-29504-6_40.
• [16] Prakken H. Models of Persuasion Dialogue. In: Argumentation in AI, Springer, 2009 pp. 281-300. doi:10.1007/978-0-387-98197-0_14.
• [17] Jones AV, Lomuscio A. Distributed BDD-based BMC for the verification of multi-agent systems. In: van der Hoek W, Kaminka GA, Lespérance Y, Luck M, Sen S (eds.), 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), Toronto, Canada, 2010, Volume 1-3. IFAAMAS, 2010 pp. 675-682. ISBN: 978-0-9826571-1-9.
• [18] Penczek W, Lomuscio A. Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundam. Inform., 2003;55(2):167-185.
• [19] Lomuscio A, Qu H, Raimondi F. MCMAS: an open-source model checker for the verification of multiagent systems. International Journal on Software Tools for Technology Transfer, 2017;19(1):9-30. doi:10.1007/s10009-015-0378-x.
• [20] Raimondi F, Lomuscio A. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic, Logic-Based Agent Verification. 2007;5(2):235-251. URL https://doi.org/10.1016/j.jal.2005.12.010.
• [21] Wells S, Reed CA. A domain specific language for describing diverse systems of dialogue. J. Applied Logic, 2012;10(4):309-329. doi:10.1016/j.jal.2012.09.001.
• [22] Ekman P. An argument for basic emotions. Cognition and emotion, 1992;6(3-4):169-200. URL http://dx.doi.org/10.1080/02699939208411068.
• [23] Kacprzak M. Persuasive Strategies in Dialogue Games with Emotional Reasoning. In: Lecture Notes in Computer Science, IJCRS (2), volume 10314 of Lecture Notes in Computer Science. Springer, 2017 pp.435-453. doi:10.1007/978-3-319-60840-2_32.
• [24] Kacprzak M, Sawicka A, Zbrzezny A. Modelling the Affective Power of Locutions in a Persuasive Dialogue Game. In: Lecture Notes in Computer Science, ICAISC (2), volume 10842 of Lecture Notes in Computer Science. Springer, 2018 pp. 557-569. doi:10.1007/978-3-319-91262-2_49.
• [25] Sawicka A, Kacprzak M, Zbrzezny A. A Novel Description Language for Two-Agent Dialogue Games. In: IJCRS (2), volume 10314 of Lecture Notes in Computer Science. Springer, 2017 pp. 466-486. doi:10.1007/978-3-319-60840-2_34.
• [26] De Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08. Springer-Verlag, Berlin, Heidelberg, 2008 pp. 337-340. URL http://dl.acm.org/citation.cfm?id=1792734.1792766.
• [27] Dutertre B. Yices 2.2. In: Biere A, Bloem R (eds.), Computer-Aided Verification (CAV’2014), volume 8559 of Lecture Notes in Computer Science. Springer, 2014 pp. 737-744. doi:10.1007/978-3-319-08867-9_49.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).