{'fraction_non_alphanumeric': 0.040343836108781596, 'fraction_numerical': 0.015334850844614832, 'mean_word_length': 4.056640920793579, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 15, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
An Abstraction Theory for Qualitative Models of Biological Systems

Multi-valued network models are an important qualitative modelling approach used widely by the biological community. In this paper we consider developing an abstraction theory for multi-valued network models that allows the state space of a model to be reduced while preserving key properties of the model. This is important as it aids the analysis and comparison of multi-valued networks and in particular, helps address the well-known problem of state space explosion associated with such analysis. We also consider developing techniques for efficiently identifying abstractions and so provide a basis for the automation of this task. We illustrate the theory and techniques developed by investigating the identification of abstractions for two published MVN models of the lysis-lysogeny switch in the bacteriophage lambda.


Introduction
In order to understand and analyse the complex control mechanisms inherent in biological systems a range of formal modelling techniques have been applied by biologists (for an overview see for example [4,7]). In particular, qualitative modelling techniques have emerged as an important modelling approach due to the lack of quantitative data on reaction rates and the noise associated with such data. Multi-valued networks (MVNs) [15,18,19] are a promising qualitative modelling approach for biological systems. They extend the well-known Boolean network approach [1,4] by allowing the state of each regulatory entity to be within a range of discrete values instead of just on/off. In this way they are able to provide a compromise between the simplicity of Boolean networks and the more detailed differential equational models.
However, the analysis of MVNs is not without problems. They suffer from the well-known state space explosion problem, a problem which is exacerbated in MVNs by the possibly large set of states associated with each individual entity. Another important shortcoming is the lack of any techniques for relating MVN models at different levels of abstraction. This hinders the comparison of MVN models and means there is no basis for the incremental development of MVNs.
In this paper we begin to address these problems by developing an abstraction theory for MVNs. Abstraction techniques are a well established approach in the area of formal verification (see for example [6,3]) which allow a simpler model to be identified which can then be used to provide insight into the more complex original model. The abstraction theory we present is based on using an abstraction mapping to relate the reduced state space of an abstraction to the original MVN model. We develop a notion of what it means for one MVN to correctly abstract another and investigate the scope and limits of the analysis properties that can be inferred from an abstraction model. We show that abstractions allow sound analysis inferences about reachability properties in the sense that any reachability result shown on the abstraction must hold on the original model. Importantly, we show that all attractors of an abstraction correspond to attractors in the original model. We illustrate the theory and techniques developed by investigating the existence of abstractions for two published MVN models for the genetic regulatory network controlling the lysis-lysogeny switch in the bacteriophage λ [17,5]. Bacteriophage λ [18,14] is a virus which after infecting the bacteria Escherichia coli makes a decision to switch to one of two possible reproductive phases. It can enter the lytic cycle where the virus generates as many new viral particles as the infected cell's resources allow and then lyse the cell wall to release the new phage. Alternatively, it can enter the lysogenic cycle where the λ DNA integrates into the host DNA providing it with immunity from other phages and allowing it to be replicated with each cell division. We consider a two and four entity MVN model [17] of the lysis-lysogeny switching mechanism and using the techniques we have developed identify corresponding abstractions for these models.
This paper is organized as follows. In Section 2 we provide a brief overview of the MVN modelling approach and present a simple illustrative example. In Section 3 we develop an abstraction theory for multi-valued networks and present a range of results concerning this theory. In Section 4 we consider the identification of abstractions and develop a basis for automating the abstraction process. In Section 5 we illustrate the theory and techniques developed by presenting two abstraction examples for published models of the lysis-lysogeny switch in bacteriophage λ . Finally, in Section 6 we present some concluding remarks and consider directions for future work.

Multi-valued Network Models
In this section, we introduce multi-valued networks (MVNs) [15,18,19], a qualitative modelling approach which extends the well-known Boolean network [1] approach by allowing the state of each regulatory entity to be within a range of discrete values. MVNs have been extensively studied in circuit design (for example, see [15,12]) and successfully applied to modelling biological systems (for example, see [19,5,16]).
An MVN consists of a set of logically linked entities G = {g 1 , . . . , g k } which regulate each other in a positive or negative way. Each entity g i in an MVN has an associated set of discrete states Y (g i ) = {0, . . . , m i }, for some m i ≥ 1, from which its current state is taken. Note that a Boolean network is therefore simply an MVN in which each entity g i has a Boolean set of states Y (g i ) = {0, 1}. Each entity g i also has a neighbourhood N(g i ) = {g i 1 , . . . , g i l(i) } which is the set of all entities that can directly affect its state. (Note that g i may or may not be a member of N(g i ).) Furthermore, interactions between one entity and another only become functional if the state of the source entity has reached some threshold state level (this threshold state level is always at least one). MVNs can therefore discriminate between the strengths of different interactions, something which Boolean networks are unable to capture. The behaviour of each entity g i based on these neighbourhood interactions is formally defined by a logical next-state function f g i which calculates the next-state of g i given the current states of the entities in its neighbourhood.
We can now define an MVN more formally as follows.
is a tuple of state sets, where each Y (g i ) = {0, . . . , m i }, for some m i ≥ 1, is the state space for entity g i ; iii) N = (N(g 1 ), . . . , N(g k )) is a tuple of neighbourhoods, such that N(g i ) ⊆ G is the neighbourhood of g i ; and iv) F = ( f g 1 , . . . , f g k ) is a tuple of next-state multi-valued functions, such that if N(g i ) = {g i 1 , . . . , g i n } then the function f g i : Y (g i 1 ) × · · · ×Y (g i n ) → Y (g i ) defines the next state of g i . P In the sequel, let MV = (G,Y, N, F) be an arbitrary MVN. In a slight abuse of notation we let g i ∈ MV represent that g i ∈ G is an entity in MV.
As an example, consider the MVN Ex1 defined in Figure 1 which consists of two entities g 1 and g 2 , such that Y (g 1 ) = {0, 1} and Y (g 2 ) = {0, 1, 2}. The update functions for each entity are defined using state transition tables (see Figure 1.(b)) where [g i ] is used to denote the next state of an entity g i . It can be seen that entity g 1 inhibits g 2 and that entity g 2 inhibits g 1 but only when it reaches state 2 (this is represented in Figure 1.(a) by labelling the corresponding edge with a 2). Note that although g 2 ∈ N(g 2 ) we have not drawn an edge for this in Figure 1.(a) since g 2 has no regulatory affect on itself and is needed simply to allow the affect of g 1 to be precisely defined.  A global state of an MVN MV with k entities is represented by a tuple of states (s 1 , . . . , s k ), where s i ∈ Y (g i ) represents the state of entity g i ∈ MV. Note as a notational convenience we often use s 1 . . . s k to represent a global state (s 1 , . . . , s k ). When the current state of an MVN is clear from the context we allow g i to denote both the name of an entity and its corresponding current state. The state space of an MVN MV, denoted S MV , is therefore the set of all possible global states S MV = Y (g 1 ) × · · · ×Y (g k ). The state of an MVN can be updated either synchronously, where the state of all entities is updated simultaneously in a single update step, or asynchronously, where entities update their state independently (see [9]). In the following we focus on the synchronous update semantics since this has received considerable attention from the biological community. Given two states S 1 , S 2 ∈ S MV , let S 1 → S 2 represent a synchronous update step such that S 2 is the state that results from simultaneously updating the state of each entity g i using its associated update function f g i and the appropriate neighbourhood of states from S 1 .
As an example, consider the global state 01 for Ex1 (see Figure 1) in which g 1 has state 0 and g 2 has state 1. Then 01 → 12 is a single synchronous update step on this state resulting in the new state 12. The sequence of global states through S MV from some initial state is called a trace. Note that in the case of a synchronous update semantics such traces are infinite. However, given that the global state space is finite, this implies that a trace must eventually enter a cycle, known formally as an attractor cycle [11,19]. We make use of this fact to define a finite canonical representation for traces which specifies a trace up to the first repeated state.

Definition 2.
Let S 0 ∈ S MV be a global state for MV. A trace is a list of global states σ (S 0 ) = S 0 , S 1 , . . . , S n such that: i) S i → S i+1 , for 0 ≤ i < n; ii) S 0 , . . . , S n−1 are unique states; and iii) S n = S i for some i ∈ {0, . . . , n − 1}. P The set of all traces Tr(MV) = {σ (S) | S ∈ S MV } therefore completely characterizes the behaviour of an MVN model under the synchronous semantics and is referred to as the trace semantics of MV.
Given a trace σ = S 1 , . . . , S n ∈ Tr(MV) for an MVN MV we let att(σ ) denote the attractor cycle that must occur in trace σ , i.e. att(σ ) = S k , S k+1 , . . . , S n , for some 1 ≤ k < n and S k = S n . We let ATT(MV) denote the set of all attractors for MV, i.e.
Attractor cycles are very important biologically where they are seen as representing different biological states or functions (e.g. different cellular types such as proliferation, apoptosis and differentiation [10]). Thus, the identification and analysis of attractor cycles for MVNs is an important subject which has warranted much attention in the literature (for example, see [11,19,8]).

An Abstraction Theory for MVNs
In this section we develop a notion of abstraction for MVNs by considering what it means for one MVN to abstractly implement the behaviour of another. This is based around the idea of showing that the trace semantics of one MVN is consistent with the trace semantics of a more complex MVN under an appropriate mapping of states.
We begin by defining how an entity's state space can be simplified using a mapping to merge states.

Definition 3.
Let MV be an MVN and let g i ∈ MV be an entity such that Y (g i ) = {0, . . . , m} for some m > 1. Then a state mapping φ (g i ) for entity g i is a surjective mapping φ The idea is that a state mapping reduces the set of states an entity can be in by merging appropriate states. The state mapping must be surjective to ensure that all states in the new reduced state space are used. Note we only consider state mappings with a codomain larger than one, since a singular state entity does not appear to be of biological interest.
As an example, consider entity g 2 ∈ Ex1 (see Figure 1) which has the state space Y (g 2 ) = {0, 1, 2}. It is only meaningful to simplify g 2 ∈ Ex1 to a Boolean entity and so one possible state mapping to achieve this would be: which merges states 0 and 1 into a single state 0, and translates state 2 into 1.
Clearly, there are a number of different possible state mappings which can be applied to reduce a node's state space from m to n states, for 1 < n < m. The complete set of all such state mappings is . . , n − 1} and φ is sur jective}. For example, the mapping set MS (3,2) consists of the following six mappings: In order to be able to consider simplifying several entities at the same time during the abstraction process we introduce the notion of a family of state mappings as follows.
is either a state mapping for entity g i or is the identity mapping Furthermore, for φ to be well-defined we insist that at least one of the mappings φ (g i ) is a state mapping. P Note in the sequel given a state mapping φ (g i ) we let it denote both itself and the corresponding abstraction mapping containing only the single state mapping φ (g i ).
An abstraction mapping can be lifted and applied to the trace semantics of an MVN as follows.
Note that φ (g 2 )(Tr(Ex1)) is non-deterministic in the sense that we have two different traces beginning with the same state 00 (i.e. starting in state 00 we have a non-deterministic choice between two abstracted traces, 00, 10, 10 and 00, 11, 00 ). This occurs as we are viewing the more complex set of behaviours captured by Tr(Ex1) from a simpler perspective.
However, it can be observed that this is not a valid trace according to Definition 5 because global state 00 can lead to two different states and will therefore be omitted from the abstracted trace semantics.
We are now ready to define what it means for one MVN to be an abstraction of another.
be two MVNs with the same structure, i.e. G 1 = G 2 and N 1 (g i ) = N 2 (g i ), for all g i ∈ MV 1 . Let φ be an abstraction mapping from MV 2 to MV 1 . Then we say that MV 1 abstracts MV 2 under φ , denoted MV 1 ¡ φ MV 2 , if, and only if, . P An abstraction MV 1 ¡ φ MV 2 indicates that the model MV 1 consistently abstracts the behaviour of a more complex model MV 2 by reducing the state space of those entities identified in the abstraction mapping φ . Note alternatively, we could consider MV 2 to be a refinement of MV 1 in the sense that MV 2 consistently extends MV 1 with the addition of further states. Such a notion of refinement is useful as it provides a framework for the incremental development of MVN models.
As an abstraction example, consider the MVN Ex2 defined in Figure 4 which has the same structure as Ex1 (see Figure 1) but is a Boolean model. Then clearly, given the abstraction mapping φ (g 2 ) intro- duced earlier, we can see that Tr(Ex2) ⊆ φ (g 2 )(Tr(Ex1)) holds and so Ex2 is an abstraction of Ex1, i.e. Ex2 ¡ φ (g 2 ) Ex1 holds.
In special cases, an abstraction may exactly capture the behaviour of the original MVN model under the given abstraction mapping. We distinguish this stronger case with the notion of an exact abstraction. Definition 7. Let MV 1 and MV 2 be two MVNs such that MV 1 ¡ φ MV 2 for some abstraction mapping φ . Then we say that MV 1 exactly abstracts MV 2 under φ , denoted MV 1 = φ MV 2 , if, and only if, Tr(MV 1 ) = φ (Tr(MV 2 )) and for every σ ∈ Tr(MV 2 ), the abstracted trace φ (σ ) is valid. P Exact abstractions are interesting as they indicate redundant states (normally corresponding to entity thresholds) which have no affect on the qualitative behaviour of an MVN. Subsequently, an exact abstraction provides a simpler representation of an MVN whilst preserving all its behaviour under the given abstraction mapping.
It is natural to consider whether every (non-Boolean) 1 MVN has an abstraction. In other words, do there exist MVNs which contain regulatory interactions which are too subtle to be represented in a simpler state domain. This is an interesting question since it provides insight into the need for non-Boolean MVN models. Unsurprisingly, it turns out that abstractions do not always exist, as formalized in the following theorem.

Theorem 8. Not every non-Boolean MVN has an abstraction.
Proof. We simply construct a non-Boolean MVN which we show has no abstractions. Let Ex3 be defined by extending Ex1 (Figure 1) with a third Boolean entity g 3 which is inhibited whenever g 2 is in a state greater than or equal to 1. The complete definition for Ex3 is given in Figure 5. We can see that g 2 ∈ Ex3 now acts in two subtly different ways: on one hand g 1 is inhibited when g 2 = 2; and on the other hand, g 3 is inhibited when g 2 ≥ 1. We can show that no abstraction exists for this model by exhaustively considering each possible abstraction mapping φ (g 2 ) and showing that for every possible candidate abstraction model MV A we have Tr(MV A ) ⊆ φ (g 2 )(Tr(Ex3)). P This is an important result which, although centered around the relationship assumption formalized by our abstraction theory, provides insight into the expressive power of MVNs and in particular, motivates the need for multi-valued modelling techniques.
One of the main motivations for defining an abstraction theory is to allow simplified models of an MVN to be identified to aid the analysis process. This therefore raises the question of what properties of an abstraction are preserved by the original MVN and we end this section by considering this question.
We begin by introducing a notion of corresponding states and traces.

Definition 9.
Let MV be an MVN with an abstraction MV A under a given abstraction mapping φ , i.e. MV A ¡ φ MV. Let S A ∈ S MV A be some global state of abstraction MV A and S ∈ S MV be a global state of the original model MV. Then we say that S A and S correspond with respect to φ , denoted S A ¡ φ S, if, and only if, S A = φ (S). Furthermore, given traces σ A ∈ Tr(MV A ) and σ ∈ Tr(MV) we say σ A and σ correspond with respect to φ , denoted σ A ¡ φ σ , if, and only if, φ (σ ) is valid and σ A = φ (σ ). P Let S 1 * → S 2 denote the fact that global state S 2 ∈ S MV is reachable from global state S 1 ∈ S MV in the model MV. We now clarify the relationship between reachability properties in an abstraction and its corresponding original MVN model.
From Definition 6, we know that Tr(MV A ) ⊆ φ (Tr(MV)) must hold. Therefore there must exist a state S 1 ∈ S MV such that . From this it is straightforward to see that there must exist the required state S 2 in trace σ (S 1 ) such that S A 2 ¡ φ S 2 and S 1 * → S 2 . P In other words, reachability properties of abstractions have corresponding reachability properties in the original MVN. However, since abstractions normally capture less behaviour than the original model, there are limitation on what can be deduced from an abstraction. It turns out that determining reachability in a model using an abstraction is a semi-decidable property: (i) By Theorem 10 we know that if one state is reachable from another in an abstraction then a corresponding reachability property must hold in the original model; (ii) However, if one state is not reachable from another in an abstraction then a corresponding reachability property in the original MVN may or may not hold and more analysis will be required.
The final result we present is important as it shows that the attractor cycles found in an abstraction are preserved by the original MVN. Theorem 11. Let MV A ¡ φ MV for some abstraction mapping φ . Then

Identifying Model Abstractions
In the previous section we defined a formal notion of what it means for one MVN to be a correct abstraction of another. Given an MVN MV and an abstraction mapping φ we can therefore define the set AS(MV, φ ) of all abstractions of MV under φ , i.e.

AS(MV, φ ) = {MV
Finding abstractions, i.e. members of AS(MV, φ ), is clearly an important task given that they provide a means of simplifying the analysis of a model and can help address the well-known problem of state space explosion. However, in practice, the brute force derivation of this refinement set becomes intractable for all but the smallest MVN. Specifically, if we have k entities each with n states, then we have a worst case upper bound of (n n k ) k possible candidate models to consider for any abstraction mapping. For instance, there are (2 2 3 ) 3 = 16777216 possible Boolean networks consisting of just three entities! The rest of this section considers techniques for efficiently identifying abstractions and provides a basis for automating this task. Initial ideas for implementing these techniques are presented in [2]. We begin by considering how an abstraction mapping can be applied to an MVN to produce a set of potential abstraction models. Definition 12. Let φ = φ (g 1 ), . . . , φ (g k ) be an abstraction mapping for an MVN MV. For each entity g i ∈ MV we can abstract the next-state function f g i : by applying φ to its definition in the obvious way. We say that MV A results from applying φ to MV iff: (1) MV A has the same entities and neighbourhood structure as MV; (2) The state space of each entity is a deterministic restriction of φ ( f g i ).
We define φ (MV) to be the set of all such MVNs, i.e. To illustrate this idea, consider applying the abstraction mapping φ (g 2 ) = {0 → 0, 1 → 0, 2 → 1} to the example MVN Ex1 introduced in Section 2 (see Figure 1). The resulting abstracted next-state functions are presented in Figure 6. The set φ (g 2 )(Ex1) will contain two candidate abstractions in which the state space for g 2 is reduced to {0, 1} and whose next-state functions are given by the two possible interpretations (highlighted in bold) for the abstracted state transition table for g 2 given in Figure 6. Figure 6: The (non-deterministic) state transition tables for φ (g 2 )(Ex1) which result from applying φ (g 2 ) to the state transition tables of Ex1 (Figure 1).
An interesting observation arises by noting that for a given model MV and abstraction mapping φ , the trace semantics of the abstracted MVN Tr(φ (MV)) is not in general the same as the abstracted trace semantics φ (Tr(MV)). In fact, it turns out that an important relationship exists between the two, in that Tr(φ (MV)) will always contain at least the traces of φ (Tr(MV)), as shown by the following theorem.
Proof. Let σ = S 0 , . . . , S n ∈ Tr(MV) be an arbitrary trace, then we need to show that if φ (σ ) is a valid abstracted trace then φ (σ ) ∈ Tr(φ (MV)). Let S i → S i+1 be an arbitrary state step in σ . Assuming MV has k entities then this state step can be broken up into k components S i → S j i+1 , for j = 1, . . . , k. Applying the abstraction mapping to each component gives φ (S i ) → φ (g j )(S j i+1 ). Clearly, by Definition 12 there must exist MV A ∈ φ (MV) whose next-state functions reproduce each of these abstracted component steps and so is able to reproduce the complete abstracted state step φ (S i ) → φ (S i+1 ). Since φ (σ ) is a valid abstracted trace it follows that we must be able to find MV A ∈ φ (MV) which is able to reproduce all the abstracted state steps φ (S i ) → φ (S i+1 ), for i = 0, . . . , n − 1. Thus, we know φ (σ ) ∈ Tr(MV A ) and so by Definition 12 we have φ (σ ) ∈ Tr(φ (MV)) as required. P From this result, it follows that any abstraction of an MVN MV must be contained within the set of potential abstractions φ (MV) as formalized in the corollary below.

Corollary 14.
Given two MVNs MV 1 and MV 2 we have that Proof. By Definition 6 we know Tr(MV 1 ) ⊆ φ (Tr(MV 2 )) and so by Theorem 13 we have Tr(MV 1 ) ⊆ Tr(φ (MV 2 )). It therefore follows by Definition 12 that MV 1 ∈ φ (MV 2 ). P Corollary 14 provides an important necessary condition for an MVN to be an abstraction of another for a given abstraction mapping. It gives us a way of restricting the models that need to be considered when iterating through possible candidate abstractions for an MVN; we simply apply the abstraction mapping to the MVN in question and then consider each possible deterministic model that results from this application. This observation results in an exponentially smaller search space and provides the basis for a more efficient abstraction finding algorithm.
To illustrate the above ideas let us consider finding all the abstractions for Ex1 under φ (g 2 ), i.e. calculating the abstraction set AS(Ex1, φ (g 2 )). Using the results from Corollary 14, we begin by abstracting the state transition tables for Ex1 using the given abstraction mapping (shown previously in Figure 6) and identifying the potential abstractions contained in φ (g 2 )(Ex1). We can see that the behaviour of g 2 is non-deterministic when g 1 = 0 and g 2 = 0. As such, we have just two possible candidate models AB 1 and AB 2 to consider, shown respectively by Figure 7.(a) and Figure 7.(b) (where the rules highlighted in bold are the only ones that differ).
the same MVN as Ex2 which was introduced as an abstraction in the previous section.) Thus, we have shown that the refinement set AS(Ex1, φ (g i )) = {AB 2 }. It can be observed that exact refinements occur precisely when the translated MVN has a singleton set of candidate abstraction models, as shown by the following theorem.
Theorem 15. Let φ be an abstraction mapping for some MVN MV. Then we know the following: (2) if φ (MV) is not a singleton set, then no exact abstraction for MV can exist under φ .

Proof.
To prove (1), we observe that if φ (MV) = {MV A } is a singleton set then for each g i ∈ MV the abstracted next-state function φ ( f g i ) must be deterministic. This implies that all abstracted traces φ (σ ), for σ ∈ Tr(MV) must be valid. Furthermore, by Definition 12 and Theorem 13 it follows that Tr(MV A ) = φ (Tr(MV)) as required.
To prove (2), note that if φ (MV) contains more than one potential abstraction model then there must exist at least one abstracted next-state function φ ( f g i ) which is non-deterministic. This implies there must exist at least one abstracted global state which leads to two or more different traces. Clearly, either some of these abstracted traces are invalid or φ (Tr(MV)) must contain more traces than any single abstraction model could capture. Therefore, there cannot exist an exact abstraction for MV. P

Illustrative Biological Examples
In this section we illustrate the theory and techniques developed in the previous sections by investigating the existence of abstractions for two published MVN models for the genetic regulatory network controlling the lysis-lysogeny switch in the bacteriophage λ [17,5]. We begin with a brief introduction to the bacteriophage λ (see [14] for a more detailed introduction). The temperate bacteriophage λ is a virus which infects the bacteria Escherichia coli [18,14]. After infection of the host cell, a decision is made by λ based on environmental factors between two very different methods of reproduction, namely the lytic and lysogenic cycles [18]. In most cases, λ enters the lytic cycle, where it generates as many new viral particles as the host cell resources allow before producing an enzyme to lyse the cell wall, releasing the new phage into the environment. Alternatively, the λ DNA may integrate into the host DNA and enter the lysogenic cycle. Importantly, genes expressed in the λ DNA synthesize a repressor which blocks expression of other phage genes including those involved in its own excision. As such, the host cell establishes an immunity to external infection from other phages, and the phage λ is able to lie dormant, replicating with each subsequent cell division of the host.

The Two Entity Core Regulatory Model
A simple MVN model of the core regulatory mechanism for the lysis-lysogeny switch was proposed in [17]. This model, which we denote as PL2, is presented in Figure 8 and is based on the crossregulation between two regulatory genes, CI (the repressor gene) and Cro. It can be seen that Cro inhibits the expression of CI and at higher levels of expression, also inhibits itself. The gene CI inhibits the expression of Cro while promoting its own expression. The full synchronous trace semantics Tr(PL2) for this MVN is presented in Figure 8.(c). We can see from the state transition graph in Figure 8.(d) that PL2 has three attractor cycles, where the attractor cycle 10 → 10 represents the lysogenic cycle since the repressor gene CI is fully expressed and 01 → 02 → 01 represents the lytic cycle. In order to identify an abstraction for PL2 we begin by selecting an appropriate state mapping φ (Cro) : {0, 1, 2} → {0, 1} for the only non-Boolean entity Cro. We use our understanding of the behaviour of Cro to define the following state mapping We can then view φ (Cro) as an abstraction mapping and following the approach in Section 4, we restrict the abstraction search space by applying the abstraction mapping φ (Cro) to PL2. This results in a set φ (Cro)(PL2) which contains two candidate abstraction models. It turns out that only one of these is a correct abstraction and we present this abstraction model APL2 in Figure 9. It is straightforward to check that the trace semantics of APL2 (see Figure 9) is indeed consistent with the abstracted trace semantics of PL2 (see Figure 10), i.e. Tr(APL2) ⊆ φ (Cro)(Tr(PL2)). Thus, we know APL2 ¡ φ (Cro) PL2 holds. φ (Cro)(σ (00)) = 00, 11, 00 φ (Cro)(σ (10)) = 10, 10 φ (Cro)(σ (01)) = 01, 01 φ (Cro)(σ (11)) = 11, 00, 11 φ (Cro)(σ (02)) = 01, 01 φ (Cro)(σ (12)) = 11, 01, 01 Figure 10: The traces φ (Cro)(Tr(PL2)) resulting from abstracting the traces of PL2 using φ (Cro).
It can be seen that the abstraction APL2 acts as a good approximation to the behaviour of the original MVN PL2 and in particular, we can see that the abstraction has captured all three attractor cycles that were present in PL2.

The Four Entity Regulatory Model
The core regulatory model presented above was extended in [17] to take account of the actions of two further regulatory genes, CII and N. The resulting four entity MVN model PL4 is presented in Figure  11 (note that the state transition tables presented use a shorthand notation where an entity is allowed to be in any of the states listed for it in a particular row). This MVN is more detailed than PL2 and  Figure 11: An extended MVN model PL4 of the control mechanism for the lysis-lysogeny switch in bacteriophage λ (taken from [17] which we use to define the abstraction mapping φ = φ (CI), φ (Cro), I CII , I N . Again, following the approach presented in Section 4 we first apply this abstraction mapping to PL4 resulting in the set φ (PL4) of candidate abstraction models. By analysing φ (PL4) we are able to establish that there are 256 possible candidate abstraction models (we have 4 choices for CI, 4 choices for Cro, 8 choices for CII, and 2 choices for N). After investigating these candidate models we were able to identify two abstractions for PL4 under φ , denoted APL4 1 ¡ φ PL4 and APL4 2 ¡ φ PL4, which are presented in Figure 12. Interestingly, both abstractions appear to capture the key behaviour of PL4 in the sense that both contain the attractor cycles 0100 → 0100 and 1000 → 1000 which correspond to those present in PL4.

Conclusions
In this paper we have developed an abstraction theory for MVN models based on the idea of using an abstraction mapping to relate the reduced state space of an abstraction to the original model. The problem of identifying suitable abstractions for an MVN was discussed and some initial ideas for restricting the number of candidate abstraction models that need to be considered were proposed. We showed that abstractions can be used to analyse an MVN since they preserve reachability properties and importantly, since all the attractor cycles of an abstraction will correspond to attractor cycles in the original model. This work was motivated by the need to be able to relate MVN models at different levels of abstraction and in particular, the idea of abstracting an MVN to a simpler model which is more amenable to analysis and visualization techniques. The abstraction theory presented can also be seen as providing a framework for an incremental refinement approach to constructing MVNs.
We illustrated the abstraction theory and techniques developed by considering two examples based on published MVN models of the genetic regulatory network for the lysis-lysogeny switch in phage λ [17,5]. We considered a simple two entity model and then an extended model that contained four entities (two of which were non-Boolean). In both cases we were able to identify meaningful Boolean abstractions which captured the key attractor cycles contained in the original models.
Further work is now needed to build on the ideas presented in Section 4 to develop tool support for automatically checking and identifying abstractions. Initial ideas for such tool support have been presented in [2] and work is on going to develop efficient algorithmic solutions to support the abstraction process. Other researchers have considered abstracting MVNs by reducing the number of regulatory entities while preserving important model dynamics (see for example [13,20]). It would be interesting to consider combining such an approach with the abstraction theory we have developed here. Finally, we note that extending the abstraction theory to asynchronous MVN models is an interesting but challenging area of future work. In particular, ways of coping with the non-deterministic choices inherent in the dynamic behaviour of asynchronous models will be needed.