On the SMT-based verification of communicative commitments

• Autorzy: Woźna-Szcześniak B. , Szcześniak I.

Identyfikatory

DOI

10.16926/m.2016.21.14

• Języki publikacji: EN

Abstrakty

EN

We propose an SMT-based bounded model checking (BMC) technique for the existential fragments of CCTL*K – an epistemic temporal logic extended to include modalities for different social commitments – and for multi-agent systems modelled by Communication Interpreted Systems (CIS). Furthermore, we exemplify the use of the technique by means of the NetBill protocol, a popular example in the MAS literature related to the modelling of business processes.

Słowa kluczowe

EN

communications commutments; langue of communication; CCTL language

PL

zobowiązania komunikacyjne; język komunikacji; semantyka mentalna; język CCTL

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2016
• Tom: Vol. 21
• Strony: 161--187
• Opis fizyczny: Bibliogr. 21 poz., rys.

Twórcy

autor

Woźna-Szcześniak B.

• Jan Długosz University in Częstochowa, Institute of Mathematics and Computer Science, al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Szcześniak I.

• Częstochowa University of Technology, Institute of Computer and Information Sciences, ul. Dąbrowskiego 69, 42-201 Częstochowa, Poland

Bibliografia

• [1] Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 26, pages 825–885. IOS Press, 2009. DOI:10.3233/978-1-58603-929-5-825.
• [2] A. Biere, K. Heljanko, T. Junttila, T. Latvala, and V. Schuppan. Linear encodings of bounded LTL model checking. Logical Methods in Computer Science, 2(5:5):1–64, 2006. DOI:10.2168/LMCS-2(5:5)2006.
• [3] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2:2000, 2000. DOI:10.1.1.19.4520.
• [4] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. ISBN: 0-262-03270-8.
• [5] M. El-Menshawy, J. Bentahar, and R. Dssouli. Verifiable semantic model for agent interactions using social commitments. In Proceedings of the 2nd International Conference on Languages, Methodologies, and Development Tools for Multi-Agent Systems (LADS’2009), volume 6039 of LNAI, pages 128–152. Springer-Verlag, 2010. DOI:10.1007/978-3-642-13338-1_8.
• [6] M. El-Menshawy, J. Bentahar, W. El Kholy, and R. Dssouli. Reducing model checking commitments for agent communication to model checking arctl and GCTL_. Autonomous Agents and Multi-Agent Systems, 27(3):375–418, 2013. DOI: 10.1007/s10458-012-9208-7.
• [7] E. A. Emerson and J. Y. Halpern. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. Journal of ACM, 33(1):151–178, 1986. DOI:10.1145/4904.4999.
• [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [9] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV’2009), volume 5643 of LNCS, pages 682–688. Springer-Verlag, 2009. DOI:10.1007/978-3-642-02658-4_55.
• [10] A.U. Mallya and M.P. Singh. An algebra for commitment protocols. Autonomous Agents and Multi-Agent Systems, 14(2):143–163, 2007. DOI: 10.1007/s10458-006- 7232-1.
• [11] Artur M¸eski, W. Penczek, M.Szreter, B. Wozna-Szczesniak, and A. Zbrzezny. BDDversus 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, 28(4):558–604, 2014. DOI: 10.1007/s10458-013-9232-2.
• [12] M. El Menshawy, J. Benthar, H. Qu, and R. Dssouli. On the verification of social commitments and time. In Proceedings of the 10th International Conference on Autonomous Agents and Multiaagent Systems (AAMAS’2011), pages 483–490. IFAAMAS, 2011.
• [13] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167–185, 2003.
• [14] M. P. Singh. A social semantics for agent communication languages. In Issues in Agent Communication, volume 1916 of LNCS, pages 31–45. Springer-Verlag, 2000. DOI:10.1007/10722777_3.
• [15] Marvin A. Sirbu. Credits and debits on the internet. IEEE Spectrum, 34(2):23–29, 1997.
• [16] M.Wooldridge. An introduction to multi-agent systems - Second Edition. John Wiley & Sons, 2009.
• [17] B. Woźna-Szcześniak. Sat-based bounded model checking for weighted deontic interpreted systems. Fundamenta Informaticae, 143(1-2):173–205, 2016. DOI: 10.3233/FI-2016-1310.
• [18] Bożena Woźna-Szcześniak. Trends in Contemporary Computer Science, chapter Formal Methods and Data Mining. On the SAT-based Verification of Communicative Commitments, pages 175–186. Białystok University of Technology Publishing Office, 2014.
• [19] L. Wu, J. Su, K. Su, X. Luo, and Z. Yang. A concurrent dynamic logic of knowledge, belief and certainty for multi-agent systems. Knowledge-Based Systems, 23(2):162– 168, 2010. DOI:10.1007/978-3-642-01818-3_16.
• [20] A. Zbrzezny. A new translation from ECTL_ to SAT. Fundamenta Informaticae, 120(3-4):377–397, 2012. DOI: 10.3233/FI-2012-768.
• [21] D. Zhang, R. Cleaveland, and E. W. Stark. The integrated cwb-nc/pioatool for functional verification and performance analysis of concurrent systems. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’03, pages 431–436. Springer-Verlag, 2003. DOI:10.1007/3-540-36577-X_31.