inforfedora17

ModelCheckingGSM-BasedMulti-AgentSystemsPavelGonzalez1,AndreasGriesmayer2,andAlessioLomuscio11DepartmentofComputing,ImperialCollege,London{pavel.
gonzalez09,a.
lomuscio}@imperial.
ac.
uk2ARM,Cambridgeandreas.
griesmayer@arm.
comAbstract.
Artifactsystemsareanovelparadigmforimplementingser-viceorientedcomputing.
Businessartifactsincludebothdataandprocessdescriptionsatinterfaceleveltherebyprovidingmoresophisticatedandpowerfulserviceinter-operationcapabilities.
Inthispaperweputfor-wardatechniqueforthepracticalvericationofbusinessartifactsinthecontextofmulti-agentsystems.
WeextendGSM,amodellinglanguageforartifactsystems,tomulti-agentsystemsandmapitintoavariantofAC-MAS,asemanticsforreasoningaboutartifactsystems.
WeintroduceasymbolicmodelcheckerforverifyingGSM-basedmulti-agentsystems.
Weevaluatethetoolonascenariofromtheservicecommunity.
1IntroductionIthaslongbeenargued[1,2]thatagentsareattingparadigmforserviceori-entedcomputing(SOC).
Indeed,agent-basedresearchhascontributedawealthoftechniquesrangingfromverication[3],protocols[4]andactualprototypeim-plementations[5].
SOCiscurrentlyafastmovingresearchareawithsignicantindustrialinvolvementwherehighlyscalableimplementationsplayakeyrole.
Agent-basedsolutionscanshapedevelopmentsinSOCiftheyremainanchoredtoemergingparadigmsbeingputforwardbytheleadingplayersinthearea.
AnincreasinglypopularparadigmbeinginvestigatedinSOCisthatofbusi-nessartifacts[6].
Inthisapproachdata,notonlyprocesses,playakeypartintheservicedescriptionandimplementations.
Whileintraditionalservicecompo-sitionprocessesareadvertisedatinterfacelevel,intheartifactapproachbothpro-cessesandthedatastructuresaregivenequalprominence.
Guard-Stage-Milestone(GSM)hasrecentlybeenputforward[7]asalanguageforimplementingbusi-nessartifacts.
GSMisadeclarativelanguagethatprovidesadescriptionofstages,whichareclustersofactivitypertainingtosomeartifactdata-structure.
StagesThisresearchwassupportedbytheEUFP7projectsACSI(FP7-ICT-257593).
WorkbytheauthorAndreasGriesmayerwasconductedinpartatImperialCollegeLondonandsupportedbytheMarieCurieFellowship"DiVerMAS"(FP7-PEOPLE-252184).
AlessioLomuscioacknowledgessupportfromtheUKEPSRCthroughtheLeadershipFellowshipgrant"TrustedAutonomousSystems"(EP/I00520X/1).
A.
R.
Lomuscioetal.
(Eds.
):ICSOC2013Workshops,LNCS8377,pp.
54–68,2014.
cSpringerInternationalPublishingSwitzerland2014ModelCheckingGSM-BasedMulti-AgentSystems55aregovernedbyguardscontrollingtheiractivationandmilestonesdeterminingwhetherornotthestagegoalshavebeenreached.
TheGuard-Stage-Milestone(GSM)approachtoartifactsystems[7]isparticularlysuitableforlargeunstruc-turedprocesseswhereusershavethefreedomtodecidewhatactionstheyperformandinwhatorder.
GSMissubstantiallyinuencingtheemergingCaseManage-mentModellingNotationstandard[8].
IBMWatsondevelopedBarcelona,aweb-basedapplicationformodellingandexecutionofGSM-basedartifactsystems[7].
Barcelonaprovidesafullymodel-drivenenvironmentwhereabusinessoperationsmodelofanartifactsystemiscreatedinaweb-baseddesigneditorcomponent,andthendirectlyusedfordeploymentonanexecutionengine.
Whilebusinessartifactsareanattractivemethodologyfordevelopingbusi-nessprocessesandGSM-basedservicesarearapidlyevolvingareaofresearch,theylackfully-edgedautomaticmethodologiesforverication,orchestrationandchoreography.
Inthispaperweputforwardatechniqueandanimplementa-tionforthepracticalvericationofbusinessartifactsfromamulti-agentsystemperspective.
Specically,wegiveaMAS-basedformalmodeltoGSMsystemsanddenethemodelcheckingproblemonthismodel.
Weobservetheproblemisundecidableingeneral,butnotethataslongaswecanshowthesystemoperateswithinbounds,theproblemisdecidable.
Withintheseparametersthemethod-ologywereportissoundandcomplete.
WehavebuiltanimplementationtoverifyautomaticallywhetheraGSMsystem,includinganumberofagents,sat-isesgiventemporal-epistemicspecicationswhichmayincludequanticationoverartifactinstances.
WetestthetechniqueagainstanoteworthyapplicationdevelopedbyIBM.
Severalcontributionshavesofarstudiedthevericationproblemfromathe-oreticalperspective[9–12].
Theresultsobtainedidentifyfragmentsofdecidablesettingseitherthroughrestrictionsonthespecicationlanguageortheseman-tics.
Whiletheseresultsarecertainlyvaluable,theyprovidenomethodologyforthepracticalvericationofGSM-basedsystems.
Theworkpresentedinthispaperisbasedon[13]whereGSMC,amodelcheckerforGSM,isintroduced.
However,thesemanticsoftheunderlyingformalismisoneofplaintransitionsystemsandnosupportforagentsinthesystemisprovided.
Withnoagentsbeingpresent,nosupportisoeredforviewsandwindows,twokeyconceptsthatwefullysupporthere.
Additionally,astheirconcernisfocusedpurelyontheartifactsystem,thespecicationlanguageonlysupportstemporallogic,therebymakingimpossibletoverifytheinformation-theoreticpropertiesofagentsthroughoutanexchangeaswedohere.
2TheGuard-Stage-MilestoneArtifactModelArtifactsystemsformaconceptualbasisformodellingandimplementingbusi-nessprocesses[6]andaregivenintermsofartifacttypes,whichcorrespondtoclassesofkeybusinessentities.
Eachtypehasalifecyclemodel,whichdescribesthestructureofthebusinessprocess,andaninformationmodel,whichgivesanintegratedviewofthebusinessdataandtheprogressofthebusinessprocess.
56P.
Gonzalez,A.
Griesmayer,andA.
Lomuscioresearch()prepare()PreparingCollectingPartsReceivingAssemblingpartreceivedallpartsreceivedreceivepart()Research&Orderpartsorderedcollectedsubmittedassemble()Fig.
1.
AlifecyclemodelTheartifactsysteminteractswithitsenvironmentviaevents.
OurformalmodelofGSMisinlinewith[7].
GSMprovidesadeclarative,hierarchicalmechanismforspecifyinglifecyclemodels.
Figure1givesaportionofthelifecycleofamanufacturingprocessandrepresentsthecoreconcepts:Theboxesdenotestages,whichrepresentclustersofactivitydesignedtoachievemilestones()thatrepresentoperationalobjectives.
Aguard()triggersactivitiesinastagewhenacertainconditionisfullled.
Stagesareorganisedhierarchically,wheretherootsarecalledtop-levelstages,theleavesarecalledatomicstagesandthenon-leafnodesarecalledcompositestages.
Atomicstagescontaintasksthatperformautomatedactions.
Stagescanruninparallelandownatleastonemilestoneandoneguard,whilebothmilestonesandguardsbelongtoexactlyonestage.
Astagebecomesopenwhenoneofitsguardsisfullledandclosedwhenoneofitsmilestonesisachieved.
Theexampleabovegivestheportionofthelifecycleofamanufacturingpro-cessthathandlestheprocuringoftherequiredbuildingpartsandtheorgani-sationoftheassembly.
Whenaneworderisreceivedbythemanufacturer,thesubmittedeventissenttotheartifactsystem,whichtriggerstheguardofthePreparingstage,andinturnstartswithCollectingParts.
Whenthisstageisopen,anemployeeofthemanufacturerresearchestherequiredcomponentsandsendstheresearcheventtotheartifactsystemwhichinturnprocessestheorderoftherequiredparts.
Whenapartisreceived(eventpartreceived),theAssem-blingoftheavailablepartsistriggered;whenallpartsarereceivedandcollected,thePreparingstagecanbeclosed.
MoredetailsonthislifecyclewillbediscussedinSection6.
Formally,anartifactsystemholdsanumberofartifactinstancesιofartifacttypeAT=R,Att,Lcyc,withRthenameoftheartifacttype;Atttheinfor-mationmodelassetofattributes;andLcycthelifecyclemodel.
TheinformationmodelAttispartitionedintothesetAttdataofdataattributestoholdbusinessdataandthesetAttstatusofstatusattributestocapturethestateofthelifecyclemodel.
Eachstage(resp.
milestone),hasaBooleanstatusattributeinAttstatus,whichistrueithestageisactive(resp.
themilestonehasbeenachieved).
BothModelCheckingGSM-BasedMulti-AgentSystems57milestonesandguardsarecontrolleddeclarativelythroughsentries.
Asentryofanartifactinstanceιisanexpressionχ(ι)intermsofincomingeventsandthestatusoftheinstance.
Theprogressofthelifecycleisdrivenbyincomingeventscontainingpayloads,whicharecalledapplicableifthelifecycleisreadytoconsumethem.
Aneventwithaspecicpayloadiscalledatypedexternalevent.
Denition1(EventType).
AneventtypeETisatupleET=E,AT,A1,Al,whereEisthenameoftheeventtype,ATisanartifacttype,andAi∈Attdata,whereAttdataisthesetofdataattributesofAT.
Inaddition,theopeningofanatomicstageactivatesataskassociatedwiththestage.
Iteitherperformsanautomatedsystemtask,suchasthecreationofanewinstance,orcorrespondstoanoperationoutsidetheartifactsystem.
AgentsarenotdirectlypresentintheGSMmodel,butitisassumedthathumanorarticialentitiesperformtasksandgenerateeventsforthesystem.
Denition2(GSMModel).
AGSMmodelΓisasetofnartifacttypesATifor1≤i≤nandmeventtypesETjfor1≤j≤m.
Denition3(SnapshotofGSMModel).
Apre-snapshotofΓisanassign-mentΣthatmapseachattributeA∈AttιofeachactiveartifactinstanceιtoanelementinthedomainofA.
AsnapshotofΓisapre-snapshotthatsatis-esthefollowingGSMinvariants:allsub-stagesofaclosedstageareclosed;allmilestonesofanopenstagearenotachieved;atmostonemilestoneofastagecanbeachievedatanytime.
TheoperationalsemanticsforGSMisbasedonthenotionofabusinessstep(B-step).
Thisisanatomicunitthatcorrespondstotheeectofprocessingoneincomingeventintothestateoftheartifactsystem.
AB-stepiscomputedbysocalledPACruleswhichareformedfromthesentriesoftheGSMmodelandhastheformofatuple(Σ,e,Σ,Gen),whereΣ,Σaresnapshots,eisanincomingexternalevent,andGenisasetofoutgoingexternaleventsgeneratedbyopeningatomicstagesduringtheB-step.
FormoredetailsonthecomputationofaB-steppleasereferto[13].
3Agent-BasedGSMAGSMprogramonlydealswiththemachineryrelatedtotheartifactsystembutdoesnotprovideadescriptionoftheagentsinteractingwithit.
Toconductthevericationofagent-basedGSMsystemsviamodelchecking,wedeneAgent-BasedGSM(A-GSM)asanextensionofGSMwithasetofexternalagents.
Theartifactsystemandagentscommunicateusingevents,wheretheavail-ableeventsforanagentdependonthecurrentstate.
Thesystemprogressesbynon-deterministicallyselectinganagent,whichsendsaneventandtriggerstheexecutionoftheAS.
SelectionoftheeventandexecutionoftheASareseenasonestep,astablestatehasnopendingevents.
58P.
Gonzalez,A.
Griesmayer,andA.
Lomuscio100νω00001Fig.
2.
StaticandDynamicvisibilityinA-GSM3.
1AgentDescriptionHereweoutlinehowtheagentsarespeciedandinteractwithGSM,therebydeninganA-GSMinstance.
ThebehaviourofanagentisdeterminedbythepermittedaccesstotheartifactsystemASandbylocaldecisionsregardingeventstosend.
Theformerisdeterminedbyanagent'srole,whilethelatteraredenedforeachagentindividually.
Theroleisdenedusingtheviewνforthevisibleattributes,thewindowωtoselectthevisibleinstances,andthesetofeventsthatareacceptedbyAS.
Whileνandaresimplelists,ωi(ι)isaformulathatisevaluatedforaspecicartifactinstanceιandanagenti.
Theinstanceisexposedtotheagentonlyifωi(ι)evaluatestotrue.
Inadditiontotherole,thedescriptionofanagentalsocontainsaprotocoltodetermineitsbehaviourdependingonthevisiblestateoftheAS,theagent'suniqueID,anditsprivatevariables.
Theconceptsofν,ωandarepowerfultoolstodenetheaspectsagentscanseeandthewaystheycaninteractwithanartifactsystem.
InFigure2thelinescorrespondtoartifactinstancesthatwerecreatedduringrun-timeandthecolumnscorrespondtodataattributes.
νdenesastaticviewofthesystem,asithidesforeachagentaxedsetofattributesdependingonhisrole.
Forexample,aCustomercanonlyseethatthestateofanordermovedfromassemblingtoshipping,whileaManufacturerseesmoredetail,e.
g.
,onsuppliers.
Incontrast,ωgivesadynamicselectionofthepartsoftheASanagentcanaccessintermsofthestateofartifactinstancesasithidescompleteinstancesdependingonthecurrentstate.
Forinstance,aManufacturermayonlyseeinstancesthatrepresentunnishedorderswhilethewindowofaCustomercanusetheIDtorestrictaccesstoitsownordersonly.
Figure3givesanexampleofagent'sdescriptionle.
Visibledataattributesarelistedinthevieweld.
Thewindoweldcontainstheformulaforωi(ι),where$$isaplaceholderfortheagent'sID.
Theeldinstantiationlistsallartifacttypesthatagentsofthisrolemayinstantiate;thecorrespondingin-stantiationeventsareaddedto.
Tospecifythestatusattributesandeventsthatareaddedtoνand,theeldtransformationholdsasetofGSMModelCheckingGSM-BasedMulti-AgentSystems59roleCustomer{view:CustomerId,ManufacturerId;window:CustomerId==$$;instantiation:CO;transformation:condense_stage(CO,Preparing);};agentDiogenes{role:Customer;vars:boolcancelled=false;protocol:Create_CO:CustomerId=="Diogenes"->cancelled=cancelled,OnCancel:true->cancelled=true;};Fig.
3.
AnagentdenitionleoperatorsthatallowtohidepartsoftheGSMmodelΓ.
Validcommandsherearehidestagestatus("S")andhidemilestone("m")tohidethestatusat-tributesofstageSandmilestonemrespectively,anddelegatesentry("s")toremoveeventsfromiiftheyareonlyusedinsentrys.
Forconvenience,themacrooperatorscondensestage("S")andeliminatestage("S")hideallsub-stagesorallinformationincludingguardsandmilestonesrespectively.
Theprivatevariablesofanagentaredenedinalistvarofvariablenamesxwiththeirtypeandinitialvalue.
Theprotocollistsentriesoftheforme:γ->μforalleventsetheagentcansend.
Multipleentriesforthesameeventaretreatedasadisjunction.
Theconditionγisgivenintermsofdataattributesoftheinstanceι,thepayload,andtheprivatevariables.
Itdenestheprotocolfunctioni(ι,x),whichgivesthesetofeventsewiththeirrespectivepayloadsthatcanbesentinthecurrentstate.
Theprotocolalsogivesanupdatefunctionμi(e,x),whichcomputesnewassignmentsforthelocalvariablesdependingontheselectedeventandthelocalstateoftheagent.
Byimposingconditionsonthepayloadofanevente,alsoallowstheagenttoassignaspecicvaluetoitsparameters,e.
g.
,CustomerIdisaparameterofCreateCO.
Tohandleautomatedtasks,wedeneanAutoAgent,whichhandlesservicecallsandcomputationsintheGSMmodelΓandreturnstheresulttotheartifactsysteminformofanevent.
TheAutoAgentholdspendingtasksinabuert,hasfullaccesstoΓ,andcansendthereturnmessagesatanytime,butisotherwisehandledlikeanyotheragent.
4Artifact-CentricMulti-AgentSystemsToanalyseinteractionswithinaGSM-basedartifactsystem,weuseartifact-centricmulti-agentsystems(AC-MAS)[10,14],asemanticsbasedoninterpretedsystems[15,16].
AsaGSMsystemsupportsmultipleactiveartifactinstances,werequirealimitedformofquantication.
WethereforeintroduceIQ-CTLK,60P.
Gonzalez,A.
Griesmayer,andA.
LomuscioanextendedversionofCTLK,whichisfrequentlyusedtodescribeagentsthatshareacommonenvironment.
IQ-CTLKisatemporal-epistemicspecicationlanguagewithquanticationoverartifactinstances.
Wegiveaformalmappingf:A-GSM→AC-MAS,suchthatfpreservessatisfactionofformulasinthespecicationlanguageIQ-CTLK.
4.
1FormalModelInanAC-MASasetofagentsAshareanenvironmentEconstitutedbytheartifactsystem,i.
e.
,theunderlyingelementsoftheenvironmentareevolvingartifactsoftypeR.
Theenvironmentandanagenti∈Ahavealocalstate(LEandLirespectively),wheretheagentcanobservepartsoftheenvironment(i.
e.
,someoftheartifactinstancesinit).
Thelocalstateofanagentthuscomprisesprivatedatafortheagentandobservableaspectsoftheartifactsystem.
WewritelE(s)torepresentthelocalstateoftheenvironmentintheglobalstates,andli(s)torepresentthelocalstateofagenti.
Denition4(Environment).
TheenvironmentrepresentsanartifactsystemASandisatupleE=LE,ActE,PE,whereLEisthesetoflocalstates;ActEisthesetoflocalactions,whichcorrespondtotheinterfaceoftheAS;andPE:LE→2ActEistheenvironment'sprotocolfunction,whichenablesactionstobeexecuteddependingonthelocalstateoftheAS.
Anagentisdenedformallyas:Denition5(Agent).
AnagentinanASisatuplei=Li,Acti,Pi,whereLiisthesetoflocalstatesincludingtheobservableaspectoftheAS;ActiisthesetoflocalactionscorrespondingtoeventsthatcanbesentbytheagentontotheASandincludinganactionskipforperforminganullaction;andPi:Li→2Actiisthelocalprotocolfunction.
AnagentiandtheenvironmentEcommunicatebysynchronisationonactions,whereActEcorrespondstoeventsenabledbytheartifactsystem,andActiActE∪{skip}isthesetoflocalactionscorrespondingtoeventsthatcanbeexecutedbytheagentandtheidleactionskip.
Giventherela-tionbetweennotionsofactionininterpretedsystemsandeventinGSM,weusethesetermsinterchangeablyintherestofthepaper.
Asinplaininterpretedsystems,protocolsareusedtoselecttheactionsperformedinagivenstate.
Followingtheterminologyof[14]wedeneanAC-MASasthecompositionoftheenvironmentandanumberofagentsasfollows:Denition6(AC-MAS).
GivenanenvironmentEandasetofagentsA,anartifact-centricmulti-agentsystemisatupleP=S,I,τ,whereSLE*L1Lnisthesetofreachableglobalstates;Iistheinitialstate;andτ:S*Act→2SwithAct=ActE*Act1*···*Actnistheglobaltransitionrelation.
Thetransitionτ(s,α)isdenedforα=aE,a1,aniaE∈PE(lE(s)),and0≤iModelCheckingGSM-BasedMulti-AgentSystems61Intuitively,theconditionsonthetransitionrelationlimitthecommunicationbetweenagentsandenvironmentsuchthatenvironmentandagentagreeonthesameaction.
Theenvironmentenablesactionswhentheartifactsystemisreadytoconsumethem,whiletheagentidecidesontheactionstoexecutedependingonalocalstrategyencodedinPi.
Onlyoneagentcaninteractwiththeenvironmentatatimewhiletheothersareidle.
Wewrites→sithereexistsanactionα,suchthats∈τ(s,α),andcallsthesuccessorofs.
Arunrfromsisaninnitesequences0→s1→.
.
.
withs0=s.
Wewriter[i]forthei-thstateintherunandrsforthesetofallrunsstartingfroms.
Astatesisreachablefromsifthereisarunfromsthatcontainss.
Inlinewiththesemanticsofepistemiclogic[16],wesaythatthestatessandsareepistemicallyindistinguishableforagenti,ori,ili(s)=li(s).
4.
2TheLogicIQ-CTLKWeareinterestedinspecifyingtemporal-epistemicpropertiesofagentsinteract-ingwiththeartifactsystem,aswellasthesystemitself.
SinceGSMsupportsthedynamiccreationofunnamedartifacts,thepropertiesneedtobeindepen-dentoftheactualnumberorpossibleIDsofartifactinstancesinthesystem.
Tospecifysuchpropertiesweheredeneatemporal-epistemiclogicthatsupportsquanticationovertheartifactinstances.
WecallthelogicIQ-CTLK,forIn-stanceQuantiedCTLK,whereCTLKistheusualepistemiclogiconbranchingtime.
ItisasubsetofFO-CTLKwherequanticationcanonlybeoverartifactinstancesbutnotdata.
ThesyntaxisdenedinBNFnotationasfollows:::=p||∨|EX|EG|E(U)|Ki|x:R|x:RwhereRisthenameofanartifacttypeandpisanatomicpropositionovertheagents'privatedataandtheattributesofactiveinstancesthatarespeciedintermsofinstancevariablesboundbythequanticationoperators.
ThequantiedinstancevariablesrangeovertheactiveinstancesofagivenartifacttypeRinthestatewherethequanticationisevaluatedandmustbebound.
WewriteR(s)forthesetofinstancesoftypeRins.
Thedenedoperatorsarereadasfollows:EXmeansthereisanextstateinwhichholds;EGconveysthereisarunwhereholdsineverystate;E(Uψ)denotesthereisaruninwhichholdsuntilψholds;Ki:expressesagentiknows;x:RrepresentsforallinstancesoftypeR;andx:RsaysthereisaninstanceoftypeR.
TheremainingCTLoperatorscanbeconstructedbycombinationoftheonesgivenaboveinthestandardway.
Forexample,AGx:OrderAFKix.
sentencodesthepropertyexpressingthatinanyreachablestate,agentiwilleventuallyknowthattheattributesentissettotrueforeveryactiveinstanceoftypeOrder.
62P.
Gonzalez,A.
Griesmayer,andA.
LomuscioWeinductivelydenethesemanticsofIQ-CTLKoveranAC-MASPasfol-lows.
AformulaistrueinastatesofP,written(P,s)|=,i:(P,s)|=pip∈s(P,s)|=iitisnotthecasethat(P,s)|=(P,s)|=1∨2i(P,s)|=1or(P,s)|=2(P,s)|=EXis:s→sand(P,s)|=(P,s)|=EGir∈rs:i≥0:(P,r[i])|=(P,s)|=E(Uψ)ir∈rs:k≥0:(P,r[k])|=ψandje.
,Kiexpresseswhatagenticaninferfromtheinformationavailabletohim.
Anagentknowsthatistrueinstatesifistrueinallstatess,whichtheagentcannotdistinguishfroms.
Finally,givenanAC-MASmodelPandanIQ-CTLKspecication,themodelcheckingproblemconcernsthedecisionastowhethertheformulaholdsattheinitialstateofP.
Notethattheabovesemanticsprovidesaninformation-theoreticdenitionofknowledge,i.
e.
,Kiexpresseswhatagenticaninferfromtheinformationavailabletohim.
Anagentknowsthatistrueinstatesifistrueinallstatess,whichtheagentcannotdistinguishfroms.
Thismeanstheagentdoesnotneedtobuildaknowledgebase,fromwhichhecandeducenewinformation,sincehealreadyknowseverythinghecouldpossiblydeduceinacertainsituation.
GivenanAC-MASmodelPandanIQ-CTLKspecication,themodelcheckingproblemconcernsestablishingwhethertheformulaholdsattheinitialstateofP,writtenP|=.
Inthecontextofourformalmodel,anAC-MASPsatisesif(P,I)|=.
IntuitivelythismeansthatthemodelPsatisesifistrueintheinitialstateofP.
Thiswasshowntobeundecidableonsimilarsemanticstructuresandmoreexpressivelogics[11].
Inthefollowingsections,wewillachievedecidabilitybyboundingthedataandthenumberofinstancespresent.
Wewillalsoshowtheimplementationofthetechniquetodemonstrateitsfeasibility.
4.
3MappingtoAgent-BasedGSMtoAC-MASWenowestablishtheformalmappingf:A-GSM→AC-MAS.
NotethatthesemanticsforthelocalstatesandprotocolsofagentsinA-GSMaregivenintermsofAC-MAS.
WedenethemapbyconstructingtheenvironmentLE,ActE,PEfromtheGSMmodelΓofagivenartifactsystemandcreateanagentL0,Act0,P0fortheAutoAgent,andLi,Acti,Piwith1≤i≤nModelCheckingGSM-BasedMulti-AgentSystems63foreachexternalA-GSMagent.
WeidentifyaGSMeventewithanAC-MASactionaandwillomittheconversioninthefollowingforeaseofpresentation.
ThesetsofactionsActE,Act0,andActiarethusdirectlydenedbytheeventstheASprovidesandthepermissionsoftheagents.
Globalstate:ToconstructaglobalAC-MASstatelE,l0,ln∈SfromansnapshotΣ,anAutoAgentbuertandthelocalagentstatesxi,weidentifylEwithΣandl0witht.
Thelocalstatesl1,lnoftheexternalagentcomprisethestateoftheprivatevariablesxiandtheprojectionsΣ|ioftheenvironmentsnapshotsuchthat:Σ|i={ι|ι∈Σ:ωi(ι)∧ι=ι|νi}whereι|νiistherestrictionoftheartifactinstanceιtothevariablesinνi(variablesnotinνiarereplacedby⊥).
TheinitialstateIistheemptystatewithoutanyartifactinstancesinΣorpendingtasksinl0.
Privatevariablesareinitialisedtotheirinitialvalue.
Protocol:Byconstruction,GSMexecutesonlyapplicableeventsandblocksallothers.
Artifactinstantiationeventsarealwayspermitted.
ThisisreectedintheenvironmentprotocolPE:PE(Σ)={a|ι∈Σ:(χ∈X(Γ)∧χ(ι,a))∨a∈inst}whereX(Γ)isthesetofallsentriesinthemilestonesandguardsofΓandχ(ι,a)istheevaluationofasentryχwithrespecttotheactionaandstatusattributesAttstatus∈ι.
Wewriteinstforthesetofartifactinstantiationevents.
TheAutoAgentstoresthesetofpendingtasksinitsbuertandsendsthematalaterpointtoΓ.
Thus,theprotocolsimplyselectsanypendingtaskfromitsbuerbyusingtheexpressionP0(t)={a|a∈t}.
Theprotocolofanagentigivesthesetofactionsthatareavailableinvisibleinstancesofitslocalstateandsatisfyitslocalprotocol:Pi(li)={a|ι∈li:a∈i(ι)∩i(ι,xi)}ThesecomponentssucetoinstantiateafullAC-MASfromDenition6.
WiththesedetailsinplaceweconcludetheformalmapfromA-GSMtoAC-MAS.
IntheremainderofthepaperwepresentanimplementationofamodelcheckerforIQ-CTLKonAC-MAS.
5ImplementationToperformAC-MASmodelchecking,wehaveextendedGSMC[13]modelcheck-ing.
Thenewversion,numbered0.
8.
51,iswritteninC++andusestheCUDD1Thepre-compiledbinariesofthetoolcanbedownloadedfromhttp://www.
doc.
ic.
ac.
uk/~pg809/gsmc/0.
8.
5.
tar.
gz64P.
Gonzalez,A.
Griesmayer,andA.
Lomuscio!
"Fig.
4.
ArchitectureofGSMClibrary[17]fortheback-endsymboliccomputations.
GSMCbuildsthemodelandthetransitionrelationandperformsasymbolicstatespaceexplorationbasedonBDDs.
TheGSMmodelandthespecicationoftheAutoAgentaredirectlyloadedfromtheBarcelonaXMLinputle;agentdenitionsaregiveninformofacongurationleasshowninFigure3.
TheinternalarchitectureofthemodelcheckerisillustratedinFigure4.
Toobtainnitestatemodels,weintroduceaboundonthenumberofinstancesthatcanbegeneratedanduseabstractiontocreatenitedata;anoverowagindicatesiftheboundwasreachedduringarun.
WeallocateBDDvariablesforthestatesoftheagentsandthemaximumnumberofartifactinstancespresentinarun.
ThebasiclayoutoftheBDDdatastructureisshowninFigure5.
WeintroduceanOverowagthatindicatesifthenumberofinstancesordatavalueswereexceededinarun.
Wepayspecialattentiontothiscasebecausesomeoftheresultsofthecheckmaybeunsoundandrequireare-checkwithhigherbounds.
WealsocapturetheEventIDandPayloadofthenextactionathatistobeexecuted.
TheartifactinstancescorrespondtoΣ.
Theactualnumberandsizeoftheseeldsdependontheartifacttypeandtheboundsthatarexedatthestartoftheverication.
ThespecialagCreatedineachartifactinstanceindicateswhetheritwasinstantiatedinthecorrespondingrun.
ThetaskbuereldstwithaPendingagandthecorrespondingpayloadbelongconceptuallytotheAutoAgent,butarestoredintheartifactstatespacefortechnicalreasons.
Privatevariablesofagentscompletethedatastructure.
AnyIQ-CTLKformulatobeveriedisrstrewrittenbyreplacingthequan-ticationoperatorswithformulasthatrangeovertheactualinstances.
However,becauseartifactinstancesarecreateddynamicallyatrun-time,thenumberofactiveinstancesisnotknownaprioriandneedstobeconsideredintheformula.
ModelCheckingGSM-BasedMulti-AgentSystems65OverflowEventIDPayloadTaskPendingTaskPayloadDataAttributesStatusAttributesCreatedTaskBuffertArtifactInstancesΣPendingEventePrivateAgentVariables.
.
.
Agent1AgentnFig.
5.
LayoutoftheBDDdatastructureWeusetheexpressioncreated(ι)tocheckifaninstancewascreated(theCreatedagisset)andrewritethequantiedformulasasfollows:x:ι∈Γcreated(ι)→x:ι∈Γcreated(ι)∧Notethat,foranyexistentialformulatobevalid,atleastoneoftheartifactinstancesneedstobeactive;thisisnotthecaseintheinitialstatebecausenoar-tifactinstancehasbeencreatedyet.
Quantierscanbearbitrarilynestedandareresolvedrecursively.
Oncethedetailsaboveareconsidered,GSMCfollowsexistingmethodologiestoperformthevericationoftemporal-epistemicformulas[18].
5.
1LimitationsTheboundinthenumberofinstancesrestrictsthepossiblebehaviourofthesystem,whiledataabstractionleadstoanoverapproximation.
Thismayleadtolossofsoundnessorcompletenesswhenthelimitofartifactinstancesisreached.
Theexactoutcomedependsonthetypeofthepropertyconsidered.
Aviolationofauniversalproperty,forinstance,doesdenoteaviolationonthefullunboundedmodeleveniftheboundwasexceededduringthecomputation.
Ifanexistentialpropertyisnotsatised,noconclusioncanbedrawnregardingthefullmodelingeneral.
Thesearelimitationsinthetechniqueatpresentbut,asweshowinthefollowing,interestingscenarioscanstillbeanalysed.
6ExperimentalResultsWeevaluatedGSMContheOrder-to-Cashscenario,asimpliedversionoftheIBMback-endordermanagementapplicationsuppliedbyIBMResearch[7].
Inthisscenarioamanufacturerschedulestheassemblyofaproductbasedona66P.
Gonzalez,A.
Griesmayer,andA.
LomuscioTable1.
PropertiesoftheOrder-To-CashcasestudyAGx:CO((x.
BId=Dio∧x.
Cancelled)→KDioEFx.
Received)(1)EFx:CO(x.
BId=Dio∧KDiox.
Received)(2)AGx:CO((x.
BId=Dio∧x.
Ready)→KDiox.
Parts=3)(3)EFx:CO(x.
BId=Dio∧x.
Cancelled∧Dio.
cancelled)(4)conrmedpurchaseorderfromacustomer.
Typically,aproductrequiresseveralcomponentsthataresourcedfromdierentsuppliers.
Afterallcomponentshavebeendeliveredtheproductisassembledandshippedtothecustomer.
TheGSMprogramisspeciedintheformofasingle-artifactBarcelonaschemaconsistingof9stagesand11milestones.
Toverifythemodelweper-formedsmallmodicationstoabstractfromconcreteproductsandcreatedthreeagentrolesfortheabovescenario:1)aCustomerwhocreatesanartifactinstancethatrepresentstheorderandcanonlyseeinstancestheycreated;2)aManu-facturerwhofullstheorderandcanseeonlyuncompletedinstancesoforderssenttohimbyacustomer;and3)aCarrierwhoshipsthenishedproducttothecustomer,andwhocanseeonlyinstancesofordersthataretobeshippedviathem.
Figure1givesthelifecycleofthePreparingstage.
Itiscontrolledsolelybythemanufacturer,who,uponreceivingtheorder,launchesaresearchprocesstoidentifysuitablesuppliersandorderstherequiredcomponents.
Theassemblingprocesscanbeginwhentherstcomponentisreceivedandremainsactiveuntilallthecomponentsarecollected.
Thisismodelledbyintroducingacounter;theprocessisconsideredcompletewhen3componentshavearrived.
Table1reportsthepropertieswecheckedfordierentnumbersofagentsandartifactinstances,whereDioisacustomeragent(Diogenes)andCOstandsfortheCustomerOrderartifacttype.
Property(1)representsthatDiogenesknowsthat,unlesshecancelsanorder,theproductcanalwaysbereceivedinallofhisorders.
(i.
e.
,thatthereisnodeadlockinprocessinganorder:Anordercanalwaysbedeliveredoriscancelled).
Tocheckthattheorderisprivatetothecustomer,property(2)expressesthatDiogenesmayknowaproductisreceivedforanorderwithdierentowner.
Property(3)encodestheabilityofanagenttodeduceinformationitcannotdirectlyobservebycheckingifDiogenesalwaysknowsthereare3PartscollectedinallofhisorderswhenthemilestoneReadyisachieved.
Property(4)impliesthatanagentotherthanDiogenescancancelanorderthatbelongstoDiogenes.
Thisisdonebyusingaprivatevariable,whichissettrueonlyifDiogenesexecutedtheCancelledevent.
Weranthetestsona64-bitFedora17Linuxmachinewitha2.
10GHzIntelCorei7processorand4GBRAMandmeasuredthenumberofreachablestates,memoryused,andCPUtimerequired.
Themodelcheckerevaluatedtheproper-ties(1)and(3)tobetrueandtheproperties(2)and(4)tobefalseinthemodel.
ThisisinlinewithourintuitionofthemodelandshowsthattheGSMprogramofOrder-to-Cashapplicationisindeedcorrectwithrespecttotherequirements.
ModelCheckingGSM-BasedMulti-AgentSystems67Table2.
Reachablestates,memoryandtimeusagefordierentnumbersofartifactinstancesιandagents3agents15agents#ι#statesMBs#statesMBs11.
17e2270.
12.
92e3310.
223.
71e3520.
74.
16e6704.
931.
16e5645.
95.
82e98465.
543.
67e69642.
18.
01e12222360.
251.
18e8195176.
71.
09e165391419.
6Table2reportstheperformancefor3agents(oneforeachrole)and15agentsrespectively(6customers,5manufacturers,and4carriers).
Weseethattherun-timegrowsexponentiallywiththenumberofartifactinstances,whilethenumberofagentsinuencestheresourceusageonlymoderately.
Thisisbecauseadditionalagentsaddfewerstatesthanadditionalartifactinstances.
Theresultsshowthatthetoolhastheabilitytoeectivelyhandlelargestatespaces,whichisrequiredtomodelrealisticartifactsystemswithcomplexagentinteractions.
7ConclusionsInthispaperweputforwardatechniqueforthepracticalvericationofGSM-basedMAS.
Theapproachconsistsofdeningaformalmapfromthedeclarative,executablelanguageGSMtoanextensionofpreviouslystudiedartifact-centricMAS,asemanticsforreasoningaboutMASinaquantiedsettingofthear-tifactsystemenvironment.
Wereportedonafully-edgedmodelcheckerthatimplementsthisformalmapandsupportstemporal-epistemicspecicationsinwhichquanticationisallowedoverartifactinstances.
TheexperimentalresultsobtainedagainsttheOrder-to-Cashapplicationledustoconcludethattheprac-ticalvericationofreasonablysophisticatedGSM-basedMASisfeasibleandscalableinvaluablescenariosinbusinessprocessesandservices.
However,GSMandBarcelonaarestillatopicofactiveresearchanddevelopmentandsophisti-catedandstablemodelsarehardtocomeby.
Weplantoextendtheworkreportedhereinanumberofways,includingthesupportoflimitedquanticationoverdata.
Theoreticalstudies[10,14]pointtohigh-undecidabilityinsettingswhereunboundeddataispresent.
Forthisreasonwewillworkonexistentialabstractionanddataabstractiontoachieveatransferofthevericationoutcomefromabstracttoconcretemodels.
Inparticularweworkon3valuedabstraction[19],anabstractiontechniquethatsupportsthedetectionofinsucientinformationintheabstraction.
68P.
Gonzalez,A.
Griesmayer,andA.
LomuscioReferences1.
Singh,M.
,Rao,A.
S.
,George,M.
:FormalmethodsinDAI:Logic-basedrepresen-tationandreasoning.
In:Wei,G.
(ed.
)MultiagentSystems:AModernApproachtoDistributedArticalIntelligence,pp.
331–376.
MITPress(1999)2.
Bultan,T.
,Su,J.
,Fu,X.
:Analyzingconversationsofwebservices.
IEEEInternetComputing10(1),18–25(2006)3.
Lomuscio,A.
,Qu,H.
,Solanki,M.
:Towardsverifyingcontractregulatedservicecomposition.
AutonomousAgentsandMulti-AgentSystems24(3),345–373(2012)4.
Singh,M.
P.
,Huhns,M.
N.
:Service-orientedcomputing-semantics,processes,agents.
Wiley(2005)5.
Baldoni,M.
,Baroglio,C.
,Mascardi,V.
:Specialissue:Agents,webservicesandontologies:Integratedmethodologies.
MultiagentandGridSystems6(2),103–104(2010)6.
Cohn,D.
,Hull,R.
:Businessartifacts:Adata-centricapproachtomodelingbusi-nessoperationsandprocesses.
BulletinoftheIEEEComputerSocietyTechnicalCommitteeonDataEngineering32(3),3–9(2009)7.
Hull,R.
,Damaggio,E.
,DeMasellis,R.
,etal.
:Businessartifactswithguard-stage-milestonelifecycles:managingartifactinteractionswithconditionsandevents.
In:ProceedingsoftheInternationalConferenceonDistributedEvent-BasedSystems(DEBS2011),pp.
51–62(2011)8.
ObjectManagementGroup:Proposalfor:Casemanagementmodelingandnota-tion(CMMN)specication1.
0,Documentbmi/12-02-09(February2012)9.
Deutsch,A.
,Sui,L.
,Vianu,V.
:Specicationandvericationofdata-drivenwebapplications.
JournalofComputerandSystemSciences73(3),442–474(2007)10.
Hariri,B.
B.
,Calvanese,D.
,Giacomo,G.
D.
,Deutsch,A.
,Montali,M.
:Vericationofrelationaldata-centricdynamicsystemswithexternalservices.
CoRR(2012)11.
Belardinelli,F.
,Lomuscio,A.
,Patrizi,F.
:Vericationofdeployedartifactsystemsviadataabstraction.
In:Kappel,G.
,Maamar,Z.
,Motahari-Nezhad,H.
R.
(eds.
)ICSOC2011.
LNCS,vol.
7084,pp.
142–156.
Springer,Heidelberg(2011)12.
Belardinelli,F.
,Lomuscio,A.
,Patrizi,F.
:VericationofGSM-basedartifact-centricsystemsthroughniteabstraction.
In:Liu,C.
,Ludwig,H.
,Toumani,F.
,Yu,Q.
(eds.
)ICSOC2012.
LNCS,vol.
7636,pp.
17–31.
Springer,Heidelberg(2012)13.
Gonzalez,P.
,Griesmayer,A.
,Lomuscio,A.
:VerifyingGSM-basedbusinessarti-facts.
In:ProceedingsofICWS2012,pp.
25–32(2012)14.
Belardinelli,F.
,Lomuscio,A.
,Patrizi,F.
:Anabstractiontechniqueforthever-icationofartifact-centricsystems.
In:ProceedingsofPrinciplesofKnowledgeRepresentationandReasoning(KR2012),pp.
319–328(2012)15.
Parikh,R.
,Ramanujam,R.
:Distributedprocessesandthelogicofknowledge.
In:Parikh,R.
(ed.
)LogicofPrograms1985.
LNCS,vol.
193,pp.
256–268.
Springer,Heidelberg(1985)16.
Fagin,R.
,Halpern,J.
Y.
,Moses,Y.
,Vardi,M.
Y.
:ReasoningAboutKnowledge.
TheMITPress(1995)17.
Somenzi,F.
:CUDD:CUdecisiondiagrampackage-release2.
5.
0(2012),http://vlsi.
colorado.
edu/~fabio/CUDD/(January2013)18.
Lomuscio,A.
,Qu,H.
,Raimondi,F.
:Mcmas:Amodelcheckerfortheverica-tionofmulti-agentsystems.
In:Bouajjani,A.
,Maler,O.
(eds.
)CAV2009.
LNCS,vol.
5643,pp.
682–688.
Springer,Heidelberg(2009)19.
Shoham,S.
,Grumberg,O.
:3-valuedabstraction:Moreprecisionatlesscost.
In-formationandComputation206(11),1313–1333(2008)