网络流量控制外文翻译文献

网络流量控制外文翻译文献网络流量控制外文翻译文献(文档含中英文对照即英文原文和中文翻译)译文：普遍布尔网络的流量控制分析1介绍在生物体和理解他们的连接和他们整个动力学是相当具有挑战性的任务，监管网络发挥着至关重要的作用。可执行模型的生物过程暗示了这些网络可以提供有用的见解。然而,构建完整详细的可执行模型的生物系统常常遭到缺乏准确、高信任度的参数有关,例如,动力学的化学反应或分子的浓度。一个可能的解决方案在于提供一种定性模型,能够把握的基本特征的动态行为。这是接下来的步骤在[33、30、31、29]的逻辑方法,普遍托马斯布尔网络(GBN),提出了。在这个模型中,每个基因的状态(视为一个监管实体)是representedby浓度阈值不同于有限数量的值,例如：低,中,高。这个模型允许一个来推断GBN生物模型不完整数据,来研究生物稳定状态和反馈(正面或负面)。然而他们的应用程序生成一个指数级增长的州,没有大量的正式技术和分析工具可用。其他可执行语言,像佩特里网[26]或进程代数(例如。[19,6])可以提供相反他们有充分根据的理论和工具支持,一旦呈现逻辑管理模型框架内他们的互补。此外,GBNs很难处理不完整的或不一致的数据,即案件中可能有不止一个下一个状态,同时,再一次,佩特里网或进程代数模型这些情况下,可以利用非决定论。最后,佩特里网和过程代数都能很容易地扩展以处理定量信息,如随机的,例如。,将利率与转换。佩特里网理论,已经利用在系统生物学(如在[15、14]),已经被用来分析的动态监管网络在一些作品(见例如。[7、27、28]),逻辑模型方面的翻译,从而利用培养皿网上面的一些有用特性。进程代数提供另一种框架来分析动力学的监管网络。他们([23、25日,24日,9、10、11、5、22、8),引用只有几个)肥沃地用于模型的几种生物系统,依靠这个想法,一个生物系统可以抽象地描述为一个并发系统。我们的方法的目的是利用过程的建模和分析GBNs代数。更多的细节,我们的目的是•引入一个可执行过程代数模型能够捕捉同步行为的GBNs,每个实体组成的网络可以改变其浓度只有当所有其他实体交互已经达到阈值;•提出一个静态分析技术,一旦应用于获得的模型,能够提供安全的近似的行为建模的实体。因此,我们可以测试的忠实性模式,还提供自信预测,以防动力学模型是足够精确的。2普遍布尔网络布尔网络(BNs)[16]介绍了在生物基因调控网络模型(入库单),即那些网络相互作用的基因,它们在蛋白质合成的基础。一个布尔网络是由一组实体,相互调节在积极或者消极的道路。每个基因的状态(视为一个监管实体)表示为一个布尔值,即活跃(1)或非活动(0)。(全球)状态的布尔网络,由n基因,被表示为一个n维向量的布尔变量,一个用于每一个基因。从一个国家的进化到下一个是计算一组n布尔函数,每个代理在每个单一变量,定义下一个状态从当前状态的基因调节它。3Sim-πn过程代数建模的GBNs同步模式,我们引入一个新的进程代数称为Sim-n,想起了π-calculus[19](没有总和与限制,限制形式的过程和一个特殊的许多许多同步机制。和谐的synchronisations获得必需的,我们的流程,代表监管实体P,得到了并联组成的特殊的子流程年代出现在定制表单。子过程年代结构两个部分:初始的警卫,由一组输入,必须所有的执行(第一部分),如果任何的,在执行之前唯一的最后输出前缀(第二部分)与美国或者子流程年代可以延续(b-S)或者可以像在π-calculus,术语0表示空的过程和运营商_表示并行成分。作为标准,我们省略0,在需要的时候,我们使用简写支∈RSi的简写并行成分的过程对我∈SiR前缀b表示输出的值b通道一个。多重选择性输入前缀警卫队{a1(x1∈x1),……,一个(xn∈xn)}。(一个b_年代)(见[4]类似的构造)同时获得输出所有渠道aibia1,……,并继续作为(b-S),但每个bi属于习近平对于每个我∈(1,n),集喜不包括任何束缚的名字。换句话说,一个价值收到沿着通道ai是只接受如果它匹配的值包含在相应的选择集习近平。请注意,输入在Sim-πn已经完全n项。减少我们的微积分的语义给出了表2。我们使用标准的概念结构一致性的π-calculus≡:特别是,流程形成一个交换幺半群就并行成分。沟通是在平行和广播,即每个顶级输出同时同步每输入相应发生的输入组合,4控制流分析控制流分析(CFA)扩展了一个用于π-calculus在[3]。CFA在近似计算安全的所有可能的值的元组变量在系统可能被绑定到,和元组值,可同时流渠道。此外,它可以建立一个因果关系的配置和下一个。换句话说,它预测所有可能的通信,因此所有可能的可配置,从浓度水平。更准确地说,分析跟踪以下信息:5可能的优化稍微修改一下我们的定义过程导出了GBNs,我们获得一个更紧凑的编码,回忆更紧凑的公式,得到了通过应用逻辑最小化技术知名。在这方面,我们可以利用完整的表达能力集在选择性输入。注意,如果实体Gi并不取决于实体Gk,然后我们可以把Xk=Bk在k位置在所有分支的Gi。在过程代数方面,这对应于有输入上的其他组件同步,独立于输出在k组件。例如,在我们的运行示例,我们可以减少分支在指定G1,如下所示:G1=G11_G12_G13G11={g1(x111∈{0,1}),g2(x211∈{0})}.(g1_1__G11)G12={g1(x112∈{0,1}),g2(x212∈{1})}.(g1_1__G12)G13={g1(x113∈{0,1}),g2(x213∈{2})}.(g1_0__G13)此外,我们可以合并在一个单一的分支,所有的组合都有一个条目,从而导致相同的结果。我们可以说明它仍然在我们运行的例子,我们的价值(G1)是1要么如果G2=0或G2=1。因此,我们可以有一个单独的分支对于这两种情况,从而进一步减少整个数量的分支,如以下规范。G1=G11_G12G11={g1(x111∈{0,1}),g2(x211∈{0,1})}.(g1_1__G11)G12={g1(x112∈{0,1}),g2(x212∈{2})}.(g1_0__G12)这个操作召回相应的简化的多维价值上分隔正常形式,得到了通过结合产品条款,由文字形式gS我哪里年代⊆Bi。这两个术语可以被组合在一起,因为他们不同在只有文字g2。最后,当一个更简洁的规范是必要的,我们甚至可以忽略输入的变量xik属于xik=Bk的规范,如:G1=G11_G12_G13G11={g2(x211∈{0,1})}.(g1_1__G11)G12={g2(x212∈{2})}.(g1_0__G12)CFA可以稍微做出相应的修改。6结论使用布尔网络模型全面监管网络提出了一些不足之处,主要是由于低数量的分析工具和困难在处理不完整的或不一致的数据。为了克服这些局限性,我们依赖于过程代数框架。我们确实已经翻译了逻辑模型Sim-πn而言,小说过程代数。因此,我们已获得流程模型显示相同的行为的原始GBNs,准备分析与通常的过程代数工具。特别是,我们应用控制流分析过程代数规范,因此获得的见解在研究生物系统,而支付较低的com-putational成本。我们有显示这些功能通过一个案例研究为代表的监管网络底层Th淋巴细胞分化。特别是,我们有调查所发挥的作用,基因组成的网络在确定最终的系统状态在不同实验条件下。这个例子显示如何我们的工具包可以被充分利用来评估生物系统感兴趣的属性。我们的方法可以特别有用,在分析大型GBN模型(如整个细胞模型)。即使部分生物知识是可用的,利用两Sim-πn和CFA允许我们设计和研究现实模型的生物系统即模型与观测一致行为的生物学配对。我们正在计划使用我们的框架来描述和分析大型的模型生物网络,如信号通路的影响。此外,我们打算分析表达能力,做的Sim-πn[17]。参考文献[1]H.K.Abbas,A.K.Lichtman,S.Pillai.Cellularandmolecularimmunology,7theditionElsevier-Saunders,2009.[2]R.M.Amadio,F.Dabrowski.FeasiblereactivityinasynchronousPi-calculus.Proc.ofthe9thInternationalACMSIGPLANConferenceonPrinciplesandPracticeofDeclarativeProgramming(PPDP’07),ACM,2007.[3]C.Bodei,P.Degano,F.Nielson,H.RiisNielson.Staticanalysisfortheπ-calculuswithapplicationstosecurity.InformationandComputation168(1):68–92,2001.[4]C.Bodei,P.Degano,C.Priami.CheckingsecuritypoliciesthroughanenhancedControlFlowAnalysisJournalofComputerSecurity13(1):49-85,2005.[5]L.Cardelli.BraneCalculi-InteractionsofBiologicalMembranes.Proc.ofComputationalMethodsinSystemsBiology(CMSB’04).LectureNotesinComputerScience3082,pp.257-278,Springer,2005.[6]L.CardelliandA.D.Gordon.MobileAmbients.TheoreticalComputerScience240(1):177-213(2000).[7]C.Chaouiya,A.Naldi,E.Remy,D.Thieffry.Petrinetrepresentationofmulti-valuedlogicalregulatorygraphsNaturalComputing10(2):727-750,2011.[8]D.Chiarugi,P.Degano,R.Marangoni.AComputationalApproachtotheFunctionalScreeningofGenomes.PLoSComputationalBiology3(9),2007.[9]V.Danos,JeanKrivine.TransactionsinRCCS.Proc.ofConferenceonConcurrencyTheory(CONCUR’05).LectureNotesinComputerScience3653,pp.398-412,Springer2005.[10]V.Danos,C.Laneve.GraphsforCoreMolecularBiology.Proc.ofComputationalMethodsinSystemsBiology(CMSB’03).LectureNotesinComputerScience2602,pp.34-46,Springer2003.原文：ControlFlowAnalysisofGeneralisedBooleanNetworksChiaraBodei,LindaBrodo,DavideChiarugi1IntroductionRegulatorynetworksplayacrucialroleinlivingorganismsandunderstandingtheirconnectionsandtheirwholedynamicsisquiteachallengingtask.Executablemodels[13]ofbiologicalprocessesimpliedbythesenetworkscanprovideusefulinsights.Nevertheless,buildingfulldetailedexecutablemodelsofbiologicalsystemsisoftenhamperedbythelackofaccurate,high-confidenceparametersregarding,say,thekineticsofthechemicalreactionsormolecularconcentrations.Onepossiblesolutionconsistsinprovidingaqualitativemodel,abletograsptheessentialfeaturesofthedynamicbehavior.Thisistheapproachfollowedin[33,30,31,29]wherethelogicalThomas’method,theGeneralisedBooleanNetwork(GBN),ispresented.Inthismodel,thestateofeachgene(seenasaregulatoryentity)isrepresentedbyaconcentrationthresholdvaluethatvariesonalimitednumberofvalues,e.g.,Low,MediumorHigh.TheGBNmodelallowsonetoinferbiologicalmodelsfromincompletebiologicaldataandtostudythesteadystatesandthefeedbacks(positiveornegative).Neverthelesstheirapplicationgeneratesanexponentialgrowthofthestatesandthereisnotalargenumberofformaltechniquesandanalysistoolsavailable.OtherexecutablelanguageslikePetriNets[26]orProcessAlgebras(e.g.[19,6])canofferinsteadtheirwell-foundedtheoryandtoolsupport,oncerenderedthelogicalregulatorymodelsinsidetheircomplementaryframeworks.Furthermore,GBNscanhardlyhandleincompleteorinconsistentdata,i.e.casesinwhichtherecouldbemorethanonenextstate,while,again,PetriNetsorProcessAlgebrascanmodelthesesituations,byexploitingnondeterminism.Finally,bothPetriNetsandProcessAlgebrascanbeeasilyextendedinordertodealwithquantitativeinformation,likestochasticones,e.g.,associatingrateswithtransitions.ThetheoryofPetriNets,alreadyexploitedinSystemsBiology(e.g.in[15,14]),hasbeenemployedtoanalysethedynamicsofregulatorynetworksinseveralworks(seee.g.[7,27,28]),inwhichthelogicalmodelsaretranslatedintermsofPetriNets,thusexploitingsomeoftheaboveusefulfeatures.ProcessAlgebrasprovideanalternativeframeworktoanalysethedynamicsofregulatorynetworks.They([23,25,24,9,10,11,5,22,8],tociteonlyafew)havebeenfruitfullyusedtomodelseveralkindsofbiologicalsystems,relyingontheideathatabiologicalsystemcanbeabstractlymodelledasaconcurrentsystem.OurapproachaimsatusingprocessalgebrasformodellingandanalysingGBNs.Moreindetails,ourpurposesare•tointroduceanexecutableprocessalgebraicmodelabletocapturethesynchronousbehaviorofGBNs,whereeachentitycomposingthenetworkcanchangeitsconcentrationonlywhenalltheotherinteractingentitieshavereachedtheirthresholdvalues;•toproposeastaticanalysistechniquethat,onceappliedtotheobtainedmodel,isabletoprovidesafeapproximationsofthebehaviorofthemodelledentities.Asaconsequence,wecantestthefaithfulnessofthemodelandalsoprovideconfidentpredictionsonthedynamics,incasethemodelissufficientlyaccurate.2GeneralisedBooleanNetworksBooleanNetworks(BNs)[16]havebeenintroducedinBiologytomodelGeneRegulatoryNetworks(GRN),i.e.thosenetworksofinteractionbetweengenesthatareatthebasisoftheproteinsynthesis.ABooleanNetworkiscomposedbyasetofentitieswhichregulateeachotherinapositiveornegativeway.Thestateofeachgene(seenasaregulatoryentity)isrepresentedbyabooleanvalue,i.e.active(1)orinactive(0).The(global)stateofabooleannetwork,composedofngenes,isrepresentedasan-dimensionvectorofbooleanvariables,oneforeachgene.Theevolutionfromastatetothenextoneiscomputedbyasetofnbooleanfunctions,eachactingoneachsinglevariable,thatdefinethenextstatestartingfromthecurrentstateofthegeneswhichregulateit.3TheProcessAlgebraSim-πnTomodelthesynchronisationpatternofGBNs,weintroduceanewprocessalgebracalledSim-n,reminiscentoftheπ-calculus[19](withoutsummationandrestriction),withrestrictedformsforprocessesandaspecialmanytomanysynchronizationmechanism.Toobtaintherequiredunisonoussynchronisations,ourprocessesP,thatrepresentregulatoryentities,areobtainedbytheparallelcompositionofspecialsubprocessesSthatappearintailoredform.Sub-processesSarestructuredintwoparts:aninitialguard,madebyasetofinputsthatmustbeallexecuted(firstpart),ifany,beforeexecutingtheonlylastoutputprefix(secondpart)inparallelwithS.Alternativelyasub-processScanbethecontinuation(a_b__S)orcanbeLikeintheπ-calculus,theterm0denotestheemptyprocessandtheoperator_denotestheparallelcomposition.Asstandard,weomit0,whenneeded,andweusetheshorthand_i∈RSiforabbreviatingtheparallelcompositionofprocessesSifori∈R.Theprefixa_b_denotestheoutputofvaluebonthechannela.Themultipleselectiveinputprefixguard{a1(x1∈X1),...,an(xn∈Xn)}.(a_b___S)(see[4]forasimilarconstruct)simultaneouslygetstheoutputsai_bi_onallthechannelsa1,...,anandcontinuesas(a_b___S),providedthateachbibelongstoXiforeachi∈[1,n],wherethesetsXidonotincludeanyboundname.Inotherwords,avaluereceivedalongthechannelaiisacceptedonlyifitmatcheswithoneofthevaluesincludedinthecorrespondingselectionsetsXi.NotethatinputsinSim-πnhaveexactlynitems.ThereductionsemanticsofourcalculusisgiveninTable2.Weusethestandardnotionofstructuralcongruence≡ofπ-calculus:inparticular,processesformacommutativemonoidwithrespecttotheparallelcomposition.Thecommunicationisinparallelandinbroadcast,i.e.eachtop-leveloutputsimultaneouslysynchroniseswitheverycorrespondinginputoccurringinthecombinationofinputs,intherestofthesystem,asexplainedbelow.NotethatintheprocessesusedtorepresentGBNsthevaluessentarenotusedforsubsequentcommunications,butarepassedforsynchronisationpurposes,unliketheπ-calculus,andmoreinCCS[20]style.Theotherrulesarestandard.Thedefinitionbelowallowstheconstructionofasystemofprocesses,givenaGeneralisedBooleanNetwork,whichshowsabehaviorequivalenttothatoftheoriginalGBN.Ourideaconsistsinhavingaprocessforeachregulativeentityandabranchforeachentryinthenext-statefunctiontable,withthesuitableselectivejointinput.Furthermore,tointroducetheinitialconditions,weusesingleoutputs,notprecededNotethat,incaseofincompletedata,i.e.casesinwhichtherecouldbemorethanonenextstate,theprocessalgebraicframeworkoffersusawayout,thankstothepossibleintroductionofthenondeterministicchoiceoperator+inthesyntax.4ControlFlowAnalysisTheControlFlowAnalysis(CFA)extendstheonefortheπ-calculusin[3].TheCFAcomputesasafeover-approximationofallthepossiblevaluesthatthetuplesofvariablesinthesystemmaybeboundto,andofthetuplesofvaluesthatmaysimultaneouslyflowonchannels.Furthermore,itcanestablishacausalrelationbetweenaconfigurationandthenextone.Inotherwords,itpredictsallthepossiblecommunications,andconsequentlyallthepossiblereachableconfigurations,intermsofconcentrationlevels.Moreprecisely,theanalysiskeepstrackofthefollowinginformation:5PossibleOptimisationsSlightlymodifyingourdefinitionofprocessesderivedbyGBNs,weobtainamorecompactencoding,thatrecallthemorecompactformulas,obtainedbyapplyingwell-knownlogicminimisationtechniques.Underthisregard,wecanexploitthefullexpressivenessofthesetsintheselectiveinputs.NotethatiftheentityGidoesnotdependontheentityGk,thenwecouldputXk=Bkinthek-thpositioninallthebranchesofGi.Ontheprocessalgebraicside,thiscorrespondstohavethattheinputontherestofcomponentssynchronises,independentlyfromtheoutputonthek-thcomponent.Forinstance,inourrunningexample,wecouldhavelessbranchesinthespecificationofG1,asfollows:G1=G11_G12_G13G11={g1(x111∈{0,1}),g2(x211∈{0})}.(g1_1__G11)G12={g1(x112∈{0,1}),g2(x212∈{1})}.(g1_1__G12)G13={g1(x113∈{0,1}),g2(x213∈{2})}.(g1_0__G13)Furthermore,wecanmergeinonesinglebranchallthecombinationsthatshareoneoftheentries,thusleadingtothesameresult.Wecanillustrateitstillinourrunningexample,wherewehavethatthevalueof[G1]is1eitherifG2=0orG2=1.Consequently,wecanhaveasinglebranchforbothcases,thusfurtherreducingthewholenumberofbranches,asinthefollowingspecification.G1=G11_G12G11={g1(x111∈{0,1}),g2(x211∈{0,1})}.(g1_1__G11)G12={g1(x112∈{0,1}),g2(x212∈{2})}.(g1_0__G12)Thisoperationrecallsthecorrespondingminimisationonthemulti-valuesdisjunctivenormalforms,obtainedbycombiningproductterms,madebyliteralsintheformgSiwhereS⊆Bi.Thetwotermscanbecombinedtogetherbecausetheydifferinonlytheliteralg2.Finally,whenamoreconcisespecificationisneeded,wecouldevenomittheinputsonthevariablesxikthatbelongtoXik=Bkinthespecification,asin:G1=G11_G12_G13G11={g2(x211∈{0,1})}.(g1_1__G11)G12={g2(x212∈{2})}.(g1_0__G12)TheCFAcanbeslightlymodifiedaccordingly.Inthenextsection,weapplyalltheaboveoptimisationstoourcasestudy.6ConclusionsUsingGeneralisedBooleanNetworkstomodelregulatorynetworkspresentssomedisadvantages,mainlyduetothelownumberofanalysistoolsandtothedifficultyinhandlingincompleteorinconsistentdata.Toovercometheselimitations,wehavereliedontheprocessalgebraicframework.WehaveindeedtranslatedthelogicalmodelsintermsofSim-πn,anovelprocessalgebra.Asaresult,wehaveobtainedprocessmodelswhichshowthesamebehavioroftheoriginalGBNsandthatarereadytobeanalysedwiththeusualprocessalgebraictools.Inparticular,wehaveappliedControlFlowAnalysistotheprocessalgebraicspecifications,thereforegaininginsightsonthestudiedbiologicalsystem,whilepayingalowcom-putationalcost.WehaveshowedthesefeaturesthroughacasestudyrepresentedbytheregulatorynetworkunderlyingThlymphocytesdifferentiations.Inparticular,wehaveinvestigatedtheroleplayedbythegenescomposingthenetworkindeterminingthefinalstateofthesystemunderdifferentexperimentalconditions.Thisexamplehaveshowedhowourtoolkitcanbefruitfullyexploitedtoassessinterestingpropertiesofbiologicalsystems.OurmethodcouldbeparticularlyusefulintheanalysisoflargeGBNmodels(e.g.wholecellmodels).Evenwhenpartialbiologicalknowledgeisavailable,exploitingbothSim-πnandCFAallowsustodesignandstudyrealisticmodelsofbiologicalsystemsi.e.modelswhichareconsistentwiththeobservedbehavioroftheirbiologicalcounterparts.Weareplanningtouseourfr