Data decision diagrams for Petri net analysis

DataDecisionDiagramsforPetriNetsAnalysisJean-MichelCouvreur1,EmmanuelleEncrenaz2,EmmanuelPaviot-Adet2,DenisPoitrenaud2,andPierre-Andr´eWacrenier11LaBRI,Universit´eBordeaux1,Talence,[e-mail]2LIP6,Universit´ePierreetMarieCurie,Paris,[e-mail]astructure,theDataDeci-sionDiagrams,equippedwithamechanismallowingthedefinitionofapplication-specificoperators.Thismechanismisbasedoncombinationofinductivelinearfunctionsofferingalargeexpressivenesswhilealle-viatingfortheusertheburdenofhardcodingtraversalsinashareddatastructure.WedemonstratethepertinenceofoursystemthroughtheimplementationofaverificationtoolforvariousclassesofPetrinetsincludingselfmodifyingandqueuingnets.Topics.PetriNets,DecisionDiagram,Systemverification.1IntroductionThedesignandverificationofdistributedsystemspresentascientificandtech-nicalchallengethatmustbemetbyacombinationoftechniquesthatscaleuptothecomplexityofsystemsproducedinindustrialapplications.Simulationisalreadyarecognizedtoolwithinindustriesdealingwithcomplexsystemssuchastelecommunicationsoraeronautics.Evenifanacceptabledegreeofconfidencecanbereachedviathistechnique,exhaustivenesscannotgenerallybereachedduetothenumberofpossiblestatesofthesesystems.Inthe90’s,theelectronicindustries,insearchoftoolstoincreasetheirconfi-dencelevelintheirfinalproduct,adoptedtheBinaryDecisionDiagrams(BDDs)[?]asawaytodealwiththehighcomplexityoftheircomponents.BDDcanbeviewedasatreestructure:binaryvariablesinvolvedinstatesareordered,asetofnodesisassociatedtoeachvariableandthevariablevaluationsareasso-ciatedtothearcsbetweennodes.Whenimplemented,theuniquenessofBDDs,combinedwiththetreestructure,ensuresanefficienttechniquetodealwithnumerousstates[?,?].Thenexhaustivenesscouldbehandled,evenwithbillionsandbillionsofstatestoverify.TheBDDsexpressivepowerislargeenoughtodealwithalargeclassoffinitestatesystem.Evendynamicsystemscanbeverifiedusingsuchatechnique[?].Therefore,otherdomains,likeparallelsystemverification,triedtouseBDDstoverifycomplexsystems[?].Sincethenumberofvariablesofthestudiedsystemisacriticalparameter,numerousBDD-likestructureswerecreatedinordertoadaptthetreestructuretoparticularneeds[?,?].LikeBDDs,theshared-treestructuresareusuallystucktoapreciseinter-pretation.Therefore,dealingwithstatesofanewkindofmodelusuallyleadstothedesignofnewkindsofstructuresortonewkindsofoperatorsonexistingstructures.Inthispaper,anewtreestructure,theDataDecisionsDiagrams(DDDs),isintroduced.OurgoalistoprovideaflexibletoolthatcanbeeasilyadaptedtoanykindofmodelandthatoffersthesamestoragecapabilitiesastheBDD-likestructures.Unlikepreviousworksonthesubject,operatorsonthestructurearenothard-coded,butaclassofoperators,calledhomomorphisms,areintro-ducedtoallowtransitionrulescoding.Aspecialkindofhomomorphisms,calledinductivehomomorphisms,allowstodefine”local”homomorphisms,i.e.homo-morphismsthatonlyuseinformationlocaltoanodeinitsdefinition.Togetherwithcomposition,concatenation,union...operations,generalhomomorphismsaredefined.Inourmodel,anodeisassociatedtoavariableandvaluationsareassociatedtoarcs.Thevariablesdomainisinteger,butwedonothavetoknowaprioribounds.AnothernicefeatureoftheDDDsisthatnovariableorderingispresupposedindefinition.Moreover,variablesarenotassumedtobepartofallpaths.Theyalsocanbeseenmanytimesalongthesamepath.Therefore,themaximallengthofapathinthetreeisnotfixed.ThisfeatureisveryusefulwhendealingwithdynamicmodelslikequeuingPetrinets,butalsowhenatemporaryvariableisneeded(cfthemechanismweusedtocodeselfmodifyingnetsfiringrules).Evenifaglobalvariableorderingisusefultoobtainanefficientstorage,thefactthatthisorderingisnotpartofthedefinitionintroducesagreatflexibilitywhenoneneedstoencodeastate.Sinceweusetechniquesthathavebeenshownefficienttostoresetofstates,sincestatecodingisveryflexibleandsinceoperatordefinitionisbasedonawell-foundedtheoreticalfoundation,DDDisatreestructurethatcanbeeasilyadaptedtoanykindofcomputationalmodel.Thispaperisstructuredthefollowingway:Section2describesDDDs,thehomomorphisms,andgivessomehintsontheimplementationwemadeinourprototype.Section3describesapossibleuseofDDDsforordinaryPetrinetsandsomeofthemostpopularextensions(inhibitorsarcs,capacityplaces,resetarcs,selfmodifyingnets,queuingnets).Section4givesconclusionswithperspectives.2DataDecisionDiagrams2.1DefinitionsofDDDsDataDecisionDiagrams(DDD)aredatastructuresforrepresentingsetsofse-quencesofassignmentsoftheforme1=x1;e2=x2;en=xnwhereeiarevariablesandxiarevalues.Whenanorderingonthevariablesisfixedandthevariablesareboolean,DDDcoincideswiththewell-knowBinaryDecisionDi-agram.Ifanorderingonthevariablesistheonlyassumption,DDDsarethespecializedversionoftheMulti-valuedDecisionDiagramsrepresentingcharac-teristicfunctionofsets[?,?].ForDataDecisionDiagram,weassumenovariableorderingand,evenmore,thesamevariablemayoccurmanytimesinanassign-mentsequence,allowingtherepresentationofdynamicstructures.Traditionally,decisiondiagramsareoftenencodedasdecisiontrees.Figure1,left-handside,showsthedecisiontreeforthesetofsequencesofassignmentsA=f(a=1;a=1);(a=1;a=2;b=0)