Advertisement

Employing Costs in Multiagent Systems with Timed Migration and Timed Communication

  • Bogdan AmanEmail author
  • Gabriel Ciobanu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12011)

Abstract

We use a process calculus to describe easily multiagent systems with timeouts for mobility and communication, and with assigned costs for agents actions and for the locations of a distributed network. After presenting an operational semantics and some results regarding this calculus, we provide a translation of the multiagent systems to weighted timed automata having a bisimilar behaviour. Such a translation allows the use of an existing software tool for verification of various properties of the multiagent systems, and for optimizing the costs involved in the distributed networks of mobile agents.

Notes

Acknowledgement

This work was partially supported by the project funded by the Ministry of Research and Innovation within Program 1 - Development of the national RD system, Subprogram 1.2 - Institutional Performance - RDI excellence funding projects, Contract no.34PFE/19.10.2018.

References

  1. 1.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi-calculus. Inf. Comput. 148, 1–70 (1999).  https://doi.org/10.1006/inco.1998.2740MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. Theor. Comput. Sci. 318, 297–322 (2004).  https://doi.org/10.1016/j.tcs.2003.10.038MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Aman, B., Ciobanu, G.: Verification of critical systems described in real-time TiMo. STTT 19, 395–408 (2017).  https://doi.org/10.1007/s10009-016-0439-9CrossRefGoogle Scholar
  4. 4.
    Barbanera, F., Bugliesi, M., Dezani-Ciancaglini, M., Sassone, V.: A calculus of bounded capacities. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 205–223. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-40965-6_14CrossRefGoogle Scholar
  5. 5.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30080-9_7CrossRefGoogle Scholar
  6. 6.
    Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.J.: Model checking AgentSpeak. In: The Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003, pp. 409–416 (2003).  https://doi.org/10.1145/860575.860641
  7. 7.
    Ciobanu, G., Koutny, M.: Modelling and verification of timed interaction and migration. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 215–229. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78743-3_16CrossRefGoogle Scholar
  8. 8.
    Ciobanu, G., Koutny, M.: Timed mobility in process algebra and Petri nets. J. Log. Algebr. Program. 80, 377–391 (2011).  https://doi.org/10.1016/j.jlap.2011.05.002MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Ciobanu, G., Prisacariu, C.: Timers for distributed systems. Electr. Notes Theor. Comput. Sci. 164, 81–99 (2006).  https://doi.org/10.1016/j.entcs.2006.07.013CrossRefGoogle Scholar
  10. 10.
    Eberbach, E.: The \$-calculus process algebra for problem solving: a paradigmatic shift in handling hard computational problems. Theor. Comput. Sci. 383, 200–243 (2007).  https://doi.org/10.1016/j.tcs.2007.04.012MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Giordano, L., Martelli, A., Schwind, C.: Verifying communicating agents by model checking in a temporal action logic. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 57–69. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30227-8_8CrossRefzbMATHGoogle Scholar
  12. 12.
    Hennessy, M., Gaur, M.: Counting the cost in the \(\pi \)-calculus (extended abstract). Electr. Notes Theor. Comput. Sci. 229, 117–129 (2009).  https://doi.org/10.1016/j.entcs.2009.06.042CrossRefzbMATHGoogle Scholar
  13. 13.
    Huang, X., Singh, A., Smolka, S.A.: Using integer clocks to verify clock-synchronization protocols. ISSE 7, 119–130 (2011).  https://doi.org/10.1007/s11334-011-0152-5CrossRefGoogle Scholar
  14. 14.
    Kiehn, A., Arun-Kumar, S.: Amortised bisimulations. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 320–334. Springer, Heidelberg (2005).  https://doi.org/10.1007/11562436_24CrossRefGoogle Scholar
  15. 15.
    Milner, R.: Communicating and Mobile Systems - The \(\pi \)-calculus. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  16. 16.
    Saeedloei, N., Gupta, G.: Timed \(\pi \)-calculus. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 119–135. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-05119-2_8CrossRefGoogle Scholar
  17. 17.
    Tomioka, D., Nishizaki, S., Ikeda, R.: A cost estimation calculus for analyzing the resistance to denial-of-service attack. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 25–44. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-37621-7_2CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Faculty of Computer ScienceAlexandru Ioan Cuza UniversityIaşiRomania

Personalised recommendations