Modeling Multi-valued Genetic Regulatory Networks

ModelingMulti-ValuedGeneticRegulatoryNetworksUsingHigh-LevelPetriNetsJean-PaulComet1,HannaKlaudel1,andSt´ephaneLiauzu1LaMI,UMRCNRS8042,Universit´ed’Evry-Vald’Essonne,BoulevardFran¸coisMitterrand,91025EvryCedex,France.tel:[phone]-fax:(33)[e-mail]:HLPN,modelingofregulatorynetworks,modelchecking.Abstract.Regulatorynetworksareatthecoreofallbiologicalfunctionsfrombio-chemicalpathwaystogeneregulationandcellcommunicationprocesses.Becauseofthecomplexityoftheinterweavingretroactions,theoverallbehaviorisdifficulttograspandthedevelopmentofformalmethodsisneededinordertoconfrontthesupposedpropertiesofthebiologicalsystemtothemodel.WerevisitherethetremendousworkofR.Thomasandshowthatitsbinaryandalsoitsmulti-valuedapproachcanbeexpressedinaunifiedwaywithhigh-levelPetrinets.Acompactmodelingofgeneticnetworksisproposedinwhichthetokensrepresentgene’sexpressionlevelsandtheirdynamicalbehaviordependsonacertainnumberofbiologicalparameters.Thisallowsustotakeadvantageoftechniquesandtoolsinthefieldofhigh-levelPetrinets.Adevelopedprototypeletsabiologisttoverifysystematicallythecoherenceofthesystemundervarioushypotheses.Thesehypothesesaretranslatedintotemporallogicformulaeandthemodel-checkingtechniquesareusedtoretainonlythemodelswhosebehavioriscoherentwiththebiologicalknowledge.1IntroductionToelucidatetheprinciplesthatgovernbiologicalcomplexity,computermod-elinghastoovercomeadhocexplanationsinordertomakeemergenovelandabstractconcepts[1].Computationalsystembiology[2]triestoestablishmethodsandtechniquesthatenableustounderstandbiologicalsystemsassystems,in-cludingtheirrobustness,designandmanipulation[3,4].Itmeanstounderstand:thestructureofthesystem,suchasgene/metabolic/signaltransductionnet-works,thedynamicsofsuchsystems,methodstocontrol,designandmodifysystemsinordertocopewithdesiredproperties[5].Biologicalregulatorynetworksplacethediscussionatabiologicallevelin-steadofabiochemicalone,thatallowsonetostudybehaviorsmoreabstractly.Theymodelinteractionsbetweenbiologicalentities,oftenmacromoleculesorgenes.Theyarestaticallyrepresentedbyorientedgraphs,whereverticesab-stractthebiologicalentitiesandarcstheirinteractions.Moreover,atagivenstage,eachvertexhasanumericalvaluetodescribethelevelofconcentrationofthecorrespondingentity.Thedynamicscorrespondtotheevolutionsoftheseconcentrationlevelsandcanberepresented,forinstance,usingdifferentialequa-tionsystems.R.Thomasintroducedinthe70’sabooleanapproachforregulatorynetworkstocapturethequalitativenatureofthedynamics.Heproveditsusefulnessinthecontextofimmunityinbacteriophages[6,7].Lateron,hegeneralizedittomulti-valuedlevelsofconcentration,socalled“generalizedlogical”approach.Moreover,theverticesofR.Thomas’regulatorynetworksareabstractedinto“variables”allowingthecohabitationofheterogeneousinformation(e.g.,addingenvironmentalvariablestogeneticones).TheR.Thomasbooleanapproachhasbeenjustifiedasadiscretizationofthecontinuousdifferentialequationsystem[8],thenhasbeenconfrontedtothemoreclassicalanalysisintermsofdifferentialequations[9].Takingintoaccount“sin-gularstates”,ThomasandSnoussishowedthatallsteadystatescanbefoundviathediscreteapproach[10].MorerecentlyThomasandKaufmanhaveshownthatthediscretedescriptionprovidesaqualitativefitofthedifferentialequationswithasmallnumberofpossiblecombinationsofvaluesfortheparameters[11].Adirectorindirectinfluenceofageneonitselfcorrespondstoaclosedorientedpathwhichconstitutesafeedbackcircuit.Feedbackcircuitsarefundamentalbecausetheydecidetheexistenceofsteadystatesofthedynamics:ithasbeenstatedthenproved[12,13,14,15]thatatleastonepositiveregulatorycircuitisnecessarytogeneratemultistationaritywhereasatleastonenegativecircuitisnecessarytoobtainahomeostasisorastableoscillatorybehavior[16].Thesestaticproperties(numberofstationarystates)canbereinforcedbyintroducingsomepropertiesonthedynamicsofthesystemextractedfromthebiologicalknowledgeorhypotheses.Itbecomesnecessarytoconstructmodelswhicharecoherentnotonlywiththepreviousstaticconditionsbutalsowiththedynamicalones.Formalmethodsfromcomputerscienceshouldbeabletohelpmodelertoautomaticallyperformthisverification.In[17,18]themachineryofformalmethodsisusedtorevisitR.Thomas’regulatorynetworks:allpos-siblestategraphsaregeneratedandmodelcheckershelptoselectthosewhichsatisfythetemporalproperties.Allthisapproachisbasedonthesemanticsoftheregulatorygraph,i.e.,itsdynamics,whichhastobecomputedbefore.Thestateexplosionphenomenoninthetransitiongraphlimitsthereadabilityofthesemodelingsandthepossibleextensionslike,forinstance,theintroductionofdelaysfortransitions.TheseobservationsmotivatedourinterestforapplyinginthiscontextthePetrinettheory.InthisarticlewepresentamodelingoftheR.Thomas’regulatorynetworksintermsofhigh-levelPetrinets.Toensuretheadequationbetweenbothfor-malisms,wefirstpresentformallythebiologicalregulatorygraphswhichde-scribetheinteractionsbetweenbiologicalentities,theparameterswhichpilotthebehaviorsofthesystemandtheassociateddynamics(section2).Then,afterabriefintroductiontothehigh-levelPetrinets,amodelingofregulat