send acknowledge i
i a
i i
i i a
Figure5: Consumerprotocol
Afterreceivingtheitemandsendingtheacknowledgethetransitionconsumemayoccur. After
thattheprotocolterminatesandcan bedeleted.
Figures4and5showtheprotocolsthatmodelaconversationbetweenproducerandconsumer.
Theyare executedwithinagentsofthetypeofgure2. Theguresformasimpleexamplethat
illustrateshowtomodelaproducer-consumerprocessbymeansofagentorientedPetrinets. The
proposedmethodologytoimplementprotocolnetsinatop-downmanner startingwithso-called
surveynetsisnotthe onlypossibilitytodevelopprotocols. Onecaneasilythinkofabottom-up
styleormixedcasesespeciallyforhierarchicalprotocolrelationships. Unfortunatelythistopiccan
notbedeepenedhere.
3 Agent oriented verication
Theanalysisofagentsystemsraisestheneedforaspecialstyleofvericationsystems. Thisneed
is due to the dynamicsand openness of agentsystems. As stated before, modeling approaches
lackauniformbasis. Thesameistruealsoforvericationapproaches.
Mostapproacheshandlemultiagentsystems(MAS)thesamewayasasingleintelligentagents.
This style is based on the traditionalarticialintelligence (AI) view, disregardingthe needs of
MAS.Itismostlybasedon(modal)logicalspecicationandmodelcheckingtechniques(cf. [HR00]
asanexample).
Ingeneral,approachesaddressingthespecialtiesofMASfocusononesingleaspectof
descrip-tion. Formobilityseveralalgebraicapproachesdescribethechangeofenvironment(cf. [MPW92],
[VC99]or[CGG99]). Adaptation(cf. [GPdFC98])andcooperation(cf. [SHM99]and[CCF +
99])
areaddressedalso.
InourpointofviewsuchapproachesareinsuÆcientfortheanalysisofanagentsystem,since
only parts of the system are specied. It is unclear whether the combination of the isolated
formalizationsleadsto a correct description of what the system does. Since the integration of
the models has do be done manually by the developer this leads to an error pruning style of
construction.
So,weconcludethatnotonlytheconstructionofanagentsystemshouldbedoneonauniform
basisbutalsotheformalpartofreasoningaboutitshouldbebasedononesinglecalculus. Inthe
following,wedescribewhichcharacteristicssuchaformalbasisshouldown.
InourMulan-approach,weunderstand thecentralparts ofadynamic,openagentsystem{
mobility,adaptation,andcooperation{asparts ofonecentralconcept: compositionality.
bility focus this pointtowardsthedynamicchange of environmentsduringruntime ofan
agentsystem.
Compositionalityisalsocentralforthedescriptionofagentgroupsandtheirmobility:agents
arecomposedto groups,whichcanbeconsideredasagentsagain.
Cooperationofagentsisalsoakindofcomposition,atleastatthetechnicallevelof
interac-tion. Sincethebehaviorofonesingleagentisexpressedbyasetofprotocols,conversations
areformedbythecompositionofseveralagentprotocols.
Adaptationis the dynamic change of agent behavior. Since behavior is a composition of
several primitive actions, adaptation must be described by the dynamic conguration of
such ancompositebehavior. So,behaviorisakindofcompositionphenomena.
These kinds of compositionalityhave been shown ingure 1 before: each zoom standsfor one
compositionmechanism.
3.1 Classication of verication approaches
The great numberof publicationsin the very general eld of verication raises the need for a
classicationscheme. Weproposeaclassicationschememainlyorientedontwocategories: rst
thetypeofprogrambeingveriedandsecond thevericationtimeandstyle.
Therstcategorydiscriminatesbythekindofmodelwhichisveried
1. Sequential block. The program is considered to be a monolithic block, usually build by
iteration, conditionals, and sequence. Central work is theapproach by Hoare [Hoa69] for
algol-likeprogramminglanguages.
2. Parallelblock. Thesecondclassalsodealswithmonolithicprograms,butallowstheconstruct
forparallelexecution. ThemostknownapproachforparallelprogramsisduetoOwickiand
Gries[OG76].
3. Top-down development. Thethirdclassincorporatestheaspectofinformationhiding.
Pro-gramsare consideredto be thecompositionof encapsulatedmodules. This styleof
devel-opment and verication is known asthe \top-down" approach. The most common proof
systemhasbeendevelopedbyApt, Francez,anddeRoever[AFdR80].
4. Bottom-up development. The fourth class considers the verication of modules on their
own. The context where modules are embedded in is not known a priori. This style of
reasoning is known as the \bottom-up" approach. A central step in the development of
bottom-upvericationsystemsistheassumption/commitmentformulationbyChandyand
Misra[MC81].
Whiletherstcategorydealswiththemodel,thesecondcategorydiscriminatesbythemoment
vericationtakesplaceandthetechniquebeingused:
1. Vericationisdoneafter programming. Firstthesystemisspecied,thencodedand
after-wardstheimplementationis checkedintermsofthespecication. Centralapproachisthe
modelcheckingtechniquebyClarkeandEmerson[EC82].
2. Vericationisdonewhileprogramming. Thiscouldbedoneiftheprogrammerhasacentral
idea how to proof the implementationwhile he programs. This kind of style is known as
\structuredprogramming".Allaxiomaticapproaches{like[Hoa69]{areexamples.
3. Proof by construction. Programming and verication are essentiallythe same. These
ap-proaches are based on constructivelogic (like COQ [BBC +
99]) or on property preserving
transformation(likein[Ber87]) oronstructural restrictionsresultinginsubclasses(likein
[BT87]).
Thisclassicationisorientedonthehistoricaldevelopmentofprogrammingstylesandmajor
post
Figure6: Classicationschemeforvericationapproaches
3.2 From compositional verication to agent oriented verication
Which approachesare suited forthe developmentandvericationof agentsystems? Inthe
fol-lowing the central requirements of MAS are contrasted with the existing verication styles, as
classiedbefore. Wewillshowthatseveralapproachesrelevantinthe\normal"caseareunsuited
forthespecialcaseofagentsystems.
Several approachestry to liftverication stylesdesigned for object oriented programsup to
theagentcontext{neglectingthespecialneedsofmultiagentsystems.
Therstspecialityisduetothenatureofagent: agentsareencapsulated,autonomousentities
whicharelooselycoupled. Theyaredevelopedwithoutanyknowledgeofthewholeagentsystem.
Developersandagentscannotknowthewholesystemorthestateofthewholesystem. Thereis
nosuchthingasglobalknowledgeforagents.
Due toencapsulation andisolated developmentonly bottom-upvericationcanapplyto the
agentcontext. Allapproachesconsideringagentsystemsasoneunitmustreject theopennessof
agentsystemsandrelyonsomekindof\closedagentworldassumptions". Onlytheassumption
basedstyleofreasoningcanapplytoopensystems.
Sinceagentsareconsideredasactiveentities(in contrasttopassiveobjects), weadditionally
takeinto accountwhois reasoningaboutthe agentsystem. Ifitis thedeveloper,weare mainly
confronted with \static" problems, if it is the agent, we are confronted with more \dynamic"
aspects. Inthesecondcasereasoningmustbedoneautomatically. Thisseemstobeharderthan
therstcase,whereitcanbedonesemi-automatically.
Reasoningatrun-timeistheconsequencewhendealingwithopensystems,wherenoonecan
know in advance, what might enter the system. Security inmobile agent systems is a central
aspect(cf. [Vig98]) whichcanonly be achievedbystructural restrictionsonagentsor on agent
behavior. Structuralrestrictionsreduce theproofburdenofanagentsystem.
If onecomparesthese requirementswith thecategoryscheme ingure6, onecanrecognize,
thatwecanrestrictourinvestigationtothe\bottom-up"columnandtherows\vericationwhile
andbydevelopment"(seegure7).
sequential parallel top-down bottom-up
post { { { {
while { { { relevantforthedeveloper
by { { { relevantfortheagent
Figure7: Vericationintheagentcontext
Besidesthesemajorissues,whichrejectseveralapproachesinadvance,someadditionalaspects
mustbehandledinvericationssystemsintheagentcontext. These aspectsmightbeofinterest
inthecontextofobject-orientation,too,but inthecontextofagentstheycannotbeignored.
implementation,andvericationshouldnotrelyontotallyorderedactionsequences. Partial
ordersemantics(trueconcurrency)shouldbeusedinstead.
3. Dynamic environment. Agentsystemsareconceptuallybasedondistributionandmobility.
Therefore,aproofsystemmustbeabletodescribeenvironmentsandtheirdynamicchange
inanexplicitway.
4. A/C-concepts. AnapproachforMASshouldallowtospecifyassumptionsandcommitments.
We additionally postulate, that these assumptions and commitments should not only be
visibleforthe verier but alsofor thedeveloper. Toavoida gapbetweenvericationand
modeling,assumptionandcommitmentsshouldbeanintegralpartofthemodel.
5. Structural properties. The systemsshouldallowto easilydescribestructural restriction in
ordertoguaranteee.g. securityproperties. These restrictionsshouldbeeasilyadaptablein
themodelingapproach.
Due tothese requirementswehavechosenthe paradigmof \nets withinnets"[Val87,Val96,
Val98] forthedevelopmentaland formalbasisof theMulan-architecture. This approach meets
theabovementionedrequirementsdirectlyorisadjustedcurrentlybytheauthors. Ithasalsothe
benetthatthe\netswithinnets"paradigmhasitnative\machine"implementedintheRenew
tool[KW98].
14
Thisapproachmeetstherequirementsforanuniedapproach. LikeeveryPetrinetformalism
itincorporates theconcept ofconcurrency. Therequirementofencapsulation and modularityis
fullledbytheconceptthatnetscouldberegardedastokensagain{aviewthat meetswellwith
modularity. The remainingrequirements{dynamicenvironment,A/Cmodelingand structural
guaranteed properties { are captured by the formalism of assumption/commitmentPetri nets,
short: A/CPetrinets. Thesubclass of A/CPetrinets, that weare presentinghere, dealswith
protocolsandisthereforecalledA/C-protocols.
The concepts {mobility, adaptation, and cooperation{ are supported by conceptson their
own as shown in gure8, where we have shown the relationsbetweenthe distributed articial
intelligence(DAI) paradigms, theMulan concepts, and thecorrespondingentitiesinthe proof
system. Theseconceptscannotbeexplainedindetail,sowesketchbrieytheideas: \Distributed
markings"(cf. [Koh00b]) describethemobilityaspectof \netswithinnets" inanalgebraicway.
Theyareespeciallysuitedfortheformalizationofagentgroupsinadistributedsystem. Adaptation
isbasedontherecongurationofcomposedA/C-Petrinets. Cooperationtakesplaceinformof
conversations,consistingoforderedA/Cagentprotocols.
DAI Mulan verication
mobility locationnets,groupagents distributedmarkings
adaptation self-modifyingprotocols A/C-Petrinets
cooperation conversation conversationorders,
A/C-protocols
Figure 8: RelationshipofDAIparadigmsand vericationof Mulanmodels
Theseconceptsarebasedonthealgebraicviewpointonnets(\Petrinetsaremonoids"[MM90])
which we addressed in former work for processes in object net systems (cf. [Koh00a]). These
dependencies{andsomemore,that cannotbedeepenedhere{areillustratedingure9.
In the further presentation we will focus our attention mainly on the aspects of the A/C
modeling and verication of agents protocols in termsof A/C-Petri nets (cf. the right part of
gure9).
14
Theworkof[BDM +
99 ]favors anapproach basedonlinearlogicinstead. Thisworkisagoodargumentfor
ourapproach,sincePetrinetsandlinearlogicarestronglyrelated(cf. [Far00]). Ourapproachhastheadditional
"nets in nets"
Figure9: FoundationsofMASverication
4 A/C Protocols
Our formal description of agent protocols is based on the explicit notion of assumptions and
commitments(A/C) made towardsthe environment. Ourgeneral model to express A/Cis the
formalismofA/C-Petrinets. Starting fromthese A/CPetrinetswedene the so calledclasses
ofbasicprotocolsPetrinets(BPPN)andofenvironmentbasedprotocolsPetrinets(EPPN).
4.1 A/C-Petri nets
modelingenvironmentalactions(Astandsforassumptions). ThesetT 0
=T nT A
arethe\core"
transitionsof the net. Havealook at gure10 foran example: theunlled transitiont
2 2 T
A
denotesanenvironmentaltransition,whilet
1
Figure10: AnA/C-Petrinet
Environmentaltransitionst
A 2T
A
arenotenabledon theirown,sinceit isassumedthat t
A
must re synchronouslywith some transitiont
U
fromthe environment U. Because of this, an
environmentaltransitiont
A 2T
A
is never enabledwithout theenvironment, ifweconsiderthe
A/C-Petrinetonitsown.
Environmentaltransitionsaremodeledbytransitionsincombinationwiththeconceptof
syn-chronouschannels.
15
Intheexampleofgure10t
2
isinscribedbytheup-link:c(). Thisapproach