Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Theoretical Aspects of Computing

ICTAC 2019: Theoretical Aspects of Computing – ICTAC 2019 pp 134–151Cite as

Verification of Multi-agent Systems with Timeouts for Migration and Communication

  • Conference paper
  • First Online:

  • 349 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11884))

Abstract

A prototyping high-level language is used to describe multi-agent systems using timeouts for migration between explicit locations and local communication in a distributed system. We translate such a high-level specification into the real-time Maude rewriting language. We prove that this translation is correct, and provide an operational correspondence between the evolutions of the mobile agents with timeouts and their rewriting translations. These results allow to analyze the multi-agent systems with timeouts for migration and communication by using the real-time Maude tools. A running example is used to illustrate the whole approach.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  2. Aman, B., Ciobanu, G.: Real-time migration properties of rTiMo verified in Uppaal. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 31–45. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40561-7_3

    Chapter  Google Scholar 

  3. 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_7

    Chapter  Google Scholar 

  4. Ciobanu, G., Juravle, C.: Flexible software architecture and language for mobile agents. Concurrency Comput. Pract. Experience 24, 559–571 (2012)

    Article  Google Scholar 

  5. Ciobanu, G., Koutny, M.: Timed mobility in process algebra and Petri nets. J. Logic Algebraic Program. 80, 377–391 (2011)

    Article  MathSciNet  Google Scholar 

  6. Ciobanu, G., Koutny, M.: Timed migration and interaction with access permissions. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 293–307. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_23

    Chapter  Google Scholar 

  7. Ciobanu, G., Prisacariu, C.: Timers for distributed systems. Electron. Not. Theor. Comput. Sci. 164, 81–99 (2006)

    Article  Google Scholar 

  8. Ciobanu, G., Zheng, M.: Automatic analysis of TiMo systems in PAT. In: IEEE Computer Society Proceedings 18th Engineering of Complex Computer Systems (ICECCS), pp. 121–124 (2013)

    Google Scholar 

  9. Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 217–273 (1992)

    Article  MathSciNet  Google Scholar 

  10. Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_3

    Chapter  Google Scholar 

  11. Meseguer, J.: Twenty years of rewriting logic. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 15–17. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_2

    Chapter  MATH  Google Scholar 

  12. Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)

    Book  Google Scholar 

  13. Ölveczky, P.C.: Real-time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42–79. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12904-4_3

    Chapter  Google Scholar 

  14. Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time Maude. Higher-Order Symbolic Comput. 20, 161–196 (2007)

    Article  Google Scholar 

  15. Thati, P., Sen, K., Martí-Oliet, N.: An executable specification of asynchronous \(\pi \)-calculus semantics and may testing in Maude 2.0. Electron. Not. Theor. Comput. Sci. 71, 261–281 (2004)

    Article  Google Scholar 

  16. Xie, W., Xiang, S.: UTP semantics for rTiMo. In: Bowen, J.P., Zhu, H. (eds.) UTP 2016. LNCS, vol. 10134, pp. 176–196. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52228-9_9

    Chapter  Google Scholar 

  17. Xie, W., Zhu, H., Zhang, M., Lu, G., Fang, Y.: Formalization and verification of mobile systems calculus using the rewriting engine Maude. In: IEEE 42nd Annual Computer Software and Applications Conference, pp. 213–218 (2018)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Computer Science, Alexandru Ioan Cuza University, Iasi, Romania

    Bogdan Aman & Gabriel Ciobanu

  2. Institute of Computer Science, Romanian Academy, Iasi, Romania

    Bogdan Aman & Gabriel Ciobanu

Authors
  1. Bogdan Aman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gabriel Ciobanu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gabriel Ciobanu .

Editor information

Editors and Affiliations

  1. University of Sheffield, Sheffield, UK

    Robert Mark Hierons

  2. University of Bordeaux, Talence, France

    Mohamed Mosbah

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Aman, B., Ciobanu, G. (2019). Verification of Multi-agent Systems with Timeouts for Migration and Communication. In: Hierons, R., Mosbah, M. (eds) Theoretical Aspects of Computing – ICTAC 2019. ICTAC 2019. Lecture Notes in Computer Science(), vol 11884. Springer, Cham. https://doi.org/10.1007/978-3-030-32505-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32505-3_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32504-6

  • Online ISBN: 978-3-030-32505-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation