SMBioNet user manual
Contents
1. 00 10 gt 20 to For instance at state 10 one can see that both variables are less than their target levels which are 2 and 1 respectively So we have two transitions a transition from 10 to 20 that allows the variable a to increase and a transition from 10 to 11 that allows the variable b to increase Note that at state 00 both variables are equals to their respective target levels 00 is a stable state of the network and by convention there exists a unique transition starting from 00 which goes to 0 0 itself 4 Summary The evolution of the network is driven by logical parameters and each monotonous parameterizations describes a possible dynamics for the network under the form of an asynchronous state transition graph 1 2 Constraints on parameters section PARA By default a logical parameter associated with a given variable takes a value in the domain of this variable The optional section PARA gives restrictions on the size of the intervals in which logical parameters take values For instance with PARA K_at P 1 2 Kb 0 K_b P 1 we say that the parameter K_a P take a value inside 1 2 instead of 0 1 2 and that the values of the parameters K_b and K_b P are 0 and 1 respectively 1 3 CTL formula section CTL The last section of the input file is the section CTL which contains a CTL formula This formula expresses a dynamical property that will be tested on all the asynchronous state trans2. a whose domain is 0 1 2 and a vari able b which is a Boolean variable The section REG describes the regulatory processes of the network A regulatory process consists in 1 a proposi tional formula constructed from simple propositions of the form a gt 1 or b lt a and connected with the logical operators amp and or and gt implication and 2 a set of target variables For instance by writing REG P a gt 0 amp b lt 1 J gt ab Q a 2 gt a we specify that the network has two regulatory precesses P and Q The for mula of Pis a gt 0 amp b lt 1 and its targets are a and b The formula of Q is a 1 and its unique target is a A discrete regulatory network can be seen as a labeled bipartite graph in which vertices are either variables or regulatory processes the predecessors of a process are the variables involves in its formula and its successors are its target variables a P a gt 0 amp b lt i a Ql a 2 In the following we say that a process is a process of a given variable if this variable is a target of the process the processes of a are P and Q and P is the unique process of b a 1 1 2 Semantic The semantic of a discrete regulatory network is given by the set of dynamics that the network can display To define these possible dynamics we need additional notions the first one being the notion of a state A state is the assignment of a value to each vari
3. of cell differen tiation and memory II Chaos 11 170 195 2001 2 G Bernot J P Comet A Richard and J Guespin Application of for mal methods to biological regulatory networks extending Thomas asyn chronous logical approach with temporal logic Journal of Theoretical Biology 229 3 339 347 2004 3 Z Khalis J P Comet A Richard and G Bernot The SMBioNet method for discovering models of gene regulatory networks Genes Genomes and Genomics 3 1 15 22 2009 4 M Huth and M Ryan Logic in Computer Science Modelling and rea soning about systems Cambridge University Press 2000 5 http nusmv irst itc it 10
4. toward which the variable evolves is great In that sense the presence of a process favors the increase of its targets For the running example the monotonicity conditions are K_a lt K_at P K_b lt K_b P K_a lt K_a Q K_a P lt K_at P Q K_a Q lt K_a P Q A parameterization is the assignment of a value to each logical parameter A parameterization satisfying the monotonicity conditions is a monotonous parameterization The following parameterization is a monotonous parame terization K_a 0 K_b 0 K a P 2 K b P 1 K a Q 1 K a P Q 2 From this parameterization and the previous table we obtain b Target of a Target of b 0 0 ONrFrF OOW omom mo HH NONO OM O FR This table gives the target level of each variable at each state This informa tion is sufficient to explicitly describe a possible dynamics for the network under the form of a state transition graph As in the multivalued logical formalism of Thomas this state transition graph is constructed by assuming that variables evolve asynchronously and by unit During a transition there is a unique variable that evolves and it evolves by unit 1 1 in the direction of its target level In addition for each variable that is not equal to its target level there exists a transition allowing this variable to evolve For the running example this updating rule leads to the following asyn chronous state transition graph 01 lt _1i11 lt 21 VM dA
5. 1 O ol Ho CTL a gt 0 gt EG a gt 0 amp a 0 gt AG a 0 the output file named input file out by default is the following VAR oO O e N we REG P a gt 0 amp b lt 1 gt ab Q a 2 gt a PARA Parameters for a 1 Ore N Parameters for b K_b 0 K b P F CTL a gt 0 gt EG a gt 0 amp a 0 gt AG a 0 MODEL 1 K_a 0 K_at P K_atQ K a P Q lor K_b 0 K_b P me MODEL 2 HH T w D Il I O e MODEL 3 K_a 0 K_at P K_atQ K a P Q I O N a AAR V w vo Onn I N MODEL 5 K_a 0 K a P K a Q K a P Q HH I NN lo W il K_b K b SELECTED MODELS CHECKED MODELS 5 10 126ms The output file begins with a summary of the specifications following the syntax of the input file actually the output file can be taken as input file Then it gives in comment all the monotonous parameterizations that are consistent with the specifications To be more precise first note that several parameterizations can lead to the same asynchronous state graph These parameterizations are then equivalent from a dynamical point of view SMBioNet proceeds as follows it enumer ates all the classes containing a monotonous parameterization satisfying the constraints of the section PARA Then for each class the corresponding asyn chronous state graph is
6. SMBioNet user manual Laboratoire I3S CNRS amp Universit de Nice March 2010 SMBioNet is a tool for modeling biological regulatory systems It is based on an extension of the multivalued logical formalism of Ren Thomas 1 2 3 and the Computational Tree Logic CTL 4 Input A discrete regulatory network with partially specified logical pa rameters and a CTL formula that expresses the biological observations or hypothesis on the behaviors of the system to model Output All the parameterizations of the network that lead to a dynamical model satisfying the given CTL formula The verification step is performed with the NuSMV symbolic model checker 5 1 Input file The input file is divided in four sections The first two sections VAR and REG describe what we call a discrete regulatory network In the third section PARA some constraints on the logical parameters associated to the network are given The last section CTL contains a CTL formula 1 1 Discrete regulatory network sections VAR and REG 1 1 1 Syntax The input file starts by describing a discrete regulatory network Such a network consists in a set of discrete variables which interact each other via regulatory processes The section VAR describes variables and their domains These domains are always finite intervals of integers For instance with VAR a 02 b 01 selection of Models of Biological Networks we declare two variables a variable
7. able of the network For the network described in the previous section there are six possible states w o vyer oo H OhHO HO At a given state we say that a process is present 1 when its formula is true and absent 0 when its formula is false P Q o o0 w o Ner OO FoOorOrF FOr Fr CO OO 2 0 From a dynamic point of view at a given state each variable evolves in the direction of a target value that only depends on the set of processes of the variable that are present This target value is given by a so called logical parameter For the running example the logical parameters are K_a K_b K a P K b P K a Q K a P Q For instance the logical parameter K a P gives the value toward which the variable a evolves when P is present and Q absent and K a gives the value toward which the variable a evolves when the regulatory processes P and Q are absent The target value of each variable at each state is thus given by the following table a b Target of a Target of b O O K_a K_b O 1 Ka K_b 1 0 K_a P K b P 1 1 Ka Kb 2 0O K a P Q K b P 2 1 K a Q Kb Logical parameters satisfy monotonicity conditions if the set of processes associated to a given parameter is included in the set of processes associated to another parameter then the value of the former parameter is at most the value of the latter In other words the more the processes of a given variable are present the more the target value
8. ition graphs resulting from a monotonous parameterizations of the network and satisfying the constraints of the section PARA For instance with CTL a gt 0 gt EG a gt 0 amp a 0 gt AG a 0 the considered property is if a gt 0 then there exists an evolution of the net work for which a gt 0 is always true and if a 0 then for all the possible evo lutions a 0 is always true Note that this property is satisfied by the asyn chronous state graph given as example in section 1 1 2 The syntax of CTL formula is the following id variable_name integer atom id lt id id gt id id lt id id gt id id wou id ctl atom win Gt Logical NOT ctl amp ctl Logical AND ctl ctl Logical OR ctl gt ctl Logical implication EX ctl Exists neXt state AX ctl For All neXt state EF ctl Exists Finally AF ctl For All Finally EG ctl Exists Globally AG ctl For All Globally E ctl U ctl Exists Until A ctl U ctl For All Until Define the semantic consists in defining the satisfactory relation between a state graph and a CTL formula We say that the state graph satisfies a formula when every state of the graph satisfies the formula the satisfactory relation between a state and a formula being defined as follows First if the formula is simply a propositional formula that is does not contain temporal operators such as EX or AG
9. symbolically described using the NuSMV language and confronted to the CTL formula with the NuSMV symbolic model checker If the state graph satisfies the formula then the corresponding class is given as output For the running example 10 classes or MODELS have been enumerated and 5 classes have been selected For instance MODEL 3 corresponds to a class containing two parameterizations K_a 0 K_a 0 K_a P 2 K_a P 2 K_at Q 1 K_atQ 0 K a P Q 2 and K_a P Q 2 K_b 0 K_b 0 K_b P 1 K_b P 1 The left parameterization is the one given in example in Section 1 and both parameterizations lead to the asynchronous state graph given in Section 1 3 Options The syntax of the smbionet command is the following smbionet v int comp dynamic o output file input file The option v int increases the quantity of information on the network given in the output the more int is great the more the quantity of information is great The option comp stops the execution of SMBioNet after the reading ofthe input file This can be useful for instance to display the logical pa rameters associated with the network The option dynamic allows NuSMV to perform a dynamic reordering of variables This often increases significantly the speed of the verification when the number of variables is large Finally the option o output file gives the name output file to the output file References 1 R Thomas and M Kaufman Multistationarity the basis
10. then the satisfactory relation is usual Second a state s satisfies a formula of the form EX ctl if there exists a transition starting from s that leads to a state satisfying the formula ctl AF ctl if every transition starting from s leads to a state satisfying the formula ctl EF ctl if there exists a path starting from s that leads to a state satisfying the formula ctl AF ctl if every path starting from s leads to a state satisfying the formula ctl EG ctl if there exists an infinite path starting from s that contains only states satisfying the formula ctl AG ctl if every infinite path starting from s contains only states satis fying the formula ctl E ctl U ctl if there exists a path starting from s that contains a state s satisfying the formula ctl and such that every state before s in the path satisfies the formula ctl A ctl U ctl if every path starting from s contains a state s satis fying the formula ct1 and such that every state before s in the path satisfies the formula ct 2 Output file The output file is obtained with the command smbionet input_file It contains all the monotonous parameterizations of the network satisfying the constraints of section PARA and leading to an asynchronous state transition graph satisfying the given CTL formula For instance with the input file o ll SO O e N we REG P a gt 0 amp b lt i gt ab Q a 2 gt a PARA K_at P K_b K b P
Download Pdf Manuals
Related Search