successorswww.avmoo.net

LivenessandBoundednessofSynchronousDataFlowGraphsA.
H.
Ghamarian,M.
C.
W.
Geilen,T.
Basten,B.
D.
Theelen,M.
R.
MousaviandS.
StuijkEindhovenUniversityofTechnology,ElectronicSystemsGroupa.
h.
ghamarian@tue.
nlAbstract.
SynchronousDataFlowGraphs(SDFGs)haveproventobesuitableforspecifyingandanalyzingstreamingapplicationsthatrunonsingle-ormulti-processorplatforms.
Streamingappli-cationsessentiallycontinuetheirexecutionindenitely.
Therefore,oneofthekeypropertiesofanSDFGisliveness,i.
e.
,whetherallpartsoftheSDFGcanruninnitelyoften.
AnotherelementaryrequirementiswhetheranimplementationofanSDFGisfeasi-bleusingalimitedamountofmemory.
Inthispaper,westudytwointerpretationsofthisproperty,calledboundednessandstrictboundedness,thatwereeitheralreadyintroducedintheSDFGlit-eratureorstudiedforothermodels.
Athirdandnewdenitionisintroduced,namelyself-timedboundedness,whichisveryimpor-tanttoSDFGs,becauseself-timedexecutionresultsinthemaxi-malthroughputofanSDFG.
Necessaryandsufcientconditionsforlivenessincombinationwithallvariantsofboundednessaregiven,aswellasalgorithmsforcheckingthoseconditions.
Asaby-product,weobtainanalgorithmtocomputethemaximalachievablethroughputofanSDFGthatrelaxestherequirementofstrongconnectednessinearlierworkonthroughputanalysis.
1IntroductionSynchronousDataFlowGraphs(SDFGs,see[13]),alsoknownasweightedMarkedGraphsinPetri-nettheory,areusedwidelyinmodellingandanalyzingdataowappli-cations.
TheyareoftenusedformodellingDSPapplica-tions[3,19]andfordesigningconcurrentmultimediaap-plicationsimplementedonmulti-processorsystems-on-chip[17].
Themodelissuitableforrealizingasystemwithpredictableperformancepropertiesasseveralanalysistech-niqueslikethroughputanalysisexist[8].
AnSDFGisagraphwithactorsasverticesandchan-nelsasedges.
Actorsrepresentbasicpartsofanapplicationwhichneedtobeexecuted.
Channelsrepresentdatadepen-denciesbetweenactors.
Executionofanactorisdesignatedbyanactorring.
Eachactorgeneratesaxednumberoftokenswhenitres.
Thesearestoredinthechannelswithunlimitedcapacities.
AnexecutionofanSDFGisase-quenceofactorringswhichrespectsdatadependencies.
Theexactorderofactorringsisnotdetermined.
Conse-quently,severalexecutionsexistforanSDFG.
BecauseoftheusageofSDFGsformodellingstreamingapplications,onlythoseSDFGswhichhaveexecutionsinwhichallac-torsareredinnitelyoftenareofinterest.
ThispropertyofSDFGsiscalledliveness.
Furthermore,onlyexecutionsThisworkwassupportedbytheDutchScienceFoundationNWO,project612.
064.
206,PROMES,andtheEU,projectIST-004042,Betsy.
thatrequireaniteamountofstorageforthechannelsareofinterest.
Thispaperformallystudiesthreedifferentinter-pretationsofthissecondproperty,allincombinationwithliveness.
Thepaperinvestigatestwoknowninterpretations,namelyboundedness(whetherthereexistsaboundedex-ecutionofanSDFG)andstrictboundedness(whetherallexecutionsarebounded).
WeprovenecessaryandsufcientconditionsguaranteeingthatanSDFGisliveand(strictly)bounded.
Forstrictboundedness,theseconditionsfollowimmediatelyfromasimilarresultknownforPetrinets.
ThenaturalwayofexecutinganSDFGinwhichallac-torsreassoonastheycanre,iscalledself-timedex-ecution.
ThisexecutionisimportantsinceitleadstothemaximalobtainablethroughputofanSDFG[19].
Becauseoftheimportanceofself-timedexecutionofSDFGsanditsapplicationsinthecontextofmulti-processorsystems,anewnotionofboundedness,namelyself-timedbound-ednessisintroduced.
Thisnotionrequiresthatself-timedexecutionofSDFGsisbounded.
Necessaryandsufcientconditionsforthelivenessandself-timedboundednessofSDFGsareproved.
Theseconditionsheavilydependonthethroughputofactors(averagenumberofringsofanactorpertimeunit).
Existingtechniquesforthroughputcalcula-tiononlyworkforstronglyconnectedSDFGs[6,8].
Weproposeanalgorithmthatdeterminesthelivenessandself-timedboundednessofanSDFGandatthesametimeex-tendsthroughputanalysistoarbitrarySDFGs.
Theconceptofself-timedboundednessandtheresultsprovenforthisnotionarethemaincontributionofthispaper.
Therestofthispaperisorganizedasfollows.
Section2formallyintroducesSDFGstoallowstudyinglivenessandboundednessinarigorousway.
Sections3and4presentre-sultsforlivenessand(strict)boundedness.
Section5iden-tiesconditionsforself-timedboundednessofSDFGsandpresentsanalgorithmforverifyingthecombinationoflive-nessandthistypeofboundedness.
Section6discussesre-latedwork,whileSection7summarizestheconclusions.
Proofsareomittedandcanbefoundin[9].
2SynchronousDataFlowGraphs2.
1BasicDenitionsThissectionformallydenesSDFGsandsomeoftheirbasicproperties.
LetIN0={0,1,andIN=IN0\1Figure1.
AnexampletimedSDFGGex.
{0})denotethe(positive)naturalnumbers.
ThefollowingdenitioncapturesthestructureofanSDFG.
Denition1[SynchronousDataFlowGraph(SDFG)]AnSDFGisapair(A,C),whereAdenotesthesetofactorsandCA2*IN2thesetofchannels.
Each(s,d,p,c)∈Cdenotesthatactorddependsonactors,wherepandcaretheproductionandconsumptionratesoftokensofsandd,respectively.
ThepredecessorsofainPred(a)={s∈A|(s,a,p,c)∈C}arethoseactorsonwhichadepends.
Thechannelsbetweenaanditspredecessorsarereferredtoastheinputchannelsofa,denotedbyIC(a).
Similarly,thesuccessorsofainSucc(a)={d∈A|(a,d,p,c)∈C}arethoseactorsthatdependona.
Theoutputchannels(channelsbetweenaanditssuccessors)ofaaredenotedbyOC(a).
Wecallachannelfromanactoratoitselfaself-loopchannel.
Wedenotethesetofself-loopchannelsofanactorabySLC(a)=IC(a)∩OC(a).
AnSDFGinwhichallproductionandconsumptionratesareoneiscalledaHomogeneousSDFG(HSDFG).
Figure1showsasimpleexampleofanSDFG.
Actorsarelabeledwiththeirnamesandexecutiontimes(introducedlater).
Channelsarelabeledwithproductionandconsump-tionrates.
Theblackdotsaretokens.
Tocapturetheexecu-tionofanSDFG,wedenethechannelstateofanSDFGasthedistributionoftokensoveritschannels.
Denition2[ChannelState]AchannelstateofanSDFG(A,C)isafunctionS:C→IN0thatreturnsthenumberoftokensstoredineachchannel.
EachSDFGhasanini-tialchannelstateS0denotingthenumberoftokensthatareinitiallystoredinthechannels.
AnexecutionofanSDFGisdenedbasedontheringsofitsactors,whichmayleadtochangesinthechannelstate.
Denition3[Firing]Leta∈AbeanactorofanSDFG(A,C).
ActoraissaidtobeenabledinchannelstateSincaseS(e)≥cforallinputchannelse=(s,a,p,c)inIC(a).
IfaisenabledinSianditres,theresult-ingchannelstateSi+1isdenedbySi+1(e)=Si(e)cforeachinputchannele=(s,a,p,c)inIC(a)\SLC(a),Si+1(e)=Si(e)+pforeachoutputchannele=(a,d,p,c)inOC(a)\SLC(a),Si+1(e)=Si(e)+pcforeachself-loopchannele=(a,a,p,c)∈SLC(a),andSi+1(e)=Si(e)forallchannelse/∈IC(a)∪OC(a).
Denition4[ExecutionandMaximalExecution]LetS0denotetheinitialchannelstateofanSDFG(A,C).
Anexecutionσof(A,C)isa(niteorinnite)sequenceofchannelstatesS0,S1.
.
.
suchthatSi+1istheresultofr-inganenabledactorinSiforalli≥0.
Anexecutionismaximalifandonlyifitisnitewithnoactorsenabledinthenalchannelstate,orifitisinnite.
NotallSDFGsareconsideredtobeusefulinpractice.
Onenormallyseeksasystemthatisdeadlock-freeorlive.
Denition5[DeadlockandLiveness]AnSDFGhasadeadlockifandonlyifithasamaximalexecutionofnitelength.
AnSDFGisliveifandonlyifithasanexecutioninwhichallactorsreinnitelyoften.
Itisknown[11]thattheexecutionofanSDFGisdeter-minate,whichmeansthattheorderofexecutiondoesnotaffectthestatesthatcaneventuallybereached.
Thus,ifoneexecutionofanSDFGdeadlocks,thenallexecutionsdead-lock.
TheexampleSDFGGexislive.
2.
2TimedSDFGsForperformanceanalysisofstreamingapplications,anSDFGisoftenextendedwithtime.
Denition6[ExecutionTime]AnexecutiontimemodelstheexecutiondurationofactorsforSDFGs.
InanSDFG(A,C),theexecutiontimeisafunctionE:A→IQ+0∪{∞}thatassignstoeachactortheamountoftimeittakestore,whereIQ+0∪{∞}isthesetofpositiverationalnumbersplus0and∞.
Fora∈A,E(a)isreferredtoastheexecutiontimeofa.
Denition7[TimedSDFG]AtimedSDFGisatriple(A,C,E)denotinganSDFG(A,C)withexecutiontimeE.
Theinniteexecutiontimesareusedlaterontomodeldead-locks.
Normally,SDFGsdonothaveinniteactorexecu-tiontimes.
NoticethatactorringsinatimedSDFGarenotatomic.
Firinganactornowtakestime.
TodenethestateofatimedSDFG,weassumethatallchangesinthenumberoftokensonallchannelsofanactorhappenattheendofitsring.
Denition8[TimedState]AstateofatimedSDFG(A,C,E)isapair(S,τ),whereSisachannelstateandτ∈IQ+0istheaccumulatedtime.
Theinitialstateof(A,C,E)isgivenbytheinitialchannelstateS0andthestarttimeofthesystemτ0=0.
Denition9[TimedExecution]AnexecutionofatimedSDFG(A,C,E)isasequenceoftimedstates(S0,τ0),(S1,τ1)whereτi+1≥τi.
Eachtwoconsecu-tivestates(Si+1,τi+1)and(Si,τi)arethesameexceptthatanactorawhichstarteditsringatτi+1E(a)nishesitsringatτi+1.
Si+1isrelatedtoSiinpreciselythesamewayasdenedinDenition3.
2Figure2.
Self-timedexecutionofGex.
Wedenotethenumberofcompletedringsofanactora∈AwhichoccurreduptotimeτbyFa,τ.
Amongalltimedexecutionstherearesomeofspecialinterest.
Atimedexecutionforwhichtheringofanactoralwaysstartsassoonaspossibleiscalledaself-timedexe-cution.
Self-timedexecutionsareimportantinthecontextofperformanceanalysisbecausetheyimplyobtainingthemaximalattainablethroughput[19].
Denition10[Self-timedExecution]Atimedexecutioniscalledself-timedifandonlyifitismaximalandallactorsstarttheirringassoonastheyareenabled.
Iftwoormoreactorscompletetheirringatsomepointintimeinaself-timedexecution,theorderoftheirappear-anceintheexecutionisnotdetermined.
Inotherwords,anypermutationofsuchactorringsresultsinaself-timedexe-cution.
Thus,thenumberofself-timedexecutionsislargerthanoneinsuchcases.
Notethatinallself-timedexecutionsthestartandendtimesofringsofallactorsareequal.
Alsothechannelsstatesaftercompletionofallactorringsthatcancompleteatacertainpointintimearethesameinallself-timedexecutions.
Figure2illustratesaself-timedexecutionoftheexam-pleSDFGGexofFigure1.
Thestatecontainsachannelcomponentwiththedistributionoftokensoverthechannelsa-a,a-b,b-c,c-b,respectively,andatimecomponent.
Inthedepictedcycle,thetimecomponentisdenotedsymbolicallytoemphasizethatthebehaviorrepeatsitselfeverysixtimeunits,aftersomeinitialtransientphase.
2.
3StructuralPropertiesThedirectedgraphofanSDFGhassomestructuralprop-ertiesthatarerelevantfordecidingboundedness.
Thispa-perassumesconnectedSDFGsforwhichthedirectedgraphconsistsofonecomponent.
SDFGsconsistingofmultiplecomponentscanbeconsideredasasetofsingle-componentSDFGs,whichcanbeanalyzedseparately.
Awellknownstrongerformofconnectivityisgivenbythefollowingtwodenitions.
Denition11[PathandCycle]Adirectedpathpisase-quenceofactorsa1,a2.
.
.
alsuchthatai+1∈Succ(ai)forall1≤i0foralla∈A.
Ifanon-trivialrepetitionvectorex-ists,theSDFGiscalledconsistent.
Thesmallestnon-trivialrepetitionvectorofaconsistentSDFGisreferredtoastherepetitionvector.
NotethatthedenitionsinthissubsectioncarryovertotimedSDFGsinastraightforwardway.
TimedSDFGGexisconsistentwithrepetitionvector(a→3,b→3,c→2).
2.
4ThroughputofTimedSDFGsInthissectionthethroughputoftimedSDFGsisdened,andtherelationbetweentheexecutionofanSDFGanditsthroughputisexplained.
Denition14[Throughput]ThethroughputTh(a)ofanactoraforaself-timedexecutionofatimedSDFG(A,C,E)isdenedastheaveragenumberofringsofapertimeunit.
Formally,Th(a)=limτ→∞Fa,ττ.
IfG=(A,C,E)isconsistent,thenitsthroughputisde-nedasTh(G)=mina∈ATh(a)γ(a),whereγistherepetitionvectorof(A,C,E).
Thatis,thethroughputofGistheminimalactorthroughputnormalizedbytherepetitionvector.
Wedenethelocalthroughputofanactorasthethroughputofthatactorinaself-timedexecutionwherenon-self-loopinputchannelsareremoved;inotherwords,thethroughputofanactorwhenitdoesnotneedtowaitfordatafromotheractors.
Denition15[LocalThroughput]ThelocalthroughputLTh(a)ofanactoraforaself-timedexecutionofatimedSDFG(A,C,E)isdenedasLTh(a)=0,ifthereisach=(a,a,p,c)inSLC(a)suchthatpAL[i].
Th16.
thenreturn"no"17.
return"yes,AL[1].
Th"Thealgorithmworksintwosteps.
Therststepchecksthelivenessandboundedness(asdenedbyDenition17)ofthegraphbycallingalgorithmisLive&Bounded(lines1and2).
Ifthegraphisnotliveandbounded,itcannotbeliveandself-timedbounded.
ThesecondstepconcernsdeterminingwhetherthereducedHSDFGisself-timedbounded(lines3to17).
IfisLive&Boundedreturns"yes",weknowthattheSDFGisconsistent.
Then,line3ofthealgorithmreducestheSDFGaccordingtoDenition35andstorestheresultinGH.
Notethatthereductionrequiresthroughputcalcula-tionsforallSCCs.
Forefciencyreasons,thesethroughputcalculationscanbedelayedtillthealgorithmreallyneedsthisinformation.
Calculationsmaythenbeavoidedifthealgorithmreturns"no"early.
Wehavenotmadethisex-plicitinthealgorithm.
SinceGisatthispointknowntobeliveandconsistent,byCorollary39,alsoGHislive.
Itremainstodetermineself-timed(un-)boundedness.
Ignoringself-loops,GHisacyclic.
Line4topologicallysortstheactorsofGH,andstorestheminarrayAL,sothatthepredecessorsofanactorAL[i]areonlyamongtheAL[j]forj≤i.
IfGHcontainsonlyoneactor,thenGisstronglyconnected,andhence,byProposition30,self-timedbounded,andthealgorithmterminates.
BasedonCorollary37,itreturnsthelocalthroughputoftheonlyac-torofGHasthethroughputofG.
Notethateveryactorinareducedgraphhasaself-loopchannelwithonetokenonit,sothisvalueisequalto1/EH(AL[1]).
AlsonotethatEH(AL[1]),andEH(AL[i])ingeneral,maybe0.
Inthiscase,weassumethat1/EH(AL[i])isequalto∞.
Eachiterationoftheloopoflines7to16startsbycal-culatingthelocalthroughputofeachactorAL[i],1≤i≤|AH|,storingtheresultinAL[i].
Th.
Incaseofdetectingasourceactor(anactorwithoutanyinputchannelexceptitsself-loopchannel)withaninnitethroughput,thealgorithmreturns"no",becausethisimpliesthatitsoutputchannelsareunbounded.
TheloopcontinuesbysettingmaxPThtozero.
ThisvariableisatemporaryvariableforstoringthemaximumthroughputofthepredecessorsofactorAL[i]initerationi.
Intheloopoflines12to14,theminimumbe-tweenthelocalthroughputofactorAL[i]andtheminimumthroughputofitspredecessorsisassignedtoAL[i].
Th.
Thisvalue,accordingtoLemma27,isthethroughputoftheac-torAL[i].
NotethatsincetheactorsaretopologicallysortedinAL,thethroughputofallpredecessorshasalreadybeencalculated.
ThemaximumthroughputofthepredecessorsofactorAL[i]isassignedtomaxPTh.
Thetestofline15checkswhetherthemaximumthroughputofpredecessorsofactorAL[i](excludingAL[i])isgreaterthanthethroughputofactorAL[i]itself.
Incaseitis,accordingtoLemma29atleastonechannelconnectingapredecessorofactorAL[i]toAL[i]isunbounded.
Ifthealgorithmreachesline17,thennounboundedchannelhasbeendetected,andthegraphisliveandself-timedbounded.
AccordingtoCorollary37andthefactthatthereducedSDFGisanHSDFGwithallrepetition-vectorentriesone,thevalueofAL[i].
ThforallactorsAL[i]∈AHisequaltothethroughputofG.
Theal-gorithmreturnsAL[1].
Th.
Theemphasisofalgorithmis-Live&SelftimedBoundedisonverifyinglivenessandself-timedboundednessofanSDFG,soitreturnsassoonasitdetectsthatthegraphisnotliveornotself-timedbounded.
ItcanbeeasilyadaptedtocomputethethroughputforSD-FGswhicharenotself-timedboundedaswell.
6RelatedWorkThereareinterestingsimilaritiesbetweenSDFGsandPetrinets.
Inparticular,thereisastraightforwardtransla-tionfromSDFGstoasubclassofPetrinets,calledweightedMarkedGraphsandviceversa,whereactorsaretransitions,andchannelsareplaces.
MarkedGraphs,alsocalledT-GraphsareknowntobethesubclassofPetrinetsthatismostamenabletorigorousanalysis.
Thus,itmakessensetocomparetheresultsobtainedinthispaperwiththecorre-spondingresultsintheliteratureconcerningPetrinets.
Westudiedlivenessincombinationwiththreedifferentdeni-tionsofboundedness(Denitions17,18and19)for(timed)SDFGs.
WedonotknowofanyrelatedresultsforboundednessasdenedbyDenition17.
Theonlyresultweknowforthistypeofboundednessisin[16]whichonlyintroducesitwithoutprovidingnecessaryandsufcientconditions,aswedo.
ForstrictboundednessinthesenseofDenition18,theproblemhasbeenstudiedfromdifferentviewpointsinthePetri-netliterature(seeforanoverview[7,15]).
Inparticu-lar,[20]givesnecessaryandsufcientconditionsforstrictboundednessofliveweightedMarkedGraphs(ourTheo-rem25).
Strictboundednessisalsotheonlykindofbound-ednesswhichhasbeeninvestigatedformallyinthelitera-tureonSDFGsthemselves;KarpandMillerintheirsem-inalpaper[11]introducedcomputationgraphs,whichareslightlymoregeneralthanSDFGs.
Theyprovednecessaryandsufcientconditionsforlivenessandstrictboundedness7intheirmodel.
Theirresultsaswellasthosein[20]corre-spondtothosepresentedinthispaper.
Ourthirddenitionofboundedness,self-timedbounded-ness(seeDenition19)isdenedontimedSDFGs.
There-fore,weneedtocompareitwithtime-enabledPetrinets.
Petrinetshavebeenextendedwithquantitativetimeindif-ferentways,byaddingtiminginformationtoplaces,transi-tionsand/ortokens(see[4]forasurvey).
ThetimedPetrinetmodelthatcomesclosesttotimedSDFGsisthe"timePetrinet"modeloriginallydenedby[14].
Thisexten-sionofPetrinetsassociatesaduration(delay)andadead-linetotransitions.
Wearenotawareofanystudyoftheself-timedboundednessproblemforthesubclassoftimeMarkedGraphs.
In[18],thelivenessandstrictbounded-nessproblemfortimePetrinetsisstudiedbutonlysomesufcientconditionsaregiven.
Theseconditionsguaran-teethatonceatimePetrinetsatisescertainsyntacticcon-straints,itisliveandstrictlyboundediftheunderlyingun-timedPetrinetisliveandstrictlybounded.
Unfortunately,theresultsof[18]cannotbeappliedinoursettingsincethesyntacticconstraintsrequiretheabsenceofeitherdurationordeadlinebothofwhicharenecessaryfortranslationoftimedSDFGstotimePetrinets.
[10]provesageneralun-decidabilityresultforstrictboundednessoftimePetrinetof[14].
However,in[2],twosufcientconditionsaregivenforstrictboundednessoftimePetrinets.
Wearenotawareofanyresultaboutself-timedboundednessasdenedinDef-inition19.
Tothebestofourknowledge,boththeconceptandthederivedresultsarenovel.
7ConclusionsWehavestudiedthelivenessandboundednessofSyn-chronousDataFlowGraphs,whicharealsoknownasweightedMarkedGraphsinthePetri-netliterature.
Live-nessandboundednessisaprerequisiteofanymeaningfulSDFGmodelofastreamingmulti-mediaapplication.
Twoknownnotionsofboundedness,namelyboundednessandstrictboundedness,havebeenstudiedrigorously,andinparticularnecessaryandsufcientconditionsforlivenessincombinationwiththesetwotypesofboundednesshavebeengiven.
Forstrictboundedness,theseconditionswerealreadyknownfromthePetri-netliterature.
Furthermore,anewnotion,self-timedboundedness,wasintroduced.
Self-timedboundednesscheckswhetherself-timedexecutionofanSDFGisbounded.
Aself-timedexecutionyieldsthemaximumthroughputforanSDFG.
Necessaryandsuf-cientconditionsforself-timedboundednessandlivenesshavebeenproven.
Analgorithmforcheckingthesecon-ditionswaspresented.
Besides,existingthroughputanaly-sistechniques,whichareonlyvalidforstronglyconnectedgraphs,areextendedtoarbitraryconsistentSDFGs.
References[1]F.
Baccelli,G.
Cohen,G.
Olsder,andJ.
-P.
Quadrat.
Synchro-nizationandlinearity:analgebrafordiscreteeventsystems.
Wiley,1992.
[2]B.
BerthomieuandM.
Diaz.
ModelingandvericationoftimedependentsystemsusingtimePetrinets.
IEEETrans-actionsonSoftwareEngineering,17(3):259–273,1991.
[3]S.
Bhattacharyya,P.
Murthy,andE.
Lee.
Synthesisofem-beddedsoftwarefromsynchronousdataowspecications.
JournalonVLSISignalProcess.
Syst.
,21(2):151–166,1999.
[4]F.
D.
Bowden.
AbriefsurveyandsynthesisoftherolesoftimeinPetrinets.
MathematicalandComputerModelling,31(10):55–68,2000.
[5]T.
Cormen,C.
Leiserson,R.
Rivest,andC.
Stein.
Introduc-tiontoAlgorithms.
MITPress,2001.
[6]A.
Dasdan.
Experimentalanalysisofthefastestoptimumcycleratioandmeanalgorithms.
ACMTrans.
onDesignAutomationofElectronicSystems,9(4):385–418,2004.
[7]J.
Esparza.
DecidabilityandcomplexityofPetrinetprob-lems-anintroduction.
InW.
ReisigandG.
Rozenberg,ed-itors,LecturesonPetriNetsI:BasicModels,AdvancesinPetriNets,volume1491ofLectureNotesinComputerSci-ence,pages374–428.
Springer-Verlag,1998.
[8]A.
H.
Ghamarian,M.
Geilen,S.
Stuijk,T.
Basten,A.
Moo-nen,M.
Bekooij,B.
Theelen,andM.
Mousavi.
Throughputanalysisofsynchronousdataowgraphs.
InACSD,Proc.
,pages25–34.
IEEE,2006.
[9]A.
H.
Ghamarian,M.
C.
W.
Geilen,T.
Basten,B.
Theelen,M.
M.
R.
,andS.
Stuijk.
Livenessandboundednessofsyn-chronousdataowgraphs.
Tech.
reportESR-2006-04,TUEindhoven,http://www.
es.
ele.
tue.
nl/esreports/,2006.
[10]N.
D.
Jones,L.
H.
Landweber,andY.
E.
Lien.
ComplexityofsomeproblemsinPetrinets.
TheoreticalComputerScience,4(3):277–299,1977.
[11]R.
M.
KarpandR.
E.
Miller.
Propertiesofamodelforparallelcomputations:Determinacy,termination,queueing.
SIAMJournalonAppliedMathematics,14(6):1390–1411,1966.
[12]E.
Lee.
Acoupledhardwareandsoftwarearchitectureforprogrammabledigiralsignalprocessors.
PhDthesis,Uni-versityofCalifornia,Berkeley,1986.
[13]E.
LeeandD.
Messerschmitt.
Synchronousdataow.
Pro-ceedingsoftheIEEE,75(9):1235–1245,September1987.
[14]P.
M.
Merlin.
AStudyofRecoverabilityofProcesses.
PhDthesis,DepartmentofInformationandComputerScience,UniversityofCaliforniaatIrvine,1975.
[15]T.
Murata.
Petrinets:Properties,analysisandapplications.
ProceedingsoftheIEEE,77(4):541–580,1989.
[16]T.
M.
Parks.
BoundedSchedulingforProcessNetworks.
PhDthesis,1995.
[17]P.
Poplavko,T.
Basten,M.
Bekooij,J.
vanMeerbergen,andB.
Mesman.
Task-leveltimingmodelsforguaranteedper-formanceinmultiprocessornetworks-on-chip.
InCASES,Proc.
,pages63–72.
ACM,2003.
[18]L.
Popova-Zeugmann.
OnlivenessandboundednessintimePetrinets.
InProceedingsoftheWorkshoponConcur-rency,SpecicationandProgramming(CS&P'95),pages136–145,1995.
[19]S.
SriramandS.
Bhattacharyya.
EmbeddedMultiproces-sors:SchedulingandSynchronization.
MarcelDekker,Inc,NewYork,NY,USA,2000.
[20]E.
Teruel,P.
Chrzastowski,J.
M.
Colom,andM.
Silva.
OnweightedT-systems.
InJensen,K.
,editor,13thInterna-tionaldConferenceonApplicationandTheoryofPetriNets1992,Shefeld,UK,volume616ofLectureNotesinCom-puterScience,pages348–367.
Springer-Verlag,1992.
8