troduisons une interprétation abstraite de l'ensemble des évaluations de paramètres admissibles (paramétrisations). L'abstraction permet de représenter n'importe quel ensemble de paramétrisations par un encodage de taille constante, au prix d'une sur-approximation conservatrice. Deuxièmement, nous élevons la sémantique d'ordre partiel sous la forme d'un déploiement des réseaux de Petri vers des réseaux de régulation paramétriques. Les graphiques d'inuence des réseaux de régulation biologique ont tendance à être relativement clairsemés, ce qui permet une grande concurrence. Cela peut être exploité par des méthodes de réduction d'ordre partiel pour produire des représentations d'espace d'état concises.

Les deux approches visent à aborder les deux aspects de la double explosion combinatoire et sont introduites de manière compatible, ce qui permet de les utiliser simultanément. Une telle application est soutenue par une implémentation prototype utilisée pour mener des expériences sur divers réseaux de régulation paramétriques. Nous considérons en outre des ranements des méthodes, comme une méthode de réduction de modèle à la volée portée aux réseaux de régulation paramétriques à partir de réseaux d'automates.

Résumé

L'analyse de la dynamique des réseaux de régulation biologique, notamment des réseaux de signalisation et de régulation génique, fait face à l'incertitude du modèle de calcul exact. En eet, la plupart des connaissances disponibles concernent l'existence d'interactions (éventuellement indirectes) entre des entités biologiques (espèces), par ex. protéines, ARN, gènes, etc. Les détails sur la manière dont les diérents régulateurs d'une même cible coopèrent, et plus encore sur les taux cohérents pour ces interactions, sont cependant rarement disponibles. A cet égard, des approches de modélisation qualitative sous forme de réseaux de régulation discrets, tels que les réseaux booléens et Thomas, orir un niveau d'abstraction approprié pour la dynamique du réseau de régulation biologique. Les réseaux de régulation discrets étant basés sur un graphe d'inuence, ils nécessitent peu de paramètres supplémentaires par rapport aux modèles quantitatifs classiques. Néanmoins, la détermination des paramètres discrets est un dé bien connu et un goulot d'étranglement majeur pour fournir des prédictions robustes à partir de modèles informatiques.

Le graphe d'inuence d'un réseau de régulation établit des dépendances pour l'évolution de chaque espèce, spéciées par les arêtes dirigées du graphe. Les dépendances seules, cependant, ne susent pas pour spécier la fonction logique régissant l'évolution d'une espèce. Au lieu de cela, les fonctions logiques associées à chaque espèce, contraintes par le graphe d'inuence, sont codées dans les paramètres d'un réseau de régulation discret. L'espace des fonctions logiques admissibles est alors représenté par un réseau de régulation paramétrique. D'une part, les réseaux de régulation paramétriques peuvent être utilisés pour l'identication de valeurs de paramètres pour lesquelles le réseau de régulation discret résultant satisfait des propriétés (dynamiques) données. L'identication des paramètres des réseaux de régulation peut ainsi être vue comme un exemple particulier de synthèse de modèle, dans le cadre contraint du graphe d'inuence sous-jacent. D'autre part, les réseaux de régulation paramétriques peuvent être analysés comme un modèle autonome, pour faire des prédictions robustes vis-à-vis de la variabilité du réseau.

L'analyse de la dynamique du réseau de régulation paramétrique est entravée par la double explosion combinatoire, de l'espace d'états et de l'espace des paramètres. Dans cette thèse, nous développons de nouvelles méthodes d'analyse de réseau de régulation paramétrique, sous forme de sémantique spécialisée, visant à atténuer l'explosion combinatoire. Tout d'abord, nous iniii Chapter 1

Introduction

Modelling in systems biology is commonly conducted manually or semi-automatically using the available molecular interaction knowledge. Qualitative models are therefore often preferred for biological systems as they require comparatively little parametrisation on top of the knowledge available in literature and databases. The biological knowledge typically consists of one-on-one interactions, positive and negative, between species (molecules) within the system. Discrete regulatory networks are particularly well suited for representing and generalising such information, making them commonplace in modelling gene regulation and signalling pathways [START_REF] Novère | Quantitative and logic modelling of molecular and gene networks[END_REF][START_REF] Kauman | Random Boolean network models and the yeast transcriptional network[END_REF][START_REF] Abou-Jaoudé | Model checking to assess t-helper cell plasticity[END_REF][START_REF] Cohen | Mathematical modelling of molecular pathways enabling tumour cell invasion and migration[END_REF][START_REF] Traynard | Logical model specication aided by model-checking techniques: application to the mammalian cell cycle regulation[END_REF][START_REF] Collombet | Logical modeling of lymphoid and myeloid cell specication and transdierentiation[END_REF] since their introduction in late 60s [START_REF] Kauman | Homeostasis and dierentiation in random genetic control networks[END_REF][START_REF] Thomas | Boolean formalization of genetic control circuits[END_REF]. Discrete regulatory networks are well known for being able to express complex emerging behaviour, owing in particular to loops on the inter-component inuences (commonly known as feedback loops) [START_REF] Thiery | Dynamical behaviour of biological regulatory networksii. immunity control in bacteriophage lambda[END_REF][START_REF] Albert | The topology of the regulatory interactions predicts the expression pattern of the segment polarity genes in Drosophila melanogaster[END_REF][START_REF] Demongeot | Genetic regulation networks: circuits, regulons and attractors[END_REF].

The modelling of gene regulatory networks or signalling pathways as discrete regulatory networks presents a challenging task due to the high level of abstraction involved. The inference of discrete regulatory networks can be classically split into two phases. First, available data on specie interaction from databases and literature is used to deduce the topology of the network in the form of an inuence graph. Inuence graph is a directed graph whose nodes represent the variables (species) of the system and edges the pairwise inuences, possibly marked as positive or negative. In the second step, a dynamical model is built from the inuence graph by specifying a regulation function. The regulation function determines the variable value evolution across dierent states of the network, given as vectors of variable values.

While the topology of the discrete regulatory networks in the form of inuence graph is often well supported by data from literature and databases, the specication of a regulation function requires additional parameter inference. Indeed, whereas the inuence graph establishes the potential dependencies (possibly signed) between the variable value changes, the pairwise dependencies are not sucient to determine the combined eect of several inuences on a single variable. In other words, it is commonly known that two variables both have a positive inuence on the value of a third variable. However, it is rarely known if both of the variables have to be active, i.e. have value above a determined threshold, for the value of the third variable to increase or if just one is sucient.

In general, the regulation function may take the form of an arbitrary logical function. The individual target values of a variable in possible combinations of the values of its regulator variables, the variables that have an inuence on it, are hence discrete parameters. The regulation function is therefore equivalent to an assignment of a value to each such parameter, referred to as parametrisation. A discrete regulatory network can thus be specied by an inuence graph, encoding the topology, paired with a parametrisation, giving the dynamics. Within the scope of this thesis we focus on discrete regulatory networks where each variable has a nite discrete domain. Finite variable domains guarantee that the number of parameters as well as each parametrisation are also nite, making it possible to enumerate them. The restriction to nite variable domains is in line with models studied in the literature, which typically utilise variable domains of very small size, often Boolean [START_REF] Thomas | Boolean formalization of genetic control circuits[END_REF][START_REF] Jong | Modeling and simulation of genetic regulatory systems: A literature review[END_REF][START_REF] Laubenbacher | A computational algebra approach to the reverse engineering of gene regulatory networks[END_REF][START_REF] Bernot | Semantics of biological regulatory networks[END_REF][START_REF] Wang | Boolean modeling in systems biology: an overview of methodology and applications[END_REF].

As biological knowledge on combined eects of two or more regulator variables is scarce, parametrisations cannot be easily derived from literature. We therefore avoid precise parametrisation specication, focusing instead on parametric regulatory networks. A parametric regulatory network is, similarly to discrete regulatory networks, based on an inuence graph. However, parametric regulatory networks do not rely on a specic regulation function, or equivalently a single parametrisation. The dynamics instead encompass any parametrisation which is compatible with the inuence graph (admissible), including any inuence signs. A parametric regulatory network is thus a formal model constructed to represent exactly the available biological knowledge. It contains all the pairwise inuence information available in the literature, however, no assumptions are made on the unknown regulator interplay, retaining all possibilities by the means of dierent parametrisations.

The analysis of parametric regulatory networks therefore does not consist merely of asking whether the model satises given dynamical properties (e.g. reachability), but with which parametrisations are the properties satised. The exploration of possible parametric regulatory network dynamics, however, suffers from dual combinatorial explosion, limiting the scalability. Not only do parametric regulatory networks experience the combinatorial explosion of the state space, where the number of states is exponential in the number of variables, a challenge also for discrete regulatory networks, but the number of parametrisations is in the worst case double exponential in the number of variables.

The dual combinatorial explosion arising from the combination of state space and number of parametrisations both being exponential in the number of variables forms the principal challenge tackled in this thesis. To this end, we propose new semantics for parametric regulatory networks.

First, we propose abstract semantics of parametric regulatory networks. The semantics rely on abstraction of the parametrisation space by the means of bounded convex sublattices of the parametrisation set with a preestablished order. Our abstraction is not only compact, being represented by only two bounds, but can reect possible state transitions without explicit enumeration of parametrisations. Furthermore, the abstraction is exact assuming no additional constraints (signs) on the inuences.

The abstraction also extends to parametric regulatory networks with signed inuences. The inuence signs translate into monotonicity constraints on the inuences. If a variable is inuenced positively (resp. negatively) by a regulator, decrease (resp. increase) in the value of the regulator may not cause increase in the value of the variable. Dierent constraints are also captured by the abstraction, such as observability. If a variable is observably inuenced by a regulator, then there must exist at least one state in which the sole change in the value of the regulator leads to a change in the value of the variable. Indeed, in the general case, we allow for an inuence to have no impact on the regulation of a variable in spite of being specied.

Such constraints on inuences are handled by the parametrisation space abstraction at the cost of over-approximation. It is shown, however, that the abstraction is tight, i.e. the proposed abstraction is the smallest bounded convex sublattice containing all the admissible parametrisations. The tightness result ensures that if a state is reachable under the abstract semantics, there exists at least one parametrisation which allows a sequence of concrete transitions leading to the state. Thus, while the over-approximation allows for false positives in the form of falsely declaring a state reachable by a particular parametrisation, it may not introduce spurious transitions.

Second, we dene partial order semantics for parametric regulatory networks in order to obtain a more compact representation of the reachable state space. The partial order semantics rely on constructing unfoldings, akin to Petri net unfoldings. The unfolding semantics may additionally by combined with either the concrete or abstract semantics of parametric regulatory networks, allowing us to use both the parametrisation space abstraction and partial order reduction at the same time, thus addressing both aspects of the dual combinatorial explosion.

Finally, we introduce a goal-oriented model reduction for parametric regulatory networks. The model reduction relies on polynomial static analysis methods to determine which transitions are guaranteed to not lead to a given target state. This allows us to prune the transitions which are known not to reach the goal, allowing us to avoid exploring dead end branches of the state space. Moreover, the method is compatible with both the abstract and the unfolding semantics of the parametric regulatory networks, allowing for the combination of all three methods. This thesis expands upon results previously published in [START_REF] Kolcák | Parameter Space Abstraction and Unfolding Semantics of Discrete Regulatory Networks[END_REF][START_REF] Haar | Combining renement of parametric models with goal-oriented reduction of dynamics[END_REF]. Several discrete regulatory network applications have also beneted from the insights gathered working with the parametric regulatory networks. Namely in the area of concurrency [START_REF] Chatain | Concurrency in boolean networks[END_REF] and a new symbolic semantics of Boolean networks that subsume any multivalued or continuous renement [START_REF] Paulevé | Reconciling qualitative, abstract, and scalable modeling of biological networks[END_REF].

Outline The thesis is partitioned into four main areas. In the rst part, we introduce in detail the necessary theoretical background. Chapter 2 denes the regulatory network model and related concepts, forming the basis for the parametric regulatory network which is the object of our studies. Chapter 3 introduces the unfolding based partial order semantics for Petri nets, including the construction of complete nite prexes.

The second area deals with our main contribution in the form both abstract semantics and partial order semantics of the parametric regulatory networks. Chapter 4 introduces the parametric regulatory networks as well as their concrete and abstract semantics. Chapter 5 extends both the concrete and abstract semantics of parametric regulatory networks to incorporate additional biological knowledge in the form of inuence constraints. Chapter 6 introduces the partial order semantics of parametric regulatory networks based on the Petri net unfolding, including the complete nite prex construction. Chapter 7 introduces an optimisation of the unfolding procedure for the parametric regulatory networks in a setting with predetermined target conguration.

The third part is dedicated to application areas of our parametric regulatory network semantics and related work. Chapter 8 explores related work on parametric regulatory networks and equivalent models within various application areas. Chapter 9 oers experimental results on the compactness of the state space representation with our parametric regulatory network semantics.

Finally, the last, fourth part gives a summary of our work and outlines possible future work. Chapter 10 oers a brief summary of our contributions. Chapter 11 describes the directions of the currently ongoing and future work related to semantics of parametric regulatory networks and regulatory networks in general.

Notations Π applied to sets denotes the Cartesian product. If the order of the elements matters, we write ≤ Π x∈X . . . where ≤ is a total order on X.

Given a sequence of n elements π = (π i ) 1≤i≤n , we write π

∆ = { π i | 1 ≤ i ≤ n }
to denote the set of its elements.

Given a monotonic function f , we write f * (x) to denote the xpoint of the iteration of the function f initially applied to x.

Given a vector v v v = (v v v 1 , . . . , v v v n ), we write v v v [i → y] to denote the vector identical to v v v except for the component i value, which is equal to y, v v v

Discrete Regulatory Networks

In this chapter we introduce discrete regulatory networks, nite transition systems which are commonly employed for modelling biological systems, especially gene regulatory and signalling networks [START_REF] Jong | Modeling and simulation of genetic regulatory systems: A literature review[END_REF][START_REF] Demongeot | Genetic regulation networks: circuits, regulons and attractors[END_REF][START_REF] Thiery | Dynamical behaviour of biological regulatory networksii. immunity control in bacteriophage lambda[END_REF].

A discrete regulatory network consists of a nite number (n) of variables (nodes). Each variable v has associated a nite discrete domain X v of possible values. For the sake of simplicity, we consider the nite set of variables to be indexed by {1, . . . , n} and by abuse of notation, we unify the variables with their respective indices. The set of states (state space) of the discrete regulatory network is then given as vectors of possible values for each variable,

n Π v=1 X v .
The dynamics of a discrete regulatory network are captured by a regulation function F which species new value each variable should take based on the current state. There are several ways to apply the regulation function, diering especially in simultaneity of updates of individual variables. To reect the possibility of updating individual variables we decompose the function F into local functions f v for each variable v.

As domain of the regulation function is the cartesian product of the domains of the individual variables, a discrete regulatory network is thus fully specied solely by the regulation function.

Denition 2.1 (Discrete Regulatory Network). A discrete regulatory network of a dimension n is a function

F : n Π v=1 X v → n Π v=1 X v
, where, for every v ∈ {1, . . . , n}, X v is nite.

A state of F is a vector x x x which assigns each variable a value from the respective domain, x x x ∈ n Π v=1 X v . The regulation functions of individual variables, f 1 , . . . , f n , are obtained as projections of F to the respective variables, for all u ∈ {1, . . . , n}:

f u : n Π v=1 X v → X u f u : x x x → F (x x x) u
In the rest of the chapter, we elaborate on discrete regulatory networks and introduce some commonly used variations. Namely, in Section 2.1 we give a detailed description of multiple dierent semantics which can be used with discrete regulatory networks. Subsequently, in Section 2.2 we introduce additional representation and constraints for discrete regulatory networks. The introduced concepts are used heavily in the parametric version of the model, elaborated on in Chapter 4. In Section 2.3 we introduce some of the most commonly used congurations of discrete regulatory networks, such as Boolean networks or multivalued networks. Finally, for comparison and to give better intuition, we introduce automata networks, a model equivalent to the discrete regulatory networks which is dened using interacting automata instead of functions, in Section 2.4.

Semantics of Discrete Regulatory Networks

The denition of discrete regulatory networks is simple, but signicantly exible, making discrete regulatory networks suitable for a variety of modelling tasks. This exibility is reected in numerous dierent updating schemes semantics used with discrete regulatory networks. The main distinction of the dierent semantics lies in simultaneity of variable updates. The variables of discrete regulatory networks may change value either simultaneously, all at the same time, (synchronous semantics) or individually, one at a time, (asynchronous semantics). Additionally, several variations of mixed semantics have been considered. We focus on the most universal of such mixed semantics, called generalised asynchronous semantics, which allows arbitrary combination of synchronous and asynchronous transitions.

Synchronous Semantics of Discrete Regulatory Networks

Using synchronous semantics, all variables are updated simultaneously, by the same transition. One can therefore envision the transitions as being simply the application of the function F on the current state of the discrete regulatory network. Denition 2.2 (Synchronous Semantics). Let F be a discrete regulatory network of dimension n. The synchronous semantics of F is a relation

F -→ sync ⊆ n Π v=1 X v × n Π v=1
X v dened as: X v has exactly one successor, namely F (x x x). Synchronous semantics of discrete regulatory networks are thus fully deterministic. The determinism of the semantics allows for relatively simpler analysis of discrete regulatory networks such as reachability or attractor analysis. However, synchronism assumes strict timing constraints on the model by demanding value changes of each variable to have the same duration, or be otherwise synchronised.

Although several real world applications, such as electronic circuits, outright rely on synchronisation, the use of synchronous semantics is much more debatable in areas where variable updates can take dierent amounts of time. In particular, the timing of substrate concentration changes in biological systems is not necessarily uniform and the precise timing is often unpredictable or scarcely known. Simultaneity therefore cannot be guaranteed, leading us to explore the asynchronous semantics which assume temporal independence of variable updates.

Asynchronous Semantics of Discrete Regulatory Networks

In asynchronous semantics, the state is updated one variable at a time. Rather than the regulation function F , the transitions are given by application of the individual regulation functions f 1 , . . . , f n . As any of the regulation functions f 1 , . . . , f n may be chosen to update the state, the asynchronous semantics is nondeterministic. Denition 2.3 (Asynchronous Semantics). Let F be a discrete regulatory network of dimension n. The asynchronous semantics of F = (f 1 , . . . , f n ) is a relation

F -→ async ⊆ n Π v=1 X v × n Π v=1
X v dened as:

(x x x, y y y) ∈ F -→ async ∆ ⇐⇒ D (x x x, y y y) = {v} ∧ y y y v = f v (x x x)
where D :

n Π v=1 X v × n Π v=1 X v → 2 {1,.
..,n} is the function computing the set of variables with dierent values in the two input states, D : x x x, y y y → {v ∈ {1, . . . , n} | x x x v = y y y v }.

Similar to the synchronous semantics, we use the inx notation x x x Since D (x x x, y y y) is a singleton set for asynchronous transitions t = (x x x, y y y) ∈ F -→ async , we denote the unique element, the only variable that changes value, as v (t) (D (x x x, y y y) = {v ((x x x, y y y))}).

One may be led to believe the asynchronous semantics are a renement of the synchronous semantics. Although true for some discrete regulatory networks, the two semantics are incomparable in the general case. The synchronous semantics often allow normal transitions transitions which are not decomposable into a sequence of asynchronous transitions, thus allowing the synchronous semantics to exhibit behaviours unreachable in the asynchronous case. The existence of normal transitions has been linked to simple structural elements of discrete regulatory networks, called NOPE cycles, by Noual et al. [START_REF] Noual | Synchronism versus asynchronism in monotonic boolean automata networks[END_REF].

Apart from the two extreme cases, the fully synchronous and the fully asynchronous semantics, other simultaneity restrictions might be considered depending on the domain. As the fully synchronous and fully asynchronous semantics are incomparable with regards to expressivity (reachability) in the general case, it is natural to consider their combination. To this end, we consider generalised asynchronous semantics, which allow any subset of variables to be updated at a time, thus allowing the fully asynchronous behaviour as well as normal transitions.

Other approaches are possible, such as globally asynchronous locally synchronous (GALS) employed extensively in circuit design [START_REF] Chapiro | Globally-Asynchronous Locally-Synchronous Systems (Performance, Reliability, Digital[END_REF], or the, essentially dual concept, of bounded asynchrony [START_REF] Fisher | Bounded asynchrony: Concurrency for modeling cell-cell interactions[END_REF]. As local synchrony is subsumed by the generalised asynchronous semantics and bounded asynchrony can be modelled with a suitable fairness criterion, we do not treat either in detail.

Generalised Asynchronous Semantics of Discrete Regulatory Networks

In the generalised asynchronous semantics, each transition updates a (nonempty) subset of variables synchronously. Denition 2.4 (Generalised Asynchronous Semantics). Let F be a discrete regulatory network of dimension n. The generalised asynchronous se-

mantics of F = (f 1 , . . . , f n ) is a relation F -→ gen ⊆ n Π v=1 X v × n Π v=1 X v dened as: (x x x, y y y) ∈ F -→ gen ∆ ⇐⇒ ∀ v ∈ D (x x x, y y y) = ∅, y y y v = f v (x x x)
where D is again the function computing the set of variables which dier in values between the input states.

Similarly to the synchronous and the asynchronous semantics, we use the inx notation x x x By denition, any behaviour exhibited by either the synchronous or the asynchronous semantics is reproducible in the generalised asynchronous semantics. However, the generalised asynchronous semantics not only retains the nondeterminism of the asynchronous semantics, it allows up to exponentially more transitions 1 . We briey revisit the question of discrete regulatory network semantics, especially for Boolean networks (see Section 2.3), in Chapter 11, where we make connection with the most permissive semantics of Boolean networks.

Inuence Graphs

The regulation functions as presented in the denition of discrete regulatory networks (Denition 2.1) take all variables of the system as the input. In real world applications, however, such `dense' interdependency is rare. In particular, the direct interaction of components of gene regulatory networks and other biological systems is often considerably sparse.

The (in)signicance of some inter-variable dependencies introduced topology to discrete regulatory network in the form of a directed graph, called inuence (or interaction) graph, whose nodes represent the variables of the network. The edges between the variables then denote the signicant inuences.

For the purposes of discrete regulatory networks, an inuence of variable u on variable v is signicant if there exists at least one state, in which the sole change in the value of variable u changes the result of the partial regulation function f v . We relax this denition, however, allowing also other variables to be declared signicant. This is to accommodate for the uncertainty involved with the design of parametric regulatory networks (Chapter 4), the denition of which is strongly tied to the inuence graphs. The above criterion then corresponds to the smallest inuence graph. Denition 2.5 (Inuence Graph). Let F be a discrete regulatory network of dimension n.

Then a graph G = {V, I} such that V = {1, . . . , n} is an inuence graph of F if, for each pair of states x x x, y y y

∈ n Π w=1 X w such that D (x x x, y y y) = {u}∧f v (x x x) = f v (y y y), (u, v) ∈ I.
We use G(F ) to denote the smallest inuence graph of the regulatory network F .

The inuence graph allows us to specify which variable values does the target value of a variable v directly depend on. We call such variables the regulators of v. Denition 2.6 (Regulator). Let G = (V, I) be an inuence graph of discrete regulatory network F of dimension n and let v ∈ {1, . . . , n} be an arbitrary variable of F .

Then, variable u ∈ {1, . . . , n} is a regulator of v according to G, if (u, v) ∈ I. We write R(v) to denote the set of all regulators of the variable v.

As the output of the regulation function f v does not change with dierent values of variables u / ∈ R(v), the domain of the regulation function may be restricted to R(v) without loss of information. We thus redene regulation functions f v for regulator states, which are projections of global states to regulators of v.

Denition 2.7 (Regulator State). Let F be a discrete regulatory network of dimension n, G an inuence graph of F and v ∈ {1, . . . , n} an arbitrary variable of F .

A regulator state of v is a vector

ω ω ω ∈ Π u∈R(v) X u .
We use

Ω v = Π u∈R(v)
X u to denote the set of all regulator states of a variable v ∈ {1, . . . , n}.

We further use Ω (F, G) (or simply Ω where F and G are obvious from the context) to denote the set of all regulator states of all variables of F , annotated with the respective variables,

Ω (F, G) = { (v, ω ω ω) | v ∈ {1, . . . , n} ∧ ω ω ω ∈ Ω v }.
Finally, given an arbitrary state

x x x ∈ n Π w=1 X w , we use ω v (x x x) = ω ω ω to denote the regulator state ω ω ω ∈ Ω v of variable v ∈ {1, . . . , n} such that ∀ u ∈ R(v), ω ω ω u = x x x u .
As regulator states are merely projections of the states, the restriction of the regulation functions f 1 , . . . , f n to variable regulators is straightforward. For all v ∈ {1, . . . , n}:

f v : Ω v → X v f v : ω ω ω → f v (x x x) where x x x ∈ n Π u=1
X u is arbitrary such that ω v (x x x) = ω ω ω. On the one hand, smaller domains of regulation functions directly translate into less parameters one needs to evaluate to fully specify the network. Thus, even if the exact regulation functions are unknown, one can greatly simplify the model inference task by considering only interactions which are known to be important in the system. The knowledge of one-to-one interaction between species is much more common in the biological setting than the complex interplay of the regulators which constitutes the regulation function. We thus assume the knowledge of the inuence graph and utilise regulator states for the denition of parametric regulatory networks in Chapter 4.

On the other hand, smaller domains of regulation functions allow us to clearly capture independence of the individual variable regulation functions. E.g. if v ∈ {1, . . . , n} is not a regulator of u ∈ {1, . . . , n} and vice versa, the variable u is not a regulator of the variable v, the two regulation functions f v and f u are independent and can be executed concurrently (the order of their execution is irrelevant). The concurrency in discrete regulatory networks can be exploited for smaller representations of the state space, which is generally exponential in the number of variables. We present such a partial order reduction method in Chapter 6.

Multivalued Networks

We have presented discrete regulatory networks in the their most generic form. In practice, however, the variables of regulatory networks are commonly an abstraction (discretisation) of a quantitative value, e.g. concentration or production rate of a certain protein [START_REF] Thomas | Boolean formalization of genetic control circuits[END_REF][START_REF] Garg | Modeling of multiple valued gene regulatory networks[END_REF][START_REF] Weinstein | A network model for the specication of vulval precursor cells and cell fusion control in caenorhabditis elegans[END_REF]. Although continuous models, such as dierential equation systems, are generally more suited for quantitative data, the use of discrete abstraction is well justied in the biological setting. As data available for biological systems is sparse, constructing a precise continuous model with all the necessary kinetic parameters is often impossible or requires many design decisions which are ad-hoc by nature. A discrete model requires less parameters whose impact on the system is easier to estimate, making them more suited for the reverse engineering scenario common for systems biology.

In this section we introduce the subclass of discrete regulatory networks suited for the aforementioned task of quantitative variable interpretation, commonly referred to as multivalued networks. 2 Multivalued networks are distinguished by having a total order associated with each variable domain. For simplicity, we can assume the variable domains to be downward closed subsets of natural numbers with zero (X v = ↓x for some x ∈ N 0 ) without loss of generality. Multivalued networks allow for all the semantics we introduced for the general discrete regulatory networks (Section 2.1). However, multivalued networks are most often used as a discretisation of a continuous system. To emulate the underlying continuous evolution, we restrict the semantics to only allow the variables to change value stepwise along the total order on their respective domains. In case of subsets of natural numbers, the variables are only allowed to change value by steps of size 1. Note that the restriction has little impact on multivalued networks with asynchronous semantics, as discrete regulatory networks inherently impose no timing information 3 . Replacing one transition 2 The term multivalued networks was adopted to distinguish them from Boolean networks which, although technically a subclass of multivalued networks, are chronologically older as they were used in the rst discrete regulatory network application [START_REF] Kauman | Homeostasis and dierentiation in random genetic control networks[END_REF]. 3 Modications exist for models where timing constraints are critical. E.g. models containing both metabolic pathways, where reactions happen within fractions of seconds, and gene regulation, which, being reliant on protein synthesis, takes time in the order of tens of minutes to hours. changing value by an absolute value of 2 by two transitions changing the value by absolute value of 1 (in the same direction) thus results in the same behaviour.

We only present the necessary modication of generalised asynchronous semantics as it subsumes both synchronous and asynchronous semantics. Denition 2.9 (Generalised Asynchronous Semantics of Multivalued Networks). Let F be a multivalued network of dimension n and m m m the vector of maximum values of the individual variables.

The multivalued generalised asynchronous semantics of

F = (f 1 , . . . , f n ) is a relation F -→ gen ⊆ X m m m × X m m m dened as: (x x x, y y y) ∈ F -→ gen ∆ ⇐⇒ ∀ v ∈ D (x x x, y y y), f v (x x x) ≥ y y y v = x x x v + 1 ∨ f v (x x x) ≤ y y y v = x x x v -1
Having total order on variable domains allows us to express several useful properties in multivalued networks. A prime example of such a property is monotonicity of inuences (or local monotonicity). As is standard, monotonicity comes in two forms. An inuence (u, v) ∈ I is said to be positive monotonic or activation if an increase in the value of the regulator u cannot cause a decrease of the value of the target variable v. Similarly, an inuence (u, v) ∈ I is said to be negative monotonic or inhibition if an increase in the value of the regulator u cannot cause an increase of the value of the target variable v. An inuence (u, v) ∈ I is positive monotonic (activation) if for any two states x x x, y y y ∈ X m m m such that D (x x x, y y y) = {u},

(x x x u < y y y u ) =⇒ (f v (x x x) ≤ f v (y y y))
u is then a positive regulator (activator) of v. Denition 2.11 (Negative Monotonicity). Let F be a multivalued network of dimension n, m m m the vector of maximum values of the individual variables and let G = (V, I) be an inuence graph of F .

An inuence (u, v) ∈ I is negative monotonic (inhibition) if for any two states x x x, y y y ∈ X m m m such that D (x x x, y y y) = {u},

(x x x u < y y y u ) =⇒ (f v (x x x) ≥ f v (y y y))
u is then a negative regulator (inhibitor) of v.

Since data on biological systems is sparse, it is often dicult or outright impossible to infer the exact regulation functions. Local monotonicity, however, describes the relationship of only couple variables in isolation, as opposed to the complex interplay of regulators. Thanks to the relative simplicity, information on inuence monotonicity is widely available. Monotonicity is thus a powerful constraint on admissible multivalued networks in place of the exact regulation functions for the purposes of network inference. The exact uses and benets of inuence monotonicity information are explored in Chapter 5.

Due to the diculty of nding correct regulation functions for multivalued networks, networks with simpler domains are often preferred in practice. In particular, two subclasses of multivalued networks with Boolean vector domain for F are commonly employed, Boolean networks and Thomas networks.

Boolean Networks

Boolean networks are the most fundamental multivalued networks and as the name suggests, they are characterised by only being composed of Boolean variables,

∀ v ∈ {1, . . . , n}, X v = B. Denition 2.12 (Boolean Network). A Boolean network F of dimension n is a function F : B n → B n on Boolean vectors of length n.
The Boolean domain is the smallest reasonable4 domain a variable of a multivalued network can have. Boolean networks of dimension n are thus the simplest (smallest) discrete regulatory networks of the dimension n. Although the Boolean domains directly translate to smaller number of possible and thus also reachable states as well as smaller number of regulation states and thus the number of parameters (more in Chapter 4), the reduction is not enough to break out of the combinatorial explosion in either case and the number of both the states and parameters is in the general case exponential in n.

Despite the minimalistic variable domains, Boolean networks exhibit relatively high expressiveness leading to their widespread use [START_REF] Jong | Modeling and simulation of genetic regulatory systems: A literature review[END_REF][START_REF] Abou-Jaoudé | Model checking to assess t-helper cell plasticity[END_REF][START_REF] Cohen | Mathematical modelling of molecular pathways enabling tumour cell invasion and migration[END_REF].

Thomas Networks

Thomas networks allow the use of Boolean regulation functions while maintaining arbitrary (natural) bounds for the individual variable domains. This is achieved by introduction of regulation thresholds in the form of labelling on inuences. More precisely, each inuence e = (u, v) ∈ I is assigned a regulation threshold t (e) ∈ X u . The threshold acts as a binarisation delimiter when feeding the multivalued state to the Boolean regulation function. Any value of the regulator u smaller than t (e) is binarised to 0, while any value of the regulator u larger than or equal to t (e) is treated as 1.

Due to the use of thresholds, Thomas networks are also known as multivalued threshold networks or simply multivalued networks with threshold. We, however, stick with the traditional nomenclature of Thomas networks, legacy of their rst use for modelling cellular regulation by René Thomas [START_REF] Thomas | Boolean formalization of genetic control circuits[END_REF] as it allows for a clearer distinction between Thomas networks and general multivalued networks. Denition 2.13 (Thomas Network). A Thomas network of dimension n is a couple (F, t) where F : B n → X m m m is the regulation function and t : {1, . . . , n} 2 →

N is a threshold labelling function such that for any pair of variables u, v ∈ {1, . . . , n}, t

((u, v)) ≤ m m m u .
Although all discrete regulatory network semantics are applicable to Thomas networks, we modify the standard denition to account for the thresholds. We present only the generalised asynchronous semantics of Thomas networks as it subsumes both the synchronous and asynchronous semantics. Denition 2.14 (Generalised Asynchronous Thomas Semantics). Let (F, t) be a Thomas network of dimension n and m m m the vector of maximum values.

The generalised asynchronous semantics of (F, t) is a relation

(F,t) -→ gen ⊆ X m m m ×
X m m m dened as:

(x x x, y y y) ∈ (F,t) -→ ∆ ⇐⇒ ∀ v ∈ D (x x x, y y y), f v (b b b v ) ≥ y y y v = x x x v + 1 ∨ f v (b b b v ) ≤ y y y v = x x x v -1 where for each v ∈ {1, . . . , n}, b b b v ∈ B n is a binarisation of x x x according to the relevant thresholds, ∀ u ∈ {1, . . . , n}, b b b v [u] = 1 ⇐⇒ t ((u, v)) ≤ x x x u .
Thomas networks naturally subsume Boolean networks and oer more expressivity while maintaining the same complexity of the regulation function. The extra expressivity, however, translates into the need to determine the regulation threshold for each inuence. The regulation thresholds essentially dictate which variables respond fastest to a monotonic change of the value of a common regulator. In other words, thresholds determine the sensitivity of variables to their regulators changing value. Such sensitivity information, however, is seldom readily available in the biological setting.

Discrete Regultory Networks as Automata Networks

In this section we approach discrete regulatory networks from a dierent standpoint. In particular, we provide an alternative denition of discrete regulatory networks in the form of automata networks making use of nite automata instead of regulation function to describe the dynamics. Although we speak of alternative denition automata networks may be independently studied as a standalone model [START_REF] Fogelman-Soulie | Automata networks as models for biological systems: (a survey)[END_REF].

An automata network is a collection of nite automata which take the current state of their neighbours as the input. Automata networks are thus closely related to cellular automata, however, instead of a grid, the topology of an automata network is given by an arbitrary directed graph. In general, automata networks may be innite. Since the number of automata in an automata network corresponds to the dimension of the equivalent discrete regulatory network 5 , however, we focus on nite automata networks to match the restriction on the dimension of discrete regulatory networks.

Although we introduce automata networks as collections of nite automata, it is usual for automata networks to produce innite executions. The nal states of the individual automata are therefore omitted in the denition. Additionally, since discrete regulatory networks do not have an explicitly dened initial state, we do the same for the automata networks and omit also the initial states of the automata. The notions of nal states and initial states may be employed for specication of a concrete, typically reachability, problem.

Denition 2.15 (Automata Network). An automata network N

= (A 1 , . . . , A n ) is a collection of simplied nite automata such that for each i ∈ {1, . . . , n}, A i = (Q i , Σ i , δ i ), where Σ i ⊆ 2 j =i Qj and δ i : Q i × Σ i → Q i .
Note that the alphabet Σ i does not necessarily contain the state of every other automaton in the network. Having a restricted alphabet identies dependencies between the automata (in-neighbours), thus dening the (graph) topology of the automata network.

One can easily nd a correspondence between automata networks with n states and discrete regulatory networks of dimension n. The individual automata A 1 , . . . , A n correspond to the variables of the discrete regulatory network. The states of the automaton are then the elements of the domain of the variable, Q i = X i , and the transition relation δ i corresponds to the individual regulation function f i , δ i (x i , {x 1 , . . . , x i-1 , x i+1 , . . . , x n }) = f i ((x 1 , . . . , x n ))6 . Following the above correspondence, one can easily apply any of discrete regulatory network semantics for the automata networks.

Examples

In this section we provide a few examples of the dierent discrete regulatory networks including the inuence graphs and dynamics for dierent semantics types. As the associated structures, such as the state space graph, tend to grow in size very quickly for larger discrete regulatory networks, we present toy examples rather than actual models from biology. While our toy examples are considerably minimalistic, they suce to illustrate the important properties in this as well as following chapters, where we repurpose them as running examples.

Example 2.1. In the following we give an example of a multivalued network

F A : x x x → (x x x a + 1) mod 3, 1 -x x x b , x x x a + x x x b 2
F A can be equivalently specied using the individual regulation functions

F A = (f a , f b , f c ): f a : x x x → (x x x a + 1) mod 3 f b : x x x → 1 -x x x b f c : x x x → x x x a + x x x b 2
Note that according to F A , respectively f a , the value of the variable a tends to increase to the maximum m m m a = 2 and tends to decrease back to 0 once the maximum value is achieved. However, as the multivalued network semantics are restricted to updating variable values by steps of size 1, the value of variable a must decrease to 1 before reaching 0, at which point the tendency changes towards increase. Variable a thus cannot reach the value 0 once it reaches 1 or 2. This is also illustrated in Figure 2

The smallest inuence graph G(F

A ) of F A is given in Figure 2.1.
The state space graph of F A with the synchronous semantics in Figure 2.2 features states with simplied notation. Instead of writing the full state notation, e.g. (0, 1, 0) for x x x with x x x a = x x x c = 0 and x x x b = 1, we use a shorthand notation with the variable values only, e.g. 010, for simplicity. The same notation is also adopted in the state space graph of F A with the asynchronous semantics Figure 2.3. Since each asynchronous transition t changes value of a unique variable v = v (t), we additionally annotate the transitions with v (t) and the direction of the value change (+ for value increase andfor value decrease) in Figure 2.3. Observe that the choice of semantics has a signicant impact on the dynamics of the regulatory network. In the case of F A , the dierence is mainly caused by the variables a and b being regulated only by themselves, R(a) = {a} and R(b) = {b}. Thus, while in the asynchronous semantics either variable a or variable b is allowed to change value independently of each other, their value updates are synchronised under the synchronous semantics. Such synchronisation is responsible for the state space graph in Figure 2 Example 2.2. individual regulation functions f a , f b , f c , f d :

F B : x x x → ((x x x b ∨ x x x c ) ∧ ¬ (x x x d ) , ¬ (x x x b ) , x x x b , ¬ (x x x d )) F B is
f a : x x x → (x x x b ∨ x x x c ) ∧ ¬ (x x x d ) f b : x x x → ¬ (x x x b ) f c : x x x → x x x b f d : x x x → ¬ (x x x d )
Since all variable domains are Boolean, the regulation functions can be specied within the Boolean algebra.

The smallest inuence graph of F B is given in Observe that similarly to Example 2.1, the choice of semantics has a signicant impact on the dynamics of the network. In particular, while the state space graph of F B is a single connected component under asynchronous semantics, it consists of several components for the synchronous case. This can be partially attributed to the synchronisation of the variable b and d value updates disallowing transitions from states where the variables b and d have the same value to states in which their values dier and vice versa. Or equivalently using the individual regulation functions f a , f b , f c :

f a : b b b → 2 (1 -x x x a ) f b : b b b → ¬ (x x x) b f c : b b b → x x x a ∨ x x x b
The states depend on the variable domains and are thus identical for (F C , t) and F A , the regulatory function itself, however, is dened on Boolean vectors for Thomas networks, F C : B 3 → [0, 2] × B 2 . While the simplication to the Boolean domain is often desired, the resulting regulatory function is not as expressive as the original F A .

Indeed, one may note that although the regulatory function F C has been constructed to emulate F A , there are dierences in the dynamics of (F C , t) and F A . In particular, the value of variable c tends to decrease when x x x a = 0 regardless of the value of x x x b under F A . In the case of (F C , t), however, the value of variable c tends to increase when x x x b = 1 regardless of the value of x x x a . This is also illustrated in the state space graph of (F C , t) in Figure 2.7.

While the dierence on the target value of variable c in state (0, 1, 0), respectively (0, 1, 1), can be amended by a dierent Thomas network, the exact behaviour of F A cannot be replicated by any Thomas network with the same variables and inuence graph. This follows from the fact that the impact of variable b on variable c is dierent for each possible value of variable a (see Table 2.1). x x x a 0 0 1 1 2 2

x x x b 0 1 0 1 0 1 f c (x x x) 0 0 0 1 1 1

Chapter 3 Partial Order Semantics of Transition System Products

The state space of discrete regulatory networks is in the general case exponential in the dimension (number of variables). As such, discrete regulatory network analysis more often than not suers from combinatorial explosion. Gene regulatory networks and other biological models that constitute our primary application domain, however, are generally sparsely connected, leading to a high degree of concurrency. For this reason, it is natural to consider partial order semantics for discrete regulatory networks, in order to benet from a more compact representation of the state space.

A well established and extensively studied partial order semantics for transition systems exists for Petri nets in the form of unfoldings, or more precisely branching processes. Thanks to their high expressivity, the unfolding semantics of Petri nets can be used for any general transition system, including discrete regulatory networks [START_REF] Esparza | Unfoldings A Partial-Order Approach to Model Checking[END_REF]. Petri net unfolding therefore appears to be the ideal partial order semantics candidate to study in relation to discrete regulatory networks, as well as their parametric extension introduced in Chapter 4.

Petri Nets

Prior to starting on the unfolding itself, we briey recall the denition of a Petri net. A Petri net is a directed bipartite graph between places and transitions. Each place can hold any natural number of tokens. Marking is a function specifying the number of tokens for each place. A transition can re (is enabled) if a token is present in all places in the set of its in-neighbours (preset). Firing a transition consumes a token from each place in the preset and produces a token in each place in the set of out-neighbours (poset) of the transition 1 thus reaching a new marking.

In this work we limit ourselves to safe Petri nets. A Petri net is safe (or 1safe) if any place has at most one token at a time in any reachable marking. The limitation is well justied as domains of all the variables of discrete regulatory networks are guaranteed to be nite. A safe Petri can thus emulate a Discrete regulatory network by representing each value of each variable by a unique place. Similarly, we consider only nite Petri nets as the number of variables in discrete regulatory networks is also nite. Observe that this representation closely resembles the automata networks. Denition 3.1 (Petri Net). A (1-safe) Petri net is a tuple (P, T, W, M ), where P ∩ T = ∅ are nite sets of places and transition, respectively, W ⊆ (P × T ) ∪ (T × P ) is a set of arcs (edges) between places and transitions and M : P → B is the initial marking.

For each node x ∈ P ∪ T we write

• x = { y ∈ P ∪ T | (y, x) ∈ W } to denote the preset of x and x • = { y ∈ P ∪ T | (x, y) ∈ W } to denote the poset of x.
Note that for safe Petri nets, a marking M can be easily represented as a set of the places which contain a token, M = { p ∈ P | M (p) = 1 }. Remark further that (P ∪ T, W ) is a directed bipartite graph between places and transitions by denition and we employ it as such. Finally, we omit the initial marking from the denition of a Petri net where convenient. When omitted, we consider the Petri net with any initial marking which supports the safeness criteria.

Unfolding

Petri net unfolding relies on branching processes, a partial order semantics of Petri nets. Intuitively, a Petri net unfolding is similar to an unfolding of a graph. Given an initial vertex, any directed graph can be unfolded into a tree whose nodes represent the paths leading from the initial vertex. Petri nets can also be unfolded into labelled occurrence nets, a subclass of Petri nets benetting from simple structure similar to trees. The resulting occurrence net is called a branching process. The nodes of the branching process are labelled with places and transitions of the original Petri net. Unfolding of a Petri net may be stopped at any time, yielding many dierent branching processes. The Petri net unfolding refers to the maximal (generally innite) branching process which unfolds as much as possible.

Petri net unfolding diers from the unfolding of the state space graph of the underlying transition systems. The Petri net transitions are local they aect only a subset of the places of the Petri net, allowing for two or more transition to act independently of each other. Such transitions are called concurrent. By exploiting concurrency, Petri net unfolding results in a more compact structure. This is achieved by allowing "merging" concurrent branches within the unfolding. Petri net unfoldings therefore avoid representing equivalent branches twice at the expense of the tree structure. We give the formal notion of concurrency below, using the causal and conict relations on the nodes of a Petri net. Denition 3.2 (Causal Relation). Let x, y ∈ P ∪ T be two nodes of the Petri net (P, T, W, M 0 ).

x and y are in causal relation, x < y, if there exists a directed path from x to y in the graph (P ∪ T, W ). Denition 3.3 (Conict Relation). Let x, y ∈ P ∪ T be two nodes of the Petri net (P, T, W, M 0 ).

x and y are in conict relation, x # y, if there exist two paths (a, t 0 , . . . , x) and (a, t 1 , . . . , y) in the graph (P ∪ T, W ) leading to x and y, respectively, which start from the same place and subsequently diverge. Denition 3.4 (Concurrency Relation). Let x, y ∈ P ∪ T be two nodes of the Petri net (P, T, W, M 0 ).

x and y are in concurrency relation, x y, if ¬ (x < y), ¬ (y < x) and ¬ (x # y).

As the causal, conict and concurrency relations suggest, occurrence nets are indeed event structures. We adapt the usual notation and call the places of an occurrence net conditions (the b notation comes from Petri's original `Bedingungen') and the transitions of an occurrence net events.

Denition 3.5 (Occurrence Net). An occurrence net

O = (B, E, F ) is a Petri net such that: 1. ∀ b ∈ B, | • b| ≤ 1;
2. The causal relation is a partial order (O is acyclic);

For every

x ∈ B ∪ E, the set { y ∈ B ∪ E | y < x } is nite (O is nitely preceded); 4. ∀ b ∈ B, ¬ (b # b) (O is conict-free).
As aforementioned, a branching process is an occurrence net whose conditions and events are labelled by the places and transitions, respectively, of the original Petri net they represent. Unlike an occurrence net, the branching process is a "proper" Petri net, including the initial marking. To ease the notation, we override the min function for occurrence nets to produce the causalityminimal subsets of nodes, min : min((O)) is the initial marking of the branching process.

(B, E, F ) → { x ∈ B ∪ E | ∀ y ∈ B ∪ E, x ≤ y }.
Many (possibly innitely many) dierent branching processes may be constructed for a single Petri net. However, all the branching processes are constructed by the same process, unfolding, diering essentially on `how much' are they unfolded. Thanks to the acyclic structure of occurrence nets and thus branching processes, everything captured by a branching process which has been unfolded less (to a lesser depth) is also captured by a larger, `more unfolded', branching process (with larger depth). The smaller, `less unfolded', branching process can thus be called a prex of the larger branching process. Denition 3.7 (Branching Process Prex). Let (O, β) and (O , β ) be two branching processes of the same Petri net (P, T, W, M ).

Then, (O, β) is a prex of (O , β ) if the following conditions are satised: The notion of prexes gives a partial order structure on branching processes allowing us to formally capture the notion of `unfolding more'. In [START_REF] Engelfriet | Branching processes of petri nets[END_REF], it has been shown that there exists a unique maximal branching process of a Petri net, up to isomorphism. The maximal branching process is known as the Petri net unfolding. Denition 3.8 (Petri Net Unfolding). Let (P, T, W, M ) be a Petri net.

1. B ⊆ B , E ⊆ E and F ⊆ F (O is a subnet of O );
The unfolding of (P, T, W, M ) is a branching process (O, β) of (P, T, W, M ) such that any other branching process (O , β ) of (P, T, W, M ) is a prex of (O, β).

The unfolding of a Petri net is unique up to isomorphism.

Behavioural Equivalence

Although the unfolding of a Petri net is in the general case innite, it gives a complete acyclic representation of the behaviour of the original Petri net. The behavioural equivalence is captured by the isomorphism of (graph) unfoldings of the reachability graphs of a Petri net and its unfolding. In particular, the set of reachable markings of a Petri net contains exactly the markings obtained as β (M ) where M is reachable in the unfolding of the Petri net. Moreover, the possible ring sequences of the Petri net are also reproduced by the unfolding.

Given a marking M reachable in the unfolding, another marking M and a transition t ∈ T of the original Petri net, An event e ∈ E such that M e -→ M and β (e) = t exists if and only if β (M )

t -→ β (M ).
To capture the notion of behavioural equivalence of Petri nets and their branching processes formally, we introduce the concepts of conguration and cut, which represent the ring sequence and marking of the original Petri net, respectively, within the branching process. Denition 3.9 (Conguration). A conguration of a branching process

(O, β) is a set of events C ⊆ E such that: 1. e ∈ C =⇒ ∀ e < e, e ∈ C (C is causally closed); 2. ∀ e, e ∈ C, ¬ (e # e ) (C is conict-free).
Conguration is a set of events which can be red within one run of the branching process. More precisely, for each conguration there exists a ring sequence which allows each event in the conguration to execute exactly once starting from the natural initial state and respecting the causal relation. These ring sequences mirror the ring sequences of the original Petri net through the labelling function β.

Thanks to being conict free and causally closed, ring each event in a conguration results in a set of concurrent conditions (coset). Since we assume our input Petri net to be 1-safe, any two conditions b, b of a branching process such that β (b) = β (b ) are either in causal relation or conict. As such, β restricted to any coset of the branching process is injective. A maximal coset of a branching process is called a cut and corresponds to a marking of the original Petri net when projected via β. Of particular interest are then cuts produced by congurations, as they represent the reachable markings.

Denition 3.10 (Cut). A set of conditions

γ ⊆ B is a cut, if ∀ b, b ∈ γ, b b and ∀ b ∈ B \ γ, ∃ b ∈ γ, ¬ (b b ).
Given a nite conguration C, the set of conditions obtained by executing every event in C from the initial state is a cut of the following form

Cut (C) = (min((O)) ∪ C • ) \ • C.
We have already stated, in less formal terms, that a marking M is reachable in the original Petri net if and only if the unfolding of said Petri net contains a conguration C such that β (Cut (C)) = M . Petri net unfoldings therefore oer a comprehensive way to study the reachable state space of transition systems in a concurrency aware environment. This property is captured in the notion of completeness of branching processes. Denition 3.11 (Complete Branching Process). Let (P, T, W, M 0 ) be a Petri net.

We say that a branching process (O, β) of (P, T, W, M 0 ) is complete, if for every marking M reachable in (P, T, W, M 0 ), there exists a conguration C in (O, β), satisfying:

1. β (Cut (C)) = M (M is represented in the branching process); 2. For every transition t ∈ T enabled in M , there exists an event e ∈ E \ C such that β (e) = t and C ∪ {e} is a conguration of (O, β) (all enabled transitions can be reproduced in the branching process).

Complete Finite Prex

Unfolding of a Petri net is trivially a complete branching process, however, the applicability of Petri net unfoldings is largely impeded by the unfoldings being innite in the general case. As the reachable state space of a nite (safe) Petri net is also nite, envisioning a branching process which is both complete and nite is far from absurd. A technique to construct such a representation, called a complete nite prex of the unfolding, has been introduced by Kenneth L.

McMillan et al. [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF] and later improved by Javier Esparza et al. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], including an upper bound on the size of the constructed prex. The construction of the complete nite prex is based on identifying events, called cut-o events, at which the unfolding procedure can be stopped while guaranteeing the resulting branching process is complete. Determining whether an event can be declared a cut-o or not relies on a key observation about the isomorphism of extensions of congurations whose cuts have the same projection via β.

More precisely, let (O, β) be a branching process of a Petri net (P, T, W, M ) with a conguration C. We write ⇑C = (O , β ) to denote the part of (O, β) which `comes after' C.

Formally, O = (B , E , F ) where B = {b ∈ B \ • C | ∀ e ∈ C, ¬ (b # e)}, E = { e ∈ E \ C | ∀ e ∈ C,
¬ (e # e ) } and F , β are restrictions of F and β, respectively, to B ∪ E . Then, (O , β ) is a branching process of the Petri net (P, T, W, β (Cut (C))). In particular, if (O, β) is the unfolding of the Petri net (P, T, W, M ), (O , β ) is the unfolding of (P, T, W, β (Cut (C))). Thus, as the unfolding is unique up to isomorphism, for any two congurations C and C such that β (Cut (C)) = β (Cut (C )), we have ⇑C = I (⇑C ) where I is the isomorphism of the unfoldings.

We therefore have an isomorphism of conguration extensions provided the congurations reach the same marking (projected via β). This very isomorphism is exploited in the construction of the complete nite prex to determine which branches of the unfolding can be omitted without loss of completeness. To be able to apply the reasoning about isomorphic extensions directly to events, McMillan et al. [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF] associate a local conguration to each event. A local conguration of an event e is the minimal conguration which allows e to re. The unfolding procedure detailed in [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF][START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] constructs the branching process by including individual events and their posets one-by-one, selecting them from a set of possible extensions. A possible extension is an event of the unfolding whose preset is already included in the prex constructed thus far and which can therefore be included in the prex with no further modication necessary. Denition 3.13 (Possible Extension). Let (O, β) be the unfolding of a Petri net (P, T, W, M ) and let (O , β ) be a prex of the unfolding.

An event e ∈ E \ E is a possible extension of the prex

(O , β ) if and only if ∀ b ∈ • e ⊆ B, b ∈ B .
The set of all possible extensions of a prex (O , β ) is denoted by PE ((O , β )).

We now have all the tools needed to dene the cut-o criterion for events, which determines when to stop the unfolding procedure. Notice that the denition of a cut-o event depends heavily on the possible extension chosen. More precisely, which events are marked cut-o depends on the order in which the unfolding procedure adds events into the constructed branching process. The inuence of the order in which potential extensions are chosen is signicant enough to separate between complete and incomplete nite prexes while using the same cut-o criterion.

Esparza et al. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] identify a class of adequate orders on congurations of the branching process and prove that including events in an order that aligns with an adequate order on the local congurations guarantees the produced nite prex to be complete. A concrete example of an adequate order based on counting transitions of the conguration (as projected via β) in a manner similar to Parikh vectors is also provided in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. Denition 3.15 (Adequate Order). Let (O, β) be the unfolding of a Petri net (P, T, W, M ).

A (partial) order ≺ on the congurations of the unfolding (O, β) is an adequate order if it satises the following requirements:

1. ≺ is well founded. 2. Given two congurations C 0 , C 1 , C 0 ⊂ C 1 =⇒ C 0 ≺ C 1 . 3. Given two congurations C 0 , C 1 with β (Cut (C 0 )) = β (Cut (C 1 )) and C 0 ≺ C 1 , for any extension C ⊆ E \C 0 of the conguration C 0 , C 0 ∪C ≺ C 1 ∪I (C )
where I is the isomorphism of the extensions of C 0 and C 1 (unfoldings of (P, T, W, β (Cut (C 0 ))), respectively, (P, T, W, β (Cut (C 1 )))).

Esparza et al. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] further prove that if the used adequate order is also a total order, the number of non cut-o events in the constructed complete nite prex is bounded by the number of reachable states of the original Petri net. This result is underlined by an example of a total adequate order, which being an extension of the partial adequate order example again counts transitions, however, does so per the causal layers of the conguration, utilising the Foata normal form.

The complete nite prex is thus guaranteed to not be (asymptotically) larger than the reachable state space graph. Moreover, by keeping track of the concurrency in the system, unfoldings and their complete nite prexes benet from partial order reduction. The complete nite prex of a highly concurrent Petri net is therefore a very compact way to represent the reachable state space.

Part II Theoretical Contributions

Chapter 4

Parametric Regulatory Networks

In this chapter we introduce parametric regulatory networks, a parametric version of discrete regulatory networks where the exact regulation function is unknown represented by parameters.

Parametric regulatory networks are motivated by the lack of precise information on the complex regulations of genes and other molecular interaction in biological systems. Parametric regulatory networks aim at extracting the available regulation information while making no assumption on the unknown interactions. This is achieved by the use of parameters to represent the target values of the individual regulation functions, where unknown.

Standing for a target value of an individual regulation function, a parameter K v,x x x ∈ X v represents the value variable v takes in state x x x (f v (x x x)). Having a parameter for each variable and each state thus allows us to completely parametrise the regulation function, yielding a parametric regulatory network.

The parameters, as illustrated above, depend on the states of the network. It is thus easy to see that the total number of parameters is exponential in the number of variables, possibly limiting the tractability of parametric regulatory network analysis. However, each state and variable combination has to be used only if no prior knowledge is considered. Not only would such construction yield an impractical network, as mentioned in Section 2.2, the knowledge of one-onone interactions between biological species is far more widespread than the information on the complex regulation. It is therefore reasonable to consider an inuence graph to be part of the input.

Having an inuence graph allows us to restrict the parameters to the regulator states of individual variables without loss of information, much like we illustrated for regulation functions of discrete regulatory networks in Section 2.2. We therefore consider parameters of the form K v,ω ω ω ∈ X v to represent the target value of variable v in the regulator state ω ω ω ∈ Ω v . Note that using regulator states does not improve on the number of parameters asymptotically, as the number of regulator states is still exponential in the number of variables in the general case. The size of the exponent, however, depends on the number of regulators of individual variables rather than the total number of variables.

In practice, this allows sparse inuence graphs to exponentially decrease the number of regulator states, and by extension parameters, compared to the theoretical maximum.

Similarly to a discrete regulatory network, which can be dened by a single function, parametric regulatory network is fully captured by the parameters that build up said function. Unlike for discrete regulatory networks, however, where the variable domains are inherently captured within the domain of the function, we have to explicitly specify the variable domains, or parameter ranges, for parametric regulatory networks. Instead of listing all the parameters in the denition, we can simply utilise the inuence graph, which by itself fully characterises all the regulator states and thus the parameters.

Denition 4.1 (Parametric Regulatory Network). A parametric regulat-

ory network G d of dimension n is a directed graph G = (V, I) such that n = |V | coupled with a function d : v → X v mapping each variable (vertex) v ∈ V to the corresponding domain X v .
Denition 4.1 captures the most generic parametric regulatory network, corresponding to the most generic discrete regulatory network in Denition 2.1. All the restrictions we discussed for discrete regulatory networks in Section 2.3, whether being a restriction on the variable domains (Boolean and multivalued networks) or also on the regulation function (Thomas networks) can be lifted to the parametric regulatory networks.

In here we focus on the multivalued restriction only, as it subsumes the Boolean networks and is a prerequisite for the Thomas networks. As the variable domains of a multivalued network must come with a total order, they can always be represented as intervals of natural numbers (with zero), ranging from zero to a given maximum.

Denition 4.2 (Parametric Multivalued Network). A multivalued para-

metric regulatory network G m m m of dimension n is a directed graph G = (V, I) such that n = |V | coupled with a vector m m m = (m m m 1 , . . . , m m m n ) ∈ N n of maximum values for each variable.
An example of a parametric multivalued network is given in Example 4.1. One may observe that Denition 4.2 does not need any further modications to work for parametric Thomas networks as the restriction to Boolean regulatory states is pushed to the inference of the regulator states from the inuence graph.

In further work, we focus almost entirely on the modelling of gene regulatory networks. As the values of variables in a model gene regulatory network most commonly represent the concentration level of a protein or another molecule within the cell, models of gene regulatory networks are a prime example of networks whose variables are discrete abstractions of real-valued measurements. As mentioned in Section 2.3, the multivalued restriction of discrete regulatory networks, and in turn of parametric regulatory networks is highly suitable for these types of models. We will thus limit ourselves to parametric multivalued networks when referring to parametric regulatory networks in further text, unless explicitly states otherwise.

Parametrisations

Semantics of parametric regulatory networks are closely tied to the semantics of discrete regulatory networks. To be able to give a formal denition of parametric regulatory network semantics, we rst have to formalise the connection between parametric and discrete networks. Intuitively, by replacing the target values of the regulation function by parameters, parametric regulatory networks obtain freedom to choose between multiple dierent regulation functions to use. As such, a parametric regulatory network can be understood as a set of discrete regulatory networks sharing common topological properties (inuence graph and variable domains). To capture this relationship formally, we employ the concept of a parametrisation.

A parametrisation is essentially a function assigning each parameter a concrete value from the associated variable domain. For practicality of presentation, however, we prefer to think of a parametrisation as a vector of the values of individual parameters. To this end we assume an arbitrary but xed total order ≤⊆ Ω v × Ω v on the regulator states of each variable v ∈ V . Such an order is guaranteed to exist for each variable as there is always only nitely many regulator states, lexicographic order is a natural example. We then use the total order ≤ on regulator states in combination with the natural total order on variables, rst utilised in Section 2.2 to represent regulator states as vectors, to obtain a total order on parameters of a parametric regulatory network:

K v,ω ω ω K w,ω ω ω ∆ ⇐⇒ (v w) ∨ ((v = w) ∧ (ω ω ω ≤ ω ω ω ))
Using as a xed order on parameters, denition of a parametrisations as vectors becomes straightforward. Denition 4.3 (Parametrisation). Let G m m m be a parametric regulatory network.

Then, a parametrisation of G m m m is a vector P P P of length |Ω (G)| and of the following form:

P P P ∈ Π (ω ω ω,v)∈Ω(G) {0, . . . , m m m v } We further use P (G m m m ) = Π (ω ω ω,v)∈Ω(G) {0, . . . , m m m v } to denote the set of all parametrisations of the parametric regulatory network G m m m .
Finally, to ease notation, we write simply P P P v,ω ω ω instead of P P P Kv,ω ω ω to denote the value of parameter K v,ω ω ω in parametrisation P P P .

The parameters stand for the values of the regulation function at individual inputs. Thus, by specifying a concrete value for each parameter, a parametrisation eectively describes a full regulation function of a discrete regulatory network. A parametric regulatory network overlaid by a parametrisation thus denes a single discrete regulatory network, or parametrised network. Then, the multivalued network

F P P P = (f 1 , . . . , f n ) with f v : Ω v → {1, . . . , m m m v } f v : ω ω ω → P P P v,ω ω ω
for variable each v ∈ {1, . . . , n}, is the parametric regulatory network G m m m parametrised by P P P .

We can now expand on the previous intuition of parametric regulatory networks being sets of discrete regulatory networks. Although a simple union is unsatisfactory, as is elaborated in Section 4.2 where the formal denition of parametric regulatory network semantics is given, the semantics of parametric regulatory networks may be understood as an aggregation over the semantics of all the parametrised networks F P P P of all the parametrisations P P P ∈ P (G m m m ). The parametrisations of G m m m assign a value to each regulator state in Ω (G m m m ). This gives us three parameters for the variable a, two parameters for the variable b and six parameters for the variable c. All the parameters, their domains inherited from the respective variable and an example parametrisation P P P are given in Table 4.1

The total number of parametrisations of the parametric network G m m m is

3 3 ×2 2 ×2 6 = 6912 = |P (G m m m )|.
One should note that the inuence graph G is relatively sparse (variables a and b only have one regulator, |R(a)| = |R(b)| = 1), a trait common for inuence graphs of gene regulatory networks. The number of parametrisations is thus not particularly high among other graphs of similar size and with the same variable domains. As biological examples naturally tend to have higher numbers of variables, the enumeration of all parametrisations is not viable for most computations.

Parametrising G m m m by P P P gives us the discrete regulatory network, in our case multivalued network, F P P P dened as, F P P P (x x x) = P P P a,ωa(x x x) , P P P b,ω b (x x x) , P P P c,ωc(x x x)

= (x x x a + 1) mod 3, 1 -x x x b , x x x a + x x x b 2 = F A
coinciding with the denition of the multivalued network F A from Example 2.1.

P P P K a,(a=0) ∈ X a 1 K a,(a=1) 2 K a,(a=2) 0 K b,(b=0) ∈ X b 1 K b,(b=1) 0 K c,(a=0,b=0) ∈ X c 0 K c,(a=0,b=1) 0 K c,(a=1,b=0) 0 K c,(a=1,b=1) 1 K c,(a=2,b=0) 1 K c,(a=2,b=1) 1 Table 4.1: Table of all parameters of the parametric multivalued network G m m m
with their respective domains. An example assignment of parameter values, a parametrisation P P P is given in the last column.

Before proceeding with the denition of parametric regulatory network semantics, we introduce a partial order on the parametrisations of a parametric regulatory network. The parametrisation order is given as a piecewise order on vectors of length |Ω|. Then the parametrisation order on the parametrisations of G m m m is the partial order ≤ Gm m m dened as P P P ≤ Gm m m P P P ∆ ⇐⇒ ∀ (v, ω ω ω) ∈ Ω, P P P v,ω ω ω ≤ P P P v,ω ω ω for all P P P , P P P ∈ P (G m m m ).

The parametrisation order allows us to showcase some nice structural properties of the parametric regulatory network semantics and forms the basis for the abstract regulatory network semantics introduced in Section 4.3.

Concrete Semantics of Parametric Regulatory Networks

We have already given the intuition of the parametric regulatory network semantics being akin to union over the semantics of all possible parametrised networks. A simple union, however, allows the parametric regulatory network to behave according to a dierent parametrised network after each transition. This would, in particular, allow the same state visited more than once to be followed by a transition from dierent parametrised network semantics each time. To eliminate such inconsistent behaviour, instead of taking the union over all the semantics, we consider the union over all the behaviours (traces) of the parametrised networks. In other words, given a trace of the parametric regulatory network, there should exists at least one parametrisation P P P , such that the parametrised network F P P P can reproduce the trace.

In this section we examine the semantics of parametric regulatory networks in detail and give a formal denition satisfying the outlined consistency condition. To this end, for each transition in the union of parametrised network semantics, we identify parametrisations which enable said transition. Intuitively, a transition is enabled (allowed) by a parametrisation if it belongs to the semantics of the corresponding parametrised network. Then, for any transition t = (x x x, y y y) ∈ P P P ∈P(Gm m m) F P P P -→, the parametrisation set p (t) enabling t is dened as follows:

p (t) ∆ = P P P ∈ P (G m m m ) t ∈ F P P P -→
The denition of p (t) can be naturally extended to sets of transitions T as the intersection of p (t) for each transition t ∈ T .

Denition 4.7 (Parametrisation Set Enabling a Transition Set). Let

G m m m be a parametric regulatory network and let

F P P P
-→ be a multivalued network semantics of an arbitrary but xed type for all P P P ∈ P (G m m m ).

Then for any set of transitions T ⊆ P P P ∈P(Gm m m) F P P P -→, the parametrisation set enabling T is dened as follows:

p (∅) ∆ = P (G m m m ), p (T ) ∆ = t∈T p (t) if T = ∅.
By denition, all transitions in a set T belong to the semantics of the parametrised network F P P P (T ⊆ F P P P -→) if and only if P P P ∈ p (T ). Thus, taking T = π to be the set of transitions of a trace π over the union of parametrised network semantics, p ( π) becomes the set of all parametrisations P P P such that π is a trace of the parametrised network F P P P . Putting the consistency condition on parametric regulatory networks semantics outlined in the beginning of the section to formal terms, a trace π over the union of parametrised network semantics is a trace of the parametric regulatory network (is realisable

) if p ( π) = ∅.
By only considering realisable traces, we prevent the network from behaving dierently in the same state over the course of a single trace. However, separate traces are still allowed to display dierent behaviours in the same state. Parametric regulatory network semantics thus cannot be dened on the states alone. To this end, we annotate the states with an information on past choices to disqualify inconsistent behaviour. As the required information is independent of the order of past transitions, the set of transition taken, or its parametrisation set directly, is sucient. Denition 4.8 (Concrete Semantics of Parametric Regulatory Networks). Let G m m m be a parametric regulatory network of dimension n and let F P P P -→ ⊆ X × X be a multivalued network semantics of an arbitrary but xed type on state space X for all P P P ∈ P (G m m m ). x,y)) = ∅ ⇐⇒ ∃ P P P ∈ P, x x x

Then the parametric regulatory network semantics of G m m m is a relation

Gm m m -→ ⊆ X × 2 P(Gm m m) × X × 2 P(Gm m m) dened as follows: (x, P) × (y, P ∩ p ((x, y))) ∈ Gm m m -→ ∆ ⇐⇒ P ∩ p ((
F P P P -→ y y y
While all subsets of parametrisations are considered for the denition, not all necessarily have to appear in the resulting transitions. We write P

P Gm m m -→ ∆ =    p (T ) T ⊆ P P P ∈P(Gm m m) F P P P -→   
The parametric regulatory network semantics as given in Denition 4.8 can be constructed for arbitrary choice of multivalued network semantics. The generality is certainly welcome in making the parametric regulatory networks more versatile. Due to the unknown nature of the multivalued network semantics used, however, no information can be obtained on the properties of the parametrisation sets enabling the individual transitions. With no structural information, one is forced to represent the parametrisation sets explicitly, despite the number of parametrisations being asymptotically double exponential in the number of variables.

To be able to exploit structural information of the parametrisation sets enabling transitions, we limit ourselves to the most widely used semantics of multivalued networks, the generalised asynchronous semantics and its subsets, such as the synchronous and asynchronous semantics. As we are working purely with multivalued networks, we consider the generalised asynchronous semantics as adjusted for multivalued networks in Denition 2.9, taking advantage of the value changes by steps of size 1.

Generalised asynchronous semantics subsumes all the types of semantics we consider, however, the very versatility of generalised asynchronous semantics may obscure some kinetic information. E.g.

x x x F -→ x x x [v → x x x v + 1]
may refer to a variety of transitions. It may refer to a fully asynchronous transition updating the value of v only. However, it may as well refer to a transition that synchronously updates values of v and another variable, or several variables, u such that F u (x x x) = x x x u . We therefore introduce S :

Gm m m -→ gen → 2 {1,...,n} to annotate each transition t ∈ Gm m m -→
gen with a set of all variables updated synchronously, even if their value is not allowed to change.

Consider now the inconsistent behaviour, where a variable v rst increases and then decreases value in a repeatedly visited state x x x. With the generalised asynchronous semantics and its subsets, we can characterise this inconsistency directly on the level of parametrisations rather than transitions. When the value increases, a regulation function with increasing value in state x x x is required f v (x x x) > x x x v , or in terms of parametrised networks, P P P v,ωv(x x x) > x x x v . On the other hand, the decrease uses f v (x x x) < x x x v , or P P P v,ωv(x x x) < x x x v . Any such inconsistency can thus be characterised by a conict on a single parameter value. Similar distinction can be made for inconsistencies when a variable v once changes value and once remains constant under the same transition t with v ∈ S (t).

A value changing (or in synchronous updates staying the same) during each transition can thus be interpreted as making a decision on the value of a particular parameter. Working only with parametrisations which comply with the previously made choices thus guarantees a consistent behaviour. We identify such compatible sets of parametrisations similarly to Denition 4.6 for transitions.

Denition 4.9 (Parametrisation Set Directing Variable Evolution).

Let G m m m be a parametric regulatory network and let Then, for any parameter K v,ω ω ω and any value i ∈ {1, . . . , m m m v }, the parametrisation sets p (K v,ω ω ω ≥ i) and p (K v,ω ω ω ≤ i) of all parametrisations that prevent v from decreasing, respectively increasing, value in ω ω ω are dened as follows:

p (K v,ω ω ω ≥ i) ∆ = { P P P ∈ P (G m m m ) | P P P v,ω ω ω ≥ i } p (K v,ω ω ω ≤ i) ∆ = { P P P ∈ P (G m m m ) | P P P v,ω ω ω ≤ i }
Although the inconsistent behaviour is fully preventable by following the decisions made on single parameter values, the decisions themselves are tied to transitions. Therefore, by grouping the parametrisation sets sharing parameter value, representing the choices of a individual parameter values, by the respective transition, we obtain a renement of Denition 4.6: Then, for any transition t = (x x x, y y y) ∈ P P P ∈P(Gm m m )

F P P P -→,

P

where K ((x x x, y y y)) is the set of all the parametrisation sets restricting individual parameters: The parametrisation set p (t) enabling the transition t is the set of all parametrisations P P P ∈ P (G m m m ) with t ∈

K ((x x x, y y y)) ∆ = p K v,ωv(x x x) ≥ y y y v v ∈ D (x x x, y y y) ∧ y y y v = x x x v + 1 ∪ p K v,ωv(x x x) ≤ y y y v v ∈ D (x x x, y y y) ∧ y y y v = x x x v -1 ∪ p K v,ωv(x x x) ≥ x x x v , p K v,ωv(x x x) ≤ x x x v v ∈ S (t) \ D (x x x, y y y)
F P P P -→.
As t is a transition of the generalised asynchronous semantics, in fact t is fully synchronous (S (t) = V ), we get:

p (t) = p (K a,2 ≤ 1) ∩ p (K b,0 ≥ 1) ∩ p (K c,20 ≤ 1) ∩ p (K c,20 ≥ 1)
by Denition 4.10. The parametrisation set p (t) is therefore the set of all parametrisations P P P ∈ P (G m m m ) with P P P a,2 ≤ 1, P P P b,0 ≥ 1 and P P P c,20 = 1.

|p (t)| = 1152 is still too many parametrisations to list. To give an example, the parametrisation P P P = (K a,0 = 1, K a,1 = 2, K a,2 = 0, K b,0 = 1, K b,1 = 0, K c,00 = 0, K c,01 = 0, K c,10 = 0, K c,11 = 1, K c,20 = 1, K c,21 = 1) from Example 4.1 belongs to p (t), P P P ∈ p (t). This is also documented by the transition t = (201, 111) appearing in the state space graph of F A = F P P P with the synchronous semantics in Figure 2.2.

By limiting ourselves to generalised asynchronous semantics and its subsets, we have obtained important link between transitions and the properties of the sets of parametrisations that enable them. This connection is heavily exploited in the following Section 4.3.

Abstract Semantics of Parametric Regulatory Networks

The parametric regulatory network semantics as per Denition 4.8 rely on annotating the states with parametrisation sets. As the number of parametrisations is exponential in the number of regulation states and thus in general double exponential in the number of variables, explicit representation of the parametrisation sets is practically infeasible. To combat the computational limitation, we introduce an abstract version of the parametric regulatory network semantics which allows us to represent the parametrisation sets without explicit enumeration of the parametrisations. To this end we rely on the structural connection between transitions and parametrisations that enable them, highlighted in Denition 4.10, maintaining the restriction to semantics

Gm m m -→ ⊆ Gm m m -→ gen .
To illustrate how the connection between transitions and parametrisations can be utilised to avoid explicit enumeration of parametrisations, consider the parametrisation set P (G m m m ) as a lattice (P (G m m m ) , ≤ Gm m m ) with the parametrisation order from Denition 4.5. We rst remark that there exists unique

≤ Gm m m -maximal parametrisation 1 1 1 Gm m m = n i=1 {m m m i } |Ωi| ∈ P (G m m m ), as well as a ≤ Gm m m -minimal parametrisation 0 0 0 Gm m m = {0} |Ω| ∈ P (G m m m ).
As such, the lattice

(P (G m m m ) , ≤ Gm m m ) is bounded.
Consider now a parametrisation P P P dened as follows for each (u, ω ω ω ) ∈ Ω:

P P P u,ω ω ω = i if (u, ω ω ω ) = (v, ω ω ω) m m m u otherwise
for arbitrary (v, ω ω ω) ∈ Ω and i ∈ {0, . . . , m m m v }. For any such parametrisation, we can construct the principal ideal P = P P P ∈ P (G m m m ) P P P ≤ Gm m m P P P of the lattice (P (G m m m ) , ≤ Gm m m ) with P P P as the principal element. Since all parameters except K v,ω ω ω are at their maximum values in P P P , any parametrisation P P P ∈ P (G m m m ) with P P P v,ω ω ω ≤ i is necessarily smaller or equal to P P P according to the parametrisation order, P P P ≤ Gm m m P P P , as it assigns smaller or equal value to each variable. We can therefore describe the principal ideal of P P P simply as P = P P P ∈ P (G m m m ) P P P v,ω ω ω ≤ i = p (K v,ω ω ω ≤ i), which is equivalent to the denition of the parametrisation set preventing variable value increase.

Symmetrically, consider the parametrisation P P P to be of the following form for each (u, ω ω ω ) ∈ Ω:

P P P u,ω ω ω = i if (u, ω ω ω ) = (v, ω ω ω) 0 otherwise
for arbitrary (v, ω ω ω) ∈ Ω and i ∈ {0, . . . , m m m v }. Then, the principal lter (the dual of a principal ideal) with P P P as the principal element is the set P = P P P ∈ P (G m m m ) P P P ≥ P P P = P P P ∈ P (G m m m )

P P P v,ω ω ω ≥ i = p (K v,ω ω ω ≥ i),
which is equivalent to the parametrisation set preventing variable value decrease by symmetrical reasoning. We know that any ideal or lter of a lattice is a convex sublattice. Additionally, a principal ideal or a principal lter of a bounded lattice is also bounded with the principal element as the maximum, respectively minimum. Any parametrisation set directing variable evolution is thus a bounded convex sublattice of the lattice (P (G m m m ) , ≤ Gm m m ) of all parametrisations. A bounded convex sublattice is uniquely identied by its minimum and maximum elements. The set of parametrisations ∅ = P ∈ P Gm m m -→ can thus be solely represented by the minimum and maximum elements, 0 0 0, 1 1 1 ∈ P, respectively. We refer to bounded convex sublattices of the lattice of all parametrisations represented by their minimum and maximum as parametrisation lattices. By abuse of notation we write P P P ∈ [0 0 0, 1 1 1] for any P P P ∈ P where (P,

≤ Gm m m ) = [0 0 0, 1 1 1].
Observe that Denition 4.11 imposes no restriction on the minimum and maximum parametrisations 0 0 0, 1 1 1. Instead, any [0 0 0, 1 1 1] with 0 0 0 > Gm m m 1 1 1 is interpreted as the empty lattice ∅ = (∅, ≤ Gm m m ) which is also a parametrisation lattice. In fact, ∅ is the only parametrisation lattice which is not bounded and convex. On the other hand, all bounded and convex sublattices of the lattice of all parametrisations (P (G m m m ) , ≤ Gm m m ) are expressible as parametrisation lattices using their bounds. This corresponds to every bounded convex sublattice [0 0 0, 1 1 1] being uniquely given as an intersection of a principal ideal, whose principal element is the maximum 1 1 1, with a principal lter, whose principal element is the minimum 0 0 0.

The parametrised lattices, being essentially bounded convex sublattices of (P (G m m m ) , ≤ Gm m m ) allow us to represent more than just parametrisation sets directing variable evolution. In particular, parametrisation sets enabling a transition are built from parametrisation sets directing variable evolution using only intersections. Similarly parametrisation sets enabling transition sets are built from parametrisation sets enabling transition using only intersections. As a non-empty intersection of bounded convex sublattices is a bounded convex sublattice, any non-empty parametrisation set enabling a transition set,

∅ = P ∈ P Gm m m
-→ , coupled with the parametrisation order is a bounded convex sublattice of the lattice (P (G m m m ) , ≤ Gm m m ) of all parametrisations. Any parametrisation set enabling a transition set thus forms a parametrisation lattice when coupled with the parametrisation order.

Hence, the parametrisation order allows us to easily capture parametrisation sets of interest by parametrisation lattices, represented by only two elements. We utilise parametrisation lattices to dene an abstraction of parametrisation sets. In formal terms, the abstraction can be captured using a Galois connection [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. Denition 4.12 (Parametrisation Set Abstraction). Let G m m m be a parametric regulatory network.

The parametrisation set abstraction of G m m m is dened by the following Galois connection 1 The inmum 0 0 0 = p(t) and supremum 1 1 1 = p(t) are given by the bounds on the parameters dening the parametrisation sets in K (t). We list the parametrsations 0 0 0 and 1 1 1 in Table 4.2.

α γ : α : 2 P(Gm m m) → P (G m m m ) γ : P (G m m m ) → 2 P(Gm m m) α : ∅ → ∅ γ : (P, ≤ Gm m m ) → P α : P → [ P , P ] for P = ∅ K a,0 K a,1 K a,2 K b,0 K b,1 0 0 0 = p(t) 0 0 0 1 0 1 1 1 = p(t) 2 2 1 1 1 K c,00 K c,01 K c,10 K c,11 K c,20 K c,21 0 0 0 = p(t) 0 0 0 0 1 0 1 1 1 = p(t) 1 1 1 1 1 1
p (t) = p (K a,2 ≤ 1) ∩ p (K b,0 ≥ 1) ∩ p (K c,20 ≥ 1).
The backwards concretisation γ ([0 0 0, 1 1 1]) is simply the parametrisation lattice [0 0 0, 1 1 1] stripped of the lattice structure (order). As such, P P P ∈ γ ([0 0 0, 1 1 1]) ⇐⇒ ∀ (v, ω ω ω) ∈ Ω, 0 0 0 v,ω ω ω ≤ P P P v,ω ω ω ≤ 1 1 1 v,ω ω ω . By foregoing all 0 valued parameters in 0 0 0 and maximum valued parameters in 1 1 1, we get P P P ∈ γ ([0 0 0, 1 1 1]) ⇐⇒ P P P a,2 ≤ 1 ∧ P P P b,0 ≥ 1 ∧ P P P c,20 ≥ 1, which is exactly when P P P ∈ p (t). Thus γ (α (p (t))) = p (t), the abstraction α (p (t)) is exact.

We use the parametrisation set abstraction to dene the abstract semantics of parametric regulatory networks. Instead of annotating the states of the network by explicit parametrisation sets, abstract semantics utilise parametrisation lattices, which are fully specied by only two parametrisations. The state annotations thus end up being of linear rather than exponential size in the number of parameters. Then the abstract parametric regulatory network semantics of G m m m is a 1 We drop p (K c,20 ≤ 1) from the intersection as 1 = m m mc giving us p (K c,20 ≤ 1) = P (Gm m m).

relation

Gm m m -→ abs ⊆ X m m m × P (G m m m ) × X m m m × P (G m m m ) dened as follows: (x, [0 0 0, 1 1 1]) × (y, [0 0 0, 1 1 1] ∩ α (p ((x, y)))) ∈ Gm m m -→ abs ∆ ⇐⇒ ∃ P P P ∈ P (G m m m ), x F P P P -→ y ∧ ([0 0 0, 1 1 1] ∩ α (p ((x, y))) = ∅)
To ease notation, we write p (t) = α (p (t)) to denote the abstract parametrisation set enabling a transition t ∈ P P P ∈P(Gm m m ) F P P P -→ and p (T ) = α (p (T )) to denote the abstract parametrisation set enabling a transition set T ⊆ P P P ∈P(Gm m m)

F P P P -→.
The Galois connection in Denition 4.12 captures arbitrary set of parametrisations P ⊆ P (G m m m ). In general, such parametrisation set P may not have a minimum, P / ∈ P or maximum, P / ∈ P (P is not bounded) or it may not be convex, with respect to the parametrisation order ≤ Gm m m . The abstraction thus constructs the smallest bounded convex cover of P in the form of parametrisation lattice [ P , P ]. Therefore, in the general case, the abstraction is an over-approximation of the parametrisation set.

As illustrated in the beginning of the section, however, the parametrisation sets enabling transition sets, P ∈ P

γ (α (P)) = P α (γ ([0 0 0, 1 1 1])) = [0 0 0, 1 1 1]
Proof. We rst prove γ (α (P)) = P.

Let us assume P = ∅ rst. By denition we have:

γ (α (P)) = γ P , P = P P P ∈ P (G m m m ) P ≤ Gm m m P P P ≤ Gm m m P
The direction P ⊆ [ P , P ] and thus also P ⊆ γ ([ P , P ]) is trivial. Since (P, ≤ Gm m m ) is an intersection of bounded convex sublattices of (P (G m m m ) , ≤ Gm m m ), it is also a bounded convex sublattice. Therefore, by boundedness, P has a minimal and a maximal parametrisation, P , P ∈ P. Consequently, by convexity, we have ∀ P P P ∈ P (G m m m ), P ≤ Gm m m P P P ≤ Gm m m P =⇒ P P P ∈ P. Thus, γ ([ P , P ]) ⊆ P and γ (α (P)) = P.

The case for empty set follows directly from denition:

γ (α (∅)) = γ (∅) = ∅
Similarly, α (γ ([0 0 0, 1 1 1])) = [0 0 0, 1 1 1] also follows directly from denition:

α (γ ([0 0 0, 1 1 1])) = α ({ P P P ∈ P (G m m m ) | 0 0 0 ≤ Gm m m P P P ≤ Gm m m 1 1 1 }) = [0 0 0, 1 1 1]
Thanks to Theorem 4.1 we can guarantee that the abstract parametrisation sets represent the exactly same parametrisations as their concrete counterpart. As such, usage of the abstract semantics of parametric regulatory networks introduces no false positives (over-approximation), nor false negatives (underapproximation) when compared against the concrete semantics. In fact, the concrete and abstract semantics of parametric regulatory networks are equivalent, provided states are only annotated by the parametrisation sets enabling transition sets, P P P ∈ P Then, for an arbitrary parametrisation lattice [0 0 0, 1 1 1] ∈ P (G m m m ) and arbitrary states x x x, y y y ∈ X m m m :

Gm m m -→ .
(x x x, [0 0 0, 1 1 1]) Gm m m -→ abs y y y, [0 0 0, 1 1 1] ∩ p ((x x x, y y y)) ⇐⇒ ∃ P P P ∈ [0 0 0, 1 1 1], x x x F P P P -→ y y y
The abstract parametrisation sets as used within the abstract semantics of parametric regulatory networks, are therefore a perfect equivalent for their concrete counterparts, while avoiding any explicit enumeration of parametrisations. The practical applicability of the abstract semantics, however, relies on computing several operations on the abstract parametrisation sets without resorting to enumeration of parametrisations. The principal operations required are the computation of p (T ∪ {t}) form p (T ) and membership checking P P P ∈ [0 0 0, 1 1 1]. While, membership checking is realisable without enumeration of parametrisations directly by denition, Then, for arbitrary transition sets T, T ∈ P P P ∈P(Gm m m)

P P P ∈ [0 0 0, 1 1 1] ⇐⇒ 0 0 0 ≤ Gm m m P P P ≤ Gm m m 1 1 1 ⇐⇒ ∀ (v, ω ω ω) ∈ Ω, 0 0 0 v,ω ω ω ≤ P P P v,ω ω ω ≤ 1 1 1 v,ω
F P P P -→: p (T ∪ T ) = p (T ) ∩ p (T )
Computation of p (T ∪ {t}) from p (T ) can thus be conducted by the operation of intersection. Intersections of bounded convex sublattices in general are easy to capture using the meet and join operators. In particular, the minimum of the intersection is the join of the minimums and the maximum of the intersection is the meet of the maximums. By including the empty lattice ∅, the set of parametrisation lattices merely become closed under intersection as opposed to general bounded convex sublattices. This is captured formally in Proposition 4.1. Then, [0 0 0, 1 1 1] ∩ 0 0 0 , 1 1 1 = 0 0 0 ∨ 0 0 0 , 1 1 1 ∧ 1 1 1 .

Proof.

P P P ∈ [0 0 0, 1 1 1] ∩ 0 0 0 , 1 1 1 ⇐⇒ (0 0 0 ≤ Gm m m P P P ≤ Gm m m 1 1 1) ∧ 0 0 0 ≤ Gm m m P P P ≤ Gm m m 1 1 1 ⇐⇒ 0 0 0 ∨ 0 0 0 ≤ Gm m m P P P ≤ Gm m m 1 1 1 ∧ 1 1 1 ⇐⇒ P P P ∈ 0 0 0 ∨ 0 0 0 , 1 1 1 ∧ 1 1 1
To fully capture the computation of p (T ∪ {t}) from p (T ), we also need to be able to infer p (t). Recall, however, that p (t) is already an intersection of the parametrisation sets in K (t). Thus, by Corollary 4.1.3, p (t) can be computed as the intersection of α (P) for each P ∈ K (t). The maximums and minimums of each p (K v,ω ω ω ≥ i) and p (K v,ω ω ω ≤ i) are obvious from denition:

p(Kv,ω ω ω ≥i) = 1 1 1 Gm m m p(Kv,ω ω ω ≤i) = Π (u,ω ω ω )∈Ω i if (u, ω ω ω ) = (v, ω ω ω) m m m u otherwise p(Kv,ω ω ω ≥i) = Π (u,ω ω ω )∈Ω i if (u, ω ω ω ) = (v, ω ω ω) 0 otherwise p(Kv,ω ω ω ≤i) = 0 0 0 Gm m m
We formalise the computation of p (T ∪ {t}) from p (T ) by a narrowing operator σ t2 . -→ be arbitrary.

Then, the narrowing operator σ t for transition t is a function dened as:

σ t : P (G m m m ) → P (G m m m ) σ t : p (T ) = [0 0 0, 1 1 1] →     Π (v,ω ω ω)∈Ω max(({ i | p (K v,ω ω ω ≥ i) ∈ K (t) } ∪ {0 0 0 v,ω ω ω })), Π (v,ω ω ω)∈Ω min(({ i | p (K v,ω ω ω ≤ i) ∈ K (t) } ∪ {1 1 1 v,ω ω ω }))    
where T ⊆ P P P ∈P(Gm m m)

F P P P -→ is arbitrary set of transitions.
It is easy to see that the time complexity of the narrowing σ t for arbitrary transition t is linear in the number of parameters, O (Ω).

Chapter 5 Inuence Constraints as Global Constraints on Parametrisations

The abstract semantics of parametric regulatory networks introduced in Section 4.3 are proven to be exact by Theorem 4.1 and the resulting corollaries. Theorem 4.1 is, however, only applicable if all considered parametrisation sets belong to P Gm m m -→ . The parametrisations of the form p (T ) ∈ P Gm m m -→ for some set of transitions T only allow us to dierentiate parametrisations solely on their ability to replicate past transitions. As discussed in Section 2.3, however, information on the monotonicity of isolated inuences, Denitions 2.10, 2.11, is often available in the literature. In this chapter we formalise the inuence monotonicity properties as global constraints on the admissible parametrisations and relax the claim in Theorem 4.1 to obtain similar results for parametrisation sets constrained by the presence of inuence properties.

We introduced the inuence monotonicity as properties of multivalued networks, Denitions 2.10, 2.11. In this section, however, we consider the inuence monotonicity to be given as an input and use it as monotonicity constraints on parametrisations [START_REF] Bernot | Semantics of biological regulatory networks[END_REF]. Intuitively, a parametrisation satises a monotonicity constraint, if the associated parametrised network has the corresponding monotonicity property. More precisely, a P P P satises a positive, respectively negative, monotonicity constraint on an inuence (u, v), if an increase in the value of u cannot cause the decrease, respectively increase, in the value of v, and vice-versa in the parametrised network F P P P . The monotonicity properties of this form are expressible as inequalities on parameter values, we therefore dene monotonicity constraints anew, without reliance on the parametrised networks.

We additionally include a constraint called observability, used to emphasise necessity of some inuences. A parametrisation P P P satises an observability constraint on inuence (u, v), if there exists a state such that the sole change in the value of u forces a change in the value of v in the parametrised network F P P P . An observability constraint therefore requires the associated inuence to be part of the minimal inuence graph. Similarly to the monotonicity constraints, an observability constraint is expressible as inequalities on the parameter values, and can be dened on the parametrisations themselves. Then, an inuence constraint r is tuple r = (e, ) ∈ I × {+1, -1, o}.

We call a constraint of the form (e, +1) a positive monotonicity constraint on inuence e. Similarly, a constraint of the form (e, -1) a negative monotonicity constraint on inuence e. Finally, a constraint of the form (e, o) is an observability constraint on inuence e.

To reduce notation nesting, we write (u, v, ) = (e, ) for any inuence e = (u, v).

Set of all inuence constraints of an inuence graph

G = (V, I) is denoted R (G) ⊆ I × {+1, -1, o}. An inuence constraint set R (G) is well-formed if for any inuence e ∈ I, {(e, +1) , (e, -1)} ⊆ R (G).
The inuence constraints can be considered labels on the edges of the inuence graph. We then consider the set of all constraints present for the given inuence graph to restrict the parametrisation space. Inuence constraints are not exclusive, meaning each inuence can have multiple constraints. This applies in particular to combinations of monotonicity and observability constraints, as having both monotonicity constraints on a single inuence is, within our framework, equivalent to having no such inuence. We thus consider only well-formed constraint sets further on, to avoid such pathological cases.

Concrete Constrained Semantics of Parametric

Regulatory Networks Denition 5.1 xes the notation for the inuence constraints, however, does not provide the semantics. The semantics of the monotonicity constraints follow the monotonicity properties in Denitions 2.10, 2.11. Without the use of parametrised networks, a parametrisation P P P ∈ P (G m m m ) satises a positive monotonicity constraint (u, v, +1), if:

∀ ω ω ω ∈ Ω v , ∀ i ∈ {1, . . . , m m m u }, P P P v,ω ω ω[u →i] ≥ P P P v,ω ω ω[u →i-1]
i.e., the sole increase of the activator u cannot cause a decrease of the regulated variable v.

Similarly, a parametrisation P P P ∈ P (G m m m ) satises a negative monotonicity constraint (u, v, -1), if:

∀ ω ω ω ∈ Ω v , ∀ i ∈ {1, . . . , m m m u }, P P P v,ω ω ω[u →i] ≤ P P P v,ω ω ω[u →i-1]
i.e., the sole increase of the inhibitor u cannot cause an increase of the regulated variable v.

Finally, a parametrisation P P P ∈ P (G m m m ) satises an observability constraint (u, v, o), if:

∃ ω ω ω ∈ Ω v , ∃ i ∈ {1, . . . , m m m u }, P P P v,ω ω ω[u →i] = P P P v,ω ω ω[u →i-1]
i.e., there exists a state where the sole change of the regulator u triggers a change of the regulated variable v.

As we are generally interested in all parametrisations that satisfy a particular constraint, we dene sets of parametrisation restricted to inuence constraints.

Denition 5.2 (Concrete Parametrisation Set Satisfying an Inuence Constraint). Let G m m m be a parametric regulatory network and let r ∈ I × {+1, -1, o} be an arbitrary inuence constraint.

Then, the set of parametrisations P r satisfying the inuence constraint r is dened as follows:

P (u,v,+1) ∆ = P P P ∈ P (G m m m ) ∀ ω ω ω ∈ Ω v , ∀ i ∈ {1, . . . , m m m u } , P P P v,ω ω ω[u →i] ≥ P P P v,ω ω ω[u →i-1] P (u,v, -1)
∆ = P P P ∈ P (G m m m ) ∀ ω ω ω ∈ Ω v , ∀ i ∈ {1, . . . , m m m u } , P P P v,ω ω ω[u →i] ≤ P P P v,ω ω ω[u →i-1] P (u,v,o) ∆ = P P P ∈ P (G m m m ) ∃ ω ω ω ∈ Ω v , ∃ i ∈ {1, . . . , m m m u } , P P P v,ω ω ω[u →i] = P P P v,ω ω ω[u →i-1]
The denition naturally extends to sets of inuence constraints by intersection.

Denition 5.3 (Concrete Parametrisation Set Satisfying Inuence Constraints).

Let G m m m be a parametric regulatory network and let R ⊆ I × {+1, -1, o} be a well-formed inuence constraint set.

Then, the set of parametrisations satisfying the inuence constraints in R is dened as follows:

P R ∆ = r∈R P r
The parametrisation restrictions imposed by inuence constraints are no longer constraints on a single parameter, but rather inequality constraints on parameter values. The intersection based construction, however, aligns with the representation of parametrisation sets enabling a transition set. Indeed, intersections are sucient to express the combination in the form of parametrisation sets enabling a transition set while satisfying a constraint set as well. The seamless inclusion of inuence constraints in the parametrisation sets enabling transition sets facilitates the denition of inuence constraint aware semantics for parametric regulatory networks. The inuence constraints are, moreover, dened for inuence graph and are therefore global for the whole parametric regulatory network. The same applies to the resulting parametrisation set satisfying the constraint set. Thanks to this, instead of using parametrisation sets as per Denition 5.4 explicitly, the constrained semantics of parametric regulatory network can be dened to the same eect simply by restricting the concrete semantics to subsets of the parametrisation set satisfying the inuence constraints. Then, the constrained semantics of the parametric regulatory network G m m m is the relation

Gm m m -→ R ⊆ X m m m × 2 P R × X m m m × 2 P R dened as: (x, P ∩ P R ) Gm m m -→ R (y, P ∩ P R ) ∆ ⇐⇒ (x, P) Gm m m -→ (y, P ) ∧ P ∩ P R = ∅
As illustrated by Denition 5.5, inuence constraints can only limit the semantics of parametric regulatory networks and therefore cannot introduce new behaviour.

Abstract Constrained Semantics of Parametric Regulatory Networks

Introduction of inuence constraints can, often signicantly, reduce the number of parametrisations that need to be considered. However, the induced reduction of parametrisation space is not asymptotic. The parametrisation sets thus not only remain exponentially large in the general case, the structure of the parametrisation sets imposed by the inuence constraints is highly nontrivial.

Considering only the monotonicity constraints, P R(G) can be used to enumerate all monotonic Boolean functions of a given dimension. Even counting monotonic Boolean functions, however, is known to be a hard problem [START_REF] Stephen | Counting inequivalent monotone boolean functions[END_REF].

To avoid explicit representation of parametrisation sets, we rely once again on the abstract semantics of parametric regulatory networks (Denition 4.13). We implement the inuence constraints r ∈ R (G) by the means of a narrowing operator σ r on the parametrisation lattices. While the narrowing operator produces over-approximation of the concrete parametrisation sets, we show the over-approximation to be optimal in terms of bounded convex sublattices.

Due to fundamental dierences in the nature of the monotonicity and observability constraints (universal versus existential quantication), we treat the denition of σ r separately depending on r being monotonicity of observability constraint. First, let us consider monotonicity constraints. Then, the narrowing operator σ r is dened as:

σ r : P (G m m m ) → P (G m m m ) σ r : [0 0 0, 1 1 1] → [f 0 * (0 0 0) , f 1 * (1 1 1)]
where the functions f 0 , f 1 : P (G m m m ) → P (G m m m ) are dened as follows:

f 0 : P P P → P P P ∨ ω ω ω∈Ωv

P P P (v, ω ω ω) → P P P v,ω ω ω[u →ω ω ωu-s]
f 1 : P P P → P P P ∧ ω ω ω∈Ωv

P P P (v, ω ω ω) → P P P v,ω ω ω[u →ω ω ωu+s]
Since both of the functions f 0 , f 1 are monotonic in ≤ Gm m m , the xed points f 0 * , f 1 * are guaranteed to exist for any input. Moreover, the restriction of parameter values by f 0 , f 1 happens progressively in the direction of the monotonicity constraint on the inuence (u, v). E.g. assuming (u, v) to be an activation, s = +1, increasing the lower bound of ω ω ω of v by f 0 leads to increase of the lower bound also for the ω ω ω [u → ω ω ω u + 1] in the subsequent iteration of f 0 , if necessary, etc. We formalise this concept by the means of a partial order on regulator states of individual variables, called monotonicity order. Denition 5.7 (Monotonicity Order). Let G m m m be a parametric regulatory network, R a well-formed inuence constraint set and v ∈ V and arbitrary variable of G m m m .

Then, the monotonicity order on Ω v is the partial order v,R ⊆ Ω v × Ω v dened as:

ω ω ω v,R ω ω ω ∆ ⇐⇒ ∀ (u, v, s) ∈ R, sign (ω ω ω u -ω ω ω u ) ∈ {0, s}
We write ω ω ω v,R ω ω ω if and only if ω ω ω and ω ω ω are not comparable according to v,R . This is the case notably when ω ω ω u = ω ω ω u for some

u ∈ R(v) such that the inuence (u, v) is not monotonic in R, {(u, v, +1) , (u, v, -1)} ∩ R = ∅.
To ease notation, we write simply v instead of v,R when the entire inuence constraint set R = R (G) is considered.

In terms of the monotonicity order, the narrowing operator simply adjusts the parameter values in 0 0 0 to maximum value of the parameters associated with v,{(u,v,+1)} -smaller regulator states and the parameter values in 1 1 1 to minimum value of v,{(u,v,+1)} -larger regulator states. An analogical operation with the maximums and minimum reversed is done for negative monotonic inuence constraints. More formally, the monotonicity order allows for an alternative denition of the monotonicity inuence constraint narrowing:

σ (u,v,s) [0 0 0, 1 1 1] ∆ =        ≤ Π (w,ω ω ω)∈Ω max { ω ω ω ∈Ωv | ω ω ω v,{(u,v,s)} ω ω ω } (0 0 0 v,ω ω ω ) if w = v 0 0 0 w,ω ω ω otherwise , ≤ Π (w,ω ω ω)∈Ω min { ω ω ω ∈Ωv | ω ω ω v,{(u,v,s)} ω ω ω } (1 1 1 v,ω ω ω ) if w = v 1 1 1 w,ω ω ω otherwise       
Note that by iterating over ω ω ω ∈ Ω v in increasing, respectively decreasing, direction of v,{(u,v,s)} , the maximum, respectively minimum, can be computed on the run, rather than explicitly for each parameter. The computation of the whole narrowing σ r is thus linear in the number of parameters of the variable

v (O (|Ω v |)).
Since the narrowing operator only computes minimums and maximums, it is easily composable with narrowing operators for other monotonicity inuence constraints on the same variable. It is enough to take the smaller of the minimums, respectively larger of the maximums, obtained for two dierent monotonicity constraints and the same parameter. This comparison is moreover automatically included once monotonicity order over both of the monotonicity constraints is considered. Indeed, replacing the order v,{(u,v,s)} in the above denition by v,R for arbitrary R ⊆ R (G) is enough to compute the narrowing operator of all monotonicity constraints in R at the same time, while keeping the linear complexity. Of particular interest is then the narrowing operator σ v using the full monotonicity order v which allows us the compute the monotonicity narrowing for all monotonicity inuence constraints on the variable v at the same time.

Unlike for the monotonicity inuence constraints, which introduce universal inequality constraints on the parameter values for individual regulator states, the observability inuence constraint is existential, yielding no global inequality constraints on parameter values. Indeed, to ensure observability, the parametrisations which do not satisfy the inuence constraint have to be removed on individual basis. Due to the nature of the abstract parametrisation lattices, namely the convexity, it is impossible to individually treat parametrisations unless they happen to be the lower or upper bounds, 0 0 0 and 1 1 1 respectively. As such, any parametrisations 0 0 0 < Gm m m P P P < Gm m m 1 1 1 that do not satisfy the observability inuence constraints are ignored, at the cost of over-approximation.

The narrowing operator σ (u,v,o) therefore translates into checking whether the observability inuence constraint (u, v, o) is satised under both of the extreme cases of 0 0 0 and 1 1 1. By negation of the observability inuence constraint condition as given in Denition 5.2, (u, v, o) is not satised under 0 0 0, respectively 1 1 1, if for each ω ω ω ∈ Ω v and each i ∈ {0, . . . , m m m u }:

0 0 0 v,ω ω ω = 0 0 0 v,ω ω ω[u →i] respectively: 1 1 1 v,ω ω ω = 1 1 1 v,ω ω ω[u →i]
Once the inuence (u, v) is determined to be unobservable under 0 0 0, respectively 1 1 1, increasing 0 0 0 v,ω ω ω , respectively decreasing 1 1 1 v,ω ω ω , for any ω ω ω ∈ Ω v ensures the observability of (u, v) under the new parametrisation. In fact, once a value is changed for one regulator state, all inuences are guaranteed to be observable under the new parametrisation unless values for each other regulator state diering only in the value of the corresponding regulator are adjusted to match the new value. This introduces a measure of distance between unobservable parametrisations, formally captured in Lemma 5.1.

Lemma 5.1 (Unobservable Parametrisation Distance). Let G m m m be a parametric regulatory network, r = (u, v, o) ∈ R (G) an arbitrary observability inuence constraint and P P P ∈ P (G m m m ) be such that the inuence (u, v) is not observable under P P P .

Then, for any ω ω ω ∈ Ω v , i ∈ {0, . . . , P P P v,ω ω ω -1, P P P v,ω ω ω + 1, . . . , m m m v } and all u ∈ R(v), the inuence (u , v) is observable under

P P P = P P P [(v, ω ω ω) → i].
Proof. Let ω ω ω ∈ Ω v , i ∈ {0, . . . , m m m v } be arbitrary such that P P P v,ω ω ω = i.

Let P P P = P P P [v, ω ω ω → i] denote the modied parametrisation and ω ω ω denote a regulator state of variable v diering from ω ω ω in the value of u,

ω ω ω = ω ω ω [u → ω ω ω u + j] where j = 1 if ω ω ω u = 0 -1 otherwise
For the inuence constraint r we get P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω and thus P P P ∈ P r . Now let us assume v has at least two (observable) inuences and let r = (w, v, o) ∈ R (G) be arbitrary such that w = u.

First, we introduce two additional regulator states. The regulator state ω ω ω identical to ω ω ω up to the value w and the regulator state ω ω ω identical to ω ω ω up to the value of w,

ω ω ω = ω ω ω [w → ω ω ω w + k] ω ω ω = ω ω ω [w → ω ω ω w + k] where k = 1 if ω ω ω w = 0 -1 otherwise
We use the four regulator states ω ω ω, ω ω ω, ω ω ω and ω ω ω to prove the inuence (w, v) is indeed observable under P P P . To do this, we need to show either P P P v,ω ω ω = P P P v,ω ω ω or P P P v,ω ω ω = P P P v,ω ω ω as both ω ω ω, ω ω ω and ω ω ω, ω ω ω dier only in the value of w. The proof also relies on the analogous proximity of ω ω ω, ω ω ω and ω ω ω , ω ω ω , which dier only in the value of u.

We know P P P v,ω ω ω = i and P P P v,ω ω ω = P P P v,ω ω ω . Thus, if i = P P P v,ω ω ω , the result is trivial.

Let us therefore assume P P P v,ω ω ω = i = P P P v,ω ω ω . Since (u, v) is not observable under P P P , P P P / ∈ P r , we have P P P v,ω ω ω = P P P v,ω ω ω and P P P v,ω ω ω = P P P v,ω ω ω . P P P only diers from P P P in the value of ω ω ω. We can thus expand the prior observation to obtain P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω and P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω . By our assumption, P P P v,ω ω ω = P P P v,ω ω ω , we obtain the coveted P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω = P P P v,ω ω ω .

While Lemma 5.1 guarantees that a single value change is sucient to ensure observability under 0 0 0, respectively 1 1 1, for all inuences of v, the value change may not be desirable for every ω ω ω ∈ Ω v . We therefore identify regulator states that are open for value change (or simply open) as regulator states ω ω ω ∈ Ω v such that increasing 0 0 0 v,ω ω ω , respectively decreasing 1 1 1 v,ω ω ω , does not break any monotonicity constraints in R (G) and does not result in an empty parametrisation lattice. Denition 5.8 (Open Regulator State For Observability Enforcement). Let G m m m be a parametric regulatory network of dimension n and let R (G) be a well-formed set of inuence constraints. Let further [0 0 0, 1 1 1] ∈ P (G m m m ) and v ∈ {1, . . . , n} be arbitrary.

Then a regulator state

ω ω ω ∈ Ω v is open to value increase in [0 0 0, 1 1 1] if 0 0 0 v,ω ω ω < 1 1 1 v,ω ω ω and for all ω ω ω ∈ Ω v such that ω ω ω v ω ω ω, 0 0 0 v,ω ω ω > 0 0 0 v,ω ω ω .
Similarly, a regulator state Then, the narrowing operator σ r is dened as:

ω ω ω ∈ Ω v is open to value decrease in [0 0 0, 1 1 1] if 0 0 0 v,ω ω ω < 1 1 1 v,ω ω ω and for all ω ω ω ∈ Ω v such that ω ω ω ≺ v ω ω ω, 1 1 1 v,ω ω ω < 1 1 1 v,ω ω ω . We write O + v ([0 0 0, 1 1 1]) = { ω ω ω ∈ Ω v | 0 0 0 v,ω ω ω < 1 1 1 v,ω ω ω ∧ ∀ ω ω ω v ω ω ω, 0 0 0 v,ω ω ω > 0 0 0 v,ω ω ω } to denote the set of all regulator states of v open to value increase in [0 0 0, 1 1 1]. Ana- logically, O - v ([0 0 0, 1 1 1]) = { ω ω ω ∈ Ω v | 0 0 0 v,ω ω ω < 1 1 1 v,ω ω ω ∧ ∀ ω ω ω ≺ v ω ω ω, 1 1 1 v,ω ω ω < 1 1 1 v,ω ω ω } is
σ r : P (G m m m ) → P (G m m m ) σ r : [0 0 0, 1 1 1] → ∅ if (0 0 0 / ∈ P r ∧ O + v ([0 0 0, 1 1 1]) = ∅) ∨ (1 1 1 / ∈ P r ∧ O - v ([0 0 0, 1 1 1]) = ∅) 0 0 0 , 1 1 1 otherwise where 0 0 0 = 0 0 0 [(v, ω ω ω) → 0 0 0 v,ω ω ω + 1] if 0 0 0 / ∈ P r ∧ O + v ([0 0 0, 1 1 1]) = {ω ω ω} 0 0 0 otherwise 1 1 1 = 1 1 1 [(v, ω ω ω) → 1 1 1 v,ω ω ω -1] if 1 1 1 / ∈ P r ∧ O - v ([0 0 0, 1 1 1]) = {ω ω ω} 1 1 1 otherwise
Determining the observability of the inuence u, v under 0 0 0 and 1 1 1 has linear complexity with respect to the number of parameters of variable v (O (|Ω v |)). By iterating over regulator states in Ω v in decreasing order of v , respectively increasing order of v , the open regulator state set

O + v ([0 0 0, 1 1 1]), respectively O - v ([0 0 0, 1 1 1]
), can be computed with the same linear complexity. Computing the narrowing operator σ (u,v, ) thus has complexity in O (|Ω v |) for both monotonicity and observability inuence constraints.

By aggregating the narrowing operators for all the individual inuence constraints we obtain a global narrowing operator σ R(G) . As observability narrowing respects the monotonicity constraints thanks to the use of the monotonicity order, the global narrowing is denable simply as a function composition.

σ R(G) = (u,v,o)∈R(G) σ {(u,v,o)} • v∈{1,...,n} σ v
The constrained abstract semantics are dened using a combination of the inuence constraint narrowing and the transition narrowing, Denition 4.14. Then the constrained abstract parametric regulatory network semantics of

G m m m is a relation Gm m m -→ R(G)•abs G m m m ⊆ X m m m × P (G m m m ) × X m m m × P (G m m m ) dened as follows: (x, [0 0 0, 1 1 1]) × y, 0 0 0 , 1 1 1 ∈ Gm m m -→ R(G)•abs G m m m ∆ ⇐⇒ ∃ t ∈ Gm m m -→ abs , t = (x, [0 0 0, 1 1 1]
)

F P P P -→ abs y, 0 0 0 , 1 1 1 ⊇ 0 0 0 , 1 1 1 ∧ 0 0 0 , 1 1 1 = σ R(G) • σ t ([0 0 0, 1 1 1])
To ease notation, we use p R (T ) to denote the over-approximation of the set of all parametrisations enabling all transitions in T while satisfying the inuence constraints in R,

p R (T ) = t∈T (σ R • σ t ) ([P (G m m m )]) = σ R • t∈T σ t ([P (G m m m )])
The constrained abstract semantics of parametric regulatory networks result in an over-approximation of the parametrisation sets, introducing false positives into reachable state space. We can show, however, that the false positives cannot introduce spurious behaviour, i.e. no transition is included unless it is supported by at least one true positive parametrisation. This is a natural consequence of the tightness of the abstraction. Then for arbitrary set of transitions T ⊆

Gm m m -→ R•abs , p R (T ) is the smallest convex cover of p R (T ), p R (T ) = [p R (T )].
Proof. Note that marking an inuence of a variable v ∈ {1, . . . , n} as either monotonic or observable does not inuence other variables u = v. We therefore conduct the proof for single variable only, allowing us to limit our attention to regulator states ω ω ω ∈ Ω v while maintaining universal applicability.

We conduct the proof of p R (T ) = [p R (T )] by mathematical induction on the transition set T . This corresponds to the actual application of the narrowing operators, as transitions are generally explored one at a time.

Base step (T = ∅):

By denition, we have p R (∅) = σ R ([P (G m m m )]). σ r for either monotonicity or observability constraints only restricts the parametrisation lattice in case r is not satised under 0 0 0 or 1 1 1. In the beginning, [0 0 0, 1 1 1] = [P (G m m m )] with 0 0 0 v,ω ω ω = 0 and 1 1 1 v,ω ω ω = m m m v for every ω ω ω ∈ Ω v . Thus, any monotonicity constraint on inuence of v is necessarily satised under both 0 0 0 and 1 1 1.

Let us now consider there exists at least one observability constraint r = (u, v, o) ∈ R on an inuence of variable v. The inuence (u, v) is not observable under 0 0 0 and 1 1 1 and the parametrisation set may thus get restricted by σ r .

The result of σ r depends on the sets of regulator states open for observability enforcement. All regulator states are assigned the value 0 in 0 0 0, O + v ([0 0 0, 1 1 1]) thus contains exactly the v -maximal regulator states. Surely, at least one such regulator state must exist, giving us σ r ([0 0 0, 1 1 1]) = ∅. Similarly, the O - v ([0 0 0, 1 1 1]) contains exactly the v -minimal regulator states. By denition, σ r ([0 0 0, 1 1 1]) = [0 0 0, 1 1 1], if there are at least two v -maximal and at least two v -minimal regulator states. Since the v is always isomorphic to its dual, the reverse v , the number of v -minimal and v -maximal regulator states is always the same. Moreover, regulator states are only incomparable with each other in the v , if they dier on a value of a non-monotonic regulator. Both The number of vmaximal and v -minimal regulator states is therefore exactly 2 to the power of the number of non-monotonic inuences of v. As such, σ r ([0 0 0, 1 1 1]) = [0 0 0, 1 1 1] if and only if all the inuences of v are monotonic.

Assuming thus, there exists a non-monotonic inuence (w, v) ∈ I, p (∅) = [P (G m m m )] = [0 0 0, 1 1 1]. Having two distinct v -maximal elements ω ω ω, ω ω ω ∈ Ω v gives us two parametrisations P P P = 0 0 0 [ω ω ω → 1] and P P P = 0 0 0 [ω ω ω → 1]. Both P P P , P P P ∈ p R (∅) as the satisfaction of monotonicity constraints comes from ω ω ω, ω ω ω being v -maximal and the satisfaction of observability constraints is thanks to Lemma 5.1. The construction for v -minimal regulator states and 0 0 0 is symmetrical, thus [p R (∅)] = [0 0 0, 1 1 1] = p (∅).

Let us now consider the situation where the v -maximal element ω ω ω ∈ Ω v is unique. Then, ω ω ω is also the only regulator state open for value increase for the purpose of the observability constraint narrowing, O + v ([0 0 0, 1 1 1]) = {ω ω ω}. Symmetrically, the unique v -minimal element ω ω ω is also the unique regulator state open for value decrease, O - v ([0 0 0, 1 1 1]) = {ω ω ω}. The inuence constraint narrowing therefore restricts both the minimal and maximal parametrisations,

σ R ([0 0 0, 1 1 1]) = [0 0 0 [v, ω ω ω → 1] , 1 1 1 [v, ω ω ω → m m m v -1]].
For the concrete set, we know 0 0 0, 1 1 1 / ∈ p R (∅) due to the observability inuence constraint. Let now P P P ∈ p R (∅) be any parametrisation such that P P P v,ω ω ω > 0 for some ω ω ω ∈ Ω v . We know ω ω ω v ω ω ω thanks to all inuences being monotonic giving us P P P v,ω ω ω ≥ P P P v,ω ω ω > 0. A symmetrical argument can be made for ω ω ω always being smaller than the maximum m m m v . Thus,

[p R (∅)] = [0 0 0 [v, ω ω ω → 1] , 1 1 1 [v, ω ω ω → m m m v -1]] = p R (∅). Induction hypothesis: p R (T ) = [p R (T )] for any set of transitions T such that |T | ≤ k where k ∈ N 0 . We now show p R (T ∪ {t}) = [p R (T ∪ {t})]
for arbitrary transition t / ∈ T . We prove the lattice equality as the two lattices being mutual sublattices of each other. Moreover, as both of the lattices use the same order and elements from the same superset, the sublattice relation is equivalent to subset relation, we thus liberally treat the lattices as sets throughout the proof.

σ v • σ t p R (T ) .
Monotonicity constraint narrowing only imposes restrictions if the constraint is not satised by either of the limit parametrisations generating the abstract parametrisation set. Since all parametrisations in p R (T ) satisfy the monotonicity constraints, only prior restriction of a v = v (t) parameter K v,ω ω ω for some ω ω ω ∈ Ω v by σ t may cause the necessary condition. It is therefore enough to consider σ v .

Let now [0 0 0, 1 1 1] = σ t p R (T ) and 0 0 0 ,

1 1 1 = σ v ([0 0 0, 1 1 1]) = v∈{1,...,n} σ v • σ t p R (T )
be the relevant parametrisation lattices and P P P ∈ p R (T ∪ {t}) arbitrary. We now prove 0 0 0 w,ω ω ω ≤ P P P w,ω ω ω ≤ 1 1 1 w,ω ω ω for each (w, ω ω ω ) ∈ Ω.

Since p R (T ∪ {t}) ⊆ [0 0 0, 1 1 1], we have ∀ (w, ω ω ω ) ∈ Ω, 0 0 0 w,ω ω ω ≤ P P P w,ω ω ω ≤ 1 1 1 w,ω ω ω . By denition, 0 0 0 w,ω ω ω = 0 0 0 w,ω ω ω and 1 1 1 w,ω ω ω = 1 1 1 w,ω ω ω for any (w, ω ω ω ) with w = v.

Let thus ω ω ω ∈ Ω v be such that 0 0 0 v,ω ω ω < 0 0 0 v,ω ω ω . Such restriction may only be due to 0 0 0 v,ω ω ω , giving us ω ω ω v ω ω ω and 0 0 0 v,ω ω ω = 0 0 0 v,ω ω ω . We know all inuence constraints are satised under P P P . ω ω ω v ω ω ω thus mandates P P P v,ω ω ω ≥ P P P v,ω ω ω ≥ 0 0 0 v,ω ω ω .

Let us now consider ω ω ω ∈ Ω v to be such that 1 1 1 v,ω ω ω > 1 1 1 v,ω ω ω . Again, the restriction is due to 1 1 1 v,ω ω ω , giving us ω ω ω ≺ v ω ω ω and 1 1 1 v,ω ω ω = 1 1 1 v,ω ω ω . And for P P P to satisfy the inuence constraints, P P P v,ω ω ω ≤ P P P v,ω ω ω ≤ 1 1 1 v,ω ω ω .

All parametrisations in the concrete set p R (T ∪ {t}) therefore t within the connes of 0 0 0 , 1 1 1 . The construction of the convex cover preserves the minimal and maximal values of the individual parameters, giving us the coveted

[p R (T ∪ {t})] ⊆ 0 0 0 , 1 1 1 = v∈{1,...,n} σ v • σ t p R (T ) .
We now conclude the soundness proof by showing that the observability constraint based restrictions are also reected in the concrete parametrisation set,

[p R (T ∪ {t})] ⊆ (u,v,o)∈R σ {(u,v,o)} • v∈{1,...,n} σ v • σ t p R (T ) = p R (T ).
Keeping to the 0 0 0 , 1 1 1 notation, we use 0 0 0 ,

1 1 1 = (u,v,o)∈R σ {(u,v,o)} 0 0 0 , 1 1 1
to denote the parametrisation lattice after applying observability constraint restrictions. Similarly to monotonicity, observability narrowing also imposes restriction only if the constraint is not satised under one, or both, of the limit parametrisations. Moreover, thanks to Lemma 5.1, observability narrowing only changes the value of at most one parameter per limit parametrisation.

Let thus ω ω ω ∈ Ω v be the unique regulator state whose associated parameter value gets changed in the minimum parametrisation, 0 0 0 v,ω ω ω = 0 0 0 v,ω ω ω + 1. By denition, ω ω ω is the only regulator state open to value increase,

O + v ([0 0 0, 1 1 1]) = {ω ω ω}. O + v ([0 0 0, 1 1 1]
) being a singleton guarantees the equality 0 0 0 v,ω ω ω = 1 1 1 v,ω ω ω for a number of regulator states ω ω ω ∈ Ω v . Namely, any ω ω ω v ω ω ω or ω ω ω v ω ω ω, as well as any ω ω ω ≺ v ω ω ω such that 0 0 0 v,ω ω ω < 0 0 0 v,ω ω ω . requisite for the action of the observability constraint narrowing. Assuming, [p R (T ∪ {t})] = ∅, we need to prove

O + v ([0 0 0, 1 1 1]) = {ω ω ω}, respectively O - v ([0 0 0, 1 1 1]) = {ω ω ω}.
Let us further assume the observability constraint r is not satised under 0 0 0 . For any parametrisation P P P ∈ 0 0 0 , 1 1 1 with P P P v,ω ω ω = 0 0 0 v,ω ω ω we know P P P / ∈ p R (T ∪ {t}). In other words, by Lemma 5.1, at least one monotonicity constraint is not satised under any parametrisation P P P ∈ 0 0 0 , 1 1 1 diering from P P P in the value of exactly one parameter other than K v,ω ω ω . This can be translated to all v -maximal regulator states ω ω ω = ω ω ω having 0 0 0 v,ω ω ω = 1 1 1 v,ω ω ω . Moreover, this applies separately for all levels of 0 0 0 values. We thus get 0 0 0

v,ω ω ω = 1 1 1 v,ω ω ω for each v -maximal ω ω ω = ω ω ω in ω ω ω ∈ Ω v 0 0 0 v,ω ω ω = k for each k ∈ N.
The v -maximal ω ω ω = ω ω ω being value locked, 0 0 0 v,ω ω ω = 1 1 1 v,ω ω ω , by denition guarantees that any ω ω ω ≺ v ω ω ω such that 0 0 0 v,ω ω ω = 0 0 0 v,ω ω ω is also value locked. This thus, in particular, holds for any ω ω ω v ω ω ω, ω ω ω v ω ω ω and ω ω ω ≺ v ω ω ω such that 0 0 0 v,ω ω ω < 0 0 0 v,ω ω ω , giving us the coveted O + v ([0 0 0, 1 1 1]) = {ω ω ω}. The proof for the observability constraint r not being satised under 1 1 1 is symmetrical. For any parametrisation P P P ∈ 0 0 0 , 1 1 1 with P P P v,ω ω ω = 1 1 1 v,ω ω ω we know P P P / ∈ p R (T ∪ {t}). Again by Lemma 5.1, all v -minimal regulator states ω ω ω = ω ω ω must have 0 0 0 v,ω ω ω = 1 1 1 v,ω ω ω . This ultimately guarantees, the value is locked for any

ω ω ω ≺ v ω ω ω, ω ω ω v ω ω ω and ω ω ω v ω ω ω such that 1 1 1 v,ω ω ω > 1 1 1 v,ω ω ω , giving us the coveted O - v ([0 0 0, 1 1 1]) = {ω ω ω}.
Finally, let us consider [p R (T ∪ {t})] = ∅. Following the same line of reasoning with the use of Lemma 5.1, we know the value is locked,

0 0 0 v,ω ω ω = 1 1 1 v,ω ω ω , for each v -maximal ω ω ω ∈ ω ω ω ∈ Ω v 0 0 0 v,ω ω ω = k , respectively v -minimal ω ω ω ∈ ω ω ω ∈ Ω v 1 1 1 v,ω ω ω = k ,

Examples

In this section, we give an example of a parametric regulatory network with inuence constraints, Example 5.1, to showcase how inuence constraints restrict the set of possible parametrisations.

We further give several examples of how the narrowing operators for inuence constraints restrict the parametrisation lattices. Finally, let G {1} 4 be a parametric regulatory network dened on the inuence graph G with Boolean variable domains. Unconstrained, 2 8 ×2 2 ×2 2 ×2 2 = 16384 = P G {1} 4 parametrisations are possible for the parametric regulatory network G {1} 4 . By introducing R (G ), the number of compatible parametrisations decreases signicantly. In some instances, such as the monotonicity minimal and maximal regulator states of a Boolean variable with all incoming inuences monotonic and at least one also observable, the values of some parameters are xed by the inuence constraint set R (G ). In our case, this applies to the all four variables a, b, c, d. Indeed, for any parametrisation P P P ∈ P R(G ) , P P P a,001 = 0, P P P a,110 = 1, P P P b,0 = 1, P P P b,1 = 0, P P P c,0 = 0, P P P c,1 = 1, P P P d,0 = 1 and P P P d,1 = 0. Example 5.4 describes in detail how these constraints can be obtained by the means of the narrowing operator.

Observe The remaining parametrisations are then all the non-constant monotonic Boolean functions on three variables which constitute the parameters of variable a. While enumerating all monotonic Boolean functions is generally not trivial [START_REF] Stephen | Counting inequivalent monotone boolean functions[END_REF], with only three variables we arrive at 18 dierent non-constant monotonic Boolean functions and thus, parametrisations P R(G ) = 18.

The dierent parametrisations in P R(G ) can also be represented as cuts of the Hasse diagram [START_REF] Birkho | Lattice Theory[END_REF] of the monotonicity order, or more precisely of the lattice of all regulator states of a variable with the monotonicity order, into two (in the Boolean case) or more convex sublattices. We give the Hasse diagram of the lattice (Ω a , a ) in Figure 5.2. For simplicity, we use the value concatena-

K c,00 K c,01 K c,10 K c,11 K c,20 K c,21 0 0 0 0 1 0 0 0 0 1 1 1 1 1 1 1 1 1
Table 5.1: The values of variable c parameters in the minimum and maximum parametrisations 0 0 0, 1 1 1.

tion shorthand for the regulator states in the Hasse diagram. To illustrate how a parametrisation corresponds to a cut in the Hasse diagram, we mark some of the regulator states in Figure 5.2 in bold. The cut is then the set of all edges from a bold to non-bold vertex and the corresponding parametrisation assigns the value 0 to all non-bold regulator states and the value 1 to all bold regulator states. The parametrisation P P P in Figure 5.2 is thus such that the parametric Boolean network G {1} 4 parametrised by P P P is exactly the Boolean network

F B from Example 2.2.
Of note is also the structure of the Hasse diagram in Figure 5.2. The Hasse diagram of the monotonicity order of Boolean network variable always takes the form of a hypercube, or several disjoint hypercubes in case not all incoming inuences are monotonic, of dimension given by the number of monotonic regulations.

Example 5.2. Consider the parametric regulatory network G m m m introduced in Example 4.1 and a set of inuence constraints R (G) = {(a, c, +1)}. Let [0 0 0, 1 1 1] be a parametrisation lattice such that the variable c parameter values in minimum and maximum parametrisations correspond to the Table 5.1.

As the maximum parametrisation 1 1 1 assign the same value 1 to each regulator state of variable c, the sole monotonicity constraint (a, c, +1) is trivially satised under 1 1 1. On the other hand, the monotonicity constraint (a, c, +1) is not satised under the minimum parametrisation 0 0 0, or any other paramet-

K c,00 K c,01 K c,10 K c,11 K c,20 K c,21 0 0 0 0 0 1 1 1 1 1 1 1 1 0 1 1 1 1
Table 5.2: The values of variable c parameters in the minimum and maximum parametrisations 0 0 0, 1 1 1.

risation P P P ∈ [0 0 0, 1 1 1] such that P P P c,11 = 0 or P P P c,21 = 0, due to

(a = 0, b = 1) ≺ c (a = 1, b = 1) ≺ c (a = 2, b = 1).
The narrowing operator σ (a,c,+1) assigns each parameter in the minimum parametrisation the maximum value across all monotonicity smaller regulator states. To illustrate we give the monotonicity order c in Figure 5.3 as the Hasse diagram of the lattice (Ω c , c ). The regulator states in Figure 5.3 are annotated by their value in the minimum parametrisation 0 0 0. In our case, the value 0 0 0 c,01 = 1 is the maximum for all three regulator states with b = 1. Let further [0 0 0, 1 1 1] be a parametrisation lattice such that the variable c parameter values in minimum and maximum parametrisations correspond to the Table 5.2.

The two regulator states

For any parametrisation P P P ∈ [0 0 0, 1 1 1] such that P P P c,00 = 0 we have P P P / ∈ P (b,c,o) as the value of variable b has not direct impact on the target value of variable c under any such P P P . In particular, the minimum parametrisation 0 0 0 is one such parametrisation. We show in detail how σ (b,c,o) restricts the parametrisation lattice, to eliminate the false positives in this case.

As there are no monotonicity constraints, all regulator states are c -minimal and c -maximal at the same time. The regulator states open for increase or decrease are thus exactly the regulator states with dierent value in 0 0 0 and 1 1 1.

K c,00 K c,01 K c,10 K c,11 K c,20 K c,21 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1
Table 5.3: The values of variable c parameters in the minimum and maximum parametrisations 0 0 0, 1 1 1.

In our case O

+ v ([0 0 0, 1 1 1]) = O - v ([0 0 0, 1 1 1]) = {(a = 0, b = 0)}.
The existence of a single open regulator state is therefore satised for both 0 0 0 and 1 1 1. The observability constraint (b, c, o) is, however, satised under the maximum parametrisation 1 1 1 ∈ P (b,c,o) and 1 1 1 is not restricted. On the other hand, the minimum parametrisation 0 0 0 / ∈ P (b,c,o) is restricted, obtaining a new parametrisation 0 0 0 = 0 0 0 [c, 00 → 1] and σ (b,c,o) ([0 0 0, 1 1 The existence of unique regulator states open for increase and decrease, respectively is thus satised. Moreover the observability constraint (b, c, o) is not satised under either 0 0 0 and 1 1 1. Both minimum and maximum parametrisations therefore get restricted by σ (b,c,o) ([0 0 0, 1 1

1]) = [0 0 0 [c, 21 → 1] , 1 1 1 [c, 00 → 0]].
Chapter 6

Unfolding Semantics of Parametric Regulatory Networks

In this chapter we introduce partial order semantics for parametric regulatory networks. We achieve this by lifting the Petri net unfoldings introduced in Chapter 3 to parametric regulatory networks. As the dynamics of parametric regulatory networks are in essence transition systems, it follows that one can represent parametric regulatory networks by the means of Petri nets. Rather than unfolding a Petri net obtained by conversion of a parametric regulatory network, however, we introduce a modied version of the unfolding procedure which acts on the parametric regulatory networks directly in spite of the output staying a Petri net. Unfolding the parametric regulatory networks allows us to keep the model concise and thus easier to process thanks to the ability to represent the transitions symbolically.

Being a partial order semantics, the true benet of unfoldings shows especially in highly concurrent systems. While the relative sparsity of inuence graphs of most gene regulatory network models promises high degree of concurrency, this is only true for asynchronous semantics. Allowing synchronous transitions essentially introduces new interdependencies into the inuence graph, prohibiting concurrent execution of transitions. To harness the full benet of the partial order reduction, we assume all parametric regulatory network use strictly asynchronous semantics throughout the chapter.

Parametric Regulatory Network Unfolding

In this section we discuss the modications necessary to the Petri net unfolding procedure to be applicable to parametric regulatory networks.

Before the denition of parametric regulatory network unfolding procedure itself, using Petri nets to represent the unfoldings of parametric regulatory networks requires a slight extension of the model. Namely, the unfolding is dependant on the initial marking, however, parametric regulatory networks provide no equivalent notion. We therefore annotate the parametric regulat- We then say the unfolding is conducted from the initial condition x x x Gm m m , PGm m m .

To simplify notation, we write x x x, P instead of x x x Gm m m , PGm m m where G m m m is obvious from context.

We proceed with the (initialised) parametric regulatory network unfolding denition by reiterating the unfolding denition for petri nets in Chapter 3.

Just like for Petri nets, the parametric regulatory network unfolding consists of the same core construction in the form of an occurrence net. Thanks to the occurrence net denition, Denition 3.5, being simplied by omitting the initial marking, no modications are necessary for application to parametric regulatory networks. Labelling of the occurrence nets by the β function is, however, strongly dependant on the structure of the original model. We thus redene the branching process for parametric regulatory networks using a new labelling function β which relates to parametric regulatory networks rather than Petri nets. 1 If unfoldings from several initial states are desired, one may benet from including an "extra selection layer" in the unfolding. This layer would serve to allow the initial state to be selected on the run during the unfolding procedure while avoiding duplicate exploration of common behaviours. While a relatively standard practice for variable values [START_REF] Chatain | Characterization of reachable attractors using Petri net unfoldings[END_REF][START_REF] Chatain | Goal-Driven Unfolding of Petri Nets[END_REF], if parametrisation sets are also to be picked freely, the scope may quickly explode. The β is constructed with conditions in the unfolding of parametric regulatory networks corresponding to a combination of variable and one of its possible values, rather than the variable alone. This construction follows from the restriction to safe Petri nets, which allows at most one token in any given place. While this representation of variable values results in Denition 6.2 being considerably technical, the requirements imposed on β correspond exactly to the requirements on β in Denition 3.6.

The labelling function β allows us to use the same occurrence nets for parametric regulatory networks as for Petri nets. Thanks to the same primary building structure being preserved, no additional changes are necessary to adapt the unfolding denition to parametric regulatory networks. In the following, we reiterate Denition 3. The unfolding of a G m m m is unique up to isomorphism.

Unfoldings of parametric regulatory networks are in the general case innite, as opposed to the parametric regulatory networks themselves. The inniteness of the model results from the same patterns as we discussed for the Petri net unfoldings, namely due to the cyclic behaviour being unfolded into an acyclic structure.

While parametric regulatory network unfolding inherits the innite structure of the Petri net unfolding, it also retains the safety conditions. Instead of reachable markings, the unfolding of parametric regulatory networks is guaranteed to contain all reachable states of the original network. Thus, for any state x x x reachable in the original model, there exists at least one reachable marking M of the unfolding such that v∈{1,...,n} (v, x x x v ) = β (M ). To ease notation, we write simply β (M ) = x x x by abuse of notation.

Similarly the traces of the original parametric regulatory network are captured within the unfolding. As such, given a marking M reachable in the unfolding, another marking M and a transition t ∈ P P P ∈ P F P P P -→ async , an event e ∈ E such that M e -→ M , β (e) = t exists in the unfolding if and only if t = β (M ) , β (M ) . Note that the traces as captured within the parametric regulatory network unfolding are not explicitly parametrisation sensitive. The parametrisation sets are handled on the level of congurations, as is illustrated also in Denition 6.5.

Thanks to the same underlying structure of the Petri net and parametric regulatory network unfoldings, we can readily adopt the same tools, congurations (Denition 3.9) and cuts (Denition 3.10), for expressing the behavioural equivalence between parametric regulatory network unfolding and the original network as well as between individual branches of the unfolding (up to isomorphism). While conguration and cut only depend on the occurrence net structure, we give a fresh denition for the complete branching process of parametric regulatory networks to properly reect the labelling function β while mirroring Denition 3.11 of complete branching process of Petri nets. Denition 6.5 (Complete Branching Process of Parametric Regulatory Networks). Let G m m m be a parametric regulatory network.

We say that a branching process O, β of G m m m is complete, if for every parametrisation P P P ∈ P and for each state x x x reachable in G m m m under P P P , there exists a conguration C in O, β , satisfying:

1. β (Cut (C)) = x x x and P P P ∈ p R(G) β (C) ∩ P (x x x is represented in the branching process with the parametrisation P P P );

2. For every transition t = (x x x, y y y) ∈ Gm m m -→ async such that P P P ∈ p R(G) (t), there exists an event e ∈ E \ C such that β (e) = t and C ∪ {e} is a conguration of (O, β) (all transitions enabled under P P P can be reproduced in the branching process).

To ease notation, we write p R (C) instead of p R(G) β (C) ∩ P to denote the set of parametrisations allowing a conguration C of the unfolding.

A branching process of parametric regulatory network is complete under the same criteria as the branching process of a Petri net. All reachable states and enabled transitions have to be represented. In the case of parametric regulatory networks, however, we additionally require the states to be represented for any parametrisation witnessing the reachability in the original network. Similarly, the transitions have to be represented for any parametrisation that enables them. These conditions ensure that no parametrisations are lost in the complete branching processes. Thus, namely, complete branching process fully encompasses the behaviour of the parametric regulatory network parametrised by any P P P ∈ P.

Complete Finite Prex of Parametric Unfolding

Parametric regulatory networks and their state transition graphs, which represent the behaviour of the networks, are nite by denition unlike the generally innite unfoldings. Addressing the discrepancy, this section presents elevation of the construction of complete nite prexes of Petri net unfoldings to parametric regulatory network unfoldings.

Similarly to the unfolding itself, complete nite prexes of parametric regulatory network unfoldings are based on the same principles as complete nite prexes of Petri nets. In particular, we capitalise on the uniqueness of the unfoldings up to isomorphism and the `self inclusion' of unfoldings from dierent initial condition. More precisely, given an unfolding (B, E, F, M 0 ) of a parametric regulatory network G m m m with a conguration C ⊆ E, a branching process

O , β such that B ∪ E = { x ∈ (B ∪ E) \ ( • C ∪ C) | ∀ e ∈ C, ¬ (e # x) }
is the unfolding of G m m m with initial condition β (Cut (C)) , p R(G) (C) . Then, thanks to unfoldings being unique up to isomorphism, we know the branching process constructed in the same fashion for any other conguration

C ⊆ E such that β (Cut (C )) = β (Cut (C)) and p R(G) (C ) = p R(G) (C) is isomorphic to O , β .
While the above highlighted isomorphism of unfolding branches is fundamentally sucient, we can benet from the structure of initialised parametric regulatory networks to obtain a more general inclusion relation for branches of parametric regulatory network unfoldings. In particular, the initial state x x x, P corresponds to the initial marking of Petri nets, the initialised para- metric regulatory networks, however, also specify the initial parametrisation set P. The parametric regulatory network unfolding are essentially a union over unfoldings of the original network parametrised by any parametrisation P P P ∈ P. It follows that the unfolding from initial condition (x x x, P) should be fully included (up to isomorphism) in the unfolding from initial condition (x x x, P ) where P ⊆ P .

Lemma 6.1 (Inclusion of Parametric Regulatory Network Unfoldings). Let

G m m m be a parametric regulatory network and let (B, E, F, M 0 ) and (B , E , F , M 0 ) be unfoldings of G m m m from initial congurations (x x x, P) and (x x x, P ) respectively, such that P ⊆ P . Let further P P P ∈ P be an arbitrary parametrisation and C ⊆ E a conguration such that P P P ∈ p R (C).

Then there exists a conguration

C ⊆ E satisfying β (C ) = β (C), β (Cut (C )) = β (Cut (C)) and P P P ∈ p R (C ).
Proof. We conduct the proof as mathematical induction on the size of the congurations of the unfolding (B, E, F, M 0 ).

For the base step,

C = ∅ = C . Cut (C) = M 0 and Cut (C ) = M 0 . By denition β (M 0 ) = x x x = β (M 0 ). β (C) = ∅ = β (C ) and P P P ∈ p R (C ) = P follow trivially. Let now C ∈ E and C ∈ E be such that β (C) = β (C ), β (Cut (C)) = β (Cut (C )) and P P P ∈ p R (C) ∩ p R (C ).
Let further e ∈ E be arbitrary such that C ∪ {e} is a conguration and P P P ∈ p R β (e) .

Consider now an event e such that β (e ) = β (e) and • e ⊆ Cut (C ). Such an event surely exists thanks to β (Cut (C)) = β (Cut (C )). Furthermore P P P ∈ p R β (e ) = p R β (e) . Since the unfolding is the largest possible branching process, we know e ∈ E (unless an isomorphic event exists in E , in which case we consider the isomorphic event to be e ). Finally, C ∪ {e } is a conguration of (B , E , F , M 0 ) by denition.

As is the case for Petri net unfoldings, the complete nite prex of parametric regulatory network unfoldings is constructed using cut-o events. To determine which events are safe to be marked as cut-o events, we once again use local congurations Denition 3.12 to associate each event in the unfolding with a unique conguration. While the denitions of local conguration and possible extension (Denition 3.13) carry over from Petri net unfoldings, we introduce a new parametric cut-o event for unfoldings of parametric regulatory networks to be able to utilise the asymmetric inclusion from Lemma 6.1. The set of parametric cut-o events cutoffs O, β is similarly to the cuto event set of Petri net unfoldings, Denition 3.14, dependant on the order in which the possible extensions are explored. To guarantee the obtained nite prex is complete, the use of adequate order as per Denition 3.15 is once again necessary. Additionally, we utilise the cut-o events for the purpose of pruning the branches that are not allowed by any parametrisation in P. This allows us to keep the denition of the branching process itself parametrisation free, and only annotate congurations with parametrisation sets.

Due to the added dependency on the parametrisation sets, however, use of total adequate order does not guarantee the obtained unfolding to be smaller than the state transition graph. Instead, parametric cut-o events being dependant on the parametrisation set inclusion introduces another optimality criterion. In particular, it is desirable to explore the possible extensions in the reverse subset order of the parametrisation sets. Unfortunately, the subset order is orthogonal with the total adequate order of Esparza et al. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. As such, using the Esparza et al. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] total adequate order, it is possible for an event e to be explored after e while β (Cut ([e])) = β (Cut ([e ])) and p R(G) (e ) ⊆ p R(G) (e). Such cases lead to what we refer to as `backwards cuto' or `backwards merge' resulting in the chronologically older event e being declared cut-o and any further events e > e being discarded or re-evaluated. Nevertheless, the obtained complete nite prexes of parametric regulatory network unfoldings while using the Esparza et al. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] total adequate order tend to be considerably small in comparison to other methods, as highlighted by results presented in the Chapter 9.

Finally, throughout this chapter, we use the concrete parametrisation set notation p with the inuence constraints R (G). However, it should be noted that any parametrisation set computation p : 2 P P P ∈ P F P P P -→ async → 2 P(Gm m m) is applicable for the complete nite prex construction, as long as, the following implication is preserved: T ⊆ T =⇒ p (T ) ⊆ p (T ). Thus, in particular, the abstract parametrisation sets used in the abstract semantics of parametric regulatory networks, Denition 5.11, are compatible. It is therefore possible to construct unfoldings and complete nite prexes of parametric regulatory networks using the abstract parametrisation sets. Such a combination results in heuristic reduction of both the exponential size parametrisation space, thanks to the abstract parametrisation sets, and the exponential size state space, thanks to the partial order semantics.

Examples

In this section we give two examples of a unfolding prex for the parametric regulatory network from Example 4.1. The rst prex, in Example 6.1, is an incomplete prex showcasing detection of a cut-o event. The second prex, in Example 6.2, is then a complete nite prex of the unfolding. The usual Petri net notation of spherical and rectangular nodes is used to distinguish conditions and events, respectively. The conditions are labelled by the variable and its value given by the labelling function β . Similarly, the events are labelled by the unique variable changing value and the nature of the value change for transition given by the labelling function β . The events are additionally numbered in the order of exploration by the unfolding process. The conditions belonging to the initial marking are highlighted in blue. The dashed event is declared as cut-o during the complete nite prex construction.

Before we discuss the cut-o event e 5 , observe that events e 1 and e 2 are concurrent, irrespective of the ring order they lead to the state (a = 1, b = 1, c = 0) via the labelling function β . In a classical state space graph computation, transitions β (e 1 ) and β (e 2 ) would appear twice. β (e 1 ) followed by β (e 2 ) in the intermediate state The conditions and events are labelled by the β in the same fashion as in Figure 6.1. The conditions representing the initial state (a = 0, b = 0, c = 0) are also coloured blue. The cut-o events are omitted to improve readability of the gure.

Chapter 7

Goal-Driven Unfolding Parametric regulatory networks encompass the behaviours of the parametrised networks for any admissible parametrisation. As such, the sheer number of dierent behavioural patterns parametric regulatory networks exhibit leads to very heavy branching in the parametric regulatory network unfoldings. Rather than the entire reachable state space, however, the interest of many reachability questions is whether a particular reachability property can be satised. By focusing only on a single reachability property, it may become possible to prune some branches of the unfolding early, knowing they may never lead to the desired outcome. For this reason we extend the unfolding semantics of parametric regulatory networks with a goal-driven application.

In this chapter, we adapt the goal-driven unfolding method for Petri nets [START_REF] Chatain | Goal-Driven Unfolding of Petri Nets[END_REF] to the unfoldings of parametric regulatory networks. The method is based on static analysis method which reduces the input model by pruning transitions that never lead to the given target property. We briey recall the model reduction method for automata networks as introduced in [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF] and adapt it to parametric regulatory networks in Section 7.1. Parametric regulatory networks need to be processed for the reduction method to be applicable. To achieve this, the information on transitions enabled by the parametrisation sets is compiled into suitable structures (Denition 7.9). Section 7.2 thus presents an example algorithm for conducting the necessary conversion.

The application within the unfolding itself mirrors the application to Petri net unfoldings [START_REF] Chatain | Goal-Driven Unfolding of Petri Nets[END_REF]. In principle, the model reduction method is executed after inclusion of an event e during the unfolding procedure. The possible extensions e such that e < e are then considered based on the reduced model. Thus, by adapting the model reduction method of [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF] to the parametric regulatory networks whose semantics rely on renement of parametrisation sets, we obtain a combination of orthogonal on-the-run reduction and renement of the model.

Goal-Driven Reduction

In this section we introduce the automata network procedure of [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF] adapted to parametric regulatory networks. 1 The original automata network reduction procedure of [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF] is based on causality analysis of transitions of individual automata within the network. The method identies and prunes transitions which are guaranteed not to lead to the target property while preserving all minimal (in terms of included loops) traces which reach the goal. As such, if the automata network allows several dierent ways of reaching the goal, the reduction preserves all of them.

As the concept of trace is heavily exploited in the dening principles of the reduction method, we rst formalise the trace of parametric regulatory networks. A trace is generally understood as a sequence of compatible transitions. Instead of using the global transitions as understood in the semantics, we dene the trace using local transitions, or more literally value updates. The local denition not only mirrors the use of local causality in the original reduction procedure for automata networks [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF], but corresponds to the usual notion of Mazurkiewicz traces used in both trace and concurrency theory [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretations[END_REF]. Then, a value update

µ = v x → v y is couple of values (x, y) ∈ {0, . . . , m m m v } 2 of variable v such that |x -y| = 1.
To ease notation, we write simply x → y instead of v x → v y when the variable v is obvious from context.

Given a state x x x ∈ X m m m such that x x x v = x, we use µ (x x x) = x x x [v → y] to denote the state reached by executing the value update µ in state x x x. The notation naturally extends to sequences of value changes: 2

() (x x x) = x x x µ • π (x x x) = π (µ (x x x))
Furthermore, given a parametrisation P P P ∈ P (G m m m ), we say that the value update µ is enabled in x x x under P P P if (x x x, x x x [v → y]) ∈

F P P P -→ async .
Finally, given a transition t = (x x x, y y y) ∈ F P P P -→ async for some P P P ∈ P (G m m m ), we say

µ (t) = x x x v → y y y v where v = v (t)
is the value update of the transition t.

The motivation being application in conjunction with unfolding, we again limit ourselves to traces of asynchronous semantics, either concrete of abstract, of the parametric regulatory networks. As such, we use value updates directly in the trace denition. An extension to generalised asynchronous semantics can be achieved by considering steps composed of value updates of several variables akin to the construction in [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF]. Then a sequence of value updates π is a (local or Mazurkiewicz) trace of G m m m starting in x x x if there exists a parametrisation P P P ∈ P (G m m m ) such that for every i ∈ {2, . . . , |π|}, ((π 1 , . . . , π i-1 ) (x x x) , (π 1 , . . . , π i ) (x x x)) ∈

F P P P -→ async .
To ease notation, we use π :i = (π 1 , . . . , π i ), π i: = (π i , . . .) and π i:j = (π i , . . . , π j ) to denote prex, sux and inx sub-traces of trace π respectively, and π • π to denote concatenation of two traces.

Finally, we write p (π, x x x) = P P P ∈ P (G m m m ) ∀ i ∈ {2, . . . , |π|} , (π :i-1 (x x x) , π :i (x x x)) ∈

F P P P -→ async
to denote the set of all parametrisations that enable the trace π from initial state x x x.

We introduce the reduction method for goal properties specied as a target value for a particular variable g of the parametric regulatory network. We say that value of variable g is reachable in G m m m from state x x x if, either x x x g = , or there exists a trace π from the initial state x x x such that π (x x x) g = .

To simplify to notation we refer to g as goal.

While the goal is dened on a single variable, the extension to values for several variables or even value sets as opposed to single value per variable is straightforward.

A goal g is commonly reachable by traces with inx loops which, by themselves, do not aect the reachability of the goal. To maximise the eciency of the reduction procedure, only minimal traces, devoid of such loops, are considered. Adapted from [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF], a trace is minimal for reachability of a goal g if there exists no other realisable trace reaching g with a subsequence of value updates through the same regulator states. Denition 7.4 (Minimal Trace). Let G m m m be a parametric regulatory network, P P P ∈ P (G m m m ) an arbitrary parametrisation, x x x ∈ X m m m a state of G m m m and g a goal.

Then a trace π from state x x x of the parametrised network F P P P such that π (x x x) g = is minimal for the reachability of g from x x x if and only if there exists no other trace ρ from state x x x of F P P P satisfying all of the following:

1. ρ (x x x) g = ; 2. |ρ| < |π|;
3. there exists a monotonic injection Φ : {0, . . . , |π|} → {0, . . . , |ρ|} such that Φ : 0 → 0 and ∀ i, j ∈ {0, . . . , |π|} , i

≤ j =⇒ Φ (i) ≤ Φ (j) ∧ π i = v x → v y = ρ Φ(i) ∧ ω v π :i (x x x) = ω v ρ :Φ(i) (x x x) .
Unlike transitions of automata networks in [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF], value updates themselves do not contain any information on the actual traversed states of the network. An extra condition on regulator state equality, ω v π :i (x x x) = ω v ρ :Φ(i) (x x x) , is therefore necessary to retain the dynamic information allowing us to distinguish dierent traces which are subsequences of value updates (See Example 7.1). Another important property of minimal traces safeguarded by the regulator state equality is their independence on the exact parametrisation. More precisely, if a trace is minimal for at least one parametrisation, then it is minimal for any other parametrisation under which it is enabled. Proposition 7.1. Let G m m m be a parametric regulatory network of dimension n and π a trace from x x x ∈ X m m m minimal for reachability of goal g in F P P P for some P P P ∈ P (G m m m ). Then, π is minimal in the network parametrised by any other parametrisation F P P P where P P P ∈ p R(G) (π).

Proof. P P P ∈ p R(G) (π) guarantees π is a proper trace of F P P P . We conduct the rest of the proof by contradiction. Let thus ρ be a trace of F P P P satisfying the conditions in Denition 7.4. From the existence of the injection Φ we get ρ ⊆ π. By denition of parametrisation sets T ⊆ T =⇒ p R(G) (T ) ⊆ p R(G) (T ). Thus, thanks to ω v π :i (x x x) = ω v ρ :Φ(i) (x x x) for all i ∈ {0, . . . , |π|}, p R(G) ( π) ⊆ p R(G) ( ρ). ρ is therefore a trace of F P P P contradicting the minimality of π.

Thanks to Proposition 7.1, it is sucient to say that a trace of a parametric regulatory network is minimal without the need to explicitly list the parametrisation bearing witness to the minimality.

The goal-driven reduction of automata networks is facilitated by pruning transitions which are not part of any minimal trace reaching the goal [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF]. The individual transitions are, however, not explicitly represented in parametric regulatory networks. While it is not a challenge to represent the removed transitions explicitly, the reduction method is proposed for the general automata networks, which allow arbitrary transitions within the automata. On the other hand, we have limited ourselves to multivalued networks that are only allowed to change value of a variable by steps of size 1. As such, if a transition increasing the value of a variable v to x ∈ {0, . . . , m m m v } is to be pruned, all transitions increasing the value of v to a value beyond, to y ≥ x, can surely be pruned as well. A symmetrical reasoning applies to decreasing transitions.

Thus, instead of pruning individual transitions of parametric regulatory networks and representing the removed/preserved transitions explicitly, we adapt the method to disable increasing, respectively decreasing, value of a variable in a given regulator state beyond a certain value (or entirely). This is achieved in a similar pattern to the parametrisation lattices. We extend the parametric regulatory networks with a record of the activation (increase) and inhibition (decrease) limits for each variable in vectors l l l A and l l l I respectively. Denition 7.5 (Directed Parametric Regulatory Network). A directed parametric regulatory network G = G m m m , l l l A , l l l I is a parametric regulatory network G m m m coupled with a vector l l l A ∈ (N ∪ {-∞})

|Ω| of activation limits for each regulator state ω ω ω ∈ Ω and a vector l l l I ∈ (N ∪ {0, ∞}) |Ω| of inhibition limits for each regulator state ω ω ω ∈ Ω.

The semantics of the directed parametric regulatory network G are the semantics of the parametric regulatory network G m m m restricted to the activation and inhibition limits, l l l A and l l l I respectively. For any t = (x x x, P)

Gm m m -→ async (y y y, P ) of the parametric regulatory network G m m m : t ∈ G -→ async ∆ ⇐⇒ sign (t) = +1 =⇒ x x x v(t) < l l l A ω v(t) (x x x) ∧ sign (t) = -1 =⇒ x x x v(t) > l l l I ω v(t) (x x x)
One may remark that the aforementioned parametrisation lattices used in abstract parametric regulatory networks already allow restriction of the activation or inhibition of variables in individual regulator states. Indeed, l l l I , l l l A forms a parametrisation lattice itself as long as it contains no innity values. The role of the parametrisation lattices as employed in the abstract parametric network semantics and of the limit vectors l l l A and l l l I , however, diers on a fundamental level.

The parametrisation lattices serve to keep track of parametrisations capable of reproducing certain behaviour(s), and thus restrict the set of enabled transitions based on their causal history. On the other hand, the l l l A and l l l I of directed parametric regulatory networks mark components whose activation or inhibition (beyond a certain value) is not necessary to reach a given goal by the means of a minimal trace. A parametrisation that allows changing a component value beyond the limit, thus allowing behaviour which does not lead to the established goal may still allow a dierent sequence of transitions leading to the goal. We want to retain such parametrisations, thus the `useless' behaviour which does not lead to the goal cannot be restricted by the means of the parametrisation lattice of the abstract parametric regulatory network semantics. While the independence from parametrisation lattices in abstract parametric regulatory network semantics requires us to keep track of the extra limit vectors l l l A and l l l I , it also guarantees that the goal-driven unfolding is applicable alongside both the concrete and the abstract semantics of parametric regulatory networks.

With the minimal traces and the directed parametric regulatory networks we have the necessary groundwork to introduce the reduction procedure itself. As we have already mentioned, the reduction relies on causality analysis. In particular, the reduction procedure identies sub-goals based on local causality for individual components, called (local) objectives. The objectives represent a change of variable value that necessarily has to occur before a certain transition can achieve later objective or the goal itself. The objectives as dened for the automata networks [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF] keep the desired value evolution abstract and thus do not specify how, i.e. by means of which transitions, the value change occurs. While we do not explicitly include this information, the restriction we have imposed on the multivalued networks allowing the variables to only change value by steps of size 1, distinctly predetermines how the desired value change may be achieved. Temporary value swings may still be necessary, however, to facilitate regulation of a necessary variable. Denition 7.6 (Objective). Let G = G m m m , l l l A , l l l I be a directed parametric regulatory network of dimension n.

Then an objective O = v x v y is a pair of values x, y ∈ {0, . . . , m m m v } of a variable v ∈ {1, . . . , n}.

We say an objective O is valid in an initial state x x x ∈ X m m m if x = y or G has a trace π from x x x such that π (x x x) v = y and there exists an index i ∈ {0, . . . , |π|} such that π

:i (x x x) v = x.
We use x y to denote v x v y where the variable v ∈ {1, . . . , n} is obvious from the context.

Each objective v x v y represents either increase or decrease of the value of the component. We use sign (v x v y ) = sign (y -x) to denote the direction of the prescribed value evolution.

We demand the traces of the parametric regulatory networks to be realisable within at least one of the associated parametrised networks. The condition on existence of a trace thus also guarantees that there exists a parametrisation that enables said trace. A valid objective is therefore surely fully realisable under at least one parametrisation.

The objective represents a change of value of only one variable v ∈ {1, . . . , n}. The trace bearing witness to the validity of such an objective may, however, require other variables to also change value, namely the regulators of v. The automata network reduction procedure associates each objective with a set of transitions which may be used to full the objective [START_REF] Paulevé | Goal-Oriented Reduction of Automata Networks[END_REF]. Such a transition set may then be used to obtain the objectives for regulators of v. In the parametric regulatory networks, however, transitions are not explicitly represented. A particular transition, or more generally, the value update of a given variable is possible if there exists a parametrisation enabling it in the associated parametrisation set. The transitions thus have to be drawn from parametrisation set, which species whether a variable value can increase or decrease within each regulator state. Denition 7.7 (Value Update Enabled in a Regulator State). Let G be a directed parametric regulatory network of dimension n, P ⊆ P (G m m m ) a parametrisation set, and ω ω ω ∈ Ω v be an arbitrary regulator state of some variable some variable v ∈ {1, . . . , n} of G.

Then a value update µ = v x → v y , such that x = ω ω ω v in case v ∈ R(v), is enabled in a regulator state ω ω ω ∈ Ω v under P if there exists a parametrisation P P P ∈ P such that sign (x -P P P v,ω ω ω ) = sign (x -y).

Given a value update µ, we refer to regulator states ω ω ω which do not enable µ as bad regulator states.

Seeing as the reduction procedure constructs the objectives based on the regulators of the variable in question, the transitions of parametric regulatory networks as given by the semantics which depend on the entire states of the network, are highly unsuitable. Instead, to maximise the eciency of the reduction procedure, a minimalistic, with respect to the number of regulators, representation of the value evolutions is desirable. One such obvious reduction is the projection from the entire state to the regulators themselves in the form of the regulator states, which we already employ within the parametrisations. A particular change in the value of a given variable is possible if there exists a parametrisation enabling it in the associated parametrisation set. The criterion being existential with respect to parametrisations, it is a common occurrence for a variable to be enabled to update value in a given direction within numerous regulator states. Enumerating the transitions for each of the regulator states individually could thus still lead to substantial redundancy. In particular, if the value update is enabled within all regulator states that dier only in the value of a particular regulator u ∈ R(v), i.e. if the value update is possible regardless of the value of u, the regulator u can be omitted as no trace that changes the value of u for the express purpose of changing value of v is minimal. To minimise the amount of regulators to be analysed within the model reduction procedure, we introduce a partial regulator state as a union over several regulator states characterised by only a subset of regulators being evaluated. By abuse of notation, a partial regulator state is also a set of regulator states,

ℵ ℵ ℵ = { ω ω ω ∈ Ω v | ∀ u ∈ R(v), ω ω ω u = ℵ ℵ ℵ u ∨ ℵ ℵ ℵ u = }. A v = ≤ Π u∈R(v) {0, . . . , m m m u } ∪ { } denotes the set of all partial regulator states of a variable v ∈ {1, . . . , n}.
Partial regulator states can be utilised to abstract the parametric regulatory network dynamics while minimising the number of repeated values for each regulator. We capture these abstractions by the means of sets of partial regulator states, called regulation cover sets, representing the enabling condition of a given value update. A regulation cover set of a value update v x → v y is subject to two conditions. First, the set has to cover all regulator states ω ω ω ∈ Ω v such that v x → v y is enabled in ω ω ω. I.e., for each such regulator state there must exist one or more partial regulator states which specify the value of each regulator in ω ω ω. Second, no bad regulator state ω ω ω, in which the v x → v y is not enabled, is subsumed by any of the partial regulator states in the cover set. The two conditions not only guarantee that the abstract dynamics enable exactly the same value changes as the concrete dynamics, but also preserve the regulator information, i.e. each value of each regulator that appears in the enabling conditions. The regulator information is necessary to accurately determine which regulator values are necessary to complete an objective. Denition 7.9 (Regulation Cover Set). Let G be a directed parametric regulatory network of dimension n, P ⊆ P (G m m m ) a parametrisation set and let µ = v x → v y a value update of variable v ∈ {1, . . . , n} from x to y.

A set of partial regulator states A µ ⊆ A v is a cover set of µ if both of the following conditions are satised: For all regulator states ω ω ω ∈ Ω v such that µ is enabled in ω ω ω under P, and for all regulators u ∈ R(v), there exists a partial regulator state

ℵ ℵ ℵ ∈ A µ , such that ω ω ω ∈ ℵ ℵ ℵ ∧ ω ω ω u = ℵ ℵ ℵ u .
For all bad regulator states ω ω ω ∈ Ω v such that µ in ω ω ω is not enabled under

P, ω ω ω / ∈ ℵ ℵ ℵ∈Aµ ℵ ℵ ℵ.
Any regulation cover set, including the concrete regulation cover set containing only fully specied regulation states { ω ω ω ∈ Ω v | µ is enabled in ω ω ω }, may be used for the express purposes of the reduction procedure. The aim of the regulation cover set is to minimise the number of individual regulator values which appear across all of the partial regulator states. In Section 7.2, we give an example of an algorithm for computation of regulation cover sets with no more regulator value specications than the concrete regulation cover set.

Since parametric regulatory networks allow only unitary value changes, the realisation of an objective v x v y involves a monotonic evolution of value of variable v from x to y, where each update of value depends on specic (partial) regulator state. This coupling of a value change with a corresponding partial regulator state is referred to as a partial transition.

The reduction of directed parametric regulatory networks relies on associating to objectives the set of partial transitions which are necessary to realise the objective. Starting from the nal (goal) objective, the procedure then recursively collects objectives related to the identied partial transitions. Denition 7.10 (Objective Transition Set). Let G be an directed parametric regulatory network of dimension n, P ⊆ P (G m m m ) a set of parametrisations and let O = v x v y be an objective for a variable v ∈ {1, . . . , n}. Let rst µ (O) be the set of all value updates covered by the objective O dened as follows:

µ (O) ∆ =    v z → v a sign (v z → v a ) = sign (O) ∧ max({z, a}) ≤ max({x, y})∧ min({z, a}) ≥ min({x, y})   
Then the objective transition set τ (O) is a set of partial transitions composed of a covered value update and a covered partial regulator state:

τ (O) ∆ = { (µ, ℵ ℵ ℵ) | µ ∈ µ (O) ∧ ℵ ℵ ℵ ∈ A µ }
Given an initial state x x x ∈ X m m m , the valid objective transition set of an objective O in state x x x is the subset of the objective transition set τ

x x x (O) ⊆ τ (O) such that (µ, ℵ ℵ ℵ) ∈ τ x x x (O) ∆ ⇐⇒ ∀ u ∈ R(v), ℵ ℵ ℵ u = =⇒ x x x u ℵ ℵ ℵ u is valid in the initial state x x x.
The (valid) objective transition sets extend to sets of objectives in the natural manner, τ (O) = O∈O τ (O).

Remark that the denition of a valid objective transition set benets from the use of partial regulator states. Indeed, instead of having to check validity of an objective for each regulator, only the minimal necessary subset of regulators is considered. Checking objective validity consists of nding a trace witness, which translates to nding all possible extensions (enabled value updates) of a trace. The parametrisation lattices used in the abstract semantics of parametric regulatory networks allow searching for enabled value updates without explicitly enumerating the parametrisations. The objective validity computation is thus compatible with the abstraction of parametrisation sets.

The goal-oriented reduction of directed parametric regulatory networks can then be dened by recursively collecting objectives from partial transitions into an reduced objective set B, and rening the component activation and inhibition limits accordingly. Denition 7.11 (Directed Parametric Regulatory Network Reduction Procedure). Let G = G m m m , l l l A , l l l I be a directed parametric regulatory network of dimension n, x x x ∈ X m m m an arbitrary initial state and g a goal.

Then, the goal-driven reduction of G is again a directed network G = G m m m , l l l A , l l l I of the same dimension n where the underlying parametric regulatory network is unchanged and the limit vectors l l l A and l l l I are dened as follows for each regulator state (v, ω ω ω) ∈ Ω:

l l l A ω ω ω = max({ x ∈ {0, . . . , m m m v } | ∃ (v x-1 → v x , ℵ ℵ ℵ) ∈ τ x x x (B), ω ω ω ∈ ℵ ℵ ℵ } ∪ {-∞}) l l l I ω ω ω = min({ x ∈ {0, . . . , m m m v } | ∃ (v x+1 → v x , ℵ ℵ ℵ) ∈ τ x x x (B), ω ω ω ∈ ℵ ℵ ℵ } ∪ {∞})
where B is the smallest set of objectives satisfying all of the following conditions:

1. x x x g g ∈ B; 2. For each O ∈ B, each (w x → w y , ℵ ℵ ℵ) ∈ τ x x x (O), and each u ∈ R(w) \ {w}, ℵ ℵ ℵ u = =⇒ x x x u ℵ ℵ ℵ u ∈ B; 3. For each O ∈ B, each (w x → w y , ℵ ℵ ℵ) ∈ τ x x x (O), and each w z w a = O ∈ B, w y w a ∈ B.
Following the interpretation of the reduction procedure a transition t = (y y y, z z z) is preserved in the reduced network G if there exists a partial transition (µ (t) , ℵ ℵ ℵ) ∈ τ x x x (B) where ω v(t) (y y y) ∈ ℵ ℵ ℵ. In particular, such partial transition must exist in the valid objective transition set of some objective O ∈ B, (µ (t) , ℵ ℵ ℵ) ∈ τ x x x (O) ⊆ τ x x x (B). As the objectives are realised in monotonic fashion in multivalued networks, we know such an O covers µ (t). The claim is formalised in Lemma 7.1.

Lemma 7.1 (Transitions Covered by an Objective in the Reduced Objective

Set are Represented in the Valid Objective Transition Set). Let G be a directed parametric regulatory network of dimension n and let π be a trace of G reaching a goal g from an initial state x x x ∈ X m m m . Let further B be the objective set constructed by the reduction procedure according to Denition 7.11. Finally, let O = v x v y ∈ B be an arbitrary objective in the reduced objective set. Then, for any i ∈ {1, . . . , |π|} such that π i ∈ µ (O), there exists

(π i , ℵ ℵ ℵ) ∈ τ x x x (O) where ω v π :i-1 (x x x) ∈ ℵ ℵ ℵ.
Proof. Since π is a trace of G, we know the value update π i is enabled in the regulator state ω ω ω = ω v π :i-1 (x x x) . Thus, by Denition 7.9 of the regulation cover sets, we know there must exist at least one partial regulator state ℵ ℵ ℵ ∈ A πi such that ω ω ω ∈ ℵ ℵ ℵ.

Then, by Denition 7.10 of objective transition sets, the corresponding partial transition (π i , ℵ ℵ ℵ) ∈ τ (O). Finally, since π itself is a witness of the validity of objectives for all regulators required by (π i , ℵ ℵ ℵ), (π i , ℵ ℵ ℵ) ∈ τ x x x (O). This leads us to formulate the soundness theorem of the reduction procedure, guaranteeing that all transitions witnessing all of the minimal traces are preserved and thus, in turn, all minimal traces are preserved. The proof of the theorem relies on Lemma 7.1 to show that any value update whose associated transition is not preserved is part of a cycle on any trace leading to the goal, and as a consequence does not belong to any minimal trace. Theorem 7.1. Let G be a directed parametric regulatory network of dimension n and let π be a trace of G from the initial state x x x ∈ X m m m minimal for a goal g . Let further B be set of objectives constructed for reachability of g from x x x according to Denition 7.11.

Then, for any i ∈ {1, . . . , |π|} with π i = v x → v y , there exists at least one partial transition

(π i , ℵ ℵ ℵ) ∈ τ (B) such that ω v π :i-1 (x x x) ∈ ℵ ℵ ℵ.
Proof. We conduct the proof by contradiction, showing that if a value change v x → v y = π i for some i ∈ {0, . . . , |π|}, is not covered by any objective in B, the trace π cannot be minimal.

Let now j < i be the largest such that v (π j ) = v and for which there exists

O ∈ B, π j ∈ µ (O), if it exists, j = 0 otherwise. Furthermore, let k > i be the smallest such that v (π k ) = v and π :k-1 (x x x) v = π :j (x x x) v , if it exists, k = |π| + 1 otherwise.
Let us now consider a value update sequence ρ obtained from π by removing all the value updates of variable v in π j+1:k-1 . The removed value updates either form a loop on the value of v or, in case j = |π| + 1, have no causal successors modifying the value of v. The evolution of v along ρ is therefore valid with respect to evolving the value by steps of size 1. For ρ to satisfy the minimality condition in Denition 7.4 with respect to π, the regulator states use by each value update have to be the same.

Let us therefore assume there exists l ∈ {1, . . . , |π|} with w = v (π l ) such that ω w π :l-1 (x x x) = ω w ρ :h-1 (x x x) where h is the new index of π l in ρ, π l = ρ h . As ρ only diers from π by the evolution of variable v value between π j and π k , π l must be a value change of a variable w = v, such that v ∈ R(w) and j < l < k.

We now show ρ l / ∈ µ (O) for any O ∈ B by contradiction. Let thus O ∈ B be such that ρ l ∈ µ (O ). v ∈ R(w) and thus by rule (2) of the reduced objective set construction in Denition 7.11, x x x v z ∈ B where z = π :l (x x x) v . We now conduct a discussion on the value of j. j = 0. p ρ :h , x x x = ∅ and p π :l , x x x = ∅ implies that ρ :h (x x x) v = z. There thus must exist a value change from x x x v towards z. Such value change is however, covered by x x x v z contradicting j = 0. The objective v a v z , respectively, O itself in case π :j (x x x) v = a and sign z -π :j (x x x) v = sign (O), covers the rst value change of v after π i . This is a contradiction with j being the largest index of a covered value change or, in case π i is the rst change of variable v value after π j , with π i not being covered.

As such, the value change ρ h is not covered by any objective in B Therefore, ρ h can be removed from ρ in the same fashion as π i was removed from π. Repeating the whole procedure leads to an even shorter value update sequence. As any minimal trace is nite, all uncovered value updates are eventually purged, leaving a valid trace.

Thanks to rule (1) of the reduced objective set construction in Denition 7.11, the objective x x x g ∈ B covers all value updates of variable g from x x x g to . However, even covered value updates may be removed if they lie between π j and π k . We thus still have to show that for any covered value update π l for j < l < k which gets removed in ρ, there exists h ≤ j such that π

:h (x x x) v = π :l (x x x) v .
Let thus O ∈ B be such that π l ∈ µ (O ) and let z be the target value of the objective O . By denition of the reduced objective set B, any target value of an objective is rst introduced by either rule (1) or (2) of Denition 7.11, giving us x x x v z ∈ B. Let us rst show j > 0 by contradiction. We can assume π :l-1 (x x x) v = x x x v , otherwise the rst value update of variable v towards π :l-1 (x x x) v is covered by x x x v z contradicting j = 0. Furthermore, π l itself is covered, giving us i < l.

Finally, k is the smallest index beyond i of a value update changing the value of variable v from x x x v . Therefore, k ≤ l, which is direct contradiction of l < k. We thus know there exists a value update π j ∈ µ (O) covered by the objective O ∈ B. Let a be the target value of the objective O, thus x x x v a ∈ B. Furthermore, by rule (3) of the reduced objective set construction in Denition 7.11, v z v a , v a v z ∈ B. Let us now conduct a discussion on the sign s ∈ {-1, 1} of the rst removed value update, i.e. the rst value update of variable v after π j . s = sign (π j ). Then, as no value update between π j and π i is covered, a = π :j (x x x) v . By a similar argument with the objective v a v z ∈ B, and using the fact that k > l is the rst value update of v starting from value a, π :j (x x x) v = z = a = π :l (x x x) v . s = -sign (π j ). We know O = x x x v a. Otherwise, O would have to have been added to B by rule (3) of Denition 7.11. The rule (3) being symmetrical, the reverse objective of O, which covers the rst value update of variable v after π j , would therefore also have to belong to B. A similar argument can be used to obtain O = x x x v z. The objective from a to the initial value of O , which again covers the rst value update of variable v after π j , would have belonged to B otherwise. Finally, since j is the last index of a covered value update before π i , it is in particular not covered by v a v z , giving us sign (O ) = sign (O). Thanks to l < k, we know π :l (x x x) v ≤ π :j (x x x) v and due to the value updates being of steps of size 1, there must exist the coveted h ≤ j with π :l (x x x) v = π :h (x x x) v facilitating the evolution of variable v value from x x x v to π :j (x x x) v .

As such, none of the variable values reached by a covered value update may be lost during the removal procedure. The newly obtained trace is therefore guaranteed to reach the goal, contradicting the minimality of π.

Computation of Regulation Cover Sets

This section introduces a sample algorithm for computation of the regulation cover sets. The algorithm relies on a simple heuristic for choosing partial regulators states to ensure each enabled regulator state is covered, while maintaining the condition that no bad regulator state is covered, thus complying with Denition 7.9. The regulation cover set computed by the algorithm in this section is guaranteed to not be larger than the concrete regulation cover set, with respect to the number of regulator value specications across all the partial regulator states in the cover set (values other than the wildcard ).

Throughout this section we limit ourselves to computation of a single regulation cover set, for a given parametric regulatory network G, value change v x → v y and parametrisation set P. Let now A ena ∆ = ℵ ℵ ℵ ∈ A v ∀ ω ω ω ∈ ℵ ℵ ℵ, ∃ P P P ∈ P, P P P v,ω ω ω = y denote the set of all partial regulator states that subsume no bad regulator state (contain only regulator states enabling v x → v y ). Further, have also been included in the regulation cover set A µ . ω ω ω is therefore in all likelihood already covered to a higher degree than ω ω ω, and likely has more covering options. The bias thus ensures ω ω ω is covered rst in order to avoid introducing potentially redundant partial regulator states into the regulation cover set.

Algorithm 1 is quasilinear in the number of regulator states and quadratic in the number of regulators. The main complexity comes from computing the local cover sets A ω ω ω . Whether a regulator state ω ω ω ∈ Ω v is covered by some partial regulator state set, in particular, A µ ∪ A ω ω ω , can be decided in O (|R(v)|). Finally, one has to consider the complexity of keeping the regulator states in a priority queue according to the weight function W. The asymptotic time complexity of the complete Algorithm 1 is therefore quasilinear in the number of regulator states

Only the relevant subsets of

O |Ω v | • log (|Ω v |) + |R(v)| 2 .
Algorithm 1 does not require explicit enumeration of parametrisations when coupled with the abstract parametric regulator network semantics. The parametrisation set is only used to determine which regulator states enable the value change (queries to A ena ). This information is readily available using the parametrisation lattices in the form of parameter values for the relevant regulator state in the minimum parametrisation and the maximum parametrisation.

Examples

In this section we present an example of directed parametric regulatory network reduction by the means of the reduction procedure from Denition 7.11, including the computation of the regulation cover set by the algorithm Algorithm 1.

Example 7.1. Consider the parametric regulatory network G {1} 4 from Example 5.1 as a directed parametric regulatory network G = G {1} 4 , l l l A , l l l I , where l l l A = {1} 4 and l l l I = {0} 4 are unrestrictive. Let further P = P P P , P P P be a parametrisation set containing only two parametrisations, P P P being the parametrisation from Figure 5.2 dening the Boolean network F B from Example 2.2. And P P P = P P P [a, 100 → 0] be a parametrisation diering from P P P only on the value of parameter K a,100 . Finally, let a 1 be a goal and x x x = (a = 0, b = 0, c = 0, d = 0) an initial state.

In Figure 7.1 we recall the dynamics of the Boolean network F B in the form of the state space graph with asynchronous semantics. As opposed to Figure 2.6, the behaviour enabled solely by parametrisation P P P is also represented. The bold lines and text indicate transitions belonging to a minimal trace to the goal a 1 and states visited by the minimal traces, respectively. In our example, three distinct minimal traces from the initial state x x x to the goal a 1 exist. Here, we list the minimal traces including the traversed states for clarity. The value updates are annotated by their variable, the nature of the value change and the regulator state: Notice that all the listed traces share a common prex. In fact, if only the value updates, without the regulator states were considered in Denition 7.4, only the rst, shortest, trace would me considered minimal. All traces, however utilise a dierent regulator state, thus eectively a dierent transition to increase the value of variable a and reach their nal state. Observe also that the rst, shortest, minimal trace is only available under the parametrisation P P P . Thanks to the regulator state equality condition, we thus preserve minimal traces also for P P P without the need to separate them.

Observe that variable d never changes value along any of the minimal traces. This follows from the fact that variable a is never allowed to increase while variable d value is 1. Thus, if variable d value increases, it has to decrease again before the goal can be reached. Variable d is only regulator of itself and variable a and has therefore no other eects on the network. Unlike the increase and decrease loop of variable b value in the third, longest, minimal trace, which is necessary for the increase of variable c value, the increase and decrease loop of variable d can therefore always be stripped from the trace to obtain a shorter, more minimal, trace. One might thus expect the value updates of variable d to be pruned by the reduction procedure, which is, indeed the case:

We start with B := {a 0 a 1 } according to rule (1) of Denition 7.11. Inference of the regulator cover set used in τ a0 a1 (x

x x) = {(a 0 → a 1 , ℵ ℵ ℵ) | ℵ ℵ ℵ ∈ A a0→a1 } = {(a 0 → a 1 , 100) , (a 0 → a 1 , 010) , (a 0 → a 1 , 110)} is illustrated in Example 7.
b 0 , b 0 b 1 , c 0 c 0 , c 0 c 1 , d 0 d 0 , b 1 b 0 , c 1 c 0 }
, with the valid partial transition set τ B (x x x) = {(a 0 → a 1 , 100),(a 0 → a 1 , 010), (a 0 → a 1 , 110), (b 0 → b 1 , 0), (b 1 → b 0 , 1), (c 0 → c 1 , 1), (c 1 → c 0 , 0)}. One may observe that the computed transition set indeed covers all the transitions used by any of the minimal traces (thick edges in Figure 7.1).

Finally, the limit vectors for the new DPRN G = G {1} 4 , l l l A , l l l I are as follows:

l l l A = (a = 1, b = 1, c = 1, d = -∞) l l l I = (a = ∞, b = 0, c = 0, d = ∞)
The variable d is indeed completely forbidden changing value in the reduced model, considerably decreasing the reachable state space that has to be explored. Notice also that decrease of variable a value is also disabled, however, in our Boolean case this has no practical eect w.r.t. reachability of the goal a 1 .

Example 7.2. Let us consider the directed parametric regulatory network G = G {1} 4 , l l l A , l l l I from Example 7.1.

We now show the regulation cover set computation for value updates of variable a. Let us start with a 0 → a 1 . We visualise the computation directly on the regulator states of variable a represented by the Hasse diagram of the lattice (Ω a , a ). The initial conguration and rst two iterations, covering of the rst two regulator states, are depicted in Figure 7. The run of the Algorithm 1 as illustrated in Figure 7.2 assumes lexicographic order is used to distinguish between regulator states with equal weights. Thus, 010 is covered in the rst iteration. Only one partial regulator state in A 1 , 10 which does not cover b = 0, contains 010. The local cover set used for 010 is therefore taken from A 0 and contains only 010 itself, A 010 = {010}. The only partial regulation state remaining in A ena \ A rmv is the regulator state 110 itself. Thus, the local cover set for 110 is also explicit, A 110 = {110}. The algorithm therefore concludes with the concrete regulation cover set A a0→a1 = {010, 100, 110}, which is the optimal solution in our case.

Let us now also consider the decreasing case a 1 → a 0 . Again we depict the computation using the Hasse diagrams of the lattice (Ω a , a ). All iterations of the Algorithm 1 using lexicographic order on regulator states of equal weight up to the nal one are given in Figure 7.3.

Four regulator states are symmetrical in the initial conguration, W (000) = W (011) = W (100) = W (111) = 2.5. The regulator state 000 is therefore covered rst. Unlike the case of a 0 → a 1 , A 2 = { 0 , 1} is not empty. However, only 0 contains 000, which is not enough for a local cover set. The local cover set is therefore chosen from A 1 , A 000 = {00 , 00}. The local cover set is represented by the double lines in Figure 7. 3 (b). Notice that in this case, the regulator state 000 gets covered by two partial regulator states having one more regulator value specication (a total of 4 specications against the explicit 3).

100 is covered next (W (100) = 1.5). 0 is no longer available and only 10 contains 100 in A 1 \ A rmv . The local cover set A 100 = {10 } is sucient, however, as A a1→a0 already contains 00 which provides the missing d = 0. Thus, 100 is covered at an additional cost of only 2 regulator value specications, eectively paying o the depth incurred while covering 000.

011 is covered next thanks to the fractional part of the weight function, The remaining regulator states 001 and 101 get covered by empty local cover sets, A 001 = A 101 = ∅ as 001 and 101 are already covered by 00 and 0 1, respectively 10 and 1 1 which are already in A a1→a0 (dashed lines). The algorithm therefore concludes with regulation cover set A a0→a1 = {00 , 00, 10 , 0 1, 11, 1 1} using 12 regulator value specications as opposed to the 18 of the concrete regulation cover set.

The fractional part of the weight function is crucial to distinguish between 011 and 001 after the second iteration,

Related Work

Modelling of biological systems is a typical reverse engineering application, and as usual, any further analysis is highly dependant on the quality of the model. Considering additionally the complexity of the biological phenomena studied, it is of no surprise that model inference and validation is a central topic of discrete regulatory network studies since the rst applications to biological systems [START_REF] Kauman | Homeostasis and dierentiation in random genetic control networks[END_REF][START_REF] Thomas | Boolean formalization of genetic control circuits[END_REF].

Model inference of biological regulatory networks is traditionally conducted by hand with the aid of ad-hoc simulations to provide a trial-and-error method [START_REF] Kaufman | Towards a logical analysis of the immune response[END_REF][START_REF] Thomas | Multistationarity, the basis of cell dierentiation and memory. i. structural conditions of multistationarity and other nontrivial behavior[END_REF]. Introduction of simulation software [START_REF] Jong | Genetic Network Analyzer: qualitative simulation of genetic regulatory networks[END_REF][START_REF] Gonzalez | Ginsim: A software suite for the qualitative modelling, simulation and analysis of regulatory networks[END_REF] facilitated the use of systematic simulations which allows the model space to be uniformly sampled, improving on the ad-hoc method.

However, simulation based approaches work with variable reliability, as it is closely tied to the sampling density of the model space. With the model space size of biological regulatory network growing fast (asymptotically double exponentially) in the number of biological species considered (variables), it may easily become infeasible to obtain a suciently dense sampling due to the computation cost of the individual simulations. Thus, in order to guarantee that all relevant models are retrieved, formal methods, such as model checking, are necessary. Simulation based approaches to model inference and approaches based on combination of simulation and formal methods, however, remain highly relevant today, especially where the biological knowledge is abundant and allows for sucient restriction of the model space.

The inference of discrete regulatory networks can be generally split into two phases. First, the inuence graph is constructed, giving the topology of the network. Second, the regulation function is specied. As the regulation function can be fully specied using the parameters of a parametric regulatory network, we refer to the second phase as parameter inference. Our methods consider the inuence graph as an input, thus we accordingly shift our focus towards parameter inference for the remainder of the chapter.

Numerous methods have been applied to parameter inference of discrete regulatory networks, ranging from comprehensive formal methods, such as model 101 checking, through analyses tailored to available dynamic data based on reachability or attractor analysis, all the way to constraint programming and in recent years, also machine learning [START_REF] Razaghi-Moghadam | Supervised learning of generegulatory networks based on graph distance proles of transcriptomics data[END_REF]. In the following sections we explore in detail some of the parameter inference approaches most comparable to our work.

Model Checking

Model checking, in its various forms, is one of the most widespread methods of mathematical model verication across numerous elds. It is therefore not surprising that model checking was the rst formal method introduced to discrete regulatory networks, in particular for the purpose of parameter inference [START_REF] Bernot | Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic[END_REF].

The work of Bernot et al. [START_REF] Bernot | Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic[END_REF] relies on model checking of discrete regulatory networks against temporal properties, given as formulae of CTL (Computational Tree Logic [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF]). Many properties of interest in the biological setting can be expressed in CTL, which being a branching-time temporal logic, is well suited for properties of discrete regulatory networks with non-deterministic semantics (e.g. asynchronous semantics). The method of Bernot et al. [START_REF] Bernot | Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic[END_REF], however, relies on explicitly enumerating the possible parametrisations and model checking the parametrised networks individually. The sheer amount of possible parametrisations thus imposes strict computational limits.

Several subsequent works aim to improve the scalability of model checking based approaches to parameter inference. In [START_REF] Klarner | Parameter identication and model ranking of thomas networks[END_REF], the authors aim to improve the scalability by model checking the parametric network directly, rather than the individual parametrised networks, as well as restrict the admissible parametrisation set by inuence constraints (akin to the constraints in Chapter 5). We utilise the same idea in unfolding the parametric regulatory network directly, rather than unfolding the individual parametrised networks in Chapter 6. As the dierent parametrised networks tend to share large portions of the expressed behaviours, avoiding repeated analysis of the shared behaviour segments benets the methods greatly.

The ability to model check the parametric regulatory network while discriminating the inconsistent behaviour obtained by a simple union over the semantics of the individual parametrised networks, the authors utilise a novel model checking methods, called coloured model checking [START_REF] Barnat | On parameter synthesis by parallel model checking[END_REF]. Although originally introduced for properties expressed in LTL (Linear Temporal Logic), coloured model checking has later been extended to also handle CTL properties [START_REF] Brim | Parameter synthesis by parallel coloured CTL model checking[END_REF].

In principle, coloured model checking operates similarly to the traditional temporal model checking. For each state satisfying the given property (accepting state), rst, the set of all states that can reach the given accepting state is computed (reverse reachability). Second, the accepting cycles on the given accepting state are computed. Instead of simply keeping the sets of initial states and accepting cycles as in classical temporal model checking, coloured model checking annotates each state with a Boolean vector, where each bit (colour) represents a single parametrisation. The colour vectors allow the algorithm to determine exactly which parametrisations allow a particular initial state to reach the accepting state, or which parametrisations enable the whole accepting cycle. The colour vector thus essentially translates to the parametrisation set we use to annotate states in the abstract parametric regulatory network semantics in Section 4.2.

Having the initial states and accepting cycles annotated with parametrisations, it is easy to determine which parametrisations (respectively, parametrised networks) satisfy the coveted property. The Boolean vector representation of the parametrisation set is suitable for the model checking application, as it allows for fast computation of intersections and unions, however, it relies on explicit enumeration of all parametrisations. Even if ltered by some initial conditions, such as inuence constraints, the number of admissible parametrisations remains in the general case exponential, making the coloured model checking of larger networks or networks with high in-degrees in the inuence graph computationally intractable.

A dierent approach appears in [START_REF] Fromentin | Analysing gene regulatory networks by both constraint programming and model-checking[END_REF]. The authors aim to avoid explicit enumeration of parametrisations by omitting the classical, Kripke structure based, temporal model checking procedure. Instead, the CTL property is translated into constraints on the parameters, which exactly characterise all the parametrisations that satisfy the given property. The approach is shown to be signicantly faster than traditional model checking of individual parametrised networks on a small example. The nontrivial translation of the until operator in CTL into constraints on parameters, however, introduces a new complexity limitation.

While the exact scope of model checking applicability is dependant on the expressivity of the associated logic, it is safe to assume that any model checking application to discrete regulatory networks subsumes reachability, which is easily expressible by a simple temporal formula. Indeed, to model check reachability properties only the rst step of the temporal model checking is required as no accepting cycle is necessary to validate the formula. Our unfolding application being limited to reachability properties, it is natural to ask if other types of questions could be answered. While model checking using the unfolding semantics of transition system products has been studied extensively [START_REF] Esparza | Unfoldings A Partial-Order Approach to Model Checking[END_REF], the feasibility of conducting model checking on the parametric unfolding remains largely unexplored.

Reachability Analysis

Many of the common regulatory network questions can be formulated as reachability properties. Reachability can be easily expressed within temporal logic using a single temporal operator, rendering much of the model checking apparatus redundant. Several works on the regulatory networks therefore aim at improving the scalability by foregoing model checking in favour of the simpler reachability analysis. Similar to our abstract semantics, in [START_REF] Ostrowski | Boolean network identication from perturbation time series data combining dynamics abstraction and logic programming[END_REF], the authors also rely on computing an over-approximation of the admissible parametrisation set. Unlike with unfolding, where the state space is explored explicitly, the authors rely on encoding the reachability problem into constraints on the parametrisation set. Although technically similar to the approach in [START_REF] Fromentin | Analysing gene regulatory networks by both constraint programming and model-checking[END_REF], which allowed translating CTL properties into constraints, Ostrowski et al. [START_REF] Ostrowski | Boolean network identication from perturbation time series data combining dynamics abstraction and logic programming[END_REF] limit themselves to reachability properties, obtaining simpler constraints.

The constraints being on the parametrisations rather than the state space, the method of Ostrowski et al. [START_REF] Ostrowski | Boolean network identication from perturbation time series data combining dynamics abstraction and logic programming[END_REF] computes an over-approximation of the parametrisation set enabling given dynamical properties directly. By computing the over-approximation rather than the precise set of parametrisations, the authors managed to obtain simpler constraints on the parametrisation set. In turn, the constraints are solvable using ecient methods, such as answer set programming. Ostrowski et al. [START_REF] Ostrowski | Boolean network identication from perturbation time series data combining dynamics abstraction and logic programming[END_REF] propose using model checking on the restricted parametrisation set to lter out false positives or further analysis. The tractability of the model checking is thus improved by restriction of the input set of parametrised models. A similar approach is possible to lter out false positives within the parametrisation sets computed within our abstract semantics. Additionally, we also allow computing complete nite prexes to represent the dynamics on the reachable state space, allowing it to be exploited during the model checking.

Corblin et al. [START_REF] Corblin | Applications of a formal approach to decipher discrete genetic networks[END_REF] also rely on constraints to over-approximate reachability properties. The constraints for a given reachability problem are formulated directly on the dynamics, essentially describing a trace. The method of Corblin et al. [START_REF] Corblin | Applications of a formal approach to decipher discrete genetic networks[END_REF] relies on translating the computed constraints to a Boolean formula, allowing them to capitalise on the ecient SAT implementations. The authors also tackle the problem of a minimal inuence graph able to express the coveted dynamical property. This is done using inuence properties akin to our observability constraint. While we do not directly support such inference, it is straightforward to obtain the inuences which are not observable under a parametrisation (or a set of parametrisations) enabling the dynamical property.

Another approach is tailored for time series data, i.e. sequence of measurements over time during an experiment. Represented as sequence of (partially) observed states, time series data are common for regulatory networks.

Cummins et al. [START_REF] Cummins | Model rejection and parameter reduction via time series[END_REF] use pattern matching of graphs to determine whether a model can reproduce the time series data. To achieve this, both the time series data and the model dynamics are represented as directed graphs representing the possible evolution of the variable values. Matching a path (trace) within the pattern graph of the time series data with a path in the search graph representing the regulatory network dynamics thus validates the model with respect to the coveted behaviour.

The approach in [START_REF] Cummins | Model rejection and parameter reduction via time series[END_REF] relies on modelling of regulatory networks as switching systems [START_REF] Cummins | Database of dynamic signatures generated by regulatory networks (dsgrn)[END_REF]. Unlike our purely discrete representation, the switching systems describe the dynamics by means of dierential equations, however, the values of the variables are interpreted in discrete fashion, based on established thresholds. Following the switching system semantics, the directed graphs used in [START_REF] Cummins | Model rejection and parameter reduction via time series[END_REF] use nodes to represent monotonic evolution of a variable, e.g. variable a is increasing, and edges to represent a variable reaching a local extrema. Discretisation based on the piecewise linearity of the variable value evolution can be more precise than classical Boolean discretisation, especially if the local maxima or minima of a single variable dier along the evolution, making it impossible to dierentiate every local extrema by a single threshold. The most-permissive semantics of Boolean networks [START_REF] Paulevé | Reconciling qualitative, abstract, and scalable modeling of biological networks[END_REF], discussed in Chapter 11, represent states in a similar fashion.

Of particular interest is the work of Gallet et al. [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF] due to the distinct similarity with our approach. Much like the parametrisation sets we use in the abstract parametric regulatory network semantics, constraints on the parametrisation set are computed on the run in [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF]. The constraints on the parametrisation space take shape of a Boolean formulae and, while exact, the formulae grow in size as new constraints are added during the computation. The parametrisation set representation using the Boolean formulae constraints can thus easily exceed our parametrisation lattice in size and complexity.

Another similarity to our work spans from the representation of the state space itself. In order to combat the combinatorial explosion of the state space, Gallet et al. [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF] use symbolic execution trees to represent the reachable state space. The symbolic execution trees are similar to the unfoldings. As the name suggests, the tree structure oers an acyclic representation of the reachable state space. Coupled with the constraint based parametrisation sets, representing behaviour of multiple parametrisations collectively becomes possible. The unfolding semantics, however, additionally allow us to exploit concurrency. While the symbolic execution trees are model checking ready [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF], the size of the complete nite prex is generally signicantly smaller than the symbolic execution trees, as illustrated by experimental results in Chapter 9.

Finally, a very elegant related work is the modication of Hoare logic for the gene regulatory networks [START_REF] Bernot | A genetically modied hoare logic[END_REF]. Hoare logic has been introduced for proves of correctness of imperative programs. More precisely, a Hoare triple consists of a pre-condition, the program itself and post-condition. The Hoare triple is satised (reducible by inference rules) if running the program under the precondition, the program nishes and the postcondition holds. The genetically modied Hoare logic of [START_REF] Bernot | A genetically modied hoare logic[END_REF] uses time series data in place of the program, allowing one to prove that under given pre-condition, the model can replicate the specied trace and the post-condition holds. Similar to the graph pattern matching approach of [START_REF] Cummins | Model rejection and parameter reduction via time series[END_REF] which is also tailored for time series data, the measurement data is interpreted as a sequence of monotonic variable value evolutions rather than the standard Boolean discretisation based on thresholds.

Constructing proves of Hoare triples allows one to prove that a given dynamical property is enabled under a chosen parametrisation or set of parametrisations. The true power of the approach in [START_REF] Bernot | A genetically modied hoare logic[END_REF], however, lies in the ability to compute the weakest pre-condition from the time series data and the postcondition. The weakest pre-condition is then the specication of all parametrisations which enable the coveted dynamical behaviour. The pre-condition and post-conditions are arbitrary propositional formulae on the variable and parameter values, leading to considerable exibility of the Hoare triple representation of the regulatory network validation against time series data. The framework therefore allows for experiment interventions, such as disabling a particular variable (knockouts), to be modelled accurately.

The weakest precondition computation of [START_REF] Bernot | A genetically modied hoare logic[END_REF] is equivalent to computing the branches of complete nite prex which correspond to the given time series data and collecting the associated parametrisation sets. Unlike our abstract parametric regulatory network semantics, however, the weakest precondition computation is precise. The parametrisation set being represented by the precondition, i.e. a propositional formula on the parameters, the size of the formula may grow signicantly larger than the parametrisation lattice, especially if monotonicity inuence constraints are represented explicitly.

Other Applications

In this section we introduce other works of interest, which do not directly fall in line with one of the two main approaches pinpointed for the parameter inference.

Streck et al. [START_REF] Streck | Comparative statistical analysis of qualitative parametrization sets[END_REF] propose a method for statistical labelling and ranking of the admissible parametrisations. Several labels, both variable and inuence specic as well as spanning the entire parametrisation are proposed. Using the labels, a partial order on the parametrisations is obtained, ranking them in terms of cost, i.e. how many transitions does the associated parametrised network require to satisfy the dynamical property, robustness, i.e. what is the probability of a random trace of the parametrised network satisfying the dynamical property, or impact of a particular inuence, i.e. how often does the value of a variable update to the one proposed by the sole action of the given inuence, etc. The ranking is then used to rene the model in line with the best scoring parametrisations. As the parametrisations are labelled on individual basis, the method relies on explicit representation of the parametrisations. While only the admissible parametrisations have to be enumerated, such as the parametrisation lattice, the explicit enumeration still negatively impacts tractability.

A commonly used characteristic of gene regulatory networks are the attractors, i.e. sets of states from which the model cannot escape (terminal or bottom strongly connected components of the state transition graph). While closely related to reachability, attractor analysis, that is identication of the attractors, is a signicantly more challenging problem. While many methods of attractor analysis have been proposed for discrete regulatory networks [START_REF] Abou-Jaoudé | Logical modeling and dynamical analysis of cellular networks[END_REF][START_REF] Chatain | Characterization of reachable attractors using Petri net unfoldings[END_REF][START_REF] Choo | An ecient algorithm for identifying primary phenotype attractors of a large-scale boolean network[END_REF][START_REF] Klarner | Computing maximal and minimal trap spaces of boolean networks[END_REF][START_REF] Akutsu | Integer programming-based methods for attractor detection and control of boolean networks[END_REF][START_REF] Devloo | Identication of all steady states in large networks by logical analysis[END_REF][START_REF] Guo | A parallel attractor nding algorithm based on boolean satisability for genetic regulatory networks[END_REF][START_REF] Mushthofa | Computing attractors of multi-valued gene regulatory networks using fuzzy answer set programming[END_REF], it is only recently that a method emerged for the parametric regulatory networks [START_REF] Barnat | Detecting attractors in biological models with uncertain parameters[END_REF].

The method of Barnat et al. [START_REF] Barnat | Detecting attractors in biological models with uncertain parameters[END_REF] relies on a parallelisable algorithm searching for terminal strongly connected components. To take parametrisations into effect, each reachability check is conditioned by the parametrisations that enable said reachability, eectively annotating states with admissible parametrisation sets akin to our parametric regulatory network semantics. To avoid explicit parametrisation enumeration, binary decision diagrams, eectively equivalent to propositional formulae, are used to represent the parametrisation sets. In case monotonicity inuence constraints are used, the binary decision diagram representation suers from the same explosion in complexity as propositional formulae due to the diculty in enumerating the monotonic Boolean functions. Unlike the parametrisation lattices, however, binary decision diagrams support unions which are necessary for the attractor analysis algorithm.

Chapter 9

Experimental Results

In this chapter we present experimental results for construction of the reachable state space using the parametric regulatory network unfolding semantics coupled with the abstraction of the parametrisation sets. The unfolding procedure and complete nite prex construction for parametric regulatory networks as per Chapter 6 have been implemented in a prototype tool Pawn written in Python. 1 The experiments make use of several well-known Boolean and general multivalued parametric regulatory networks that have been studied in the literature. These results have rst been published in [START_REF] Kolcák | Parameter Space Abstraction and Unfolding Semantics of Discrete Regulatory Networks[END_REF].

Several regulatory network models were selected for the experiments varying in size of the network, in average connectivity of the nodes in the inuence graph and in the network type (only Boolean versus general multivalued). Each experiment consists of constructing the full representation of the reachable state space as a complete nite prex of the unfolding from a given initial state and all possible parametrisations ( P = P (G m m m )). All parametric regulatory networks considered are also equipped with a well-formed inuence constraint set according to which each inuence is considered both monotonic and observable. The number of events outside of cut-os corresponds to the number of reachable state and parametrisation set combinations. The number of non-cut-o events therefore gives a good notion of size of the computed complete nite prex. We construct multiple complete nite prexes from dierent initial states for some of the models, where the initial state signicantly impacts the size of the reachable state space. By default, however, we consider the initial states as introduced in the original model from the literature.

To illustrate the compaction achieved by the combination of unfolding semantics and parametrisation set abstraction, we compare the size of the unfoldings with the size of the complete symbolic execution tree computed from the same initial state. To construct the symbolic execution trees, we employ the tool SPuTNIk [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF] which implements automata-based LTL model checking of parametric regulatory networks by (nite) symbolic execution of the product automaton. SPuTNIk explicitly traverses the product states using a depth-rst 1 Pawn is available online: https://github.com/GeorgeKolcak/Pawn. search approach while symbolically executing the transitions representing constraints on the parameters, such as the inuence constraints or constraints based on previously executed transitions. To achieve exactly the reachable states of the state space graph of the regulatory network, we employ a Büchi automaton with a single state looping over an atomic proposition satised in every state of the model.

In [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF], the authors consider an additional constraint on the parametrisation sets called Min-Max, which is also implemented in the SPuTNIk tool. The Min-Max constraint requires that in every state of the parametric regulatory network where all the activators (respectively inhibitors) are at their maximum values and all of the inhibitors (respectively activators) are zero at the same time, the regulation function for the variable in question must point to the maximum (respectively minimum) possible value. Such states correspond to the v -maximal (respectively v -minimal) regulator states of the relevant variable. As such, Min-Max constraint translates to xing the value of the v -maximal regulator state to maximum in 0 0 0 (respectively the v -minimal regulator state to minimum in 1 1 1) within the initial parametrisation lattice [0 0 0, 1 1 1]. To this end, we have also included the Min-Max constraint in Pawn.

As aforementioned, the inuence constraint set of all the considered parametric regulatory networks contain both a monotonicity and an observability constraint for each inuence in the network. Application of the additional Min-Max constraint is explicitly indicated.

First of the parametric regulatory networks we use is a Boolean model of the gene regulatory network underlying mammalian cortical area development [START_REF] Giacomantonio | A boolean model of the gene regulatory network underlying mammalian cortical area development[END_REF], shown in Figure 9.1. We consider two dierent initial conditions, or more precisely, initial states for the unfolding. First, with all the variables initialised to zero and second, with all variable inactive (zero) with the exception of the Fgf8, which is initialised to one. The smallest of the multivalued parametric regulatory networks we consider is the extensively studied regulatory network of the bacteriophage λ life cycle [START_REF] Thiery | Dynamical behaviour of biological regulatory networksii. immunity control in bacteriophage lambda[END_REF] (known colloquially as λ-switch) shown in Figure 9.2 This model has also been studied in other works aimed at analysis of parametric networks [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF][START_REF] Klarner | Parameter identication and model ranking of thomas networks[END_REF]. We consider only one initial state for the λ-switch, which sets all variables to zero. We do, however, utilise the model in two experiments, one with and one without the Min-Max constraint.

As an example of a larger Boolean model, we consider a model of EGF-TNFα signalling pathway [START_REF] Macnamara | Statetime spectrum of signal transduction logic models[END_REF][START_REF] Ostrowski | Boolean network identication from perturbation time series data combining dynamics abstraction and logic programming[END_REF] shown in Figure 9.3. In the case of this parametric regulatory network, the initial state of the unfolding sets the variables tnfa and egf to active (value one) whereas all other variables are considered inactive (value zero).

Finally, we consider a couple of larger multivalued networks (with more than 10 variables). First, we analyse a parametric regulatory network adopted from [START_REF] Mbodj | Logical modelling of drosophila signalling pathways[END_REF]. The model, illustrated in Figure 9.4, represents several key signalling pathways of Drosophila, including inuences between the pathways (cross-talks).

Second, we analyse a model describing the control of the developmental process in primary sex determination of placental mammals [START_REF] Sánchez | Primary sex determination of placental mammals: a modelling study uncovers dynamical developmental constraints in the formation of sertoli and granulosa cells[END_REF]. While slightly smaller in terms of number of variables, 14, than the Drosophila network, the primary sex determination model, depicted in Figure 9.5, is highly intercon- Computations conducted on all the dened models have led to results shown in Table 9.1. Complete nite prexes of the unfoldings constructed by Pawn are characterised by their size given by both total number of events and events without cut-os. A relatively large portion of cut-o events indicates the large number of dierent behaviours spread among the dierent parametrisations. The number of symbolically executed states computed by SPuTNIk is given for comparison.

Since both tools are implemented as prototypes without any optimisations, we do not include computation times but rather focus on size of the reachable state space representation. However, in all models with the only exception of the Primary Sex Determination model, the computation by Pawn concluded within a couple of minutes. In case of the Primary Sex Determination model, Pawn constructed the complete nite prex in 2 hours whereas SPuTNIk has been stopped in 3 days without achieving results. In case of the Drosophila model, SPuTNIk has been stopped after 2 days of computations whereas Pawn needed a couple of minutes to compute the complete nite prex. SPuTNIk reached a symbolic execution tree of size at least 7, 000, 000 before being timed out in all three relevant cases. As timing was not a concern, all experiments have been conducted on a standard laptop computer.

Using the concurrency aware, partial order semantics shows a great improvement in the compactness of the resulting structure. It is striking in the case of models of signalling pathway cross-talks (Drosophila and EGF-TNFα) where the amount of concurrency among the variables is high due to the sparsity of the inuence graph. The size of unfolding prexes remains very compact even in cases with more interwoven topology. It is worth noting that the constructed Comparison of the size of the obtained structures between complete nite prexes of the unfolding and the symbolic representation for dierent models. The number of unfolding events is specied as a total number of non-cut-o events. The number including cut-o events is given in brackets. Symbolic representation size is the number of states of the complete execution tree constructed by SPuTNIk. The notation '>7,000,000' refers to the size being over 7, 000, 000 by the time the particular experiment has been stopped after 2 or more days of computation.

complete nite prexes preserve the set of reachable states and any process can be reconstructed from the prex with an additional computation cost [START_REF] Esparza | Unfolding based algorithms for the reachability problem[END_REF].

Another interesting observation can be made on the model of cortical development in mammals, showing that the unfolding and consequently the complete nite prex is sensitive to the initial state. In this model, the considered initial states give the same reachable state space. However, depending on the initial state, the respective unfoldings have substantially dierent size. This can be attributed especially to the dependence on the parametrisation sets, and their incompatibility with the total adequate order [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], which may result in higher fragmentation of the parametrisation sets in some cases.

Theorem 5.1 ensures that the set of reachable states in the complete nite prex is exact despite the over-approximation of the parametrisation sets. I.e. for each reachable state there exists at least one parametrisation which is a true positive within the computed parametrisation set. The false positives can be identied by running model checking or other exact algorithm on the overapproximated parametrisation set, thus obtaining a much smaller and much more manageable set of initial parametrisations.

Summary

This thesis explores in detail the parametric model of regulatory networks and associated algorithms. The parametric regulatory network analysis is largely hampered by combinatorial explosion in the number of states, same as discrete regulatory networks, as well as the number valid combinations of parameter value assignments called parametrisations. We tackle those challenges by specialised semantics, which allow exploration of the parametric regulatory network behaviour without explicit enumeration of states or parametrisations.

To avoid explicit enumeration of parametrisations, we introduce an abstraction of parametrisation sets by the means of their convex cover. We show that this abstraction is exact for the parametric regulatory networks without inuence constraint and it leads to a sound and minimal over-approximation if inuence constraints are considered.

Rather than abstraction, we evade explicit state enumeration by the means of partial order reduction. We elevate the unfolding semantics from Petri nets to parametric regulatory networks, thus being able to capitalise on the concurrency abundant in biological systems.

Both of the introduced approaches are expressed as dierent semantics of parametric regulatory networks. Thanks to being orthogonal not only in their purpose, but also in their design, the two semantics can be naturally combined, allowing us to alleviate both sources of combinatorial explosion at once. The resulting combined semantics have been implemented for the purposes of reachable state space exploration and experimental results show the resulting representation of the reachable state space is signicantly smaller compared to other approaches.

We further investigate the possibility of using known target state to optimise the state space exploration of parametric regulatory networks. To this end, we elevate a model reduction method based on pruning transitions which cannot lead to a target state from automata networks to parametric regulatory networks.

The thesis oers a thorough analysis of parametrisation set abstraction and unfolding semantics for parametric regulatory networks. Many questions 119 related to parametric regulatory networks remain unanswered, however, opening up multiple possibilities for future development, not only in the area of parametric regulatory networks themselves, but also in exploration of related concepts where parametric regulatory network might help in providing the necessary insight. Chapter 11 Ongoing and Future Work

In this chapter we explore ongoing and future work building up on the analysis of the parametric regulatory networks as well as related concepts. The work conducted and potential future work contains several renements and extension of the abstract and unfolding semantics of the parametric regulatory networks, new application areas beyond reachability, as well as questions of expressivity and monotonicity of continuous models of regulatory networks and their discrete counterpart.

The rst potential area for future work is the abstraction of parametrisation space. The parametrisation set abstraction as we introduce it uses very basic algebraic structures. While this ensures many nice properties for the abstraction, including a small static size, it also makes the abstraction considerably rigid. This opens up potential for introduction of a more complex as well as more permissible structure which could help reduce the over-approximation, optimise the restriction to inuence constraints or even tackle fundamental limitations of the convex sublattice approach which renders ecient unions impossible (unions are crucial for some applications, see Section 11.1).

On a related note, the abstract semantics of the parametric regulatory networks have the potential to be amended to account for more constraints than the monotonicity and observability inuence constraints we consider. This potential is illustrated by the adaptation of the Min-Max constraint considered in [START_REF] Gallet | Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014[END_REF] in Chapter 9. While the Min-Max constraint is relatively simple, more complex constraints could be considered on both the inuences or the parameters directly.

Renement of the unfolding semantics also opens up many interesting avenues for future work. Due to the nature of the asynchronous multivalued network semantics as we dene them, only one variable changes values with each transition. However, the transition being enabled may be dependent on the values of numerous other variables. As a result, each event in the parametric regulatory network unfolding has to consider such a variable among its preconditions only to include a postcondition labelled by the same variable and value. Instead, this dependency could be represented by an equivalent of 121 a read arc used in contextual Petri nets. Petri net unfolding semantics have been extended to contextual Petri nets relying on asymmetric conict relation, which allows a condition to be read without producing a copy [START_REF] Baldan | Ecient unfolding of contextual petri nets[END_REF]. This not only contributes to smaller prexes overall but also to overall improvement of the running time. As the parametric regulatory network unfoldings are very similar to Petri net unfoldings there is good reasoning to believe that the techniques used in [START_REF] Baldan | Ecient unfolding of contextual petri nets[END_REF] could be adapted to parametric regulatory network unfolding almost eortlessly and should certainly be considered for implementation of an ecient tool for parametric regulatory network unfolding to replace the prototype tool Pawn.

Another potential for improvement of the unfolding semantics lies in the adequate order. Designing a total adequate order that could minimise the required amount of backwards cut-os would be greatly benecial for reducing the runtime of the unfolding algorithm. While nding a suitable adequate order is a highly nontrivial problem, there is a potential for obtaining insights into other unfolding applications that rely on annotated events and suer from a similar diculty during complete nite prex construction.

Another signicant potential for expansion of the presented results is the exploration of further application areas. In our work we have focused mostly on reachability problems. As discussed in Chapter 8, however, other applications are highly relevant for the study of biological regulatory networks.

One such application is model checking. Our results are already highly compatible with model checking approaches for discrete regulatory networks. In particular, by rst utilising our abstract semantics to obtain a restricted set of parametrisations, one could greatly reduce the number of models for which model checking is necessary. Running model checking directly on the parametric regulatory networks, however, is a far more attractive application. While parametric regulatory networks with abstract semantics are in essence model checking ready and model checking algorithms have also been proposed for unfoldings [START_REF] Esparza | Unfoldings A Partial-Order Approach to Model Checking[END_REF], porting of model checking algorithms to parametric regulatory network unfoldings remains nontrivial and will likely result in the need to compute unions of abstract parametrisation sets.

An alternative to full scale model checking may be ecient algorithms for another common problem on regulatory networks beside reachability, such as attractor analysis briey discussed in Section 8.3 of Chapter 8. As the topic of attractor analysis subsumes several nontrivial approaches, we explore it in the detail it warrants in Section 11.1.

Very interesting work has also been done on models that might be employed to model biological regulatory networks from a perspective similar to parametric regulatory networks. In particular, promising results have been obtained for new symbolic semantics of Boolean networks called most-permissive semantics [START_REF] Paulevé | Reconciling qualitative, abstract, and scalable modeling of biological networks[END_REF]. While the most permissive semantics are fundamentally unrelated to parametric regulatory networks, both are essentially abstractions of Boolean networks or more broadly discrete regulatory networks. We compare the two approaches in Section 11.2.

Finally, work on relational properties of monotonic continuous systems [START_REF] Kol£ák | Relational dierential dynamic logic[END_REF] 11.1. ATTRACTOR ANALYSIS 123

shows promise for a further development of the notion of monotonicity across the spectrum of biological regulation models using dierent levels of abstraction, spanning from continuous and hybrid systems all the way to Boolean networks.

Attractor Analysis

An attractor of a discrete regulatory network is a set of states corresponding to a bottom strongly connected component in the state transition graph. In other words, for any state in the attractor it is possible to reach any other state in the same attractor, but no other state outside the attractor. Attractors of discrete regulatory networks therefore represent the long-term, stable behaviours of the system. The study of such behaviours is highly relevant in many high prole areas such as cell dierentiation, oncology and synthetic biology [START_REF] Huang | Cell fates as highdimensional attractor states of a complex gene regulatory network[END_REF][START_REF] Huang | Cancer attractors: A systems view of tumors from a gene network dynamics and developmental perspective[END_REF][START_REF] Mandon | Sequential reprogramming of boolean networks made practical[END_REF]. While attractor analysis approaches based on the unfolding semantics have been successful [START_REF] Chatain | Characterization of reachable attractors using Petri net unfoldings[END_REF], extension of such approaches to parametric regulatory networks is highly nontrivial. The technique of Chatain et al. [START_REF] Chatain | Characterization of reachable attractors using Petri net unfoldings[END_REF] relies on identifying candidate markings as the markings of maximal congurations and then checking each candidate marking by constructing another unfolding with the candidate marking as initial marking. If a dierent candidate marking is discovered during the follow-up unfolding, the initial marking is removed from the set of candidate markings because it either does not belong to an attractor, in case it is not reachable from the other candidate marking, or the same attractor will be discovered when unfolding from the other candidate marking, owing to attractors being strongly connected.

Adapting the method of [START_REF] Chatain | Characterization of reachable attractors using Petri net unfoldings[END_REF] to unfoldings of parametric regulatory networks, however, faces fundamental challenges. Parametric regulatory network unfolding may contain several instances of the same candidate marking with dierent parametrisation sets. As unions of abstract parametrisation sets cannot be eciently represented in the general case, each instance of a candidate marking has to be unfolded separately, signicantly increasing the number of unfoldings that have to be computed. Moreover, the unfoldings from the candidate markings tend to lead to larger complete nite prexes due to candidate markings being disqualied per parametrisation. With the two above diculties combined, the resulting algorithm has been found intractable for practical application. While an optimisation of the method might be envisioned to obtain practical algorithms for parametric regulatory networks, it is unlikely to be possible without ecient computation of abstract parametrisation set unions.

A promising future work on the attractor analysis of parametric regulatory networks might instead built upon the results of [START_REF] Barnat | Detecting attractors in biological models with uncertain parameters[END_REF]. The method of Barnat et al. [START_REF] Barnat | Detecting attractors in biological models with uncertain parameters[END_REF] relies on binary decision diagrams for encoding the admissible parametrisations. Computing unions for binary decision diagrams is simple, however, the size of the diagram grows with the number of variables. Indeed, the size of the binary decision diagram is exponential in the number of variables of a monotonic Boolean function. This is a challenge which does not apply to the abstract parametrisation sets, whose encoding is of constant size.

A clever combination of the two approaches thus promises a fruitful collaboration. A modication of the binary decision diagrams to accommodate the bounded convex sublattices of parametrisations could thus help keep the size of the binary decisions diagrams manageable even for variables with numerous regulators. On the other hand, splitting the parametrisation lattices into a well designed decision diagram structure might allow for ecient unions. The application of the successful combination of the two formalisms might even extend beyond attractor analysis.

Most Permissive Semantics

The most permissive semantics of Boolean networks are symbolic semantics, assigning two transitional values , to variables on top of the two Boolean values. In simple terms, the transitional values represent a variable increasing value (tending towards the maximum), respectively decreasing value (tending towards the minimum). More precisely, any variable in a transitional value may collapse to the respective Boolean value, i.e. 0 for and 1 for at any time, while any variable in the role of a regulator with transitional value may be read as either 0 or 1, irrespective of the direction. Thus, for the purposes of regulation, a variable has to either be in the Boolean value prescribed by the regulation function or in any of the transitional values , .

Boolean networks with the most-permissive semantics exhibit more behaviours than the standard semantics we introduced in Chapter 2. While the increase in expressivity may appear to be far too liberal, most permissive semantics have been shown to successfully discriminate behaviours [START_REF] Paulevé | Reconciling qualitative, abstract, and scalable modeling of biological networks[END_REF]. On the other hand, Boolean networks with most permissive semantics can reproduce any behaviour generated with generalised asynchronous semantics, or even any behaviour generated by a multivalued or continuous renement 1 of the Boolean network. Moreover, analysis of Boolean networks with most permissive semantics is computationally cheaper. Reachability properties in the most permissive semantics, for instance, can be translated to SAT problems, facilitating the use of some of the fastest NP algorithms.

Albeit fundamentally dierent, the most permissive semantics of Boolean networks as well as parametric regulatory networks serve to lessen the mathematical rigidity of discrete regulatory networks with the standard semantics, thus reducing the number of parameters required for modelling. In spite of helping to achieve the same result, the approaches are dierent not only in nature but also by interpretation. Whereas parametric regulatory networks abandon the standard regulation function, but by the means of parametrisations retain full specication of the emergent behaviour, the most permissive semantics are applied to Boolean networks specied by the regulation function, but abstract away the exact specication of the resulting behaviour. 1 Please refer to [START_REF] Paulevé | Reconciling qualitative, abstract, and scalable modeling of biological networks[END_REF] for details.

The duality between most permissive semantics and parametric regulatory networks opens up several questions of interest. One such a question is naturally the possibility to combine the two approaches while preserving their respective strengths. While it might be possible to directly elevate the most permissive semantics to Boolean parametric regulatory networks, the use of symbolic states makes it unlikely that parametrisation sets could be eciently restricted. A dierent point of view, a translation between traces of a Boolean network with most permissive semantics and parametrisation sets of a corresponding parametric regulatory network and vice versa, shows promise for the purposes of parameter inference and model renement.

Study of the connection between traces or behaviours and parameters is of signicance even beyond a precise translation. Linking behavioural patterns observable in Boolean networks with most permissive semantics to parameter values and their relations has the potential to uncover new meaningful constraints for parametric regulatory networks that could help restrict or otherwise shape the admissible parametrisation sets.

The development of most permissive semantics also stands to benet from establishing relations to parametrisation. In particular, in regards to the local monotonicity of the regulation function, which is often at least partially known in the literature. The monotonicity constraints on inuences form the cornerstone of parametrisation set restriction, the most permissive semantics of Boolean networks however, lack any means to discriminate between monotonic and nonmonotonic behaviour. This is underlined by the capability of a variable with increasing value, to be rst used as if valued 1 and subsequently as if valued 0 for regulation of another variable, thus violating the intuition of increasing its value. A preliminary study of the monotonicity under the most permissive semantics shows that while enforcing monotonic behaviour is possible, the usual notion of monotonicity in multivalued and continuous models does not straightforwardly translate into the Boolean abstraction with transitional values , . Classifying the behaviours generated by Boolean networks with most permissive semantics based on local monotonicity inferred from parametric representation might thus lead to valuable insights into monotonicity under most permissive semantics as such as well as relations of monotonicity across various renements of Boolean networks. The details on how dierent regulators cooperate, and even more so on rates for those interactions, however, are rarely available. Discrete regulatory networks thus oer an approprite abtraction as they require few parameters compared to quantitative models. Nevertheless, determining the discrete parameters is a well known challenge. The set of admissible parameter value assignements (parametrisations) is represented by parametric regulatory networks. The analysis of parametric regulatory network dynamics is, however, hampered by dual combinatorial explosion, of the state space and of the parametrisation space. We develop methods aimed at alleviating the combinatorial explosion. First, we introduce abstract interpretation for the set of admissible parametrisations, achieving constant size encoding, at the cost of a conservative overapproximation. Second, we lift partial order semantics in the form of unfolding from Petri nets to parametric regulatory networks, harnessing concurrency for ecient state space representation.

Université Paris-Saclay Espace Technologique / Immeuble Discovery Route de l'Orme aux Merisiers RD 128 / 91190 Saint-Aubin, France

∆

  ⇐⇒ y y y = F (x x x)We use the natural inx notation x x x F -→ sync y y y to denote membership in the semantics relation, (x x x, y y y) ∈

  of state y y y from state x x x by synchronous transitions. Under synchronous semantics, each state x x x ∈ n Π v=1

  membership in the semantics relation and the reexive and transitive closure x x x F -→ * async y y y to denote reachability of state y y y from state x x x in F .

  for membership and the reexive and transitive closure x x x F -→ * gen y y y to denote reachability of state y y y from state x x x in F .

Denition 2 . 8 (

 28 Multivalued Network). A multivalued network F of dimension n is a function F : n Π v=1 ↓m m m v → n Π v=1 ↓m m m v where ↓x = { y ∈ N 0 | y ≤ x } is the smallest downward closed subset of natural numbers with zero containing x, And m m m = (m m m 1 , . . . , m m m n ) ∈ N n is the vector of maximum values of the individual variables. To simplify notation, we write X m m m = n Π v=1 ↓m m m v to denote the state space of multivalued networks.

Denition 2 . 10 (

 210 Positive Monotonicity). Let F be a multivalued network of dimension n, m m m the vector of maximum values of the individual variables and let G = (V, I) be an inuence graph of F .

FFigure 2 . 1 :

 21 Figure 2.1: The smallest inuence graph of the multivalued network F A .

  .2 and Figure 2.3 showing the state space graph of F A with synchronous semantics,

Figure 2 . 2 :Figure 2 . 3 :

 2223 Figure 2.2: The state space of the multivalued network F A with the synchronous semantics. States are represented by concatenation of variable values in the natural order.

  .2 being split into two connected components. One component drains into the loop 101 ↔ 210 (a and b change value in the same direction) while the other drains into the loop 111 ↔ 201 (a and b change value in the opposite direction).

Figure 2 . 4 :

 24 Figure 2.4: The smallest inuence graph of the Boolean network F B .

Figure 2 . 4 .

 24 While variables b, c, d only depend on a single regulator (|R(b)| = |R(c)| = |R(d)| = 1), the value of variable a evolves according to 3 regulators (R(a) = {b, c, d}).

Figure 2 . 5 and

 25 Figure 2.6 illustrate the state space graphs of F B with synchronous semantics sole regulators of variables b and d are the variables themselves, R(b) = {b}, R(d) = {d}. Moreover, since the variables b and d have negative monotonic inuence on themselves, they are frustrated in each state, f b (x x x) = x x x b and f d (x x x) = x x x d for any state x x x. The variables b and d wanting to change value in any state leads to signicant number of transitions in the asynchronous semantics. The transitions updating the value of the variables b and d are thus abstracted in Figure 2.6 to improve readability.

Figure 2 . 5 :Figure 2 . 6 :

 2526 Figure 2.5: The state space graph of the Boolean network F B with synchronous semantics. States are represented by concatenation of variable values in the natural order.

F

  C : b b b → (2 (1 -b b b a ) , ¬ (b b b b ) , b b b a ∨ b b b b )

Figure 2 . 7 :

 27 Figure 2.7: The state space of the Thomas network (F C , t) with the asynchronous semantics. States are represented by concatenation of variable values in the natural order and transitions are annotated by the unique variable changing value (v (t)) and the direction of the change.

Denition 3 . 6 (

 36 Branching Process). A branching process of a Petri net (P, T, W, M 0 ) is an occurrence net O labelled with function β : B ∪ E → P ∪ T such that: 1. β (B) ⊆ P and β (E) ⊆ T (β preserves the nature of nodes).

2 .

 2 Given an arbitrary event e ∈ E. ∀ b ∈ • e, β (b) ∈ • β (e) and vice versa, ∀ p ∈ • β (e), there exists a unique b = β -1 (p) and b ∈ • e. (β restricted to • e is a bijection.) Similarly, ∀ b ∈ e • , β (b) ∈ β (e) • and vice versa, ∀ p ∈ β (e) • , b = β -1 (p) is unique and b ∈ e • . (β restricted to e • is a bijection.) 3. ∀ b ∈ min((O)), β (b) ∈ M 0 and ∀ p ∈ M 0 , b = β -1 (p) is unique and b ∈ min((O)). (β restricted to causality-minimal conditions is a bijection with the initial marking.) 4. ∀ e 0 , e 1 ∈ E, • e 0 = • e 1 ∧ β (e 0 ) = β (e 1 ) =⇒ e 0 = e 1 (No duplicate transitions).

2 . 3 .

 23 min((O )) ⊆ B (The natural initial marking is the same for both branching processes); For each condition b ∈ B and the single event e ∈ E such that e ∈ • b (if it exists), e ∈ E; 4. Similarly, for each event e ∈ E and each condition b ∈ B such that b ∈ • e ∪ e • , b ∈ B; 5. For each x ∈ B ∪ E, β (x) = β (x) (β is the restriction of β to O).

Denition 3 . 12 (

 312 Local Conguration). Let (O, β) be a branching process with O = (B, E, F ) and let e ∈ E be an arbitrary event. The local conguration [e] ⊆ E of event e is the downward closure, with respect to the causality relation, of the singleton set {e} within the set of events E, [e] = { e ∈ E | e ≤ e }. The local conguration of any event e ∈ E is trivially a conguration of (O, β). Any conguration C containing an event e is necessarily an extension of the local conguration, e ∈ C =⇒ [e] ⊆ C. Thus, shall there exist a dierent event e with β (Cut ([e])) = β (Cut ([e ])), there must exist an extension of [e ] isomorphic to C, or more precisely to C \ [e].

Denition 3 .

 3 14 (Cut-O Event). Let (O, β) be a nite branching process of a Petri net (P, T, W, M ) and let (O , β ) be another branching process of the same Petri net such that B = B ∪ e • and E = E ∪ {e}, where e ∈ PE ((O, β)) is a possible extension of the branching process (O, β). Then the event e is a cut-o in (O , β ), e ∈ cutoffs ((O , β )), if and only if there exists an event e ∈ E such that β (Cut ([e])) = β (Cut ([e ])).

Denition 4 . 4 (

 44 Parametrised Network). Let G m m m be a parametric regulatory network of dimension n and let P P P ∈ P (G m m m ) be a parametrisation of G m m m .

Example 4 . 1 .

 41 Let G = G(F A ) be the minimal inuence graph of the multivalued network F A from Example 2.1 and let m m m = (2, 1, 1). G m m m is then the parametric regulatory network with the same inuence graph and variable domains as the multivalued network F A .

Denition 4 . 5 (

 45 Parametrisation Order). Let G m m m be a parametric regulatory network.

Denition 4 . 6 (

 46 Parametrisation Set Enabling a Transition). Let G m m m be a parametric regulatory network and letF P P P-→ be a multivalued network semantics of an arbitrary but xed type for all P P P ∈ P (G m m m ).

  Gm m m -→ to denote the set of all parametrisation sets of G m m m enabling some transition set possible under the semantics Gm m m -→, formally:

F

  synchronicity relation S for all P P P ∈ P (G m m m ).

Denition 4 . 10 (F

 410 Parametrisation Set Enabling a Transition under Generalised Asynchronous or Derived Semantics). Let G m m m be a parametric regulatory network and let network semantics of an arbitrary but xed type for all P P P ∈ P (G m m m ).

  the parametrisation set p (t) enabling t is dened as follows: p ((x x x, y y y)) ∆ = P P P ∈ P (G m m m ) (x x x, y y y) ∈ F P P P -→ = P∈K((x x x,y y y))

Example 4 . 2 .

 42 Take the parametric regulatory network G m m m from Example 4.1 and a generalised asynchronous transition t = (201, 111) with S (t) = {a, b, c}.

Denition 4 .

 4 11 (Parametrisation Lattice). Let G m m m be a parametric regulatory network and let (P (G m m m ) , ≤ Gm m m ) be the lattice of all parametrisations of G m m m with the parametrisation order. Then, a parametrisation lattice generated by 0 0 0, 1 1 1 ∈ P (G m m m ) is the lattice [0 0 0, 1 1 1] = (P, ≤ Gm m m ) where P = { P P P ∈ P (G m m m ) | 0 0 0 ≤ Gm m m P P P ≤ Gm m m 1 1 1 }. We write P (G m m m ) = { [0 0 0, 1 1 1] | 0 0 0, 1 1 1 ∈ P (G m m m ) } to denote the set of all parametrisation lattices of the parametric regulatory network G m m m .

Denition 4 .

 4 13 (Abstract Semantics of Parametric Regulatory Networks). Let G m m m be a parametric regulatory network of dimension n and let F P P P -→ ⊆ F P P P -→ gen be a multivalued network semantics of xed type for all P P P ∈ P (G m m m ).

  Gm m m -→ , are exactly the element sets of the parametrisation lattices. The abstraction restricted to P Gm m m -→ is hence exact.

Theorem 4 . 1 (

 41 Parametrisation Set Abstraction is Exact). Let G m m m be a parametric regulatory network with semantics Gm m m -→ ⊆ Gm m m -→ gen . Then, for any P ∈ P Gm m m -→ and for any [0 0 0, 1 1 1] ∈ P (G m m m ):

  Corollary 4.1.1 (Concrete and Abstract Semantics of Parametric Regulatory Networks are Equivalent). Let G m m m be a parametric regulatory network and let Gm m m be the concrete and abstract semantics of G m m m of arbitrary but xed type. Then, for an arbitrary set of transitions T ∈ P P P ∈P(Gm m m ) F P P P -→ and arbitrary states x x x, y y y ∈ X m m m : (x x x, p (T )) Gm m m -→ (y y y, p (T ∪ {(x x x, y y y)})) ⇐⇒ x x x, p (T ) Gm m m -→ abs y y y, p (T ∪ {(x x x, y y y)}) Theorem 4.1 also gives us stronger grasp on the abstract parametrisation sets enabling a transition themselves. In particular, we now have P P P ∈ α (p (t)) ⇐⇒ P P P ∈ p (t). This allows us to simplify the Denition 4.13 of abstract parametric regulatory network semantics, similarly to the concrete semantics, Denition 4.8. Corollary 4.1.2 (Equivalent Denition of Abstract Parametric Regulatory Network Semantics). Let G m m m be a parametric regulatory network and let Gm m m be abstract semantics of G m m m .

  ω ω the computation of p (T ∪ {t}) benets again from Theorem 4.1. Corollary 4.1.3 (Abstract Parametrisation Set Enabling a Union of Transition Sets is the Intersection). Let G m m m be a parametric regulatory network with semantics

Proposition 4 . 1 (

 41 Intersection of Parametrisation Lattices). Let G m m m be a parametric regulatory network and let [0 0 0, 11 1] , 0 0 0 , 1 1 1 ∈ P (G m m m ) be two arbitrary parametrisation lattices of G m m m .

Denition 4 . 14 (

 414 Narrowing Operator of Abstract Parametrisation Sets). Let G m m m be a parametric regulatory network with abstract semantics Gm m m -→ abs ⊆ Gm m m -→ abs•gen and let t ∈ P P P ∈P(Gm m m) F P P P

Denition 5 . 1 (

 51 Global Constraints on Parametrisations). Let G m m m be a parametric regulatory network with inuence graph G = (V, I) and let e = I be arbitrary inuence.

Denition 5 . 4 (

 54 Concrete Parametrisation Set Enabling a Transition Set and Satisfying Inuence Constraint Set). Let G m m m be a parametric regulatory network with semantics R ⊆ I × {+1, -1, o} be a well-formed inuence constraint set. Then the set of parametrisations p R (T ) enabling a transition set T ⊆ P P P ∈P(Gm m m ) F P P P -→ and satisfying the constraint set R is dened as follows: p R (T ) ∆ = p (T ) ∩ P R

Denition 5 . 5 (

 55 Constrained Semantics of Parametric Regulatory Networks). Let G m m m be a parametric regulatory network, let Gm m m of parametric regulatory network semantics and let R ⊆ I × {+1, -1, o} be a well formed inuence constraints of the inuence graph G.

Denition 5 . 6 (

 56 Monotonicity Constraint Narrowing of Abstract Parametrisation Sets). Let G m m m be a parametric regulatory network and let r = (u, v, s) ∈ R (G) where s ∈ {+1, -1} be an arbitrary monotonicity constraint.

  used to denote the set of all regulator states of v open to value decrease in [0 0 0, 1 1 1]. The action taken by the narrowing operator depends on the regulator states open in the parametrisation lattice [0 0 0, 1 1 1]. If no regulator states are open, an empty state is returned to reect that the inuence u, v is not observable under any parametrisation in [0 0 0, 1 1 1]. If, on the other hand, more than one regulator state is open to value increase, respectively value decrease, no values are increased, respectively decreased, to preserve all possibilities at the cost of overapproximation. The value is only restricted if a unique regulator state is open to value increase, respectively decrease. Denition 5.9 (Observability Constraint Narrowing of Abstract Parametrisation Sets). Let G m m m be a parametric regulatory network and let r = (u, v, o) ∈ R (G) be an arbitrary observability inuence constraint.

Denition 5 .

 5 10 (Inuence Constraint Set Narrowing). Let G m m m be a parametric regulatory network of dimension n and R (G) a well-formed set of inuence constraints. Then the global inuence constraint narrowing operator σ R(G) : P (G m m m ) → P (G m m m ) is dened as a function composition:

Denition 5 . 11 (

 511 Constrained Abstract Parametric Regulatory Network Semantics). Let G m m m be a parametric regulatory network of dimension n and let R (G) be a well-formed set of inuence constraints.

Theorem 5 . 1 (

 51 Abstraction Computed by Inuence Constraint Set Narrowing is Tight). Let G m m m be a parametric regulatory network and let R = R (G) be a well-formed set of inuence constraints.

  First, we show [p R (T ∪ {t})] ⊆ p R (T ∪ {t}) (soundness of the abstraction). If p R (T ∪ {t}) = ∅, the resulting convex cover is also empty, [p R (T ∪ {t})] = ∅ ⊆ p R (T ∪ {t}), which is in turn surely a sublattice of the abstract parametrisation set. We now assume p R (T ∪ {t}) = ∅. By Denition 5.10 and Denition 5.11, the computation of p R (T ∪ {t}) = (u,v,o)∈R σ {(u,v,o)} • v∈{1,...,n} σ v • σ t p R (T ) is divided into three iterations of narrowing. Starting with the transition t and followed by monotonicity inuence constraints and nally observability inuence constraints. We follow this separation in the soundness proof. We rst show [p R (T ∪ {t})] ⊆ σ t p R (T ) . From Theorem 4.1 we have [p (T ∪ {t})] = p (T ∪ {t}) = σ t p (T ) . We start by intersecting both sides of the equation by p R (T ), thus obtaining [p (T ∪ {t})] ∩ p R (T ) = σ t p (T ) ∩ p R (T ). Since both [p R (T ∪ {t})] ⊆ [p (T ∪ {t})] and by induction hypothesis [p R (T ∪ {t})] ⊆ [p R (T )] = p R (T ), we replace the left hand side by [p R (T ∪ {t})] changing the equality relation to a subset one, [p R (T ∪ {t})] ⊆ σ t p (T ) ∩ p R (T ). The restriction imposed by the narrowing operator σ t does not depend on the actual parametrisation set. σ t p (T ) can thus be rewritten as p (T ) ∩ p (t). As p (T ) ⊆ p R (T ), the right hand side becomes p R (T ) ∩ p (t) = σ t p R (T ) , giving us the coveted [p R (T ∪ {t})] ⊆ σ t p R (T ) . What remains to be proven is that any restriction by σ R on σ t p R (T ) is reected in [p R (T ∪ {t})]. We continue with the monotonicity inuence constraint narrowing to rst prove [p R (T ∪ {t})] ⊆ v∈{1,...,n}

  for each k ∈ N. Again, this by denition guarantees that any other regulator state is also value locked, giving us the coveted O + v ([0 0 0, 1 1 1]) = ∅, respectively O - v ([0 0 0, 1 1 1]) = ∅. This concludes the proof of p R (T ∪ {t}) ⊆ [p R (T ∪ {t})]. Combined with the soundness proof, we obtain the coveted p R (T ∪ {t}) = [p R (T ∪ {t})].

Example 5 . 1 .Figure 5 . 1 :

 5151 Figure 5.1: Inuence graph G of the Boolean network F B . The inuences are labelled with +1, -1 and o for positive monotonicity, negative monotonicity or observability constraints, respectively, that exists for the inuence in R (G ).

  that since the variables b, c and d only have one regulator, |R(b)| = |R(c)| = |R(d)| = 1, they only have two parameters each. Thus, the values of all the parameters of variables b, c and d are xed by the inuence constraint set R (G ).

Figure 5 . 2 :

 52 Figure 5.2: The Hasse diagram of the lattice (Ω a , a ). The regulator states are labelled by the concatenation of the regulator values. The diagram species the values of the parameters of variable a in the parametrisation P P P by the means of non-bold regulator states having value 0 and bold regulator states having value 1.

Figure 5 . 3 :

 53 Figure 5.3: The Hasse diagram of the monotonicity order on the regulator states of variable c. The regulator states are annotated by concatenation of individual regulator values as well as their respective parameter value in the minimum parametrisation 0 0 0. The regulator states whose values are inconsistent with the inuence constraint (a, b, +1) are labelled in bold.

  (a = 1, b = 1) and (a = 2, b = 1), highlighted in bold, thus have their minimum value increased by the narrowing operator. As such, σ (a,c,+1) ([0 0 0, 1 1 1]) = [0 0 0 [(c, 11) , (c, 21) → 1] , 1 1 1] Example 5.3. Similarly to Example 5.2, consider the parametric regulatory network G m m m from Example 4.1 and a set of inuence constraints R (G) = {(b, c, o)}.

  1]) = 0 0 0 , 1 1 1 . Example 5.4. Following from Example 5.2 and Example 5.3, consider again the parametric regulatory network G m m m from Example 4.1 and a dierent set of inuence constraints R (G) = {(a, c, +1) , (b, c, +1) , (b, c, o)}. Let [0 0 0, 1 1 1] be again a parametrisation lattice whose variable c parameter values correspond to the Table 5.3. 0 0 0 c,ω ω ω < 1 1 1 c,ω ω ω for every regulator state ω ω ω ∈ Ω c and every regulator state of variable c is thus a candidate for being open for increase and decrease. However, due to the monotonicity constraints (a, c, +1) and (b, c, +1), there exists a unique c -minimal element (a = 0, b = 0) and a unique c -maximal element (a = 2, b = 1). We thus get the following open regulator states O - v ([0 0 0, 1 1 1]) = {(a = 0, b = 0)} and O + v ([0 0 0, 1 1 1]) = {(a = 2, b = 1)}.

69 ory 1 Denition 6 . 1 (

 69161 network model with initial condition consisting of initial state and initial parametrisation set. Initialised Parametric Regulatory Network). An initialised parametric regulatory network G m m m , x x x Gm m m , PGm m m of dimension n is a parametric regulatory network G m m m of the same dimension n coupled with a state x x x Gm m m , PGm m m ∈ X m m m × 2 P(Gm m m) . When referring to unfolding semantics of parametric regulatory network G m m m we automatically assume G m m m is initialised by an initial condition x x x Gm m m , PGm m m .

Denition 6 . 2 ( 2 .

 622 Branching Process of a Parametric Regulatory Network). A branching process of a parametric regulatory network G m m m of dimension n, is an occurrence net O labelled with function β : B ∪ E → v∈{1,...,n} ({v} × {0, . . . , m m m v }) ∪ P P P ∈ P such that: 1. β (B) ⊆ v∈{1,...,n} ({v} × {0, . . . , m m m v }) and β (E) ⊆ P P P ∈ P F P P P Given an arbitrary event e ∈ E with β (e) = t = (x x x, y y y). ∀b ∈ • e there exists a unique v ∈ {v (t)} ∪ R(v (t)) such that β (b) = (v, x x x v ) and vice versa, ∀v ∈ {v (t)} ∪ R(v (t)) there exists a unique b = β -1 ((v, x x x v )) and b ∈ • e. (β restricted to • e is a bijection.)

  Similarly, ∀b ∈ e • there exists a unique v ∈ {v (t)} ∪ R(v (t)) such that β (b) = (v, y y y v ) and vice versa, ∀v ∈ {v (t)}∪R(v (t)) there exists a unique b = β -1 ((v, y y y v )) and b ∈ e • . (β restricted to e • is a bijection.) 3. ∀b ∈ min((O)) there exists a unique v ∈ {1, . . . , n} such that β (b) = (v,x x x v ). and ∀v ∈ {1, . . . , n} there exists a unique b = β -1 ((v,x x x v )) and b ∈ min((O)). (β restricted to causality-minimal conditions is a bijection with the initial state.) 4. ∀ e 0 , e 1 ∈ E, • e 0 = • e 1 ∧ β (e 0 ) = β (e 1 ) =⇒ e 0 = e 1 (No duplicate transitions).

3 . 5 .

 35 7 and Denition 3.8 with respect to the new labelling function β . Denition 6.3 (Parametric Regulatory Network Branching Process Prex). Let O, β and O , β be two branching processes of the same parametric regulatory network G m m m . Then, O, β is a prex of O , β if the following conditions are satised: 1. B ⊆ B , E ⊆ E and F ⊆ F (O is a subnet of O ); 2. min((O )) ⊆ B (The natural initial marking is the same for both branching processes); For each condition b ∈ B and the single event e ∈ E such that e ∈ • b (if it exists), e ∈ E; 4. Similarly, for each event e ∈ E and each condition b ∈ B such that b ∈ • e ∪ e • , b ∈ B; For each x ∈ B ∪ E, β (x) = β (x) (β is the restriction of β to O).Denition 6.4 (Parametric Regulatory Network Unfolding). Let G m m m be a parametric regulatory network. The unfolding of G m m m is a branching process O, β of G m m m such that any other branching process O , β of G m m m is a prex of (O, β).

Denition 6 . 6 (

 66 Parametric Cut-O Event). Let O, β be a nite branching process of a parametric regulatory network G m m m and let (O , β ) be another branching process of the same parametric regulatory network such that B = B ∪ e • and E = E ∪ {e}, where e ∈ PE O, β is a possible extension of the branching process (O, β). Then the event e is a cut-o in (O , β ), e ∈ cutoffs ((O , β )), if and only if p R ([e]) = ∅ or there exists an event e ∈ E such that β (Cut ([e])) = β (Cut ([e ])) and p R ([e]) ⊆ p R ([e ]).

Example 6 . 1 .

 61 In this example we show the detection of a cut-o event in a prex of the unfolding of the parametric regulatory network G m m m from Example 4.1 with the monotonicity constraints from inuence constraints set R (G) = {(a, a, -1) , (b, b, -1) , (a, c, +1) , (b, c, +1)}. The prex shown in Figure 6.1 captures the status of the unfolding procedure after processing the fth event e 5 .

1 Figure 6 . 1 :

 161 Figure 6.1: A prex of the unfolding of the parametric regulatory network G m m m with the inuence constraint set R (G).The usual Petri net notation of spherical and rectangular nodes is used to distinguish conditions and events, respectively. The conditions are labelled by the variable and its value given by the labelling function β . Similarly, the events are labelled by the unique variable changing value and the nature of the value change for transition given by the labelling function β . The events are additionally numbered in the order of exploration by the unfolding process. The conditions belonging to the initial marking are highlighted in blue. The dashed event is declared as cut-o during the complete nite prex construction.

Figure 6 . 2 :

 62 Figure 6.2: The complete nite prex of the unfolding of the parametric regulatory network G m m m with the inuence constraint set R (G). The cut-o events are not represented.

Denition 7 . 1 (

 71 Variable Value Update). Let G m m m be a parametric regulatory network of dimension n and let v ∈ {1, . . . , n} be an arbitrary variable of G m m m .

Denition 7 . 2 (

 72 Parametric Regulatory Network Trace). Let G m m m be a parametric regulatory network of dimension n and let x x x ∈ X m m m be an arbitrary state of G m m m .

Denition 7 . 3 (

 73 Goal Reachability). Let G m m m be a parametric regulatory network of dimension n, x x x ∈ X m m m a state of G m m m , g ∈ {1, . . . , n} a variable of G m m m and ∈ {0, . . . , m m m g } a value of the variable g.

Denition 7 . 8 (

 78 Partial Regulator State). Let G m m m be a parametric regulatory network of dimension n and let v ∈ {1, . . . , n} be a variable of G m m m . Then a partial regulator state of v is a vector ℵ ℵ ℵ ∈ ≤ Π u∈R(v) {0, . . . , m m m u } ∪ { } assigning a value or a wildcard to each regulator u of v.

j > 0 .

 0 By denition, π j ∈ µ (O) where O ∈ B. Let a be the target value of O. Then, by rule (3) of the reduced objective set construction in Denition 7.11, v a v z ∈ B.

  A i for each i ∈ {0, . . . , |R(v)|} are considered for the local cover sets. Thus, each ω ω ω ∈ Ω v tests at most |R(v)| local cover sets, although usually much less. As such, the local cover set of a single regulator state can be computed in O |R(v)| 2 . Given that local cover sets are computed for each regulator state which enables the value change, computing all the local cover sets takes asymptotically O |Ω v | • |R(v)| 2 .

Figure 7 . 1 :

 71 Figure 7.1: The state space graph of the directed parametric regulatory network G with parametrisation set P P P , P P P . Transitions changing the value of b and d are displayed schematically. Transitions only enabled by a single of the parametrisations are labelled by the respective parametrisations. Bold font and lines indicate states and transitions used by at least one minimal trace from the initial state to the goal a 1 .

2 .

 2 By rule (2) of Denition 7.11: B := B ∪ {b 0 b 0 , b 0 b 1 , c 0 c 0 , c 0 c 1 , d 0 d 0 }. For arbitrary variable v, the objective v 0 v 0 has an empty valid transition set τ v0 v0 (x x x) = ∅ and thus neither of rules (2) or (3) are applicable. For the remaining objective b 0 b 1 and c 0 c 1 , rule (2) produces only duplicate objectives b 0 b 0 and b 0 b 1 , respectively. Rule (3), however, may be applied to b 0 b 1 and b 0 b 0 , as well as c 0 c 1 and c 0 c 0 to obtain B := B ∪ {b 1 b 0 , c 1 c 0 }. Only duplicate objectives are obtained by further application of either rule (2) or (3). The construction of the B thus concludes with B = {a 0 a 1 , b 0

2 .

 2 Bold font in Figure 7.2 indicates the three regulator states which enable the increase of variable a value. The partial regulator states from A 1 correspond to edges in the Hasse diagram. E.g. the partial regulator state 11 is represented by the edge connecting regulator states 111, 110 ∈ 11 . Thick edges indicate

Figure 7 . 2 :

 72 Figure 7.2: Regulator states of variable a during computation of regulation cover set for value update a 0 → a 1 in the form of the Hasse diagram of the monotonicity order a . Only the leftmost edges in (a) are labelled by the corresponding partial regulator states 11 , 1 1 and 01 for the sake of readability. Bold text and lines indicate partial regulator states which enable the value update, A ena . Underlined regulator state is the state covered in the respective iteration and dashed lines represent removed partial regulator states, A rmv .

Figure 7 . 5 .

 75 2 (b) depicts the conguration after the rst iteration, including the removed partial regulator states, A rmv represented by the dashed lines.In the second iteration 100 is covered as 1.25 = W (100) < W (110) = 1.As hinted by the symmetric position with respect to 010, 100 is covered in the same fashion, by local cover set A 100 = {100}. The result is shown

Figure 7 . 3 :

 73 Figure 7.3: Regulator states of variable a during computation of regulation cover set for value update a 1 → a 0 in the form of the Hasse diagram of the monotonicity order a . Bold text, lines and shaded areas indicate partial regulator states which enable the value update, A ena . The underlined regulator state is the regulator state covered in the respective iteration. Dashes represent removed partial regulator states, A rmv , and double lines represent partial regulator states included in the regulation cover set A a1→a0 .

2 . 5 =

 25 W (011) = W (111) < W (001) = W (101) = 2.75. Owing to the symmetry of the hypercube diagram, 011 and 111 are covered by the partial regulator state 0 1, 11 and 1 1 following the same reasoning (Figure 7.3 (d) and (e)).

Figure 7 .

 7 3 (c)). Covering 001 before 011 would include 1 in regulation cover set A a0→a1 . As covering 011 and 111 would still require all three partial regulator states 0 1, 11 and 1 1, the inclusion of 1 would be redundant.

Figure 9 . 1 :

 91 Figure 9.1: The inuence graph of the parametric regulatory network modelling mammalian cortical area development. All variables are Boolean and initialised to zero in the initial state, with the exception of Fgf8 (in blue) which has been considered with both zero and one for the initial value. The inuences are labelled with the inuence constraints considered in the experiments.

Figure 9 . 2 :

 92 Figure 9.2: The inuence graph of the parametric Thomas network of bacteriophage λ life cycle. Variable domains as given by the maximum vector m m m = (cI = 2, cII = 1, cro = 3, N = 1) are included in variable labels. The inuences are labelled with the inuence constraints considered in the experiments as well as their respective threshold values.

Figure 9 . 3 :

 93 Figure 9.3: The inuence graph of the parametric Boolean network of EGF-TNFα signalling pathway. The variables shown in blue are set to value 1 in the initial state. The inuences are labelled with the inuence constraints considered in the experiments.

Figure 9 . 5 :

 95 Figure 9.5: The inuence graph of the parametric multivalued network of primary sex determination of placental mammals. The variables with value 1 in the initial state are shown in blue.

  abstraite pour réseaux de régulation biologiques paramétrés Mots clés: Concurrence, Biologie des systèmes, Interprétation abstraite Résumé: L'analyse de la dynamique des réseaux de régulation biologique est confrontée à l'incertitude du modèle informatique exact. Les connaissances disponibles concernent principalement l'existence d'interactions entre espèces biologiques. Les détails sur la façon dont les différents régulateurs coopèrent, et encore plus sur les taux pour ces interactions, sont cependant rarement disponibles. Les réseaux de régulation discrets orent ainsi une abstraction appropriée car ils nécessitent peu de paramètres par rapport aux modèles quantitatifs. Néanmoins, la détermination des paramètres discrets est un dé bien connu. L'ensemble des aectations de valeurs de paramètres admissibles (paramétrisations) est représenté par des réseaux de régulation paramétriques. L'analyse de la dynamique des réseaux de régulation paramétriques est cependant entravée par la double explosion combinatoire, de l'espace d'état et de l'espace de paramétrisation. Nous développons des méthodes visant à atténuer l'explosion combinatoire. Premièrement, nous introduisons une interprétation abstraite pour l'ensemble des paramétrisations admissibles, en obtenant un codage de taille constante, au prix d'une surapproximation conservatrice. Deuxièmement, nous soulevons la sémantique des ordres partiels sous la forme d'un déploiement des réseaux de Petri aux réseaux de régulation paramétriques, en exploitant la concurrence pour une représentation ecace de l'espace d'état. Title: Unfoldings and Abstract Interpretation for Parametric Biological Regulatory Networks Keywords: Concurrency, Systems Biology, Abstract Interpretation Abstract: The analysis of dynamics of biological regulatory networks faces the uncertainty of the exact computational model. The available knowledge concerns predominantly the existence of interactions between biological species.

Table 2 .

 2 1: The table of target values of variable c (f c ) in the multivalued network F A for all possible combinations of variable a and b values. Note that dierent target values are observed for all three values of variable a.

Table 4 .

 4 2: The inmum and supremum parametrisations of the parametrisation set p (t).where ∧ and ∨ are the standard lattice operators of meet and join, in the lattice of all parametrisations (P (G m m m ) , ≤ Gm m m ).

Example 4.3. Let p (t) be the parametrisation set enabling the transition t = (201, 111) with S (t) = {a, b, c} from Example 4.2. The abstraction α (p (t)) = p(t) , p(t) is characterised by the inmum and supremum of p (t). From Example 4.2,

  Model (init. state)Type # nodes # events (incl. cut-os) Sym. exec. size

	Cortical Dev. (Fgf8=0) Cortical Dev. (Fgf8=1) EGF-TNFα λ-switch λ-switch w/ Min-Max Prim. Sex Det. w/ Min-Max Drosophila Signalling Drosophila w/ Min-Max	BN BN BN MN MN MN MN MN	5 5 13 4 4 14 15 15	554 (1,939) 1,054 (3,530) 1,057 (2,658) 170 (575) 157 (527) 19,954 (88,994) 781 (2,698) 731 (2,507)	8,312 8,312 534,498 68,011 15,139 >7,000,000 >7,000,000 >7,000,000
	Table 9.1:

While in asynchronous semantics, there is one transition per variable, the generalised asynchronous semantics have one transition for each subset of variables.

Excluding the pathological case of singleton sets.

This is true for networks of deterministic automata. Nondeterministic nite automata in the network should be converted to deterministic automata rst as nondeterminism on the level of automata is equivalent to F being a regulation relation instead of a function.

For convenience, we list a value for each automaton in the network in the input of A i . However, only a subset of the automata (the in-neighbours) has to be considered in general. The automata which are not in-neighbours of A i have no direct impact on δ i .

2.5. EXAMPLES

In the general case, the arcs of a Petri net may have labels specifying the number of tokens consumed/produced by a transition. The same quantities of tokens then apply to both enabling and ring of the transition. Within our work, however, we assume all arcs to be unlabelled (labelled with 1).

We refer to the σt operator as narrowing, for a lack of a better name. However, the σt operator is not be confused with the usual notion of narrowing in abstract interpretation[START_REF] Cousot | Abstract interpretation frameworks[END_REF].

Note that while the original model reduction method is dened for automata networks, as mentioned in Section

2.4, automata networks and discrete regulatory networks are expressivity equivalent. As such, the adaptation is essentially lifting from the parametrised to the parametric regulatory networks.[START_REF] Abou-Jaoudé | Logical modeling and dynamical analysis of cellular networks[END_REF] Note that this operation corresponds to the monoidal category action[START_REF] Maclane | Categories for the Working Mathematician[END_REF] of the trace monoid on states of the network.

Let now P P P ∈ p R (T ∪ {t}) be arbitrary. We prove 0 0 0 v,ω ω ω ≤ P P P v,ω ω ω and thus P P P ∈ 0 0 0 , 1 1 1 . Unlike under 0 0 0 , all observability constraints are satised under P P P , thus namely there must exist at least one ω ω ω ∈ Ω v such that P P P v,ω ω ω > 0 0 0 v,ω ω ω . Following from the previous part of the safety proof, P P P ∈ p R (T ∪ {t}) gives us P P P v,ω ω ω ≤ 1 1 1 v,ω ω ω and thus ω ω ω v ω ω ω and 0 0 0 v,ω ω ω = 0 0 0 v,ω ω ω . Following from all monotonicity contraints being satised under P P P , we get P P P v,ω ω ω ≥ P P P v,ω ω ω > 0 0 0 v,ω ω ω = 0 0 0 v,ω ω ω and therefore the coveted P P P v,ω ω ω ≥ 0 0 0 v,ω ω ω .

The proof for the upper limit restriction of ω ω ω

Then, for any P P P ∈ p R (T ∪ {t}), there must exist ω ω ω ∈ Ω v such that P P P v,ω ω ω < 1 1 1 v,ω ω ω . P P P ∈ p R (T ∪ {t}) gives us P P P v,ω ω ω ≥ 0 0 0 v,ω ω ω and thus ω ω ω v ω ω ω and 1 1 1 v,ω ω ω = 1 1 1 v,ω ω ω . Following again from monotonicity constraint satisfaction, P P P v,ω ω ω ≤ P P P v,ω ω ω < 1 1 1 v,ω ω ω = 1 1 1 v,ω ω ω and therefore the coveted

Same as for the monotonocity case, the concrete parametrisation set therefore ts within the connes of 0 0 0 , 1 1 1 . The minimum and maximum values of individual parameters being preserved by the construction of the convex cover, we are done proving the safety of the abstraction,

We now proceed with the proof of the minimality of the over-approximation

Adopting the generating lattice notation 0 0 0 , 1 1 1 = p R (T ∪ {t}) and 0 0 0 , 1 1 1 = [p R (T ∪ {t})], allows us to express the sublattice relation in terms of the limit parametrisations, 0 0 0 ≥ Gm m m 0 0 0 and 1 1 1 ≤ Gm m m 1 1 1 . We prove the inequalities by showing that inequalities on individual parameter values hold in the same direction.

Let us rst establish a common starting point [0 0 0,

and by the induction hypothesis also p R (T ∪ {t}) ⊆ σ t p R (T ) = [p R (T )] ∩ p (t). Let further p R (T ∪ {t}) = ∅ as the sublattice relation is trivial for the empty lattice.

Let now ω ω ω ∈ Ω v be such that 0 0 0 v,ω ω ω > 0 0 0 v,ω ω ω , respectively, 1 1 1 v,ω ω ω < 1 1 1 v,ω ω ω . Any such restriction on the value limits of the parameter K v,ω ω ω has to be justied by one or more inuence constraints. The monotonicity inuence constraints are the simple case, where ω ω ω v ω (t) and 0 0 0

With [0 0 0, 1 1 1] as the input, the minimum, respectively maximum, value of the parameter K v,ω ω ω gets restricted by σ v , giving us the coveted:

Let us therefore assume ω ω ω to be such that

It is important to note that 0 0 0 , 1 1 1 cannot be limited much further as both 0 0 0 , 1 1 1 ∈ p (T ∪ {t}) ∩ (u,v,s)∈R P (u,v,s) by construction. As such any further restriction to K v,ω ω ω values results from observability. Thus by Lemma 5.1, such a ω ω ω is unique for 0 0 0, respectively 1 1 1.

We therefore know there exists an observability inuence constraint r ∈ R which is not satised under 0 0 0 , respectively 1 1 1 , giving us the rst pre-

to denote the sets of all partial regulator states ranked by the number of wildcard values. A 0 is thus isomorphic to the regulator state set Ω v while

is the singleton set containing the partial regulator state which assigns wildcard value to each regulator. The algorithm consists of choosing partial regulator state set, local cover set A ω ω ω , to cover each (concrete) regulator state ω ω ω enabling the value change. The extension sets A ω ω ω are computed separately for each regulator state in increasing order of a suitable weight function W. The weight function is constructed to represent the exibility of how the particular regulator state may be covered. I.e. The more partial regulator states ℵ ℵ ℵ ∈ A ena such that ω ω ω ∈ ℵ ℵ ℵ exist, the larger the result of the weight function for ω ω ω. By ensuring the regulator states ω ω ω with few possible local cover sets A ω ω ω are covered rst using the weight function, it becomes possible to choose such cover sets A ω ω ω for the remaining regulator states that are most compatible with the already included partial regulator states, minimising redundancy. To further amplify this benet, the algorithm keeps track of partial regulator states that are removed from further computation, denoted A rmv . In particular, every time a local cover set A ω ω ω is picked for a regulator state ω ω ω, all partial regulator states ℵ ℵ ℵ ∈ A ena \ ℵ ℵ ℵ ω ω ω such that ω ω ω ∈ ℵ ℵ ℵ are removed, ℵ ℵ ℵ ∈ A rmv . This ensures that no redundancy is introduced to the covering of ω ω ω in further computation. Finally, to reect the possibility of many local cover sets for a particular regulator state ω ω ω being disabled due to partial regulator state being removed, the weight function takes the removed states into consideration and depends on the size of

The local cover set A ω ω ω is chosen from subsets of A i limited to partial regulator states ℵ ℵ ℵ such that ω ω ω ∈ ℵ ℵ ℵ, in decreasing order of i. Such a local cover set surely exists among the subsets of A i as for i = 0, the relevant subset contains only the singleton set containing the regulator state itself. Once a suitable local cover set A ω ω ω is obtained, it is directly included in the nal regulation cover set A µ . As aforementioned, the remaining relevant partial regulator states, which do not belong to the selected local cover set, are removed at the same time.

As the weight function essentially counts partial regulator states, it in general only gives a partial order on the regulator states. As such, the algorithm is forced to make nondeterministic choices. Such a situation occurs, however, only when the outcomes of the choice are isomorphic from the perspective of further computation. Therefore, an arbitrary extension of the partial order given by the weight function (e.g. lexicographic order) can be chosen to obtain a fully deterministic algorithm. The pseudocode of the sample algorithm for regulation cover set inference is given in Algorithm 1.

The correctness of the algorithm comes directly from the construction. No bad states may be included as the algorithm works only with the set of partial regulator states which include no bad states. On the other hand, all regulator states which enable the value change are fully covered as the algorithm ensures this for each of them individually.

The resulting cover set computed by Algorithm 1 contains no more explicit Algorithm 1 Computation of Regulation Cover Set function Weight(ω ω ω)

end while return A µ end function regulator value specications than the concrete regulation cover set. This is a consequence of the order in which the individual regulator states are handled. Suppose a regulator state ω ω ω is covered by several partial regulator states which contain more regulator value specications than ω ω ω itself. Each partial regulator state ℵ ℵ ℵ ∈ A 1 with ℵ ℵ ℵ u = is shared with exactly max(u) -1 other regulator states. Thus, the partial regulator states included to cover ω ω ω can be utilised while covering max(u)-1 other regulator states. Finally, since W (ω ω ω) ≥ 2 is the smallest weight among all uncovered regulator states, all the other uncovered regulator states are also sharing partial regulator states among themselves, thus closing the loop and guaranteeing the regulator value specication debt eventually gets `payed o'.

The fractional part of the weight function is included to introduce bias towards states that have less partial regulator states in the beginning due to sharing more partial regulator states with bad regulator states. If there are two regulator states ω ω ω and ω ω ω such that W (ω ω ω) = W (ω ω ω ) but W (ω ω ω) < W (ω ω ω ), we know that both regulator states have equally many partial regulator states to choose from for their respective cover sets. However, more of the partial regulator states containing ω ω ω have been removed and thus, quite possibly,