• Develop extensions of COIL to provide mobile and dynamic contexts. This would enable the modelling of contexts specific to a given agent, and following it in its migrations, in a manner close to the ambient calculus [9].
• A Java code generator to implement mobile agents automatically from their CO-OPN/2 specifications. This work is based on the results described in [7][10] and on the J-SEAL2 mobile agent framework [4] as concrete target platform.
• Transformation of subsets of CO-OPN/2 into CPN-AMI coloured Petri nets [12] in order to formally verify CO-OPN/2 models with the analysis techniques available for classical Petri nets. Currently, only simulation is possible for analyzing CO-OPN/2 models, due to indecidability problems which are similar to those found in all coloured Petri nets which allow an infinite number of colours. Although this is not the purpose of this paper, verification is one of the important uses of for-mal methods; these aspects will be studied in the future, with emphasis on how to express properties related to the locality and globality of activities.
7. Conclusion
This paper described how it is possible to use the CO-OPN/2 language for the formal specification of distributed applications involving mobile agents. To our knowledge, this is the first proposal for modelling true mobility with structured Petri nets, i.e.
consisting not only of dynamic updating of communication channels, but also describing a complete change of the agent’s local environment and visibility. Related proposals can be found, e.g. in [1], but focusing more on providing a concise semantics, and less on software development principles, thus resulting in a radically different solution, lacking e.g. the notion of modularity.
We refer the reader to the survey performed in [11] for a wider study of formal methods developed for mobile agents. The ben-efits a software engineer can obtain from our approach are: the safety of a modelling language with well-defined semantics, a strong integration in the development process, as well as a resulting specification with a clear graphical presentation and a struc-ture and semantics close to current implementation paradigms. In this work, we put emphasis on formal design principles; we believe one valuable result is that it will thus be possible to model and validate many new distributed algorithm issues found in mobile agent applications.
Acknowledgements
The authors would like to thank Alex Villazon, Mathieu Buffo, Giovanna Di Marzo and Olivier Biberstein for their valuable contributions. This work was funded by the Swiss National Science Foundation under grants 20-54014.98 and 20-47030.96.
Bibliography
[1] Andrea Asperti and Nadia Busi, “Mobile Petri Nets”, Technical Report UBLCS-96-10, Laboratory for Computer Science, University of Bologna, Italy, 1996.
[2] Stéphane Barbey, Didier Buchs and Cécile Péraire, “A Theory of Specification-Based Testing for Object-Oriented Soft-ware”, in proceedings of EDCC2 (European Dependable Computing Conference), Taormina, Italy, October 1996, Lecture Notes in Computer Science vol. 1150, Springer-Verlag, 1996, pp. 303-320.
[3] Olivier Biberstein, Didier Buchs, and Nicolas Guelfi, ’’Object-oriented nets with algebraic specifications: The CO-OPN/2
formalism’’, In G. Agha, F. De Cindio and G. Rozenberg, editors, Advances in Petri Nets on Concurrent Object-Oriented
Programming and Petri Nets, Lecture Notes in Computer Science. Springer-Verlag, LNCS 2001, pp. 70-127.
[4] W. Binder, “J-SEAL2, A secure high-performance mobile agent system”, in proceedings of the IAT'99 Workshop on Agents in Electronic Commerce, Hong Kong, Dec. 1999.
[5] Didier Buchs and Nicolas Guelfi, “A Formal Specification Framework for Object-Oriented Distributed Systems”, IEEE Transaction on Software Engineering, vol. 26, no. 7, July 2000, pp. 635-652.
[6] Mathieu Buffo and Didier Buchs, “A Coordination Model for Distributed Object Systems”, Proceedings of the Second International Conference on Coordination Models and Languages COORDINATION’97, September 1997, Lecture Notes in Computer Science, vol. 1282, Springer Verlag, 1997.
[7] Didier Buchs and Jarle Hulaas, “Evolutive Prototyping of Heterogeneous Distributed Systems Using Hierarchical Alge-braic Petri Nets”, Procs. IEEE International Conference on Systems, Man and Cybernetics, SMC’96, Beijing, China, Oct.
14-17 1996, pp. 3021-3026.
[8] Didier Buchs, Jarle Hulaas and Pascal Racloz, “Exploiting Various Levels of Semantics in CO-OPN for the SANDS Envi-ronment Tools”, Tool Presentations, International Conference on Application and Theory of Petri Nets ICATPN’97, Tou-louse, France, 1997, 1997, pp. 34-43.
[9] L. Cardelli and A.D. Gordon, “Mobile ambients”, in Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), European Joint Conferences on Theory and Practice of Software (ETAPS), Springer Verlag, Ber-lin, Germany, 1998.
[10] Stanislav Chachkov and Didier Buchs, “From Formal Specifications to Ready-to-Use Software Components: The Con-current Object Oriented Petri Net Approach”, accepted for publication at the International Conference on Application of Concurrency to System Design (ICACSD 2001), Newcastle upon Tyne, U.K., 25-29 June, 2001.
[11] G. Di Marzo, M. Muhugusa, C. F. Tschudin, “A Survey of Theories for Mobile Agents”, World Wide Web Journal, Spe-cial Issue on Distributed World Wide Web Processing: Applications and Techniques of Web Agents, pp. 139-153, Baltzer Science Publishers, 1998.
[12] Pascal Estrailler and Claude Girault, “Applying Petri Net Theory to the Modeling, Analysis and Prototyping of Distrib-uted Systems”, in Proc. of the IEEE/SICE Int.Workshop on Emerging Technologies For Factory Automation: State of the Art and Future Directions, Australia, August 1992.
[13] Robin Milner, “The polyadic pi-calculus: a Tutorial”, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, No. ECS-LFCS-91-180, 1991, Appeared in Proceedings of the Interna-tional Summer School on Logic and Algebra of Specification, Marktoberdorf, August 1991. Reprinted in Logic and Alge-bra of Specification, eds. F. L. Bauer, W. Brauer, and H. Schwichtenberg, Springer-Verlag, 1993.
[14] R. Valk, “Concurrency in Communicating Object Petri Nets”, In G. Agha, F. De Cindio and G. Rozenberg, editors, Advances in Petri Nets on Concurrent Object-Oriented Programming and Petri Nets, Lecture Notes in Computer Science.
Springer-Verlag, LNCS 2001, pp. 164-195.
[15] C. Lakos, “Object Oriented Modeling with Object Petri Nets”, In G. Agha, F. De Cindio and G. Rozenberg, editors, Advances in Petri Nets on Concurrent Object-Oriented Programming and Petri Nets, Lecture Notes in Computer Science.
Springer-Verlag, LNCS 2001, pp. 1-37.
[16] J. Vitek and G. Castagna, “Seal: A framework for secure mobile computations”, In Internet Programming Languages,
1999.
Verication of Multi Agent Systems
MichaelKohler HeikoRolke
UniversityofHamburg,DepartmentofComputerScience
Vogt-Kolln-Strae30,D-22527 Hamburg
{koehler, roelke}@informatik.uni-hambu rg.de
Abstract
Forcomplexsoftwaresystemsanagent-orienteddesignisassumed. Thequestionof
mod-elingandvericationisourresearcharea. Inthispresentationweoutlineanuniedapproach
formultiagentsystemswithrespecttomodelingandverication.
Thisgeneralarchitecture{calledMulan{isformulatedintermsofhighlevelPetrinets,
namelyreference nets. Theformalism of reference netsis based onthe \netswithin nets"
paradigmofValk,whichtswellinthecontextofagentsystems.
Here, we rst show how multi agent systems should be modeled. In the second step
we analyze whichare the requirements for a verication systemsdealing with multiagent
systems.Inbothcaseswearriveattheconclusionthatreferencenetsarewellsuitedtomodel
andverifycentralaspectsofagentsystems,likemobility,adaptation,andcooperation.
Inthisworkwefocusonmodelingandvericationofagent conversations. Ourapproach
isbasedoninter-actingagentprotocols. Toexpressourideaswehavechosenthewellknown
producer-consumerscenariobothforthemodelandtheformaltreatment.
Keywords: modeling,multiagentsystems,netswithinnets,referencenets,verication.
1 Introduction
Correctnessof softwareis crucialin almosteverysystem. Agent orientedmodelingis an
estab-lishedapproachto modelcomplex,exible systems. Thepropertreatmentof encapsulationand
compositionraisesquestionbothintheeldofarchitecturalmodelsandcompositionalverication.
The multi agent architecture Mulan 1
{ designed and implemented at our department { is
completelymodeled with Petri nets (cf. [KMR01]). Mulan is a Petri net based architecture,
whichisbothanimplementationofamultiagentplatformandalsoaframeworkforthemodeling
of agent applications. The Mulan architecture is based on the \nets within nets" paradigm{
formulatedbyValkin[Val87]fortaskowsystemsandin[Val96, Val98] forobjectnetsystems.
Mulanisspeciedinthereferencenetformalism(cf. [Kum98]) andimplementedwith thetool
Renew(cf. [KW98]).
Currently, agentsare generallyprogrammedusing high-levellanguagessuch asJava(namely
in agent frameworks as Jackal [CFL +
98]) or they are dened by simple scripts. A graphical
modelingtechniquethat capturesallparts ofagentsandtheirsystems{asUML 2
inthecontext
ofobject-orientation{is neitherproposed noringeneraluse.
3
An unifyingframeworkbasedon
thevisual programming conceptof Petri nets{ asproposed by Mulan {thus bridges the gab
betweenmodelingandprogramming.
Multiagentsystemsrelyheavily onthemechanismofcomposition: agentprotocolsare
com-posed to agentbehavior,agentbehavioriscomposed to agents, agentsarecomposed to groups,
groupsarecomposedwithinagentplatforms,platformsarecomposedtoagentsystems-toname
theobviousones. Alltheseexamplesleadstowardsthetopicofcompositionalverication{a
cen-tralrequirementforaproofsystemforanagent-architecture. Compositionalityofproofsrequires,
1
MulanstandsforMultiagentnets.
2
UMLstandsforUniedModelingLanguage. Seeforexample[RJB99 ].
3
1 n
spec(S
i
)ofthecomponents(cf. [Zwi89]):
spec(S
1 jj:::jjS
n
)=f(spec(S
1
);:::;spec(S
n ))
Wewillshow,thatcompositionalityinmultiagentsystemshastobebasedontheconceptof
environment: Inthesystemspecicationofasinglemodule,theenvironmentisconsideredto be
necessarilyspeciedinaddition. Itisunclearwhethertheenvironmentshouldbeincludedinthe
model(asdonee.g. in[DE96])orwhetherthemoduleanditsenvironmentshouldbeformulated
separatelybutconnectedinan\assumption-commitment"pattern{astyleofreasoningthathas
beenproposedbyChandyandMisrain[MC81].
Our work is structuredas follows: section2 introducesinthe MAS-architecture Mulan; in
section3 we describe the generalrequirementstowardsa verication system forMAS and how
they are met by Mulan; as a result we obtain the necessity to explicitly include assumptions
andcommitments(A/C)inourframework.
4
Suchan explicitnotionof A/Cis expressedbythe
formalismof A/C-Petrinets,described insection 4. Theformalismisillustratedinsection5by
aformaltreatmentoftheproducer-consumerscenario. Theworkcloseswithaconclusion.
2 The Mulan architecture
Thissectiongivesashortintroductiontoamultiagentsystemmodeledintermsof"netswithin
nets". This surveyisgivento makethegeneralideasvisiblethat are prerequisiteto the
under-standingoftheconcepts that followinlater sectionsof thispaper. Itis neitheranintroduction
to multiagent systemsnor the assets and drawbacks of dividing the system into platforms are
discussedhere. For abroadintroduction see forexample[Wei99], thespecialviewtakeninour
workisastandardproposalofthe"FoundationforIntelligentPhysicalAgents"(FIPA)[FIP98a].
ThelatestpublicationsoftheFIPAcanbefoundin[FIP].
2.1 Reference nets
MulanisbasedonthespecialPetrinetformalismofreferencenets[Kum98].
5
As forothernet
formalismsthereexisttoolsforthesimulationofreferencenets[KW98]. Referencenetsshowsome
expansionsrelatedto"ordinary"coloredPetrinets: netsastokenobjects,dierentarctypes,net
instances, and communication via synchronous channels. Beside this they are very similar to
colouredPetrinetsasdened byJensen[Jen92]. Thedierencesarenowshortlyintroduced.
Nets as tokens Reference nets implement the "nets within nets" paradigm of Valk [Val96,
Val98]. This paperfollowshisnomenclatureand denominatesthesurroundingnet\system net"
andthetokennet\objectnet". Certainlyhierarchiesofnetwithinnetrelationshipsarepermitted,
sothedenominatorsdepend onthebeholder'sviewpoint.
Arc types In addition to the usual arc typesreference nets oerreservation arcs, that carry
anarrowtip at both endings and reserveatoken solelyfor one occurrence of atransition, test
arcsandinhibitorarcs. Test arcsdonotdraw-oatokenfromaplacewhyatokencanbetested
multipletimessimultaneously,evenbymorethanonetransition(testonexistence). Inhibitorarcs
preventoccurrencesoftransitionsaslongastheconnectedplacesaremarked.
Net instances Net instances are similar to the objects of an object oriented programming
language. They are instantiated copies of a template net like objects are instances of a class.
Dierentinstancesofthesamenetcantakedierentstatesatthesametimeandareindependent
fromeachother inallrespects.
4
Thenotionof\assumptionsandcommitments"doesnotrelydirectlyontheoriginaldenitionofChandyand
Misra,butratherdenotesastyleofreasoning.
5
ItisassumedthroughoutthistextthatthereaderisfamiliarwithPetrinetsingeneralaswellascolouredPetri
time)forthe durationofoneoccurrence. Inreference nets(see[Kum98])achannelis identied
byitsnameanditsarguments.Channelsaredirected,i.e.exactlyoneofthetwofusedtransitions
indicatesthenetinstanceinwhichthecounterpartofthechannelislocated. Theothertransition
cancorrespondinglybeaddressedfromanynetinstance.Theowofinformationviaasynchronous
channelcantakeplacebidirectionalandisalsopossiblewithinonenetinstance.
2.2 Architecture
Takealook at gure1: Thegrayrounded boxesenclosenets(net instances)of theirown right.
TheZOOM linesenlarge object nets that are tokens inthe respectivesystem net.
6
The upper
left net of the gure is an arbitrary agent system with places containing agent platforms and
transitionsmodelingcommunicationchannelsbetweentheplatforms.
7