Abstract
Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we used them to represent complex protocols in a very compact way, and we exploited them to dynamically verify actual agents’ interactions with respect to different protocols in both Jason and JADE. The main drawback of our previous approach is the full centralization of the monitoring activity, which is delegated to a unique monitor agent in charge of verifying that the messages exchanged among all the agents are compliant with the protocol. This approach works well for MASs with few agents, but could become unsuitable in communication-intensive and highly-distributed MASs where hundreds of agents should be monitored.
In this paper we define an algorithm for projecting a constrained global type onto a set of agents Ags, by restricting it to the interactions involving agents in Ags, so that the outcome of the algorithm is another constrained global type where interactions involve only agents in Ags. The projection mechanism is the first step towards distributing the monitoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partitioning the agents of the MAS into small sets of agents, and by assigning to each partition Ags a local monitor agent which checks all interactions involving Ags against the projected constrained global type.
Although the projection of well formed constrained global types can be always performed, the resulting projected protocol does not always model all the constraints as the original one. We describe a generate and test algorithm that provides hints on the correctness of the protocol distribution, leaving for further investigation the formal characterization of which protocols can be distributed onto which agents’ subsets.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Ancona, D.: Regular corecursion in Prolog. Computer Languages, Systems & Structures 39(4), 142–162 (2013)
Ancona, D., Barbieri, M., Mascardi, V.: Constrained global types for dynamic checking of protocol conformance in multi-agent systems. In: Shin, S.Y., Maldonado, J.C. (eds.) Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC 2013, pp. 1377–1379 (2013)
Ancona, D., Drossopoulou, S., Mascardi, V.: Automatic Generation of Self-monitoring MASs from Multiparty Global Session Types in Jason. In: Baldoni, M., Dennis, L., Mascardi, V., Vasconcelos, W. (eds.) DALT 2012. LNCS, vol. 7784, pp. 76–95. Springer, Heidelberg (2013)
Baldoni, M., Baroglio, C., Capuzzimati, F.: 2COMM: A commitment-based MAS architecture. In: Cossentino, M., El Fallah Seghrouchni, A., Winikoff, M. (eds.) EMAS 2013. LNCS (LNAI), vol. 8245, pp. 38–57. Springer, Heidelberg (2013)
Baldoni, M., Baroglio, C., Chopra, A.K., Desai, N., Patti, V., Singh, M.P.: Choice, interoperability, and conformance in interaction protocols and service choreographies. In: Sierra, C., Castelfranchi, C., Decker, K.S., Sichman, J.S. (eds.) 8th International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2009, vol. 2, pp. 843–850. IFAAMAS (2009)
Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007)
Bravetti, M., Zavattaro, G.: Contract compliance and choreography conformance in the presence of message queues. In: Bruni, R., Wolf, K. (eds.) WS-FM 2008. LNCS, vol. 5387, pp. 37–54. Springer, Heidelberg (2009)
Briola, D., Mascardi, V., Ancona, D.: Distributed runtime verification of JADE multiagent systems. In: Camacho, D., Braubach, L., Venticinque, S., Badica, C. (eds.) Intelligent Distributed Computing VIII. SCI, vol. 570, pp. 81–92. Springer, Heidelberg (2014)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)
Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Logical Methods in Computer Science 8(1) (2012)
Chen, T.: Lightening global types. In: Donaldson, A.F., Vasconcelos, V.T. (eds.) Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2014. EPTCS, vol. 155, pp. 38–46 (2014)
Chopra, A.K., Dalpiaz, F., Giorgini, P., Mylopoulos, J.: Reasoning about agents and protocols via goals and commitments. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2010, vol. 1, pp. 457–464. IFAAMAS, Richland (2010)
Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Self-adaptive monitors for multiparty sessions. In: 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, pp. 688–696. IEEE (2014)
Drusinsky, D., Shing, M.-T.: Verifying distributed protocols using MSC-assertions, run-time monitoring, and automatic test generation. In: Proceedings of the 18th IEEE/IFIP International Workshop on Rapid System Prototyping, RSP 2007, pp. 82–88 (May 2007)
German, E., Sheremetov, L.B.: An agent framework for processing FIPA-ACL messages based on interaction models. In: Luck, M., Padgham, L. (eds.) AOSE 2007. LNCS, vol. 4951, pp. 88–102. Springer, Heidelberg (2008)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273–284. ACM (2008)
Krüger, I.H., Meisinger, M., Menarini, M.: Runtime verification of interactions: From MSCs to aspects. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 63–74. Springer, Heidelberg (2007)
Lam, S., Shankar, A.U.: Protocol verification via projections. IEEE Transactions on Software Engineering SE-10(4), 325–342 (1984)
Lanese, I., Guidi, C., Montesi, F., Zavattaro, G.: Bridging the gap between interaction- and process-oriented choreographies. In: Cerone, A., Gruner, S. (eds.) Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, pp. 323–332. IEEE Computer Society (2008)
Mascardi, V., Ancona, D.: Attribute global types for dynamic checking of protocols in logic-based multiagent systems. Theory and Practice of Logic Programming, 13(4-5-Online-Supplement) (2013)
Mascardi, V., Briola, D., Ancona, D.: On the expressiveness of attribute global types: The formalization of a real multiagent system protocol. In: Baldoni, M., Baroglio, C., Boella, G., Micalizio, R. (eds.) AI*IA 2013. LNCS (LNAI), vol. 8249, pp. 300–311. Springer, Heidelberg (2013)
Meron, D., Mermet, B.: A tool architecture to verify properties of multiagent system at runtime. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.) PROMAS 2006. LNCS (LNAI), vol. 4411, pp. 201–216. Springer, Heidelberg (2007)
Modgil, S., Faci, N., Meneguzzi, F., Oren, N., Miles, S., Luck, M.: A framework for monitoring agent-based normative systems. In: Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2009, vol. 1, pp. 153–160. IFAAMAS, Richland (2009)
Neykova, R., Yoshida, N., Hu, R.: SPY: Local verification of global protocols. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 358–363. Springer, Heidelberg (2013)
Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the theoretical foundation of choreography. In: Proceedings of the 16th International Conference on World Wide Web, WWW 2007, pp. 973–982. ACM, New York (2007)
Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. (2009)
Winikoff, M.: Implementing flexible and robust agent interactions using distributed commitment machines. Multiagent and Grid Systems 2(4), 365–381 (2006)
Wörn, H., Längle, T., Albert, M., Kazi, A., Brighenti, A., Seijo, S.R., Senior, C., Bobi, M.A.S., Collado, J.: DIAMOND: Distributed multi-agent architecture for monitoring and diagnosis. Production Planning & Control 15(2), 189–200 (2004)
Yolum, P., Singh, M.P.: Commitment machines. In: Meyer, J.-J.C., Tambe, M. (eds.) ATAL 2001. LNCS (LNAI), vol. 2333, pp. 235–247. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Ancona, D., Briola, D., El Fallah Seghrouchni, A., Mascardi, V., Taillibert, P. (2014). Efficient Verification of MASs with Projections. In: Dalpiaz, F., Dix, J., van Riemsdijk, M.B. (eds) Engineering Multi-Agent Systems. EMAS 2014. Lecture Notes in Computer Science(), vol 8758. Springer, Cham. https://doi.org/10.1007/978-3-319-14484-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-14484-9_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14483-2
Online ISBN: 978-3-319-14484-9
eBook Packages: Computer ScienceComputer Science (R0)