Recognizing finite repetitive scheduling patterns in manufacturing systems

MartijnHendriks1∗,BarendvandenNieuwelaar2†,FritsVaandrager1∗

1NijmeegsInstituutvoorInformaticaenInformatiekunde,

UniversityofNijmegen,TheNetherlands

martijnh@cs.kun.nl,fvaan@cs.kun.nl

2DepartmentofMechanicalEngineering,

EindhovenUniversityofTechnology,TheNetherlands

N.J.M.v.d.Nieuwelaar@tue.nl

Abstract

Optimizationoftimingbehaviourofmanufacturingsystemscanbere-gardedasaschedulingprobleminwhichtasksmodelthevariouspro-ductionprocesses.Typicalformanymanufacturingsystemsisthattasksorcollectionsoftaskscanbeassociatedwithmanufacturingen-tities,whichcanbestructuredhierarchically.Executionofproductionprocessesforseveralinstancesoftheseentitiesresultsinnestedfiniterepetitions,whichblowsupthesizeofthetaskgraphthatisneededforthespecificationoftheschedulingproblem,and,inanevenworseway,thenumberofpossibleschedules.WepresentasubclassofUMLactivitydiagramswhichisgenericforthenumberofrepetitions,andthereforesuitableforthecompactspecificationoftaskgraphsforthesemanufacturingsystems.Theapproachtoreducethecomplexityoftheschedulingproblemexploitstherepetitivepatternsextractedfromtheactivitydiagrams.Itreducestheoriginalproblemtoaproblemcontain-ingsomeminimalnumberofidenticalrepetitions,andafterschedulingofthismuchsmallerproblemthescheduleisexpandedtotheoriginalsize.Wedemonstrateourtechniqueonareal-lifeexamplefromthesemiconductorindustry.

Keywords:Scheduling,manufacturingsystems,UMLactivitydiagrams,finiterepet-itivebehaviour.

∗Supported†Part-time

bytheEuropeanCommunityProjectIST-2001-35304(AMETIST).softwarearchitectatASML.

1.Introduction

Schedulinginmanufacturingsystemshasreceivedmuchattentionintheliterature.Thebasicschedulingissue,theassignmentofmutuallyexclusiveresourcestotasks,isaddressedintheJobShopSchedulingliterature[13,19].Inaddition,insomecasesalsotheorderoftasksforasingleresourceinfluencestemporalbehaviourofthemanufacturingsystem[8],analogoustotheTravelingSalesmanProblem[10].BothoftheseproblemsareNPhardtosolve.Combinationoftheseoptimizationproblemsandthesizeanddiversityofpracticalmanufacturingcasesmakesschedulingofmanufacturingsystemsaninterestingchallenge.In[12],anoverviewofspecificschedulingissuesplayingaroleinman-ufacturingsystemscanbefound.Oneofthemisthefactthatthesamemanufacturingprocesseshavetobeexecutedrepetitivelyforseveralin-stancesofmanufacturingentities.Often,therelationsbetweentheman-ufacturingentitiesarehierarchical.Forexample,consideranassemblysystem.Afinalproductinsuchasystem,calledanassembly,cancon-sistofsub-assemblies,whichinturncanconsistofsub-sub-assemblies.Productsaremanufacturedinbatchesandmanufacturingordersconsistofmultiplebatches.Therelationshipsbetweenthemanufacturingenti-tiesofthissystemcanbeexpressedbytheEntity-RelationshipDiagram(ERD)ofFigure1.

Entity A

1

n

Entity B

1

n

Entity C

1

n

Entity D

1

n

Entity E

Figure1:Hierarchicalstructureofmanufacturingentities.

Fortheassemblysystemexample,entitiesAthroughEcanbeasso-ciatedwithorder,batch,product,sub-assembly,andsub-sub-assembly,respectively.Anotherexamplewithhierarchicalmanufacturingentityrelationsconcernspackaging.Forinstance,amanufacturingorderofabeerbreweryconsistsofseveralpallets,containingseveralcrateswithseveralbottlesofbeer.Athirdexampleconcernsawaferscannerman-ufacturingsystemfromthesemiconductorindustry[1].Wafersarealsoproducedinbatches(lots).Awaferscannerprojectsamaskonawafer,usinglight.Eventually,theprojectedmasksresultinIntegratedCircuits(ICs).Ononewafer,multipleICsandtypesofICsaremanufactured.MultipletypesofICsinvolvemultiplemasks,andmultiplemasksareplacedonareticle.ThemanufacturingentitiescanbemodeledasinFigure1,whereentityAthroughEcanbeassociatedwithlot,wafer,reticle,mask,andIC,respectively.Asthisexampleconcernsnotonlyentitiesthatendupinthefinalproductbutalsootherentitiesrequired

formanufacturing,thisexampleisconsideredintheremainderofthispaper.

Repetitiveexecutionofmanufacturingprocessesforseveralinstancesofmanufacturingentitiesleadstofiniterepetitivepatternsinmanufac-turingschedules.Inpractice,executionofthefirstfewinstancesandlastfewinstancesofamanufacturingentitydifferslightlyfromtherest.Thisisalargedifferencewithunlimitedrepetitivebehaviourofmanufac-turingsystems,whichhasreceivedmuchattentioninliterature[14,20].Furthermore,thehierarchicalstructureofthemanufacturingentitiesleadstopatternsonseveralgranularitylevels.Thepurposeofthispa-peristodescribeanapproachtoidentifyexactlyidenticalrepetitiveschedulingpatternsinordertoreducethecomplexityoftheschedul-ingproblem.Withthisinformation,a(sub-)optimizedmanufacturingschedulecanbecreatedbyconcatenationoftheoptimizedsub-schedulesofthepatterns.Withoutthisinformation,combinationofthepossiblesub-schedulesfortheserecurrentpatternsblowsupthenumberofpos-sibleoverallschedulesdramatically.

Concretely,ourcontributionistwofold.First,weintroduceasubclassofUMLactivitydiagrams[16,17]forthecompactspecificationoftaskgraphswhichmaycontainfiniterepetitivebehaviour.Essentially,thesametypeofactivitydiagramsisusedwithinASMLtospecifyschedul-ingproblems.Thekeytechnicaldifficultythatwefacewhengivingaformaldefinitionofthissubclassofactivitydiagramsistoruleoutcertainundesiredraceconditions.Thesecondpartofourcontributionconsistsofamethodforfindingrepetitivesubgraphsinthesetaskgraphsusingtheactivitydiagrams.Thisinformationcanbeexploitedtospeeduptheschedulingprocessinadramaticway.Weshowthisbyapplyingourtechniquetoareal-lifeexamplefromthesemiconductorindustry.Relatedwork.In[15]UMLactivitydiagramsthatspecifyschedulingproblemsaretranslatedtotimedautomatamodels.Schedulabilityoftheactivitydiagramistranslatedtoareachabilityproperty,whichischeckedbytheUppaalmodelchecker[9].Ifthepropertyissatisfied(theactivitydiagramisschedulable),thenatracethatprovesthepropertyisequivalenttoaschedulefortheactivitydiagram.Althoughtheexplosionoftheschedulingeffortduetohierarchical,finiterepetitionsisrecognizedin[15],nosolutionisprovided.

Relatedworkw.r.t.thesemanticsofUMLactivitydiagramsincludestheverificationofworkflowmodelsspecifiedbythesediagrams[4].Incontrasttoourwork,thesemanticsof[4]associatesatransitionsystemtoeachactivitydiagram,usingsomeformof“tokengame”.Thetran-sitionsystemsemanticsof[4]canserveasabasisforverificationusingmodelcheckingbut,unlikeourtaskgraph(partialorder)semantics,it

cannotbeusedasastartingpointforsolvingschedulingproblems.An-othersemanticsforUMLactivitydiagramsisprovidedby[6],usingastraightforwardtranslationtoPetrinets.However,thissemanticsdoesnotaddresstheevaluationofconditionals,andasaresultitisunclearhowtoextractataskgraphinordertoaddressschedulingissues.

Relatedworkw.r.t.thesecondpartofourcontributionincludestheCabinssystem[11].Itis“anintegratedframeworkofiterativerevisionintegratedwithknowledgeacquisitionandlearningforoptimizationinill-structureddomains”(quotedfromtheCabinsweb-site).Inthisap-proachknowledgeabouttaskpatternsthatalreadyhavebeenscheduledbeforeisusedtoimproveschedules.Thereare,however,numerousdif-ferencebetweentheCabinsapproachandours.Forinstance,wedonotuselearning,andCabinssupportsrun-timeschedulingwhereasourapproachisstatic.

Alsorelatedisthecomputer-aideddesignofvideoprocessingalgo-rithmsof[18].Mostvideoalgorithmsconsistofrepetitiveexecutionsofoperationsondata,whichcanbedescribedbyusingnestedloopsandmultidimensionalarrays.Theschedulingprobleminthiscaseistominimizeaparticularcostfunctionwhilesatisfyingcertaintiming,resourceandprecedenceconstraints.However,apparentlynoexploita-tionofequalityofloopinstancestakesplace.Ourworkalsorelatestowideningandaccelerationtechniques(e.g.,[3]and[2,7]),whichtrytoacceleratethefixed-pointcomputationofreachablesets.Atleasttheapproachesinthelattertwousestaticanalysisofthecontrolgraph(thesyntax)todetectinterestingcycles,ofwhichtheresultofiteratedexecutioncanbecomputedbyonesinglemeta-transition.Thesemeta-transitionsarethenaddedtothesystemandfavoredbythestatespaceexplorationalgorithm,resultinginfasterexplorationofthestatespace.Ourtechniquealsoexploitscyclicstructures,yetnotinthesyntax,butinthesemanticsoftheactivitydiagrams,toderivefuturebehaviour.Whenthisisdoneduringtheactualscheduling,itcanberegardedasaformofacceleration.Wearenotawareofanyotherrelatedwork.

Outline.Thepaperisstructuredasfollows.InSection2,activitygraphs–asubclassofUMLactivitydiagrams–areintroduced,whicharesuitedtomodelfiniterepetitivebehaviourofmanufacturingsys-tems.Subsequently,weformallydefinethesyntaxofactivitygraphs,andwedefinethesemanticsbyassociationoftaskgraphs.Section3discussesanapproachtorecognizerepetitivepatternsintaskgraphsus-ingtheactivitydiagramitisassociatedwith.Moreover,weshowhowthisinformationcanbeusedinareal-lifeindustrialexample.Finally,concludingremarksarepresentedinSection4.

2.ActivityGraphs

Taskgraphsarebasicobjectsforthespecificationofschedulingprob-lems.Theyarelesssuitedforthespecificationofmanufacturingsystemswithfiniterepetitivebehaviour.Considerfigure1andassumethatweneedtoproduce5unitsofeachentitytobeabletoproduceitsparententity.Ataskgraphdescribingsuchaproblemthenconsistsof55subgraphsfortheproductionoftheneededquantityofentityE.Inotherwords,thetaskgraphmaybeexponentiallylarge(orevenworse!)inthenumberofdifferententities,whichmakesspecificationusingataskgraphandschedulinginconvenient.

InSection2.1weintroduceasubclassofUMLactivitydiagramsforthecompactspecificationoftaskgraphswhichmaycontainlim-itedrepetitivebehaviour[16,17].Section2.2associatestaskgraphswithactivitydiagramsusingtheso-calledrelevancymapping,whichisneededtoexcludethepossibilitythatanactivitydiagramisambiguous(i.e.canbeassociatedwithmultipletaskgraphs)duetoraceconditions.

2.1FormalDefinitionofActivityGraphs

Activitygraphsaredirectedgraphswithdifferenttypesofvertices(a.k.a.nodes),whichcorrespondtothetypesinUMLactivitydiagrams,andwithanannotationoftheconditionalnodes,whichisusedtospecifyfiniterepetitionsofsubgraphs.Theactualschedulingoftaskgraphsisnotconsideredinthepresentpaper.Therefore,weomitthedurationsandresourcerequirementsoftheactivities/tasksinalldefinitions.

Definition1(Activitygraph)Anactivitygraphisdefinedbyatuple(N,n0,󰀁,c),where

Nisafinitesetofnodes,partitionedintothesetsC,F,J,A,MandEwhicharesetsofconditional,fork,join,activity,mergeandexitnodesrespectively,n0∈F∪A∪Mistheinitialnode,

󰀁⊆N×Nisthesetofprecedenceedgessuchthat:

–exitnodeshavenosuccessors,forknodeshaveatleasttwosuccessors,conditionalnodeshavetwosuccessors,andothernodeshaveonesuccessor,and

–joinandmergenodeshaveatleastonepredecessor,andothernodeshaveonepredecessor.Theinitialnodeisanexceptionsinceitmayhavenopredecessors.Wewritev󰀁v󰀂for(v,v󰀂)∈󰀁.

c:C→N×(N\\{0})×N×2Cistheconditionalfunctionsuchthat:ifc(v)=(v󰀂,n,v󰀂󰀂,R),thenv󰀁v󰀂andv󰀁v󰀂󰀂.Wecallv󰀁v󰀂thetrueedgeofv,ntheupperboundofvdenotedbyub(v),v󰀁v󰀂󰀂thefalseedgeofv,andRtheresetsetofv.Wecanexplaintheconditionalfunctioncasfollows.Assumethatc(v)=(v󰀂,n,v󰀂󰀂,R).Thismeansthatinitiallythetrueedgeofvisenabledandthefalseedgeofvisdisabled.Afternexecutionsofthetrueedgeitbecomesdisabledandthefalseedgebecomesenabled.Theenablednesscanberesettotheinitialsituationbytakingafalseedgeofaconditionalwsuchthatvisintheresetsetofw.

WeusetheregularUMLconventionsforthegraphicalrepresentationofactivitydiagramstorepresentouractivitygraphs[16].Summariz-ing,forksandjoinsarerepresentedbybars,mergesbydiamondshapeswithoneoutgoingarrow,activitiesbyboxeswithanameinside,exitsbycircledblackdots,andconditionalsbydiamondswithtwoguardedoutgoingedges.Theinitialnodeisprecededbyablackdot.Inourrepresentationweusetheconditionalsas“counters”tokeeptrackofthenumberofexecutionsofthetrueedgeoftheconditional.

A1[c1>=2][c1<2][c2<2][c2>=2]A2A3Figure2:Asmallactivitygraph.

Forinstance,Figure2depictsasmallactivitygraphthathasthreeactivitiesandusestwoconditionals,c1andc2.Thereisonecycle,con-trolledbytheconditionals,thatisexecutedtwiceandinwhichactivitiesA2andA3canruninparallel.ActivityA1mustberunonce,andthiscanhappeninparallelwiththecycle.

2.2FromActivityGraphstoTaskGraphs

Wedefinethesemanticsofanactivitygraphbyunfoldingit(whichmeansresolvingtheconditionalchoices)toobtainallreachableinstancesofnodesandtheirprecedencerelation.Forinstance,Figure3depictstheintendedunfoldingoftheactivitygraphinFigure2.

A2A3A2A3A1Figure3:TheintendedunfoldingoftheactivitygraphofFigure2.

Althoughtheunfoldingoperationisintuitivelyquiteclear,adifficultyconcerningraceconditionsexists.Consider,forinstance,theactivitygraphofFigure4.Wecanunfoldthisgraphintwoways,sincewecanchoosewhentoresetc1.Thefirstunfoldingcontainsoneinstanceofbothactivities,whereasthesecondunfoldingcontainstwoinstancesofactivityA1andoneinstanceofactivityA2.Thisexampleshowsthatanactivitygraphmaycontainraceconditionsinwhichtwoparallelbranchesofaforkusethesameconditionalcounter,whichresultsinanon-uniqueunfolding.Suchraceconditionsareundesirableandwewanttorestrictourselvestoasubclassofactivitygraphsthatdonotcontainraceconditionsandwhichhaveauniqueunfolding.

[c1>=2][c1<2][c1>=1][c1<1][c2>=1]c1:=0[c2<1]A1A2A1A2Figure4:Anon-deterministicactivitygraph.

Figure5:Anactivitygraphwhichrequirestheuseofadditionalcoun-ters.

Inordertoforbidsituationsinwhichanactivitygraphcanbeunfoldedinmorethanoneway,werequiretheexistenceofadistributionoftheprivilegesofusingtheconditionalsoverthevariousparallelbranchesin

theactivitygraph.Weobtainsuchadistribution,arelevancymapping,byassigningasetofrelevantconditionalnodestoeachnodeinanac-tivitygraph.Inordertoexcluderaceconditions,weforbidparallelismofnodesthathaveoverlappingrelevancysets.Forinstance,thecondi-tionalc1isrelevantforbothparallelbranchesoftheforknodeinFigure4,whichrendersauniqueunfoldingimpossible.

Toavoidproblemswith,forinstance,theunfoldingoftheactivitygraphinFigure5,weextendtherangeoftherelevancymappingtoallnodes1.Therationalebehindtheformaldefinitionoftherelevancymappingisasfollows.First,werequirethatanodeisrelevantforitself,andtheresetsetofaconditionalisrelevantforthatconditional.Second,werequirethatrelevancyispassedontoneighboringnodes,exceptnotforwardthroughforksandnotbackwardthroughjoins(weconsidertheselasttwosituationsseparately).Thisisnecessarytogiveaninductivedefinitionoftheunfoldingoperation.Third,ifanodeisrelevantforthesuccessorofafork,thenitisalsorelevantforthefork.Moreover,therelevancysetsofanytwodifferentsuccessorsofaforkaredisjoint.Thefirstpartisnecessaryfortheinductivedefinition,andthesecondpartistoavoidraceconditions.Fourth,werequirethatthesetofrelevancysetsofthepredecessorsofajoinisapartitioningoftherelevancysetofthejoin,which,again,isnecessaryfortheinductivedefinition.Thesefourpointsareformalizedasfollows:

Definition2(Relevancymapping)Arelevancymappingforanac-tivitygraph(N,n0,󰀁,c)isafunctionX:N→2Nsuchthat:

(i)Ifvisaconditionalnodewithc(v)=(v󰀂,n,v󰀂󰀂,R),then{v}∪R⊆

X(v).Otherwise,v∈X(v).(ii)Ifv󰀁v󰀂,visnotaforknodeandv󰀂isnotajoinnode,then

X(v)=X(v󰀂).(iii)Ifvisaforknodewithsuccessorsv1,...,vn,then∪ni=1X(vi)⊆X(v)

andX(vi)∩X(vj)=∅forall1≤i=j≤n.(iv)Ifvisajoinnodewithpredecessorsv1,...,vn,thenwerequire

X(v)=∪nj≤n.i=1X(vi)andX(vi)∩X(vj)=∅forall1≤i=

thatthenodesinaunfoldingaretuples(v,γ),wherevisanodeandγisavaluation

oftheconditionalswhicharerelevantforthatnode(γ(v)countsthenumberofexecutionsofthetrueedgeofvsinceitslastreset).NowconsiderFigure5.Whenweconstructthesetofrelevantconditionalsforeachnode,weseethateitherA1mustbelabeledwithc1orA2mustbelabeledwithc1(otherwisewecannotgiveacleaninductivedefinitionoftheunfoldingoperation).IfweassumethatA1islabeledwithc1,andweunfoldtheactivitygraph,thenweseethatonlyoneinstanceofA2appears,namely(A2,∅),sinceA2hasanemptyrelevancyset.This,ofcourse,isnotwhatweexpectfromtheunfolding.

1Assume

WecanshowthattheproblemwhetherageneralactivitygraphhasarelevancymappingisNP-completebyareductionfrom3-SATwithoutnegationandwithexactlyonetrueliteralperclause[5].However,forthemorerestrictedclassofactivitygraphsforwhichholdsthateverynodeisreachablefromtheinitialnode–whichisnotalimitingassumption–wecannotfindareduction,yetwealsocannotfindapolynomialalgorithm.Inpracticeweuseanadhocalgorithmtofindarelevancymappingthatworksfineforallactivitygraphsthatappearinthepresentpaper.

Inordertodefinethesemanticsofanactivitygraph,wedefineΓNforanactivitygraphwithnodesNasthesetofpartialfunctionswithtypeN󰀁→N.Wecallaγ∈ΓNanodevaluationandweusethefollowingabbreviations:γ[v:=v+1]mapseverynodenotequaltovtothesamevalueasγ,anditmapsv,ifitisdefinedbyγ,tothevalueγ(v)+1.Similarly,γ[R:=0]agreeswithγonthevalueofeverynodenotinRanditmapseverynodeinR,ifitisdefinedbyγ,tozero.Ifγ,γ󰀂∈ΓNandtheybotharedefinedfordisjointsetsofnodes,thenweletγ∪γ󰀂denotethenodevaluationthatisdefinedfortheunionofthesenodesetsaccordingtoγandγ󰀂.Finally,ifγ∈ΓNandSisasubsetofnodes,thenwelet[γ]SdenotethepartialnodevaluationthatisobtainedbyprojectingγtoS.

Forsimplicitywemaketwoassumptionsaboutouractivitygraphs:(1)aconditionalnodeisnotimmediatelyfollowedbyajoinnode,and(2)aforknodeisnotimmediatelyfollowedbyajoinnode.Notethatwecaneasilyeliminatetheseconstructionsinanactivitygraphbyadding“dummymerges”withonlyonepredecessor.Therefore,theseassump-tionscanbemadewithoutlossofgenerality,yettheymakethefollowingdefinitionmuchshorter.

Definition3(Unfolding)LetA=(N,n0,󰀁,c)beanactivitygraph(Nispartitionedintheusualway)withrelevancymappingX.TheunfoldingofAisadirectedgraph(V,→),whereV⊆N×ΓNisthesetofnodeinstances,and→⊆V×Visasetofdirectededges,inductivelydefinedasfollows:

(i)Thebaseclauseis:{(n0,γ0)}∈V,whereγ0(v)=0ifv∈X(n0)

anditisundefinedotherwise.(ii)Theinductiveclausesare2:

(v,γ)∈Vv∈J∪M∪Av󰀁v󰀂v󰀂∈/J󰀂󰀂󰀂󰀂󰀂(v,γ)∈V(v,γ)→(v,γ)whereγ=γ[v:=v+1]2Essentially

(1)

thisisaparameterizeddefinition.Thus,foreachactivitygraph,wecanfinda

finitesetofinductiveclauses,whichare“instances”oftheparameterizedclauses,thatareusedfortheconstructionoftheunfoldingofthatparticularactivitygraph.

(v,γ)∈Vv∈Fv󰀁v1,···,v󰀁vn

(vi,γi)∈V(v,γ)→(vi,γi)whereγi=[γ]X(vi)[v:=v+1](v1,γ1),···,(vn,γn)∈Vv1󰀁v,···,vn󰀁v

γ1(v1)=···=γn(vn)v∈J

(v,γ)∈V(vi,γi)→(v,γ)whereγ=∪ni=1γi[vi:=vi+1](v,γ)∈Vv∈Cc(v)=(v󰀂,n,v󰀂󰀂,R)γ(v)(v󰀂󰀂,γ󰀂󰀂)∈V(v,γ)→(v󰀂󰀂,γ󰀂󰀂)whereγ󰀂󰀂=γ[v:=v+1][R:=0](2)

(3)(4)(5)

Allsuccessorsorpredecessorsareconsideredinrules(2)and(3).Theinductivedefinitionoftheunfoldingofanactivitygraphhasauniquesolution.Forinstance,theunfoldingoftheactivitygraphinFigure2indeedistheoneinFigure3(weomittedthenodevaluations,sincethatunnecessarilycomplicatesthepicture).

Anactivitygraphforwhichholdsthatitsunfoldinghasno“looseends”(whicharenonexitinstanceswithnosuccessors)iscalledwell-defined.Forinstance,theunfoldinginFigure3iswell-defined.However,ifweconstructtheunfoldingfortheactivitygraphinFigure2inwhichwehavereplacedtheupperboundofconditionalc1with3,thenweseethatthethirdinstanceofactivityA2isalooseend,sincetherewillbeonlytwoinstancesofactivityA3.

Notethattheunfoldingofawell-definedactivitygraphcanbeconsid-eredasanewactivitygraphinwhichallconditionalshavebeenreplacedbymerges.Compare,forinstance,theactivitygraphinFigure2anditsunfoldinginFigure3.

Letaandbbetwoinstancesinsomeunfolding.Ifthereisapathfromatob,thenwedenotethisbya→∗b.Apathconsistingofatleastoneedgeisdenotedbya→+b.Wedefineparallelismofinstancesasfollows:

a󰀘b

⇐⇒

(a→∗b∧b→∗a)

Wesaythataninstanceaisnon-parallelifthereisnoinstancebsuchthata󰀘b.Wenowinformallystatesomeusefulpropertiesofunfoldings.(Fortheformalstatementandproofoftheseitemswerefertotheappendix.)

Manydifferentrelevancymappingsmayexistforanactivitygraph,buttheyallleadtoisomorphicunfoldings(Lemma12).

A2A3A1

A2A3Figure6:ThetaskgraphoftheunfoldinginFigure3.

Raceconditionsdonotappearinactivitygraphswhichhavearel-evancymapping.Thus,nodeinstanceswhichusethesamenodesarenotparallel(Lemma5).

Theinstancesinawell-definedunfoldingsatisfythesamerequire-mentsonthenumberofsuccessorsandpredecessorsastheirnodesintheactivitygraph,exceptthatmergeinstanceshaveonepre-decessorandconditionalinstanceshaveonesuccessor(Lemmas8and6).

Anunfoldingisacyclic,butitmightbeinfinite(Lemma9).Thereexistsasufficientsyntacticalconditiononactivitygraphsthatensuresfinitenessoftheunfolding.Wecancheckthiscondi-tionintimepolynomialinthesizeoftheactivitygraph(Lemma10).

Thecontrolstructureinstances(allinstancesbutthoseofactivitynodes)canbe“strippedaway”asconditionalandmergeinstanceshavenofunctionanymore(seethethirdbulletabove).Theresultingstructureisthetaskgraph.Hence,wecallinstancesofactivitynodestasks.

Definition4Let(V,→)betheunfoldingofactivitygraphA.ThetaskgraphofAisthetuple(T,→),where

T={(v,γ)∈V|visanactivitynode},and→⊆T×Tdefinedas:a→bifandonlyif–a→+b,and

–noc∈T\\{b}existssuchthata→+candc→+b.

Thefactthattherearenocyclesinanunfoldingimpliesthatthetaskgraphisacyclictoo.Forinstance,Figure6depictsthetaskgraphoftheunfoldinginFigure3.(Again,thenodevaluationsoftheinstancesarenotdepicted.)

3.

AnApproachtoExploitRepetitiveStructuresinActivityGraphs

Intheprevioussectionweintroducedactivitygraphsasameansforthespecificationofschedulingproblemsformanufacturingsystemswithafiniterepetitivecontrolstructure.Thesemanticsoftheseactivitygraphswasdefinedintermsofunfoldings,whichinturndefine(possiblyinfinite)taskgraphs.

ApartfromtheknownNP-hardnessofthetaskgraphschedulingproblem,wealsofaceapossibleblow-upinsizeofthetaskgraphduetonestedcycles.Thismakestheapproachinwhichwestraightforwardlyunfoldtheactivitygraphandfeedittoaschedulerinfeasible.Instead,wefindso-calledcyclicstructuresintheactivitygraph,whicharesubgraphsthatappearmorethanonceintheunfolding.Thesecyclicstructurescanbeexploitedduringscheduling,sincetheyalsodefinereappearingsubgraphsinthetaskgraph.Hence,onlyonesuchasubgraphneedstobescheduled.

Ourapproachconsistsofthreesteps.First,welowertheupperboundsofconditionalstovaluesassmallaspossible,whichmeansthatwearejustabletorecognizecyclicstructuresinthecondensedactivitygraph.Second,wecomputethetaskgraphofthecondensedgraph,anduseregularschedulingtoolstofindasolutionforthisrelativelysmallprob-lem.Third,usingthecyclicstructuresandtheschedule,weconstructaschedulefortheoriginal,generallymuchlarger,activitygraph.

3.1FormalizingtheApproach

Inthissectionweformalizeourthreestepplanintroducedaboveforschedulingactivitygraphs.Thefirststepinvolvesdecreasingtheupperboundsoftheconditionalsthatcontrolthecyclesintheactivitygraphsuchthattheyareminimalw.r.t.todetectingthecyclicstructures.Atthismoment,ourapproachforfindingtheminimalactivitygraphisasfollows:

Theactivitygraphhasbeenconstructedwithaclearviewofwhatitshouldmean.Therefore,itisknownwhichconditionals(orsetsofconditionals)specifythecyclesofthemanufacturingprocess.Thefirststepistosettheupperboundsofalltheseconditionalstothevaluesuchthatatleastoneregularinstanceofthemanu-facturingentityispresent.E.g.,allleadingmanufacturingentities(thatdifferslightlyfromnormalones)arepresent,plusasingleregularentity.Iftheactivitiestobedoneforallentitiesarethesame,thentheupperboundissettoone.

Incrementthelowerboundsofallconditionalsthatcontrolasinglecycle,untiltheactivitygraphis“extendable”fortheconditionals(belowweformallyexplainwhatextendabilitymeans).Theorderofthissearchprocesscanbearbitrary.

Wedefinewhatweexactlymeanwithincrementingupperbounds.

Definition5((G,n)-extension)LetAbeanactivitygraph,letGbeasubsetofconditionalsofA,andletn∈N.Wedefinethe(G,n)-extensionofA,denotedbyE(A,G,n),astheactivitygraphinwhichtheupperboundsoftheconditionalsinGhavebeenincrementedwithn.Clearly,arelevancymappingforanactivitygraphisalsoarelevancymappingforanyextensionofthatactivitygraph.Inthegeneralcase,however,theunfoldingofsuchanextensiondoesnotneedtobewell-defined,aswealreadyhaveshownintheprevioussection.Next,wedefinewhatweexactlymeanwitha“cyclicstructure”inanactivitygraph.

Definition6(Cyclicstructure)LetAbeanactivitygraphandletA󰀂=(N󰀂,󰀁󰀂)beasubgraphofA.WecallA󰀂acyclicstructureofAiffthereexistsmorethanoneisomorphicembeddingofA󰀂intotheunfolding(V,→)ofA,i.e.,aninjectivefunctioni:N󰀂→Vsatisfying

i(v)=(v󰀂,γ󰀂)⇒v=v󰀂v󰀁v󰀂⇐⇒i(v)→i(v󰀂)

Thisdefinitioncarrieseasilyovertotaskgraphs.Notethatrepeatedpatternsinanunfoldingareduetoacycleintheactivitygraph.Thescopeofthispaperisfiniterepetitivebehaviour,whichimpliesthatthecyclesintheactivitygrapharecontrolledbyconditionals.Therefore,wetrytograsprepetitivestructuresusingsubsetsofconditionals.First,wedefinethesetofdirectsuccessorsofasubsetofinstancesN,andasubsetofthe→edgerelationthatexcludesincomingedgesofasetofnodesG:

next(N)={b|a→b∧a∈N}

→G={((v,γ),(v󰀂,γ󰀂))∈→|v󰀂∈/G}

(6)

(7)

+

bifandonlyifthereexistsapathfromatobWesaythata→Gwhichconsistsofoneormoreedgesin→G.Usingthesetwodefinitionswecandefinethenotionofrepetitivestructurewithinanunfolding.

Definition7(Repetitivestructure)LetAbeawell-definedac-tivitygraphwithafiniteunfolding(V,→)andletGbeasubsetofcondi-tionalsofA.TherepetitivestructureinducedbyAandGisinductivelydefinedasfollows:

(i)Base:R0={(n0,γ0)}andB0={(v,γ)|(n0,γ0)→+(v,γ)}.G(ii)Induction:Ri=next(Bi−1)\\Bi−1andBi={b|a→+b∧a∈Ri}.GArepetitivestructureconsistsofonlyafinitenumberofnon-emptysetssinceweassumedthattheunfoldingisfinite,andwehaveproventhatitisacyclic.AlsonotethatRionlycontainsinstancesofcondition-alsinGfori>0,andalledgesleadingoutsideBileadtoRi+1.Figure7givesagraphicalrepresentationofarepetitivestructurewhereallsetsRiandRjaredisjoint.

VR1B1R2RkFigure7:Arepetitivestructure.

∗astheIfallinstancesinRiarepairwiseparallel,thenwedefineγi

unionofallnodevaluationsinRiprojectedtothedomainofthecondi-tionals(thesetC)oftheactivitygraphasfollows(itiswell-definedbyLemma5oftheappendix):

󰀂

γ(v)if∃v󰀂(v󰀂,γ)∈Ri∧γ(v)=↑∧v∈C∗

γi(v)=

↑otherwise

Next,wedefinethesituationinwhichweareabletorecognizecyclic

structuresfromtherepetitivestructure.Theideaisthatwestatecondi-tionsontherepetitivestructureofasetconditionalGsuchthatcertain

setsRi∪Biidentifycyclicstructuresoftheactivitygraph.Asare-sult,wecancopy-pastethesesetstoincreasetheupperboundsoftheconditionalsinGtoextendtheactivitygraph.

Definition8(Extendability)LetGbeasubsetofconditionalsofanactivitygraphAandletR={R1,...,Rk}and{B1,...,Bk}betheassociatedrepetitivestructure.WecallGextendable,if

thesetRisapartitioningofthesetofallinstancesofconditionals

∗isdefined:seetheproofofinG,suchthat|Ri|=|G|(hence,γi

thelemmabelow),

if(v,γ)→(v󰀂,γ󰀂)and(v󰀂,γ󰀂)∈Bi,then(v,γ)∈Bi∪Ri,theoutgoingedgesofRieitherarealltrueedgesorallfalseedges,and

ifRiexitswithtrueedgesandRi+1exitswithfalseedges,then:

󰀃∗󰀁∗c∈G⇒γi+1(c)=γi(c)+1

∧󰀃∗󰀁∗∗(c)≥ub(c)∧γ∗(c)≥ub(c))c∈/G⇒γi(c)=γi+1(c)∨(γii+1WecallthesetRi∪Biarepetitiveset.

Theugly-lookingformulainthefourthitemofthedefinitioninfor-mallymeansthat(i)conditionalsinGhavetakentheirtrue-edgesonce

inBi,and(ii)thestatusofconditionalsnotinGhasnotchanged:if

∗,thenthetrue-edgethetrue-edge(false-edge)isenabledaccordingtoγi

∗.(false-edge)isenabledaccordingtoγi+1

Lemma9IfanactivitygraphAiswell-definedandextendableforG,

thenE(A,G,n)iswell-definedforanyn∈N.Moreover,thesubgraphsofAassociatedwiththerepetitivesetsarecyclicstructuresoftheextension.Proof(sketch).LetR={R1,...,Rk}andB={B1,...,Bk}betherepetitivestructureofGforanactivitygraphA.Let{i1,...,im}bethesetofindicesoftherepetitivesets.Weassumethattheindicesarestrictlyincreasing,thatisjFirstweprovethattheinstancesinRiarepairwiseparallel.FromDefinition7followsthat(i)everyelementofRiisaninstanceofaconditionalinG,(ii)everyelementofRihasapredecessorinBi−1,and(iii)Bi−1∩Ri=∅.Nowassumethatv󰀘v󰀂andv,v󰀂∈Ri.Thenthereexistsapathfromvtov󰀂.Sincetheunfoldingisacyclic,andconditionalinstanceshave1predecessor,thispathmustpassthroughBi.Sincethe

B-setsdonotcontaininstancesofconditionalsinGv󰀂mustbeinthesetRjsuchthati=j.Thus,Risnotapartitioning,whichweassumed.Therefore,v󰀘v󰀂.

Nowconsiderthe(G,n)-extensionofA,denotedbyA󰀂.Therele-vancymappingforAalsoisarelevancymappingforA󰀂andweusethatrelevancymappingtoconstructtheunfoldingofA󰀂.

SinceonlytheupperboundsoftheconditionalsinGareincreased,wecanuseexactlythesameinductiveclausesfromDefinition3toconstructtheunfoldinguptotheconditionalsinthesetRi1+1.Nowinsteadoftakingthefalseedgesoftheconditionals,thetrueedgesmustbetaken,sincetheupperboundsofallcountersinGhavebeenincreasedwithn.BythefourthiteminDefinition8weknowthatinthissituationexactlythesameconditionaledgesareenabledasfromtheconditionalsinRi1.Moreover,theseconditemofDefinition8tellsusthatthestructureRi1∪Bi1isindependentfromtherestoftheunfolding(inparticularitcontainsnojoininstancesthathaveapredecessorthatisnotinRi1∪Bi1).Finally,thethirditemtellsusthateveryinstanceofaconditionalinGtakesitstrueedgefromRi1anditsfalseedgefromRi1+1.Therefore,wecansaythatthesubgraphRi1∪Bi1exactlydefinesthelastexecutionofthecyclethatiscontrolledbythesetofconditionalsG.Inotherwords,wecanapplythesameinductiveclausesthatweusedtoshowthatRi1∪Bi1ispartoftheunfoldingtoshowthata“copy”ofthissetsalsoispartoftheunfolding.Thus,wecancopyRi1∪Bi1ntimesbeforeweproceedwiththesetRi1+1.

Ifwedothiscopy-pastingforalltheindices{i1,...,im},thenwehaveextendedallconditionalinstances,sincebythefirstitemofDefinition8weknowthattherearenoconditionalsinGthatarenotinsomeR-set.Theresultingunfoldingistheunfoldingofthe(G,n)-extensionofA.Moreover,itiswell-definedsinceAiswell-definedandtheseconditemofthedefinitionensuresthatcopy-pastingintroducesnolooseends.Finally,itisclearthatthesubgraphsofAassociatedwiththesetsRij∪Bijarecyclicstructures,sincewehaveshownthatthesesubgraphsreappearinthe(G,n)-extensionofAduetothecopy-pastingsketchedabove.󰀂Thepreviouslemmaonlycoverstheextensionofasinglesetofcon-ditionals,whereasingeneralweneedtheextensionofseveralsetsofconditionals.Thenextdefinitioncovershierarchy(ornesting)betweencyclicstructuresofdifferentsetsofconditionals,whichisneededforsuchaparallelextension.

Definition10(Hierarchy)LetAbeanactivitygraphandletGandG󰀂beadisjointsetsofconditionalsofA,whichbothareextendablefor

A.WesaythatG≺G󰀂ifandonlyifforallrepetitivesetsRi∪BiofG

󰀂intheB-setofG󰀂suchthatR∪B⊂B󰀂.wecanfindaBjiijThenextlemmastatesthatwecanextendanactivitygraphfortwo

setsofconditionals,iftheyarehierarchical.Notethatwecaneasilygeneralizethislemmatoanarbitrarynumberofhierarchicalsetsofconditionals.

Lemma11IfanactivitygraphAiswell-definedandextendableforGandforG󰀂andG≺G󰀂,thenE(E(A,G,n),G󰀂,n󰀂)iswell-definedforanyn,n󰀂∈N.Moreover,thesubgraphsofAassociatedwiththerepetitivesetsofGandG󰀂arecyclicstructuresoftheextension.

Proof(sketch).TheideaistoconstructtheextensionofAinsideout.ThismeansthatwefirstapplythemethodsketchedintheconstructiveproofofLemma9toG,andthentoG󰀂.AssumethattherepetitivestructureofGisgivenbyR={R1,...,Rm}andB={B1,...,Bm},

󰀂,...,R󰀂}andthattherepetitivestructureofG󰀂isgivenbyR󰀂={R1n

󰀂󰀂󰀂andB={B1,...,Bn}.

ByDefinition10wecanfindforeveryrepetitivesetRi∪BiofG󰀂suchthatR∪B∈B󰀂.Thus,wecopy-pastethesetR∪BnaBjiiiij

󰀂timesandalsoaddthenewinstancestothesetBj.Lemma9then

saysthatthiscreatestheextensionE(A,G,n).Next,wemustprovethatG󰀂stillisextendableforthisextension.Therefore,weobservethatthecopy-pastingdoesnotchangethestatusofconditionalsnotinG,

󰀂thatduetothefourthitemofDefinition8.Thus,the“new”setRj

󰀂isstillequivalenttotheoldonew.r.t.thefollowstheenlargedsetBj

statusoftheconditionals.Therefore,E(A,G,n)isstillextendablefor

󰀂∪B󰀂arecyclicstructuresG󰀂,andthepossiblyenlargedrepetitivesetsRjj

󰀂󰀂ofE(E(A,G,n),G,n).󰀂Thisconcludesthefirststepofourapproach.Wenowcanlowerthe

upperboundsofasetofconditionalsinanactivitygraphAsuchthattheseconditionalsarejustextendable(Definition8).Lemma9provesthatthesubgraphsofAassociatedwiththerepetitivesetsindeedarecyclicstructuresoftheextensionofA.Definition10andLemma11generalizethistomultiple,hierarchicalsetsofconditionals.

Thesecondstepofourapproachconsistsofusingregularschedulingtoolstofinda(optimal)solutionforthecondensedactivitygraphthatwehavefoundinstepone.Weassumethatwecanobtainsuchasolu-tion,sincetheactualschedulingfallsoutsidethescopeofthispaper.Itisnoteworthy,however,thatschedulingataskgraphconsistsofintro-ducingextraprecedenceedgesbetweentasksthatareparallelandshareresourcestoensuremutualexclusionofsuchtasks.

Thethirdstepconsistsofusingtherepetitivesetsofthecondensedactivitygraphofsteponeandthescheduleofsteptwotoconstructaschedulefortheoriginalactivitygraph.Therearemanydifferentstrategiestodothis.Forexample,onecouldonlyconsiderthescheduleoftherepetitivesets.Thealreadypartiallyscheduledunfolding(andtaskgraph)oftheoriginalactivitygraphcanthenbeobtainedusingthemethodsketchedintheproofofLemma9.Atthismomentwearehappywithsucha(hopefully!)goodandnon-trivialstartingpointfortheschedulingactivity.Ofcourse,mattersofoptimalityareimportantinthisstepandweregarditasanimportantsubjectoffuturework.

3.2ExampleApplicationoftheApproach

Inthissubsectionweapplyourapproachtopartofaschedulingprob-lemfromawaferscanner.ItsactivitygraphisdepictedinFigure8.Inordertoachievemaximalutilization,awaferscannerhasaworkqueueofrecipestodo.Thisqueueisextendedwithextrarecipeseveryonceinawhile.Onsuchoccasionthescheduleisextended,whichimpliesaschedulingactionofa(static)activitygraph.Theconditionalupperboundsofthegraphareinstantiatedinaccordancewiththenumberofentitiesoftherecipesinthequeue.Thisexamplecoversthreeoutoffivemanufacturingentitiesthatwerediscussedintheintroduction:reticles,masks,andICs.

Thenumberofreticlesinvolvedis15inthiscase.TheconditionalsetthatcanbeassociatedwiththisGC={c0,c1}.Obviously,theupperboundsoftheseconditionalsequal15.

Thenumberofmasksinvolvedis8.TheconditionalsetthatcanbeassociatedwiththisGD={c2,c3}.Forthefirstmaskofeveryreticle,someadditionalactivitiesmustbeexecuted,whichiscontrolledbyconditionalsc4,c5,c6,andc8.

ThenumberofICsinvolvedis43,whichiscontrolledbyconditionalsetGE={c7}.Therefore,thetotalamountofICsinthespecifiedschedulewillbe15×8×43=5160.

Itisclearthatthetaskgraphassociatedwiththisactivitygraphisquitelargeandnoteasilyschedulable.WehaveimplementedthetheoryinthispaperinJava,andwecanshowinafewminutesthatthetaskgraphconsistsof11655tasks(constructionoftherelevancymappingtakesvirtuallynotime).

Wetrytoapplythetechniqueexplainedintheprevioussection.Thefirststepconsistsoffindingsmallestupperboundsoftheconditionals

[c0>=15]c2:=0c4:=0c5:=0c8:=0c0:=0[c0<15][c1>=15]c1:=0[c1<15][c7>=43]c7:=0[c7<43]E21E39[c2>=8][c3>=8][c2<8][c3<8]c3:=0c6:=0E40[c6<1][c4>=1][c8<1][c4<1]E29E30E31E32E33E23E20E25[c8>=1][c6>=1]E22E26E24E36E34E35[c5<1]E27[c5>=1]E37E28E38Figure8:Anactivitygraphwhichspecifiespartofareal-lifeschedulingproblemforawaferscanner.

thatspecifytherepetitionsforthereticles,masksandICs.WestartbysettingtheupperboundsofGCandGEto1,sinceeveryrepetitionisequal.However,wesettheupperboundsofGDto2,sincethefirstimageofeveryreticlediffersfromtherest.Next,wechecktheextendabilityofGC,GDandGEforthiscondensedgraphwhichwecallA0:theyareallextendable.Moreover,GE≺GD≺GCasexpected,whichenablesthe“parallel”extensionoftheconditionalsets(seeLemma11).Com-

putationofthecyclicstructuresandcheckingtheextendabilitytakes–forthisparticularexample–fractionsofasecondusingourtool.

Forthesecondstepweusearegularschedulingtooltofindanoptimalscheduleforthecondensedactivitygraph.OnesuchanoptimalscheduleisshowninFigure9asaGanttchart.

R1R2R3R4R5R6R7R8R9R10a b c dFigure9:Anoptimalscheduleforthecondensedactivitygraph.

InthethirdstepweusetherepetitivestructuresofGC,GDandGEtoconstructaschedulefortheoriginalactivitygraph.Theserepetitivestructuresaregivenduringcomputationoftheextendabilityofthesetsofconditionals(seeDefinition8andLemma9).Furthermore,duringtheschedulingoftheactivitygraphinstep2,tasksthatshareresourcesareputinacertainordertosatisfythemutualexclusionpropertyofresourcesthatplaysaroleinthiskindofschedulingproblems.Thiscorrespondstoaddingadditionalprecedencestotheactivitygraph,suchthatthetaskorderisforcedtobethesameasintheschedule.

Forourexample,step3ofourapproachcanbedescribedusingFigure9asfollows.TherepetitivestructurethatcanbeassociatedwithGCistheentireGanttchart.Thetasksinthetimeinterval[b,d]areassociatedwithGD.Finallythetasksintheintervals[a,b]and[c,d]areassociatedwithGE.AccordingtoLemma11weneedtoconstructtheschedulefortheoriginalproblemfromtheinsideoutwards.First,weincreasetheupperboundoftheconditionalinGE.Therefore,wecopy-

pastetheinterval[a,b]42times,andthenwecopy-pastetheinterval[c,d]42times.Next,weproceedwithcopy-pastingtheintervalthatcanbeassociatedwithGD6timestoincreasetheupperboundsofconditionalsinGDtotheiroriginalvalues.Finally,wecopy-pastalltasksintheupdatedGanttchart14timestoincreasetheupperboundoftheconditionalsinGC.Notethatthiscopy-pastingdoesnotconcernatimeinterval,butasubgraphofthetaskgraph.Thetasksonresource7and9thatareshownattheleftofFigure9willsucceedthetaskthatendsatd,andtheprecedencesadmitthatitisexecutedinparallelwiththetaskstartingatdontheresources3and5.Webelievethatthescheduleisstilloptimalafterextensioninthiscase.

Itisclearthatourmethodonlyinvolvestheschedulingoftherela-tivelysmalltaskgraphofthecondensedproblem.Thisrendersitinmanycasesmuchmoresuitablethanthestraightforwardapproachofschedulingtheoriginal,verylarge,taskgraph.Itisnecessarytoquan-tifythe(sub)optimalityofthegeneratedschedule,andweregardthisasanimportantsubjectforfuturework.

4.Conclusions

Theideaofthisworkistoreducethecomplexityofschedulingprob-lemsbeingfacedinmanymanufacturingsystemsbyexploitationoftherepetitivepatternsthatcanberecognizedinthem.Thetaskgraphthatusuallyformsabasisfordescriptionofaschedulingproblemisextendedwithadditionalmodelingfeaturestodescribethisfiniterepet-itivebehaviour.ThisextendedmodelfollowstheUMLactivitydiagramstandard,andiscalledanactivitygraph.Infact,anactivitygraphisafolded-inequivalentofataskgraphwithrepetitivepatterns,whichisgenericforthenumberofpatternrepetitions.Theactivitygraphisfor-mallydefined,andsoisitsequivalencewithataskgraph.Animportantissueistheabsenceofraceconditionsoftheactivitygraph,whichcanbeprovenstaticallybyconstructionofarelevancymapping.

Theexpressivityoftheactivitygraphsissufficientforasubsetofprac-ticalcasesfromindustry.Itispossibletomodelparallelismofdifferentinstancesofonemanufacturingentitybyintroductionofmultiplecon-ditionalscontrollingexecutionofactivitiesthatcanruninparallelforthesedifferentinstancesinthesystem.Asaconsequenceofthefactthatconditionalsarenothierarchical,i.e.,aconditionalthatcanbeassoci-atedwithalowerlevelisnotachildofaconditionalofahigherlevel,itisnotpossibletodescribeasysteminwhichmanufacturingentitiescan“overtake”eachother.Thismeansthatprocessingordermustbefirstin,firstout,whichisfineformostpracticalcases.Extensionofactivity

graphsforhierarchicalconditionalscouldbeconsideredforfuturework.Thesamegoesforthead-hocalgorithmtodeterminearelevancymap-ping,whichseemstobeacceptableforpracticalcases,butapolynomialonewouldbepreferable.

Theapproachforreductionofthecomplexityoftheschedulingprob-lemsexploitsthehierarchicalmanufacturingentitystructurethatre-sultsinnestedpatternsintheschedule.First,theschedulingproblemisreducedwithrespecttothenumberofrepetitions.Subsequently,thereducedproblemintheformofanactivitygraphisconvertedtotheusualformbasedonataskgraphandcanbescheduledusingappropri-atetooling.Finally,thescheduleofthereducedproblemisextendeduptothesizeoftheoriginalproblemusingrepetitivestructures.Thisextensionalgorithmisingeneralmuchmoreefficientthanschedulingtheoriginaltaskgraph.Webelievethatpreservationof(makespan)optimalityisensuredforasubsetofproblemsthatcanbedescribed.Thismeansthatforcasesinwhichinstancesofmanufacturingentitiesareprocessedsequentially,recurrentTSP-alikeproblemsarerecognizedandthereforearetobescheduledonlyoncewhilepreservingoptimality.Findingthissubsetisanimportantsubjectforfutureresearch.

References

[1]AvailablethroughURLhttp://www.asml.com/.

[2]B.BoigelotandP.Wolper.Symbolicverificationwithperiodicsets.In6th

InternationalConferenceonComputerAidedVerification,number808inLNCS,pages55–67.Springer–Verlag,1994.

[3]P.CousotandR.Cousot.Abstractinterpretationandapplicationtologic

programs.JournalofLogicProgramming,13(2–3):103–179,1992.(Theeditorof

JournalofLogicProgramminghasmistakenlypublishedtheunreadablegalleyproof.Foracorrectversionofthispaper,seehttp://www.di.ens.fr/~cousot.).

[4]R.EshuisandR.Wieringa.VerificationsupportforworkflowdesignwithUML

activitygraphs.InProceedingsofInternationalConferenceonSoftwareEngi-neering,2002.

[5]M.R.GareyandD.S.Johnson.ComputersandIntractability.Aguidetothe

TheoryofNP-Completeness.W.H.FreemanandCompany,1979.

[6]T.Gehrke,U.Goltz,andH.Wehrheim.ThedynamicmodelsofUML:Towards

asemanticsanditsapplicationinthedevelopmentprocess.InHildesheimerInformatik-Bericht11/98.Institutf¨urInformatik,Universit¨atHildesheim,1998.[7]M.HendriksandK.G.Larsen.Exactaccelerationofreal-timemodelchecking.

InE.Asarin,O.Maler,andS.Yovine,editors,ElectronicNotesinTheoreticalComputerScience,volume65.ElsevierSciencePublishers,April2002.

[8]C.M.H.Kuijpers,C.A.J.Hurkens,andJ.B.M.Melissen.Fastmovementstrate-giesforastep-and-scanwaferstepper.StatisticaNeerlandica,51(1):55–71,1997.[9]K.G.Larsen,P.Pettersson,andW.Yi.Uppaalinanutshell.International

JournalonSoftwareToolsforTechnologyTransfer,pages134–152,1998.

[10]E.L.Lawler,J.K.Lenstra,A.H.G.RinnooyKan,andD.B.(eds.)Shmoys.The

TravelingSalesmanProblem:AGuidedTourofCombinatorialOptimization.Wiley,NewYork,1985.[11]K.MiyashitaandK.Sycara.CABINS:Aframeworkofknowledgeacquisition

anditerativerevisionforscheduleimprovementandreactiverepair.ArtificialIntelligenceJournal,76(1-2):377–426,1995.[12]N.J.M.vandenNieuwelaar,J.M.vandeMortel-Fronczak,andJ.E.Rooda.De-signofsupervisorymachinecontrol.AcceptedbyEuropeanControlConference2003.[13]M.Pinedo.Scheduling:Theory,Algorithms,andSystems.PrenticeHall,1995.[14]X.Puquan,L.Changyou,andX.Xinhe.Onsequencingproblemsofrepetitive

productionsystems.IEEETransactionsonAutomaticControl,38(7),1993.[15]S.Roels.Applicabilityofmodel-checkingmethodstoschedulinginmachines.

Master’sthesis,NijmeegsInstituutvoorInformaticaenInformatiekunde,Uni-versityofNijmegen,TheNetherlands,October2002.Confidential.[16]J.Rumbaugh,I.Jacobson,andG.Booch.TheUnifiedModelingLanguage

ReferenceManuals.Addison-Wesley,1999.[17]OMGUnifiedModelingLanguageSpecification–version1.4,September2001.

AvailablethroughURLhttp://www.omg.org/uml/.[18]W.F.J.Verhaegh.MultidimensionalPeriodicScheduling.PhDthesis,Eindhoven

UniversityofTechnology,theNetherlands,1995.[19]M.Wennink.AlgorithmicSupportforAutomatedPlanningBoards.PhDthesis,

EindhovenUniversityofTechnology,theNetherlands,1995.[20]J.I.vanZante-deFokkertandT.G.deKok.Thesimultaneousdeterminationof

theassignmentofitemstoresources,thecycletimes,andthereorderintervalsinrepetitivepcbassembly.AnnalsofOperationsResearch,92:381–401,1999.

Appendix:Proofs

instancesWsuchthateither

Definition1(Witness)Awitnessforaninstance(v,γ)isafinitesetof

W=∅and(v,γ)=(n0,γ0),or

H

thereexistsan(instanceofan)inductiveclauseH󰀁inDefinition3(ii)such

󰀂

that“(v,γ)∈V”occursinH,andthesetofinstancesappearinginHequalsW.

Definition2(Proof)Aproofofaninstance(v,γ)isafinitelabeledtreesuch

thattherootislabeledwith(v,γ),andifanodeislabeledwith(v󰀂,γ󰀂),thenthelabelsofitschildrentogetherareawitnessfor(v󰀂,γ󰀂).ThesizeofaproofPisthenumberofnodesinthetree,denotedby|P|.

Notethateveryinstanceofanunfoldinghasaproof.

Lemma3IfXisarelevancymappingand(v,γ)isaninstanceoftheunfolding

thathasbeencreatedusingX,thenthedomainofγequalsX(v).

Proof.ThelemmacanbeprovenbyinductiononthenumberofapplicationsoftheclausesofDefinition3thatareneededtoshowthat(v,γ)ispartoftheunfolding.

Base:1application.Then(v,γ)istheinitialinstance,andclearlyitholdsthatthedomainofγ0equalsX(n0).

Induction:assumethatitholdsforaninstancewhoseexistencecanbe“proven”withnapplications.Wecaneasilyshow,usingtheextremalclausesofDefini-tion3,thatthepropositionmustalsoholdforinstanceswhoseexistencecanbeprovenwithn+1applications.

󰀂

Lemma4Let(v,γ)beaninstanceinanunfolding(V,→)suchthatq∈X(v).

Thenareturnpath(n0,γ0)→∗(v,γ)existsofwhichallnodesarelabeledwithqbyX.

Proof.WeprovethelemmabyinductiononthenumberofapplicationsofthebaseandinductiveclausesofDefinition3thatisneededtoshowthat(v,γ)∈V.Thebaseoftheinductionisformedbyoneapplicationofaclause.Sincethefirstapplicationmustbethebaseclause,wecanonlyshowthat(n0,γ0)∈V.Therefore,(v,γ)=(n0,γ0),whichclearlyprovesthatthepathexists.

NowletusassumethatthedesiredpathexistsforallinstancesforwhichwecanshowthattheybelongtoVwithnapplicationsofthebaseandinductiveclauses.Letusconsideraninstance(v󰀂,γ󰀂)forwhichwecanshowinn+1applicationsofthebaseandinductiveclausesthatitbelongstoV.Thenobviously(v,γ)→(v󰀂,γ󰀂),andwedistinguishtwocases:

Theedge(v,γ)→(v󰀂,γ󰀂)isaddedbyinductiveclause1,2,4,or5.Therefore,v󰀂isnotajoin,andwecanconcludebyDefinition2thatq∈X(v󰀂)impliesthatq∈X(v).Byapplyingtheinductionhypothesiswecanconcludethatthedesiredpathexists.

Theedgeisaddedbyinductiveclause3.Thenweknowthat(v1,γ1)→(v󰀂,γ󰀂),...,(vm,γm)→(v󰀂,γ󰀂)suchthat(v,γ)=(vi,γi)forsome1≤i≤m.Moreover,wecanshowwithnapplicationsofthebaseandinductiveclausesthat(vi,γi)belongstoVforall1≤i≤m.ByDefinition2weknowthatq∈X(v󰀂)impliesthatq∈X(vi)forsomei.Thus,byapplyingtheinductionhypothesiswecanconcludethatthedesiredpathexists.

󰀂

Thenextlemmaistheykeylemmathatensuresthatraceconditionsdonotappearinactivitygraphswhichhavearelevancymapping.

Lemma5If(v,γ)and(v󰀂,γ󰀂)aretwodifferentinstancessuchthatq∈X(v)∩

X(v󰀂),thenapathfrom(v,γ)to(v󰀂,γ󰀂)(orthereversepath)existsofwhichallnodesarelabeledwithqbyX.

Proof.Considertwoinstances(v,γ)and(v󰀂,γ󰀂)suchthatq∈X(v)∩X(v󰀂).LetPbetheproofof(v,γ)andletP󰀂betheproofof(v󰀂,γ󰀂).Weprovethelemmabyinductionon|P|+|P󰀂|.Thebasecaseitthat|P|+|P󰀂|=2,inwhichcase(v,γ)=(v󰀂,γ󰀂)=(n0,γ0).Weassumed,however,thattheinstancesaredifferent.

Fromthiscontradictionweconcludethatthepropositionholdsforthebasecase.Nowconsiderthecasewhere|P|+|P󰀂|=n.Theinductionhypothesisthensays:

If(v,γ)and(v󰀂,γ󰀂)aretwodifferentinstanceswithproofsPandP󰀂respectively,andq∈X(v)∩X(v󰀂),and|P|+|P󰀂|UsingLemma4wecansaythattwopathsthatarecompletelylabeledwithqexist:

(u0,γ0)→(u1,γ1)→(u2,γ2)→...→(um,γm)

󰀂󰀂󰀂󰀂󰀂󰀂󰀂

(u󰀂0,γ0)→(u1,γ1)→(u2,γ2)→...→(un,γn)

󰀂00󰀂󰀂󰀂󰀂

where(u0,γ0)=(u󰀂0,γ0)=(n,γ),(um,γm)=(v,γ),and(un,γn)=(v,γ).Con-siderthelongestcommonprefixofthesepaths;assumethatthepathsareequaluptoindexi.Clearly,ifi=mori=n,thenthepropositionholds.Theothercaseis

󰀂󰀂󰀂

thatiuiisafork.Thenui+1andu󰀂i+1arenotjoinnodesbyassumption(just

󰀂

aboveDefinition3).Ifui+1=ui+1,thenwecanconcludebyDefinition3that

󰀂

γi+1=γi+1,whichcontradictstheassumptionthatthei+1-thinstancesaredifferent.Hence,ui+1=u󰀂i+1.However,botharelabeledbytherelevancymappingwithq.Thisviolatesthedisjunctionrequirementonforksoftherelevancymapping.Thiscontradictionshowsthatuicannotbeafork.uiisnotafork.Therefore,weknowthatui+1=u󰀂i+1.Theonlywayto

󰀂󰀂

achievethat(ui+1,γi+1)=(ui+1,γi+1)isthatui+1=u󰀂i+1isajoinnode,andthatthereexistsapredecessorof(ui+1,γi+1),say(w,γ∗),andapredecessor

󰀂󰀂󰀂󰀂󰀂

of(u󰀂i+1,γi+1),say(w,γ∗),suchthatw=wandγ∗=γ∗.Notethatby

󰀂

Definition3weknowthatγ∗(w=w󰀂)=γi(ui)=γ∗(w=w󰀂).Sincew=w󰀂,weknowthatw=w󰀂∈X(w)∩X(w󰀂).Moreover,Pclearlycontainsaproof

󰀂

for(w,γ∗)thatissmallerthanP,andP󰀂clearlycontainsaprooffor(w󰀂,γ∗)

󰀂

thatissmallerthanP.Therefore,wecanapplytheinductionhypothesis.

󰀂󰀂

Thusapath(w,γ∗)→+(w󰀂,γ∗)orapath(w󰀂,γ∗)→+(w,γ∗)existsthatis

󰀂

completelylabeledwithw=w󰀂.Inthefirstcase,γ∗(w=w󰀂)>γ∗(w=w󰀂),sincethevalueofwisincrementedonexitof(w,γ∗)andneverreset,becauseweassumedthatitcannotbeaconditionalnode(justaboveDefinition3).Thiscontradictstheinformationderivedabove.Thesecondcaseissimilar.

WecanconcludefromthesecontradictionsthatthecasethatiLemma6Instancesofanunfoldingeitherhavethesamenumberofsuccessors(or

1successorincaseofconditionalinstances)astheircounterpartsintheactivitygraph,ortheyhavezerosuccessors.

Proof.Supposethatwehaveaninstance(v,γ)whichhasmorethanitsallowednumberofsuccessors.Inotherwords,wecanfindtwosuccessors(v󰀂,γ󰀂)and(v󰀂󰀂,γ󰀂󰀂)suchthatv󰀂=v󰀂󰀂(byDefinitions1and3).ByLemma3weknowthatthedomainofγ󰀂equalsthedomainofγ󰀂󰀂.Nowwedistinguishtwocases:

v󰀂=v󰀂󰀂isnotajoinnode.Bydefinition,γundergoesthesametransformation,sincebothedgesmustbeaddedbythesameinductiveclause.Thereforewecanconcludethatγ󰀂=γ󰀂󰀂,whichcontradictsourassumptions.

v󰀂=v󰀂󰀂isajoinnode.Then,ofcourse,(v󰀂,γ󰀂)and(v󰀂󰀂,γ󰀂󰀂)havetheir

󰀂󰀂󰀂󰀂

othernecessarypredecessors(seeDefinition3),say(v1,γ1),...,(vn−1,γn−1)

󰀂󰀂󰀂󰀂󰀂󰀂󰀂󰀂

and(v1,γ1),...,(vn−1,γn−1)respectively.Withoutlossofgeneralitywemay

󰀂󰀂󰀂󰀂󰀂󰀂

assumethatvi=vi.Itisclearthatγi=γiforatleastone1≤i󰀂󰀂󰀂

otherwiseγ=γ,whichisacontradictionofourinitialassumption.More-󰀂󰀂󰀂󰀂󰀂󰀂

over,weknowthatγi(vi)=γi(vi)bythecombinationofinductiveclause(3)

󰀂󰀂󰀂󰀂󰀂󰀂

andthefactthatγ(v)=γi(vi)andγ(v)=γi(vi).NowweapplyLemma

󰀂󰀂󰀂󰀂󰀂󰀂

5tothedifferent(asarguedabove)instances(vi,γi)and(vi,γi)(remember

󰀂󰀂󰀂󰀂󰀂󰀂󰀂󰀂󰀂

thatvi=vi).Thus,weseethatapathfrom(vi,γi)to(vi,γi)existsthatis

󰀂

completelylabeledwithvi(ortheotherwayaround,butthatcaseissimilar).

󰀂󰀂󰀂

Moreover,vi=viisnotaconditionalnode(sinceweassumedjustaboveDefinition3thatconditionalscannotdirectlyleadtoajoininactivitygraphs)

󰀂󰀂󰀂󰀂󰀂󰀂

anditsvalueisthereforeneverreset.Inotherwords,γi(vi)>γi(vi)whichisincontradictionwithknowledgederivedabove.

Ofcourse,duetofailedsynchronizationsinjoinnodes,predecessorsofjoinnodesmayhavezerosuccessors.Theresultingunfoldingisnotwell-defined.󰀂ThenextlemmaisusedintheproofofLemma8.

Lemma7ConsideranactivitygraphAwithaconditionalnodevandrelevancy

mappingX.Ifvisreachablefromtheinitialnode,thenthereexistsanon-conditionalnodev󰀂suchthatv󰀂∈X(v).

Proof.ConsidertheactivitygraphAwithaconditionalnodevandrelevancymappingX,andassumethatvisreachablefromtheinitialnodeofA.LetusassumethatX(v)doesnotcontainanon-conditionalnode,andconsiderthepathinAfromtheinitialnodetov,sayv0,v1,...,vn,wherev0istheinitialnodeandvnisv,andsuchthatvi=vjforall0≤i=j≤n.Definition2tellsusthatvn−1mustbeaforknodeoraconditionalnode.Ifitisaconditionalnode,thenwecanrepeatthisargumentation.Sincetheinitialnodecannotbeaconditionalnode,aforknodevionthepathexistssuchthatvjisaconditionalnodeforalliNowconsiderthetwosuccessorsofv,sayv󰀂andv󰀂󰀂.Clearly,v󰀂=vjandv󰀂󰀂=vjforalliWecanrepeattheargumentationaboveandconcludethatAmustcontainin-finitelymanyconditionalnodes,whichisacontradictionbyDefinition1.HenceweconcludethatX(v)doescontainanon-conditionalnode.󰀂

Lemma8Everyinstancehasauniquewitness.

Proof.Letusconsideraninstance(v,γ)intheunfolding.First,observethat(v,γ)hasatleastonewitness,becauseitisintheunfolding.Weprovethatthiswitnessis

uniquebycontradiction.Thus,weassumethatWandW󰀂aredistinctwitnessesof(v,γ),anddistinguishthreecases:

visamerge,activity,forkorexit.ThenweknowbytheinductiveclausesthatwecanwriteW={(v󰀂,γ󰀂)}andW󰀂={(v󰀂󰀂,γ󰀂󰀂)}.Thus,(v󰀂,γ󰀂)→(v,γ),and(v󰀂󰀂,γ󰀂󰀂)→(v,γ).BydefinitionoftherelevancymappingX,weknowthatv∈X(v󰀂)andv∈X(v󰀂󰀂).Lemma5saysthatapath(v󰀂,γ󰀂)→(v1,γ1)→∗(v󰀂󰀂,γ󰀂󰀂)(ortheotherwayaround,butthatcaseisidentical)existssuchthatv∈X(vi)forallinstances(vi,γi)onthatpath.Wedistinguishtwocases:–(v1,γ1)=(v,γ).ByLemma6wecansaythatv󰀂isaforknodeandthatv1=v.Byconstructionofthepathweknowthatv∈X(v1).Thus,therelevancymappingforthesuccessorsoftheforknodev󰀂doesnotsatisfythedisjunctionrestriction,whichisacontradiction.–(v1,γ1)=(v,γ).Accordingtotheinductiveclauseswecanderivethatγ󰀂󰀂(v)>γ(v),sincethevalueofvisincreasedonexitof(v,γ)andneverresetbecausevisnotaconditionalnode.Moreover,since(v󰀂󰀂,γ󰀂󰀂)→(v,γ)andvisneverresetweknowthatγ(v)≥γ󰀂󰀂(v).Combinationofthesetwoequationsgivesusthatγ(v)>γ(v),whichclearlyisacontradiction.visajoin.ThenwecanwriteW={(vi,γi)|1≤i≤n}andW󰀂=󰀂󰀂󰀂󰀂{(vi,γi)|1≤i≤n},wherevi=viforsomen.Nowassumethatγi=γi

󰀂󰀂

forsomei(otherwise,W=W󰀂).Then(vi,γi)→(v,γ)and(vi,γi)→(v,γ).Notethatweassumed(seethetextjustaboveDefinition3)thataconditional

󰀂

oraforkcannotbefollowedbyajoinnode.Therefore,vi=viisnotacondi-󰀂󰀂tionalorfork.ByLemma5wethusknowthatapathfrom(vi,γi)to(vi,γi)exists(ortheotherwayaround,butthatissimilar)thatiscompletelylabeled

󰀂

withvi=vibytherelevancymapping.Moreover,byLemma6wecancon-󰀂cludethatthepathpassesthrough(v,γ)(sincevi=viisnotafork).Since

󰀂

vi=viisnotaconditional,itsvalueisneverrest.Thus,wecanderivethat󰀂󰀂󰀂󰀂󰀂󰀂󰀂γi(vi=vi)≥γ(vi=vi)andγ(vi=vi)>γi(vi=vi),sincethevalueofvi=vi

󰀂󰀂

isincrementedonexitof(vi,γi).Thisclearlyisacontradiction.visaconditional.ThenweknowbytheinductiveclausesthatwecanwriteW={(v󰀂,γ󰀂)}andW󰀂={(v󰀂󰀂,γ󰀂󰀂)}.Thus,(v󰀂,γ󰀂)→(v,γ),and(v󰀂󰀂,γ󰀂󰀂)→(v,γ).ByLemma7weknowthatw∈X(v)forsomenon-conditionalnodew.Bydefinitionoftherelevancymappingalsow∈X(v󰀂)andw∈X(v󰀂󰀂).Wenowcanrepeattheargumentationofthefirstitemtoshowacontradiction.

Therefore,(v,γ)hasauniquewitness.

󰀂

Thenextlemmastatesaveryusefulpropertyofourunfoldings,namelythattheyareacyclic.Thismeansthatanunfoldingdefinesapossiblyinfinitepartialordering,whichisexactlywhatweintended.

Lemma9Anunfoldingisacyclic.

Proof.First,weprovethatifthereisacycleinanunfolding,thentheinitialinstance(n0,γ0)isonthatcycle.Assumethatthereisacycle,say(v1,γ1),...,(vn,γn),(v1,γ1),suchthattheinitialinstanceisnotpartofthecycle.Inorderforthiscycletobepartoftheunfolding,atleastapathfromtheinitialinstancetothiscyclemustexist(seetheextremalclauseofDefinition3).

FromLemma8weconcludethatoneoftheinstancesinthecycle,say(vi,γi),isajoininstancethatconnectstheinitialinstancetothecycle(sinceonlyjoininstancescanhavemultiplepredecessorsandtheinitialinstanceisnotonthecycle).However,byDefinition3weknowthatγi+1(vi)=γi(vi)+1.Sincethevalueofajoinnodecannotbereset,itisimpossiblethat(vi+1,γi+1)→∗(vi,γi).Fromthiscontradictionweconcludethattheinitialinstancemustbepartofthecycle.

Next,weprovethelemmabycontradiction.Therefore,letusassumethatacycleexistsintheunfolding.Abovewehaveshownthat(n0,γ0)isonthecycle.WiththeknowledgethattheinitialinstancecannotbeaconditionalinstancebyDefinition1(anditsvaluethusisneverreset),wecanuseasimilarargumentasabovetoshowthatthecyclecannotbeacycle.Therefore,nocyclesexistinunfoldings!󰀂Thenextlemmastatesasufficientconditiononthesyntaxofactivitygraphsforfinitenessoftheirunfoldings.

Lemma10LetA=(N,n0,󰀁,c)beanactivitygraph.IfforallcyclesinA,say

v1,...,vn,suchthatn≤4·|󰀁|holdsthattheycontainaconditionalnode,sayvi,suchthat(vi,vi+1)isthetrueedgeandviisnotresetonthecycle,thentheunfoldingofAisfinite.

Proof.Weprovethelemmabycontradictionandthereforeassumethatthepremiseshold,buttheunfoldingisinfinite.Thismeansthatthereexistsaninfinitepath,andsinceanactivitygraphisfinite,atleastonenode,sayvmustappearinfinitelyofteninthispath.Thiscanonlyoccur,ifvisonacycle.Sincethiscyclesatisfiestheprecondition,thecounterofthe“exit”conditionalv󰀂ofthiscyclemustberesetinfinitelyoften(otherwisethecycleisnotinfinitelyoftenenabled).Thismeansthattheremustbeanothercycleinvolvingnodevthatresetsthecounter.Thus,connectingthesecyclesgivesusalargercyclethatcontradictsourassumptionaboutthecyclesoftheactivitygraph(namelythatthecounteroftheexitconditionalisnotreset).Thequestionnowishowlongthesetwocyclescanbe.

Wefirstconsiderthecyclewhichcontainsthetrueedgeoftheexitconditional,sayv󰀂󰀁v󰀂󰀂.Thepathfromvtov󰀂canbeboundedby|󰀁|,sinceanypathfromvtov󰀂thatislongerthan|󰀁|,caneasilybetransformedtoapathwithlengthboundedby|󰀁|.Thesameholdsforthepathfromv󰀂󰀂tov,withtheresultthatthelengthofthisfirstcyclecanbeboundedby2·|󰀁|.(Moreprecisely,ifthereisacycleintheactivitygraphinvolvingvandv󰀂󰀁v󰀂󰀂withalengthgreaterthan2·|󰀁|,thenthereexistsacyclealsoinvolvingvandv󰀂󰀁v󰀂󰀂withalengthlessorequalto2·|󰀁|.)

Wecanusethesameargumenttoshowthatthecyclefromvtotheresettingconditionalofv󰀂andbackalsocanbeboundedby2·|󰀁|.Combinationgivestherequiredupperbound.󰀂

Lemma11If(v,γ)→+(v󰀂,γ󰀂)andw∈X(v)∩X(v󰀂),then(v,γ)occursonthe

returnpathof(v󰀂,γ󰀂)forw.

Proof.StraightforwardusingLemma6.

󰀂

Lemma12IfXandX󰀂arerelevancymappingsforanactivitygraph,thenthetwo

resultingunfoldingsareisomorphic.

Proof.Considerthetworesultingunfoldings(V1,→1)and(V2,→2),respectively.Inductively,weconstructamappingf:V1→V2suchthat

f(v1,γ1)=(v2,γ2)

(A.1)

f(v1,γ1)=(v2,γ2)⇒γ1andγ2agreeonintersectionofdomains(A.2)(v,γ)→1(v󰀂,γ󰀂)⇔f(v,γ)→2f(v󰀂,γ󰀂)(A.3)

⇒

v1=v2

󰀂

Supposethatfhasbeendefinedforallpredecessorsofsomenode(v󰀂,γ1)ofV1.Let

󰀂󰀂

Wbetheunique(byLemma8)witnessfor(v,γ1).Weconsiderthreecases:

󰀂󰀂

1W=∅.Then(v󰀂,γ1)istheinitialinstance,i.e.,v󰀂=n0andγ1(v)=0

0

ifv∈X(n)anditisundefinedotherwise.Wemaptheinitialinstanceof

󰀂0

(V1,→1)totheinitialinstanceof(V2,→2),i.e.,wedefinef(v󰀂,γ1)=(n0,γ2),

0󰀂0󰀂

whereγ2(v)=0ifv∈X(n)anditisundefinedotherwise.Sincebothγ1and󰀂00γ2mapasubsetofnodesto0,weseethatγ1andγ2agreeontheintersectionoftheirdomains.

2|W|=1.Inthiscase,let(v,γ1)betheuniqueelementofW.Sinceawitnessforajoinnodealwayscontainsatleasttwoelements,v󰀂isnotajoinnode.Letf(v,γ1)=(v,γ2).Thenγ1andγ2agreeontheintersectionoftheirdomains.Weconsiderthreesubcases:

󰀂

(a)v∈J∪M∪A.Thenγ1=γ1[v:=v+1].ByDefinition3,(v,γ2)→2

󰀂󰀂󰀂

(v,γ2),whereγ2=γ2[v:=v+1].Bythedefinitionofrelevancymap-󰀂

ping,thedomainofγ1equalsthatofγ1,andthedomainofγ2equalsthat

󰀂󰀂

ofγ2.Thus,alsoγ1andγ2agreeontheintersectionoftheirdomains.

󰀂󰀂

Thus,ifweextendfbydefiningf(v󰀂,γ1)=(v󰀂,γ2)wemaintainprop-erties(A.1)and(A.2).Clearly,falsopreservesthe(unique)incoming

󰀂󰀂

transitionsof(v󰀂,γ1)and(v󰀂,γ2).

(b)v∈F.Similartothecasev∈J∪M∪A.(c)v∈C.Similartothecasev∈J∪M∪A.

1n

3|W|>1.Inthiscasev󰀂isajoinnode.LetW={(v1,γ1),···,(vn,γ1)}.

iii

Letf(vi,γ1)=(vi,γ2),for1≤i≤n.Sinceviisinthedomainsofγ1andiiiγ2,γ1andγ2agreeontheintersectionoftheirdomains,andWisawitness,1nγ2(v1)=···=γ2(vn).Hencef(W)(definedbypointwiseextension)isa

󰀂󰀂i

witnessforthenodeinstance(v󰀂,γ2),whereγ2=∪ni=1γ2[vi:=vi+1].Thus,

󰀂󰀂

ifwedefinef(v󰀂,γ1)=(v󰀂,γ2),wepreservenodesandincomingtransitions.Theproof(A.2)islefttothereader(uselemma11).

󰀂