Chemical and biological systems have similarities with ITsystems as they can be observed as sequences of events. Most available tools propose simulation frameworks to explore biological pathways (i.e., sequences of events). Simulation only explores a few of the most probable pathways in the system. On the contrary, techniques such as model checking, coming from IT-systems analysis, explore all the possible behaviors of the modeled systems, thus helping to identify interesting pathways. A main drawback from most model checking tools in the life sciences domain is that they take as input a language designed for computer scientists, that is not easily understood by non-expert users. We propose in this article an approach based on Domain Specific Languages. It provides a comprehensible language to describe the system while allowing the use of complex and powerful underlying model checking techniques.
Because of their stochastic and combinatorial nature, many biological systems
such as cellular and supra-cellular interactions are very hard to investigate.
Current practice is mainly limited to the use of in vivo and in vitro experiments.
Investigation through formal models of biological systems is currently a rather
restricted research field, unlike what has been done in other natural sciences
such as chemistry and physics. There is clearly an emerging field of research
where future experiments can be partially performed in silico, i.e., by means
of techniques from computer science. One of the main approaches of biological
modeling is the so-called regulatory networks [
Among the tools available in this domain, the main analysis approach for regulatory networks is simulation. Simulation is generating and analyzing a limited sample of possible system behaviors. This technique is not convenient when the main purpose of the research is to look for rare or abnormal behaviors (e.g., cancer). The main approach in this case is to use model checking instead of simulation. Model checking consists in generating and analyzing the complete set of possible states of the system. Naturally, this technique suffers from the drawback of the enormous number of possible states of biological systems.
It is interesting to note that this problem is well-known to the model checking
community in computer science, where it is called the state space explosion [
In this paper we show a work in progress in our group. We present Gene Regulation Language (GReg), our first attempt to build a framework for modeling and analyzing biological systems based on formal modeling and reasoning. Advanced techniques for defining Domain Specific Languages, giving their semantics and analyzing them using symbolic model checking are presented. First, Section 2 describes precisely the biological domain considered by GReg, then Section 3 outlines the state of the current research in the field and Section 4 describes in detail the creation and usage of Domain Specific Languages. The following two chapters describe GReg itself. Section 5 describes the language designed for expressing biological mechanisms and the corresponding queries, and Section 6 provides a simple example taken from the literature. Finally, Section 7 concludes the article and discusses the future research perspectives in this area. 2
tra nscriptio
n DNA splicing
translation pre-mRNA
mRNA
The purpose of GReg is to describe genetic regulatory mechanisms controlling the DNA to protein process (Figure 1). This process comprises three steps: transcription, splicing and translation. The regulation of each step can be modeled using standard chemical reactions, presented in Section 2.1. For the transcription initiation we use the genetic regulatory mechanism model, presented in Section 2.2. Finally we define a cell network in Section 2.3. We separate these three domain models to clearly distinguish chemical from biological concepts.
We use the same definition of molecule level as presented in [
Chemical compartment model A chemical compartment = hM ; Ri 2 K , is composed of a non-empty set of molecules (? 6= M M olecules) and a set of reactions (R Reactions). Two compartments may be separated by a membrane (i.e., selective barrier), thus allowing molecule transfer between them.
A chemical reaction = hRe; Pr ; Ca; k; type i 2 R, where Re; Pr ; Ca M(M ) K , the reactants (Re), products (Pr ) and catalysts (Ca) are defined as the association of a multiset of one molecule (M(M )) with a given compartment ( 2 K ).
Catalysts (Ca) have the particularity to appear as reactants and products in a chemical reaction. We have chosen to define the catalysts in a distinct set, therefore no catalyst can appear as reactant or product: 8m 2 M ; m 2 Ca =) m 2= Re ^ m 2= Pr .
A reaction may be either irreversible or reversible, type 2 firr; revg. In reversible reactions an equilibrium constant (k) is defined with the ratio of both direction rates. 2.2
Genetic regulatory mechanism model A genetic regulatory mechanism = h ; C i, is composed of a non-empty set of genes ( ). Genes are organized into one or more chromosomes (C ). A genetic regulatory mechanism is contained in a chemical compartment, this specification will be presented in Section 2.3.
A chromosome c = 1; : : : n 2 C is a sequence of loci. A gene may have different version (i.e., alleles) at a given chromosome location (i.e., locus). And a locus = h i defines a non-empty set of genes (? 6= ) that are located at a given locus. Then the set of all possible chromosomes in a mechanism is the Cartesian product of the set of genes at each locus: Chromosomes = 1 n .
A gene = hM ; i 2 is a portion of DNA that codes for at least one molecule (? 6= M M ), and may contain some regulation sites ( Sites).
A regulation site = hM ; type i 2 defines the non-empty set of regulatory molecules (? 6= M M ) associated to the regulation site of a given gene. Note that when using anti-termination sites, genes order matters, therefore chromosomes must be defined.
I1 O1
In On start
A1 T1
An Tn stop promoter region
transcribed region
Our idealized gene structure (Figure 2) is composed of two regions: promoter and transcribed. Note that the exact position in the gene of each regulatory site is not specified, i.e., we are mainly interested in its regulatory role. The type of a regulation site is type 2 fI;O;A;Tg.
Initiation (I) the portion of DNA where bound activators increase the rate of the transcription process. It is located in the promoter region; Operator (O) the portion of DNA where bound repressors block the transcription process. It is located in the promoter region; Anti-termination (A) the portion of DNA where activators continue the transcription process. It is located in the transcribed region. These sites may also allow the transcription of the next gene; Termination (T) (also called attenuator) the portion of DNA where repressors stop the transcription process. It is located in the transcribed region; thus, it produces a reduced RNA. 2.3
Cell network The cell network model is designed to model the interactions of different cells with their environment and also with their inner components (i.e., organelles). This model authorizes the construction of currently not observed cells, e.g., prokaryote with nucleus, eukaryote with multiple nuclei, etc. The validity of the specification is delegated to the user (i.e., domain expert).
This model defines three chemical compartments, therefore they inherit both sets M and R.
Organelle, ! = hM ; R; i is the lowest compartment in the compartment hierarchy. An organelle may contain a mechanism ( ), e.g., nucleus, mitochondrial DNA, etc.
Cell, = hM ; R; ; i contains a possibly empty set of organelles ( ). The model of a prokaryote cell would define a mechanism ( ), by cons an eukaryote cell would define instead an organelle with a mechanism (i.e., nucleus). Network, = hM ; R; i represents the environment and contains one or more cells ( ). 3
In this section we compare three well-known tools with our approach. We first define a few criteria such as the kind of analysis, the supported formalism and the supported exchange format. Table 1 presents a summary of the resulting comparison.
Domain language To be productive, the syntax of the input language should
be as close as possible to the actual domain of the user. This input
language can be textual (like in tools that use Systems Biology Markup
Language (SBML) [
Discrete & continuous Continuous models are closer to the real biological
systems than discrete models, but unlike the latter they are not adapted for
model checking techniques. Discrete formalisms allow a complete exploration
of the state space while preserving the qualitative properties of the system,
as mentioned in [
Exchange format The supported interchange format is an important feature as it allows us to bridge the gap between different tools and therefore enables the user to use the most adapted tool to hand. SBML is a common interchange format based on XML. It is used to describe biochemical reactions, gene regulation and many other topics.
Cell Illustrator [
Gene Interaction Network simulation a.k.a. GinSim [
Cytoscape [
Model checking involves verifying whether a property holds on the whole set of possible states of a given model. To generate this complete state space, the model must be expressed in a formal language intended for this operation, like Petri Nets (PNs). This makes the model checking approach impractical for people who do not master these formal languages. We propose using DSLs for this purpose.
Cell Illustrator 3 3 5 5 3 3
A DSL is a programming or specification language tailored for a given domain; it presents a reduced set of instructions closely related to this domain. Using a DSL has two main objectives. First, learning the language should be easy for someone with enough knowledge about the domain, even if this person does not have previous knowledge of other languages. Second, the number of errors made by a novice user should be drastically reduced as the expressivity of the language is reduced to the minimum.
The DSL semantics are defined by transformation into a target language, which is a formal language where complex operations (like model checking) can be performed. Usually, the scope of the target language is broader than the scope of the DSL. This allows using the same target language and its associated tools for different DSLs. Moreover, while creating a new DSL, it is often possible to use an already-existing language as a target, thus facilitating the language creation process. The results obtained in the target language are translated again into the DSL and returned to the user. This process is described in Figure 3. After the creation of the initial model, all the following steps must be fully automatic, to hide the underlying complexity from the end user.
Manual intervention Automatic processing
Model of the system Domain Specific
Language
T r a n s fr o m a it o n Model of the system
Formal language
Domain expert Computation tool
Counter-example Domain Specific
Language n o it a m fr o s n a r
T Counter-example Formal language Language engineer
Transform.
The person in charge of the DSL creation is a language engineer. This person should obviously have a certain knowledge about the language creation process, but he should also master the target platform language, in order to define efficient and correct transformations. Furthermore, he should be in contact with at least one domain expert, in order to settle the requirements and verify the correctness and completeness of the language created. The creation of a DSL follows a set of specific steps. First, the language engineer must identify the abstract concepts of the domain. These concepts include the basic elements of the domain, the interactions between these elements and the precise boundaries of the domain considered. Based on these concepts, the language engineer must define a set of expressions used to create a specific model in the domain, i.e., a concrete syntax. Finally, the language engineer must define the semantics of the language created, usually by transformation to an existing platform. The whole process must be validated by one or more domain experts. Domain experts must validate the three steps of the DSL creation process: the domain must have been correctly defined, the expressions of the concrete syntax must be close to the already existing languages in the domain, and the execution must return the expected results. This creation/validation process often leads to an iterative development of the language. We show this entire process in Figure 4.
There exist various DSLs tailored for the biological processes, e.g., SBML [
While creating GReg, we used the Eclipse Modeling Project (EMP)[
The modular structure of GReg’s definition would allow us to replace the target domain while keeping exactly the same language. If needed, we could, for example, define a transformation to SBML using a model to text transformation tool like XPand. 5
GReg is a Domain Specific Language designed to describe genetic regulatory
mechanisms. We built it in order to illustrate the DSL approach, and the benefits
it provides to research in the life sciences domain. Throughout this section, we
introduce the GReg language using an excerpt of the lac operon model [
We first show how to describe a regulation mechanism. Listing 1 shows the overall structure of a GReg mechanism specification. The mechanism is named (lac_operon). It specifies the molecules occurring in the mechanism, and the chemical reactions between these molecules. The GReg description also specifies the genes with their properties and organization into chromosomes. mechanism lac_operon i s molecules
d e c l a r a t i o n o f m o l e c u l e s reactions
d e c l a r a t i o n o f c h e m i c a l r e a c t i o n s chromosomes
d e c l a r a t i o n o f chromosomes gene d e c l a r a t i o n o f a g e n e
d e c l a r a t i o n o f o t h e r g e n e s end lac_operon
Listing 1: GReg mechanism specification
The molecules section of a GReg mechanism lac_operon i s description specifies the molecules oc- molecules curring in the mechanism. For in- lactose , allolactose , stance, in Listing 2, the lac_operon lacI , lacZ , lacY , lacA , mechanism uses molecules lactose, cAMP , CAP allolactose, lacI, lacZ, etc. ...
Molecules are only described by end lac_operon their names, as it is the only infor- Listing 2: Molecules declaration mation relevant in our language. The DSL approach emphasizes specification of only the required information for the particular domain. No molecules other than the ones described here can be used in the mechanism. This constraint is useful for the user creating a GReg specification: spelling errors in molecule names are detected, see Figure 5.
After the molecules declaration, a GReg description specifies the chemical reactions that take part in the mechanism. Listing 3 presents the reactions part of the mechanism.
mechanism l a c _ o p e r o n i s ... r e a c t i o n s in du ct io n : lacI + a l l o l a c t o s e ! _ allo : lactose ! a l l o l a c t o s e cat lacZ ... end l a c _ o p e r o n
In GReg, each reaction has a name, for instance induction. As usual in chemical notations, a reaction is a relation among (weighted) molecules. The molecule weight is usually called the stoichiometric coefficient. By default, stoichiometric coefficients are valued 1.
A reaction can be either irreversible ( ! ) or reversible ( $ ). In our example, the reaction induction is a degradation of lacI and allolactose. A degradation is an irreversible reaction where products are not interesting, thus the reactants are simply removed from the system.
If needed, each direction of the reaction can be given a reaction rate (i.e., probability). Each reaction can also have catalysts specified using the keyword cat. For instance allo is a reaction catalyzed by lacZ.
Listing 4 presents the genes specification. For instance, rep is a minimal gene (i.e., not regulated). A minimal gene defines at least the molecules it codes. If they are relevant, regulation sites are also specified in a section with the sites keyword. The lac gene defines a regulated gene with two regulation sites I and O , together with the molecule acting on them. Note that GReg also allows us to define several regulation sites for I, O, A, T. mechanism l a c _ o p e r o n i s ... gene rep
codes lacI end rep gene lac codes lacZ , lacY , lacA s i t e s
I : cAMP and CAP = 1
O : lacI @ 2 end lac end l a c _ o p e r o n
As molecules may be present at different levels, the @ keyword allows the specification of the required molecules levels acting at a regulation site. By default, molecule levels are valued 1. As several molecules can act on one regulation site, GReg allows to combine molecules with Boolean operators for a regulation site. There are two operators defined : and and or. For instance the I site of lac gene specifies that cAMP and CAP are required to activate this site. The = keyword allows to specify the target level attributed to the gene once this site is active.
Note that for A sites, it is also possible to specify the next gene target level. As the role of a T site is to interrupt the transcription process, we allow the specification of the reduced set of produced molecules when these sites are active.
The chromosomes section is used to specify one or more chromosomes.
A chromosome defines the sequence of loci. A locus is defined between two braces. Note that genes’order in each locus does not matter. This section is mandatory when taking into account A sites. mechanism la c_ ope ro n i s ... chromosomes
c : { rep } , { lac , lac ’} ... end la c_ ope ro n
Listing 6 shows an example of GQL specification. The use keyword imports the lac_operon mechanism from another file, allowing us to reference the molecules declared in lac_operon mechanism from a query specification. A GQL file specifies the levels and the queries.
The levels section is used to de- use " la c_o pe ro n . greg " fine the combination of levels. A com- l e v e l s bination of levels is a partial or to- l1 : lacZ = 1 tal definition of molecule levels, while l2 : lacZ = 0 , lacI = 2 unspecified molecules may match any queries possible value. For instance l1 speci- bool a : e x i s t s l1 fies only the level of lacZ among all ppaatthhss bc :: ppaatthhss ll11 , ..l2 l2 molecules defined in lac_operon. The exists query returns true if predefined Listing 6: GQL queries specification level exists. The paths query is used to retrieve all paths from the state space matching the sequence of predefined levels. The query b returns the path where l2 is a direct successor of l1. But query c does not require that l2 is a direct successor of l1.
Listing 7 shows an example of use " la c_o pe ro n . greg " a GReg configuration specification use " la c_o pe ro n . gql " given outside the mechanism, usually i n i t i a l l y la c_ ope ro n has in a separate file. This allows to eas- lactose = 1 ily repeat experiments for the same lacI = 1 mechanism with several initial quan- execute tities. The first section starts with i f a then ( b and c ) the initially keyword and defines the Listing 7: GReg specification genes or molecules initial levels. The second section starts with the execute keyword and is used to specify which queries will be executed by the model checker. 6
We present a simple example of a genetic regulatory mechanism taken from [
X
Y Z mechanism example i s molecules x , y , z gene X codes x
s i t e s O : z end X gene Y codes y
s i t e s I : x end Y gene Z codes z
s i t e s O : y end Z end example
From theses models AlPiNA is able to compute the state space and to identify all deadlock without requiring any additional input from the user.
A deadlock is a situation where no more events can occur in the system. Strictly speaking, in real biological systems there are no deadlocks but livelocks, a situation where events still occur but without changing the state of the system. The states where such situations occur are usually called stable states or attractors.
But we can also search for specific properties of the biological system. As previously mentioned, the state space might contain too many states to be used as it is. Therefore we propose a way to extract portions of state space (e.g., subsets Xpre
Xabs X 0 x Xact Xrep Xact
Yrep Zpre Xabs
Yact Zact Zrep Zact of states, paths, cycles, ...) through GQL queries. In Listing 9, we have defined one level (l1) and one query (at).
s1 : e x i s t s ( $x in x , $y in y , $z in z : (( $x equals suc ( zero )) and ( $y equals suc ( zero ))) = false
Listing 10: AlPiNA property expression of query in Listing 9
The example in Figure 6 and Listing 8 has eight states reachable from the initial marking, where all molecules are initially at level zero (x,y,z) = (0,0,0), see Figure 9. Model checking of the example PN finds two stable states: (1,1,0) and (0,0,1) and returns for s1 the two states: (1,1,0) and (1,1,1). x = 1 y = 1 z = 0 x = 1 y = 1 z = 1
Xact Xrep x = 0 y = 1 z = 0 Zrep x = 0 y = 1 z = 1
Legend
Yrep Yact Yact Yrep
Fig. 9: State space of example in Figure 6 and Listing 8 7
This paper introduces Gene Regulation Language (GReg), a language dedicated to the modeling of regulatory mechanisms. We explain the need to explore completely the sets of possible behaviors of a given model in order to detect rare events. GReg includes a query language used to express the properties of such events.
From a technical point of view, we explain that the techniques proposed are based on general principles borrowed from software modeling and verification. These techniques include the use of a dedicated DSL defined with a metamodeling approach and the translation of this language into a formal verification platform called AlPiNA.
The languages and transformations shown in this article have been implemented and tested on several toy examples. We also asked biologists to assess the expressivity and usability of the language. Although the first feedback seems promising, there is much room for improvement. We foresee three main axes of future development: improving the expressivity of the modeling and query languages, assessing the usability of the approach and exploring the mitigation of the state space explosion.
Extending the expressivity of GReg Concepts such as time and probabilities play an important role in biology and are therefore good candidates for a language extension. As the current underlying formalism, APNs, does not support these notions, such extension would require changing the target platform. Good examples of target formalisms are timed Petri nets and stochastic Petri nets. As mentioned in 4, the techniques used to create GReg allow changing the target language without changing the language itself. Note that we do not plan to add continuous concepts, used in languages such as HFPNe.
Improving the usability of our tool Textual domain specific languages constitute a first step towards democratization of formal methods. Although highly efficient, textual languages are usually not as intuitive as graphical languages. On the other hand, graphical domain specific languages are especially good in the early phase of the modeling as well as for documentation, but they are often less practical when the model grows. The tools in EMP that were used to create GReg allow us to define a graphical version of the same language, thus keeping the best of both worlds.
Another way to ease the modeling phase is to allow import/export of models from/to other formalisms and standards such as SBML and to integrate it with Cytoscape through its plug-in mechanism.
Mitigating the state space explosion So far, we have done little
experimentation in this area for biological processes. Nevertheless, we conducted several
studies on usual IT protocols and software models that show that AlPiNA
can handle huge state spaces[
The development of GReg is a work in progress, we would like to set up more collaborations with biologists interested in exploiting formal techniques from computer science to discover rare events. We think that we can make, in the near future, a useful contribution to life sciences based on advanced techniques borrowed from computer science.