Published in Volume XXII, Issue 2, 2012, pages 267-326, doi: 10.7561/SACS.2012.2.267
Authors: F. Damiani, P. Giannini, A. Ricci, M. Viroli
Abstract
Formal models, core calculi, and type systems, are important tools for rigorously stating the more subtle details of a language, to characterise and study its features and the correctness properties of its programs. In this paper we present {FsimpAL} (FsimpaALlong), a formal calculus modelling the agent and artifact program abstractions provided by the simpA{} agent framework. The formalisation is largely inspired by textsc{Featherweight Java}. It is based on reduction rules applied at certain evaluation contexts, properly adapted to the concurrency nature of simpA{}. On top of this calculus we introduce a standard type system and prove its soundness, so as to guarantee that the execution of a well-typed program does not get stuck. Namely, all primitive mechanisms of agents (activity execution), artifacts (field/property access and step execution), and their interaction (observation and invocation) are guaranteed to be used in a way that is structurally compliant with the corresponding definitions: hence, there will not be run-time errors due to {FsimpAL} distinctive primitives.
Full Text (PDF)References
[1] M. Abadi and L. Cardelli. A Theory of Objects. Springer, 1996.
[2] Gul Agha. Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge, MA, USA, 1986.
[3] Gul Agha, Peter Wegner, and Akinori Yonezawa, editors. Research directions in concurrent object-oriented programming. MIT Press, Cambridge, MA, USA, 1993.
[4] Joe Armstrong. Erlang. Commun. ACM, 53:68-75, September 2010. http://dx.doi.org/10.1145/1810891.1810910 .
[5] Fabio Luigi Bellifemine, Giovanni Caire, and Dominic Greenwood. De- veloping Multi-Agent Systems with JADE. Wiley, 2007.
[6] Nick Benton, Luca Cardelli, and Cedric Fournet. Modern concurrency abstractions for C#. ACM Trans. Program. Lang. Syst., 26(5):769-804, 2004. http://dx.doi.org/10.1145/1018203.1018205 .
[7] R. H. Bordini, M. Dastani, J. Dix, and A. El Fallah Seghrouchni, editors. Multi-Agent Programming: Languages, Platforms and Applications (vol. 2). Springer, 2009.
[8] Rafael Bordini, Mendi Dastani, Jurgen Dix, and Amal El Fallah Seghrouchni, editors. Multi-Agent Programming: Languages, Platforms and Applications (vol. 1). Springer, 2005.
[9] Rafael Bordini, Jomi Hubner, and Mike Wooldridge. Programming Multi-Agent Systems in AgentSpeak Using Jason. John Wiley & Sons, Ltd, 2007.
[10] Jean-Pierre Briot, Rachid Guerraoui, and Klaus-Peter Lohr. Concurrency and distribution in object-oriented programming. ACM Comput. Surv., 30(3):291-329, 1998. http://dx.doi.org/10.1145/292469.292470.
[11] Tony Clark. Speci cation and implementation of a multi-agent calculus based on higher-order functions. Technical report, Department of Computing, University of Bradford, 1999.
[12] J-L. Colaco, M. Pantel, and P. Sall. CAP: An actor dedicated process calculus. In In the ECOOP96 Workshop on Proof Theory of Concurrent Object-Oriented Programming (PTCOOP96), 1996.
[13] Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. On Re-classi cation and Multi-threading. Journal of Object Technology (www.jot.fm), 3(11):5-30, 2004. http://dx.doi.org/10.5381/jot.2004.3.11.a1 .
[14] Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Re-classi cation and multi-threading: FickleMT. In Proceedings of the 2004 ACM symposium on Applied computing, SAC ’04, pages 1297-1304, New York, NY, USA, 2004. ACM. http://dx.doi.org/10.1145/967900.968163 .
[15] Ferruccio Damiani, Elena Giachino, Paola Giannini, and Emanuele Cazzola. On state classes and their dynamic semantics. In Joaquim Filipe, Boris Shishkov, and Markus Helfert, editors, Software and Data Technologies, volume 10 of Communications in Computer and Information Science, pages 84-96. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-70621-2_8 .
[16] Ferruccio Damiani, Elena Giachino, Paola Giannini, and Sophia Drossopoulou. A type safe state abstraction for coordination in Java-like languages. Acta Informatica, 45(7-8):479-536, 2008. http://dx.doi.org/10.1007/s00236-008-0079-y .
[17] Ferruccio Damiani, Paola Giannini, Alessandro Ricci, and Mirko Viroli. FEATHERWEIGHT AGENT LANGUAGE – A Core Calculus for Agents and Artifacts. In ICSOFT 2009 – Proceedings of the 4th International Conference on Software and Data Technologies, volume 1, pages 218-225. INSTICC Press, 2009.
[18] Ferruccio Damiani, Paola Giannini, Alessandro Ricci, and Mirko Viroli. A calculus of agents and artifacts. In Jose Cordeiro, AlpeshKumar Ranchordas, and Boris Shishkov, editors, Software and Data Technologies, volume 50 of Communications in Computer and Information Science, pages 124-136. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-20116-5_10 .
[19] Mehdi Dastani. 2APL: a Practical Agent Programming Language. Autonomous Agents and Multi-Agent Systems, 16(3):214-248, 2008. http://dx.doi.org/10.1007/s10458-008-9036-y .
[20] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. KLAIM: A Kernel Language for Agents Interaction and Mobility. IEEE Trans. Software Eng., 24(5):315-330, 1998. http://dx.doi.org/10.1109/32.685256 .
[21] Louise A. Dennis, Berndt Farwer, Rafael H. Bordini, Michael Fisher, and Michael Wooldridge. A common semantic basis for BDI languages. In Mehdi Dastani, Amal El Fallah Seghrouchni, Alessandro Ricci, and Michael Winiko#, editors, Programming Multi-Agent Systems, volume 4908 of Lecture Notes in Computer Science, pages 124-139. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-79043-3_8 .
[22] Rogier M. van Eijk, Frank S. de Boer, Wiebe van der Hoek, and John-Jules Ch. Meyer. Operational semantics for agent communication languages. In Issues in Agent Communication, pages 80-95, London, UK, UK, 2000. Springer. http://dx.doi.org/10.1007/10722777_6 .
[23] Jacques Ferber and Olivier Gutknecht. Operational semantics of multi-agent organizations. In Intelligent Agents VI, Agent Theories, Architectures, and Languages (ATAL), volume 1757 of Lecture Notes in Computer Science, pages 205-217. Springer, 2000. http://dx.doi.org/10.1007/10719619_15 .
[24] C#edric Fournet and Georges Gonthier. The Join Calculus: A Language for Distributed Mobile Programming. In Applied Semantics, Interna- tional Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, pages 268-332, London, UK, 2002. Springer. http://dx.doi.org/10.1007/3-540-45699-6_6 .
[25] C#edric Fournet, Georges Gonthier, Jean-Jacques L#evy, Luc Maranget, and Didier R#emy. A calculus of mobile agents. In Proceedings of the 7th International Conference on Concurrency Theory, CONCUR ’96, pages 406-421, London, UK, 1996. Springer. http://dx.doi.org/10.1007/3-540-61604-7_67 .
[26] Philipp Haller and Martin Odersky. Actors that unify threads and events. In Proceedings of the 9th international conference on Coordination models and languages, COORDINATION’07, pages 171-190, Berlin, Heidelberg, 2007. Springer. http://dx.doi.org/10.1007/978-3-540-72794-1_10 .
[27] Matthew Hennessey and James Riely. Type-safe execution of mobile agents in anonymous networks. In Jan Vitek and Christian D. Jensen, editors, Secure Internet programming, pages 95-115. Springer, London, UK, UK, 1999. http://dx.doi.org/10.1007/3-540-48749-2_5 .
[28] Matthew Hennessy and James Riely. Resource access control in systems of mobile agents. Inf. Comput., 173(1):82-120, February 2002. http://dx.doi.org/10.1006/inco.2001.3089 .
[29] Koen Hindriks, Frank de Boer, Wiebe van der Hoek, and John-Jules Meyer. Formal semantics for an abstract agent programming language. In Munindar Singh, Anand Rao, and Michael Wooldridge, editors, Intelligent Agents IV Agent Theories, Architectures, and Languages, volume 1365 of Lecture Notes in Computer Science, pages 215-229. Springer, 1998. http://dx.doi.org/10.1007/BFb0026761 .
[30] Koen V. Hindriks. Programming rational agents in GOAL. In R. H. Bordini, M. Dastani, J. Dix, and A. El Fallah Seghrouchni, editors, Multi-Agent Programming: Languages, Platforms and Applications (2nd volume), pages 3-37. Springer, 2009.
[31] Kohei Honda and Mario Tokoro. An object calculus for asynchronous communication. In Pierre America, editor, ECOOP’91 European Conference on Object-Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 133-147. Springer, 1991. http://dx.doi.org/10.1007/BFb0057019 .
[32] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems (ESOP), volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. http://dx.doi.org/10.1007/BFb0053567 .
[33] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming lan- guages, POPL ’08, pages 273-284, New York, NY, USA, 2008. ACM. http://dx.doi.org/10.1145/1328438.1328472 .
[34] A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396-450, 2001. http://dx.doi.org/10.1145/503502.503505 .
[35] Atsushi Igarashi. A Featherweight Approach to FOOL. In Mira Mezini, editor, ECOOP 2011 – Object-Oriented Programming – 25th European Conference, Lancaster, UK, July 25-29, 2011 Proceedings, volume 6813 of Lecture Notes in Computer Science, page 433. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-22655-7 .
[36] G. S. Itzstein and D. Kearney. Join Java: an alternative concurrency semantics for Java. Technical Report ACRC-01-001, Univ. of South Australia, 2001.
[37] Nicholas R. Jennings. An agent-based approach for building complex software systems. Commun. ACM, 44(4):35-41, 2001. http://dx.doi.org/10.1145/367211.367250 .
[38] Christoph G. Jung and Klaus Fischer. A layered agent calculus with concurrent, continuous processes. In Proceedings of the 4th International Workshop on Intelligent Agents IV, Agent Theories, Architectures, and Languages, pages 245-258, London, UK, 1998. Springer. http://dx.doi.org/10.1007/BFb0026763 .
[39] Rajesh K. Karmani and Gul Agha. Actors. In Encyclopedia of Parallel Computing, pages 1-11. Springer, 2011.
[40] Rajesh Kumar Karmani, Amin Shali, and Gul Agha. Actor frameworks for the JVM platform: A Comparative Analysis. In In the proceedings of the 7th International Conference on the Principles and Practice of Programming in Java (PPPJ), pages 11-20, 2009. http://dx.doi.org/10.1145/1596655.1596658 .
[41] Naoki Kobayashi. Type systems for concurrent programs. In Bernhard Aichernig and Tom Maibaum, editors, Formal Methods at the Crossroads. From Panacea to Foundational Support, volume 2757 of Lecture Notes in Computer Science, pages 439-453. Springer, 2003. http://dx.doi.org/10.1007/978-3-540-40007-3_26 .
[42] Open System Laboratory. ActorFoundry, http://osl.cs.uiuc.edu/af/ .
[43] Y. Lesperance, H. J. Levesque, and R. Reiter. A situation calculus approach to modeling and programming agents. In Foundations of Rational Agency, pages 275-299. Kluwer, 1999.
[44] T. Massart. An agent calculus with simple actions where the enabling and disabling are derived operators. Information Processing Letters, 40(4):213 – 218, 1991. http://dx.doi.org/10.1016/0020-0190(91)90080-2 .
[45] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, i. Inf. Comput., 100(1):1-40, September 1992. http://dx.doi.org/10.1016/0890-5401(92)90008-4 .
[46] Alvaro F. Moreira, Renata Vieira, and Rafael H. Bordini. Extending the Operational Semantics of a BDI Agent-Oriented Programming Language for Introducing Speech-Act Based Communication. In Joao Leite, Andrea Omicini, Leon Sterling, and Paolo Torroni, editors, Declarative Agent Languages and Technologies, volume 2990 of Lecture Notes in Computer Science, pages 135-154. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-25932-9_8 .
[47] Andrea Omicini, Alessandro Ricci, and Mirko Viroli. Artifacts in the A&A Meta-Model for Multi-Agent Systems. Autonomous Agents and Multi-Agent Systems, 17, 2008. Special Issue on Foundations, Advanced Topics and Industrial Perspectives of Multi-Agent Systems. http://dx.doi.org/10.1007/s10458-008-9053-x .
[48] Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, 1996. http://dx.doi.org/10.1109/LICS.1993.287570 .
[49] A. S. Rao and M. P. George#. BDI Agents: From Theory to Practice. In First International Conference on Multi Agent Systems (ICMAS95), 1995.
[50] Anand S. Rao. AgentSpeak(L): BDI agents speak out in a logical computable language. In Proceedings of the 7th European workshop on Modelling autonomous agents in a multi-agent world : agents breaking away: agents breaking away, MAAMAW ’96, pages 42-55, Secaucus, NJ, USA, 1996. Springer.
[51] Alessandro Ricci and Andrea Santi. Typing Multi-Agent Programs in simpAL. In Proceedings of the Tenth International Workshop on Programming Multi-Agent Systems (ProMAS’12), pages 132-147, 2012.
[52] Alessandro Ricci, Mirko Viroli, and Maurizio Cimadamore. Prototyping Concurrent Systems with Agents and Artifacts: Framework and Core Calculus. Electron. Notes Theor. Comput. Sci., 194(4):111-132, 2008. http://dx.doi.org/10.1016/j.entcs.2008.03.102 .
[53] Alessandro Ricci, Mirko Viroli, and Giulio Piancastelli. simpA: An agent-oriented approach for programming concurrent applications on top of Java. Science of Computer Programming, 76(1):37 – 62, 2011. Selected papers from the 6th InternationalWorkshop on the Foundations of Coordination Languages and Software Architectures – FOCLASA’07. http://dx.doi.org/10.1016/j.scico.2010.06.012 .
[54] Stuart Russell and Peter Norvig. Arti cial Intelligence, A Modern Approach (second edition). Prentice Hall, 2003.
[55] Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. Location-independent communication for mobile agents: A two-level architecture. In ICCL Workshop: Internet Programming Languages, volume 1686 of Lecture Notes in Computer Science, pages 1-31. Springer, 1998. http://dx.doi.org/10.1007/3-540-47959-7_1 .
[56] Peter Sewell, Pawel T. Wojciechowski, and Asis Unyapoth. Nomadic pict: Programming languages, communication infrastructure overlays, and semantics for mobile computation. ACM Trans. Program. Lang. Syst., 32(4), 2010. http://dx.doi.org/10.1145/1734206.1734209 .
[57] Alexandru Suna and Amal El Fallah-Seghrouchni. Programming mobile intelligent agents: An operational semantics. Web Intelligence and Agent Systems, 5(1):47-67, 2007.
[58] Herb Sutter and James Larus. Software and the concurrency revolution. ACM Queue: Tomorrow’s Computing Today, 3(7):54-62, September 2005. http://dx.doi.org/10.1145/1095408.1095421 .
[59] Danny Weyns, Andrea Omicini, and James J. Odell. Environment as a rst-class abstraction in multi-agent systems. Autonomous Agents and Multi-Agent Systems, 14(1):5-30, February 2007. Special Issue on Environments for Multi-agent Systems. http://dx.doi.org/10.1007/s10458-006-0012-0 .
[60] Michael Wooldridge and Nicholas R. Jennings. Intelligent agents: Theory and practice. Knowledge Engineering Review, 10:115-152, 1995. http://dx.doi.org/10.1017/S0269888900008122 .
[61] Mike Wooldridge. An Introduction to Multi-Agent Systems. John Wiley & Sons, Ltd, 2002.
[62] A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 1(115):38-94, 1994. http://dx.doi.org/10.1006/inco.1994.1093 .
[63] A Yonezawa and M Tokoro, editors. Object-oriented concurrent pro- gramming. MIT Press, Cambridge, MA, USA, 1986.
[64] Nobuko Yoshida and Matthew Hennessy. Assigning types to processes. Inf. Comput., 174(2):143-179, May 2002. http://dx.doi.org/10.1006/inco.2002.3113 .
Bibtex
@article{sacscuza:damiani2012stsfaaa,
title={Standard Type Soundness for Agents and Artifacts},
author={F. Damiani and P. Giannini and A. Ricci and M. Viroli},
journal={Scientific Annals of Computer Science},
volume={22},
number={2},
organization={``A.I. Cuza'' University, Iasi, Romania},
year={2012},
pages={267--326},
doi={10.7561/SACS.2012.2.267},
publisher={``A.I. Cuza'' University Press}
}