Abstract
Side effects are an important characteristic of MAS, and proving them is an interesting issue. They often can be expressed as liveness properties. But there is no system dedicated to this kind of proof. The GDT4MAS framework allows to specify and prove the correctness of multiagent systems. This framework is mainly dedicated to prove safety properties about the system and to prove that agents achieve their goal(s). However, there is no proof principle to prove that agents satisfy liveness properties that are not part of their goal(s). In this article, we propose a proof mechanism that addresses this kind of problem: we show how we can add to GDT4MAS a proof mechanism adapted to prove leads-to properties, a subclass of liveness properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Mermet, B., Simon, G.: GDT4MAS: An extension of the GDT model to specify and to verify MultiAgent Systems. In: Decker, et al. (eds.) Proc. of AAMAS 2009, pp. 505–512 (2009)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)
Lamport, L.: The syntax and semantics of TLA? + ?. Part 1: Definitions and Modules (June 1996)
Milner, R., Parrow, J., Wlaker, D.: A calculus of mobile processes. Journal of Information and Computation 100 (1992)
Mermet, B., Simon, G., Zanuttini, B., Saval, A.: Specifying and verifying a MAS:The robots on mars case study. In: Dastani, M., El Fallah Seghrouchni, A., Ricci, A., Winikoff, M. (eds.) ProMAS 2007. LNCS (LNAI), vol. 4908, pp. 172–189. Springer, Heidelberg (2008)
SRI International: PVS, http://pvs.csl.sri.com
Dastani, M.: 2APL: A practical agent programming language. Journal of Autonomous Agents and Multi-Agent Systems 16, 214–248 (2008)
Fisher, M.: A survey of concurrent METATEM – The language and its applications. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol. 827, pp. 480–505. Springer, Heidelberg (1994)
Dennis, L., Fisher, M., Webster, M., Bordini, R.: Model checking agent programming languages. Automated Software Engineering 19(1), 5–63 (2012)
NASA: Java Path Finder, http://babelfish.arc.nasa.gov/trac/jpf
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Softw. Eng. 23, 279–295 (1997)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)
Abrial, J.R.: Formal methods in industry: achievements, problems, future. In: International Conference on Software Engineering, pp. 761–768 (2006)
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
Mermet, B., Simon, G. (2014). Side Effects of Agents Are Not Just Random. 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_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-14484-9_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14483-2
Online ISBN: 978-3-319-14484-9
eBook Packages: Computer ScienceComputer Science (R0)