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 Theo-
ries, 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}
}