Adrien Basso-Blandin

Franck Delaplace
email: franck.delaplace@ibisc.univ-evry.fr

gubs, a behavior-based language for open system dedicated to synthetic biology

In this article, we propose a domain specific language, GUBS (Genomic Unified Behavior Specification), dedicated to the behavioral specification of synthetic biological devices, viewed as discrete open dynamical systems. gubs is a rule-based declarative language. By contrast to a closed system, a program is always a partial description of the behavior of the system. The semantics of the language accounts the existence of some hidden non-specified actions possibly altering the behavior of the programmed device. The compilation framework follows a scheme similar to automatic theorem proving, aiming at improving synthetic biological design safety.

Introduction

The field of synthetic biology is looking forward principles and tools to make the biological devices inter-operable and programmable [START_REF] Lu | Next-generation synthetic gene networks[END_REF] with, as long-term goal, the design of de-novo synthetic genome [START_REF] Gibson | Creation of a bacterial cell controlled by a chemically synthesized genome[END_REF]. In this endeavor, computer-aided-design (CAD) environments play a central role by providing the required features to engineer systems: specification, analysis, and tuning [START_REF] Bilitchenko | Eugene-a domain specific language for specifying and constraining synthetic biological parts, devices, and systems[END_REF][START_REF] Pedersen | Towards programming languages for genetic engineering of living cells[END_REF][START_REF] Umesh | Programming languages for synthetic biology[END_REF][START_REF] Czar | Writing DNA with GenoCAD[END_REF].

Pioneer applications demonstrate their valuable potential in igem competition.

Scaling up the complexity of devices necessitates to harness the development of CAD environments based on an automatic conversion of the design specification into DNA sequences, like compilers for programming languages. The goals are twofold: to facilitate the design of large biological synthetic system, and to ensure the safety and the reliability of the synthetic systems.

Currently, domain specific languages for synthetic biology mainly address the design of structure, namely the biological component assembly, where programming relates to DNA sequence description as in genocad [START_REF] Cai | Modeling structure-function relationships in synthetic DNA sequences using attribute grammars[END_REF]. Although the structural description is an indispensable step in the design-to-manufacture chain and provide an accurate description of devices, the abstraction level seems inappropriate for tackling large bio-systems. The required size of program for sequence description likely makes the task error-prone and un-come-at-able. Therefore, there is a significant need for completing the structural description by an additional, more abstract, programming layout. High level programming language for synthetic biology is announced as a key milestone for the second wave of synthetic biology to overcome the complexity of large synthetic system design [START_REF] Purnick | The second wave of synthetic biology: from modules to systems[END_REF]. Nonetheless, in this domain, language technology is still in its infancy and transforming this vision into a concrete reality remains a daunting challenge.

In hardware description languages like vhdl [START_REF] Pj Ashenden | The designer's guide to VHDL[END_REF] or verilog [START_REF] Thomas | The Verilog Hardware Description Language[END_REF], the device specification address the functional description as well as the structural description. The functional specification describes the expected behavior of the system followed by an automated or semi-automated translation to a structure. In this framework, the components are selected and organized to achieve the specified function at compile phase, providing a structural description of the device.

In this article, we propose a biological functional/behavioral description language, called gubs where the program specifies the synthetic biological devices behaviorally. More precisely, gubs is a rule-based declarative language dedicated to the behavioral specification of discrete open dynamical systems for synthetic biology interacting with its environment. gubs symbolically defines the behaviors to provide a relative independence from structure by postponing the biological components selection at compile phase. Within this framework, the compiler translates the behavioral specification to a structural description of a device whose behavior carries the functional features defined by a program. The proposed compilation method is inspired by automated theorem proving.

After an introduction of the main features of gubs language (Section 2), we define the semantics of gubs based on hybrid logic. Then, we detail the proof-based principles governing the compilation (Section 3) illustrated by a complete example (Section 3.2). After a survey of the related works, Section 4, we conclude (Section 5).

gubs language

In this section, we describe the main features of gubs.

Constant and variables. In gubs, two kinds of objects are distinguished: the constants and the variables. The constants designate pre-defined objects in a corpus of knowledge. In biology, the constants may represent proteins or genes of interest. For example, the agent LacZ refers to LacZ protein or gene. By convention, their name starts with a capital letter. Variables refer to an abstraction of these pre-defined objects and can be potentially replaced (substituted) by any constant. By convention, variable name starts with a minuscule letter.

Agents, attributes and states. The agents represent the biological objects. Their observable states characterize their behavior, actually representing their capacity for actions on the state of other agents. They are characterized symbolically by a set of attributes, categorizing the different capacities for actions of an agent. The real significance of the attributes is a matter of convention, depending on the targeted realization (e.g., protein pathways, gene network) and will be addressed through examples. For instance, the regulatory activity of a gene is observationally related to thresholds of rna transcripts concentration. At a given threshold a gene regulates a given set of genes whereas at another threshold the regulation applies to another set of genes (See Figure 1). The different thresholds define the levels of the gene activity leading to different regulatory activities. For a gene G, if we identify three different kinds of regulatory activities, the state of this gene will be defined by three different attributes {Low, Mid, High}, characterizing the three possible behaviors symbolically. For example, G(Low) expresses the fact that agent G is in state Low and then ready for the action corresponding to the attribute Low. In some cases, a single state is sufficient to qualify the capacity for action of the agent. In this case, the agent is identified to its capacity and G means that agent G is available for its action. G(Low) signifies that the state of the agent is not the attribute Low (G when an agent has a single capacity). It is worth to point out that, not being in an attribute for an agent state, does not mean to be in another predefine state. Indeed, for open systems, the state of the agents could be of any sort that not necessarily belong to those defined by the program. Moreover, the description of the observation of an agent state is extended to a set of agents as follows: g 1 + . . . + g n , meaning that all the agent states, g i , are observed at the same time/period.

Two kinds of relations on attributes are defined: an order, ≺, meaning "less capacity than" and an inequality, ≉, meaning "different capacity than". Then Low ≺ Mid implies that the capacity for actions of G(Mid ) includes the capacity related to G(Low ). In gene regulatory model [START_REF] Delaplace | Discrete causal model view of biological networks[END_REF], it is usual to consider that the set of genes regulated at a given level will also be regulated at higher levels. By contrast, in signaling pathways, the phosphorylation of a protein induces a conformational change of the structure leading to a specific signaling potentiality which does not occur in the unphosphosrylated conformation. Assuming that Phos and UnPhos respectively represents the phosphorylated and the unphosphorylated conformations of protein P , we have Phos ≉ UnPhos. Then, P (Phos) implicitly implies P (UnPhos). Attributes and relation on attributes will be declared as follows: G ∶∶ {Low ≺ Mid, Mid ≺ High}, P ∶∶ {Phos ≉ UnPhos}. A simple set of attributes replaces the relations if unknown. In this case, no specific relation is set concerning the capacity for actions of an agent.

Trace, event, and history. To understand what "behavior" formally means, we focus on the notion of trace and history. A trace is a symbolic representation of the evolution of some quantities related to the agents of interest. The trace is said observationally consistent with the behavior if it is recognized trough the events occurring in the trace. Formally a trace, (T t ) 1≤t≤m , is a finite sequence of agent state set where each set contains the agent states at a given instant. For instance, the evolution of a concentration evolving from Low to High for G may be described by the following trace of 6 instants: ({G(Low)},{G(Low)},{G(M id)},{G(M id)},{G(M id)},{G(High)}), .

1 2 3 4 5 6 7
However, a behavior is characterized by some essential steps in the evolution. As the evolution is emphasized by three essential events: Low, Mid, High for G, without necessarily accounting the way and the time needed for the evolution, the recognition of the behavior is based on these events only. Then, the consistency addresses a series of essential events occurring in a trace. Such series is called the history of a trace. More precisely, an history is defined from a chronological division of a trace into periods emphasizing the essential event steps of the evolution behavior. The events of a period are all the agent states occurring at each instant in the period. Given a trace (T t ) 0≤t≤m , and a chronological division, (d i ) 1≤i≤n , corresponding to a sequence of the starting dates for each period, the history is a sequence of agent states occurring in each period, (H i ) 1≤i<n , such that each H i = ⋃ di≤t<di+1 T t , (See also Figure 1 depicting the trace and history of the dependencies). For instance, a chronological division stressing the evolution Low, Mid and finally High is (1, 3, 6, 7), but (1, 2, 4, 7) is also a chronological division whose history is consistent with the expected evolution since Low, Mid and High occur in the successive periods. However, the chronological division (1, 3, 7) leads to an inconsistent history because the level Mid is not seen as an intermediary event in the history.

Behavioral dependence and observation spot. The behavioral dependencies identify relations between behaviors as causal relations on events. Basically, the dependencies should stress the control of agents on another. However, the definition of the causality needs to tackle with the openness of a system leading to adapt the definition of the causality. A seminal definition of the causality, proposed by Hume [START_REF] Hume | A Treatise of Human Nature, Being an Attempt to introduce the experimental Method of Reasoning into Moral Subjects[END_REF], is formulated in terms of regularity on events: "[we may define] a cause to be an object, followed by another, and where all the objects similar to the first are followed by objects similar to the second." Although this definition appropriately characterizes the notion of control, the openness of the system implies to account the environment actions, possibly altering the causal dependence chain. For example, a programmed activation G 1 + → G 2 may be contradicted by an existing inhibition G 3 -→ G 2 addressing the same target gene G 2 . Hence, while G 1 is active, it may appear that G 2 will not be active because the regulatory strength of G 3 is greater than the regulatory strength of G 1 , contradicting the expected activation by an hidden inhibition. Hence, pushed to the limit, this consideration contradicts the ability to describe a behavior evolution causally because any programmed action can be unexpectedly preempted by an external one.

However, by assuming that the design always describes a new functionality which is not observed naturally, the effect becomes the event indicating the effectiveness of a causal relation. Moreover, as no cause external to the description can trigger the effect, the over-determination by unknown causes is prevented, then insuring that the program is the sole device entailing the expected effect in the biological system. Hence, the definition of the causal dependence will be governed by the effect, leading to the following definition of the dependence: "if effect e would occur then c occurs". Moreover, the scope of future (resp. past) is narrowed to a closest future (resp. past) period, representing the fact that a response is always expected in a given delay. Notice that, the proposed definition circumvents the afore mentioned problem illustrated by the hidden inhibition because if the effect does not occur the question of the existence of a cause is meaningless. This definition is somehow equivalent to the causal claims proposed by Lewis [START_REF] Lewis | Causation as influence[END_REF] in terms of counter-factual conditionals, i.e., "If c had not occurred, e would not have occurred".

Three behavioral dependencies are defined in gubs: the normal denoted by ◯→, persistent by ⊙→, and remanent by ⊕→. Informally, for normal dependence the cause precedes the effect providing the effect is observed; for persistent dependence the cause still precedes the effect but it is maintained while the effect is observed; and for remanent dependence, the effect is maintained despite the cause has disappeared. These dependencies symbolize common biological interactions. For instance, in genetic engineering, the recombination enables the emergence of a regulated gene or an hereditary trait permanently. A such mechanism typifies the remanent dependence in biology. The relations between gene expression at steady state are symbolized by persistent dependence. The behavioral dependences are defined as follows (see Section 2.1 for their formalization):

• c ◯→ e: if e occurs then c occurs in the closest past.

• c ⊙→ e: if e occurs then c occurs in the closest past and also currently.

• c ⊕→ e: if e occurs then, either e occurs in the closest past or the dependence complies to the property of the normal dependence.

Figure 1 exemplifies the correspondence between experimental traces, symbolic traces and the history for the causal dependencies. All the dependences are extended to a set of causes and a set of consequences, i.e., c 1 + . . . + c n ◯→ e 1 + . . . + e m . For example, let us define the activation and the inhibition as follows:

g 1 + → g 2 ≡ g 1 ⊙→ g 2 , g 1 ◯→ g 2 and g 1 - → g 2 ≡ g 1 ⊙→ g 2 , g
1 ◯→ g 2 the program depicting a negative regulatory circuit with two genes, i.e., g 1

+ → g 2 , g 2 - → g 1 , is: {g 1 ⊙→ g 2 , g 1 ◯→ g 2 , g 1 ⊙→ g 2 , g 1 ◯→ g 2 }. time q. T H ∅ ∅ {c} {c} ∅ ∅ {e} {e} ∅ ∅ ∅ c ◯→ e c e ∅ {c} {e} ∅ time q.
T H

∅ ∅ {c} {c, e} {c, e} {e} ∅ ∅ ∅ ∅ ∅ c ⊙→ e c e ∅ {c} {c, e} ∅ time q.
T H The observation spots describe the set of observations expected in a trace. For instance, observing that gene G is at level high is written Obs::G(High). As the activation of a dependence lies on the observation of the effect, the observation spot is used to determine which effects must be necessarily observed. For example, in the negative regulatory circuit, the characteristic observation spots are: obs 1 ::g 1 + g 2 , obs 2 ::g 1 + g 2 .

∅ ∅ {c} {c} ∅ ∅ ∅ {e}
Compartment & Context. A compartment encloses a set of dependences making them local to the compartment. For instance, C{g 1 ◯→ g 2 } describes a normal dependence occurring in compartment C. Compartments are hierarchically organized and all the compartments are included in another except for the outermost one. Although compartments directly refer to the compartmentalized cellular organization (e.g., nucleus, mitochondria), they are also used to emphasize the isolation of some interactions by syntactically enclosing dependencies into a compartment. C.s refers to an agent state in compartment C.

A context refers to a stimulus acting on the system, as environmental conditions or external signaling. The application of a context c to a set of dependences b is written [c]b where c is either a variable or a constant. It means that dependencies of b are triggered when the context c is present. For instance, recently, Ye et al. [START_REF] Ye | A synthetic optogenetic transcription device enhances blood-glucose homeostasis in mice[END_REF] explore the opto-genetics signaling to control the expression of target transgenes. The blue-light induces the expression of transgene (tg) via a signaling cascade leading to the binding of nfat transcription factor to a specific promoter (pnfat). The following program using context summarizes the process: [BlueLight]{NFAT ⊙→ tg}. A context can be decomposed to several contexts, [k 1 , . . . , k n ]b, meaning that all the conditions must be met to trigger the dependences of b. The interpretation is equivalent to a context cascading,

[k 1 ][k 2 ] . . . [k n ]b.
Moreover, the observation spots and attribute definition are context insensitive.

Semantics of gubs

The interpretation of gubs is a formula such that the set of all models validating it defines all the possible histories complying to the programmed behavior while considering the openness of system. The interpretation is based on multi-modal hybrid logic with the "Always" operator, H(A, @).

Hybrid logic.

In what follows, we recall the formal syntax and semantics of hybrid logic. The hybdrid logic [START_REF] Blackburn | Handbook of Modal Logic[END_REF][START_REF] Braüner | Hybrid Logic and Its Proof-Theory[END_REF] offers the possibility to denominate worlds by new symbols called nominals. They will be used in satisfaction modal operators @ a ; the formula @ a φ asserts that φ is satisfied at the unique point named by the nominal a identifying a particular truth values of a formula at this point. Given a set of propositional symbol, PROP, a set of relational symbol REL, and a set of nominal NOM disjoint to PROP, a set of well formed formula in the signature of ⟨PROP, NOM, REL⟩ is defined as follows:

φ ∶∶= ⊺ p a ¬φ φ ∧ φ @ a φ ⟨k⟩φ ⟨k⟩ -φ Aφ.

with p ∈ PROP, a ∈ NOM and k ∈ REL. Moreover, the syntax is extended to other logical operators

classically 1 : , ∨, →, [k], E.
Interpretation is carried out using the Kripke model satisfaction definition (Table 2.1). M, w ⊩ φ is interpreted as the satisfaction of a formula φ by a model M at world w where ⊩ stands for the realizability relation (i.e., "is a model of"). A model validates a formula, denoted by M ⊩ φ, if and only if it is satisfied for all the worlds of the model (i.e., ∀w ∈ Dom M ∶ M, w ⊩ φ).

Definition 1 (Kripke model). A Kripke model is a structure M = ⟨W, (R k ) k∈τ , V ⟩ where W = Dom M is a non-empty set of worlds, τ ⊆ REL a subset of relational symbols denoting the modalities, R k ⊆ W × W, k ∈ τ a relation of accessibility, V ∶ (PROP ∪ NOM) → 2 W an interpretation attributing to each nominal and propositional variable a set of worlds such that any nominal addresses one world at most (i.e., ∀a ∈ NOM ∶ V (a) ≤ 1).

By convention, R stands for the union of the accessibility relation, R = (⋃ k∈τ R k ).

A modal theory of a model M regarding to a set of formulas F , TH F (M), is the set of formulas of F validated by M, i.e., TH F (M) = {φ ∈ F M ⊩ φ}. KS(φ) denotes the set of all models validating φ, i.e., KS(φ) = {M M ⊩ φ}.

Semantics. A gubs program is interpreted by a hybrid logic formula where the modal operators characterize here temporal observation on history: [ ] means "observed in all the closest futures" and ⟨ ⟩ means "observed in a possible closest future at least" (resp. ⟨ ⟩ -, [ ] -for the closest past). Moreover, we assume that the accessibility relations, (R k ) k∈τ , are indexed by the non empty parts of the set of all the contexts of a program P , denoted by K P (i.e., τ = 2 K P ∖ {∅}). Then, a non-empty set of contexts ,∅ ⊂ K ⊆ K P , is a modality, i.e., ⟨K⟩, [K] with ⟨ ⟩ = ⟨∅⟩ by convention. Let ⟨W, •, Λ⟩ be the set of words W with the concatenation operation and the neutral element, the

M, w ⊩ ⊺ iff true M, w ⊩ a iff w ∈ V (a), a ∈ NOM ∪ PROP M, w ⊩ ¬φ iff M, w ⊮ φ M, w ⊩ φ1 ∧ φ2 iff M, w ⊩ φ1 and M, w ⊩ φ2 M, w ⊩ @aφ iff w ′ ∈ V (a) and M, w ′ ⊩ φ M, w ⊩ ⟨k⟩φ iff ∃w ′ ∈ W ∶ M, w ′ ⊩ φ and wR k w ′ M, w ⊩ ⟨k⟩ -φ iff ∃w ′ ∈ W ∶ M, w ′ ⊩ φ and w ′ R k w M, w ⊩ Aφ iff ∀w ′ ∈ W ∶ M, w ′ ⊩ φ Table 1: Hybrid logic interpretation.
empty word Λ and F H the set of well-formed formulas of H(A, @), the semantics is defined by four functions:

⟦.⟧ ∶ P → F H , ⟦.⟧ P ∶ P → W → 2 W → F H , ⟦.⟧ B ∶ B → W → F H , ⟦.⟧ R ∶ R → W → F H ,
where P, B, R respectively stand for the set of gubs programs, the set of agent state set and the set of relations on attributes. ⟦.⟧ initiates the interpretation. Table 2.1 defines these functions.

⟦{b}⟧ = A ⟦b⟧ P (Λ)(∅) ⟦ ⟧ P (C)(K) = ⊺ ⟦b 1 , b 2 ⟧ P (C)(K) = ⟦b 1 ⟧ P (C)(K) ∧ ⟦b 2 ⟧ P (C)(K) ⟦s 1 ◯→ s 2 ⟧ P (C)(K) = ⟦s 2 ⟧ B (C) → ⟨K⟩ -⟦s 1 ⟧ B (C) ⟦s 1 ⊙→ s 2 ⟧ P (C)(K) = ⟦s 2 ⟧ B (C) → ⟦s 1 ⟧ B (C) ∧ ⟨K⟩ -⟦s 1 ⟧ B (C) ⟦s 1 ⊕→ s 2 ⟧ P (C)(K) = ⟦s 2 ⟧ B (C) → (⟨ ⟩ -⟦s 2 ⟧ B (C)) ∨ (⟨K⟩ -⟦s 1 ⟧ B (C)) ⟦g 1 , ⋯, gn ∶ {r 1 , ⋯, rm}⟧ P (C)(K) = ⋀ n i=1 ⋀ m j=1 ⟦r j ⟧ R (C.g i ) ⟦l::s⟧ P (C)(K) = @ l ⟦s⟧ B (C) ⟦C ′ {b}⟧ P (C)(K) = ⟦b⟧ P (C.C ′ )(K) ⟦[K]{b}⟧ P (C)(K ′ ) = ⟦b⟧ P (C)(K ∪ K ′ ) ⟦s 1 + . . . + sn⟧ B (C) = ⋀ n i=1 ⟦s i ⟧ B (C) ⟦C ′ .s⟧ B (C) = ⟦s⟧ B (C.C ′ ) ⟦g(a)⟧ B (C) = C.ga ⟦g(a)⟧ B (C) = ¬C.ga ⟦g⟧ B (C) = C.g ⟦g⟧ B (C) = ¬C.g ⟦a 1 ≺ a 2 ⟧ R (g) = ga 2 → ga 1 ⟦a 1 ≉ a 2 ⟧ R (g) = ga 1 → ¬ga 2 ∧ ga 2 → ¬ga 1 ⟦a⟧ R (g) = ⊺
Table 2: Semantics of gubs. In the definition, a represents an attribute, b a behavior, g an agent, s a set of agent states or an agent state, r a relation on attributes, C a compartment, K a set of contexts and b a set of behaviors (i.e., contexts, compartments, dependences, attributes, observation spots).

For instance, the program of the negative regulatory network,

{g 1 ⊙→ g 2 , g 1 ◯→ g 2 , g 1 ⊙→ g 2 , g 1 ◯→ g 2 , obs 1 ∶∶ g 1 + g 2 , obs 2 ∶∶ g 1 + g 2 }
, is translated into the following formula:

A( g2 → ((⟨ ⟩ -¬g1) ∧ ¬g1) ∧ ¬g2 → ((⟨ ⟩ -g1) ∧ g1) ∧ g2 → ((⟨ ⟩ -g1) ∧ g1) ∧ ¬g2 → ((⟨ ⟩ -¬g1) ∧ ¬g1)∧ @ obs 1 (g1 ∧ ¬g2) ∧ @ obs 2 (¬g1 ∧ g2)
Consistent history. Now, we formally define the consistency of the history with regards to program. An history is assimilated to a path in a model ending by a world labelled with an observation spot label. The set of Kripke-models validating the interpretation of a program P , KS(⟦P ⟧), not only contains all the consistent histories, but also the possible histories corresponding to behavioral alterations due to external perturbations. Hence, the compilation generates a device such that all the models validating its interpretation encompass all the possible observations related to the program, including the consistent and the inconsistent ones. More precisely, the consistency lies on the identification of the largest number of "relevant" events characterizing a complete causal chain described in a program. As a history is also a model, a consistent history should validate the interpretation of the complete causal chain by contrast to inconsistent histories. The dependence formula set, F P , of a program P corresponds to a set of formulas corresponding to the interpretation of each dependence taken separately with the attributes related to the involved agents. By definition of the semantics, any model validating the interpretation of a program also validates each formula of this set. The consistency of a history is then based on the validated formulas of this set by this history. An history M H is consistent for P if and only if no other modal theory of histories based on F P (i.e., TH F P (M) with M as a history), ending with the same labeled world includes the modal theory of this history (i.e., TH F P (M H ) ⊈ TH F P (M)).

Compilation

At compile phase, a program is transformed to a structure (e.g., a dna sequence) while inserted in a vector cell, should behave according to the programmed specification. The structure will result to an assembly of several devices stored in a library of components (e.g., parts registry). As the design relates here to a behavioral/functional description, we need to bridge the gap between structural and functional description. This stage is called the functional synthesis. The issue is to select a set of components whose assembly preserves the behavior of the program. To achieve this goal, a gubs program is associated to each component to describe its behavior. Thereby, the component assembly corresponds to a program assembly preserving the behavior of the compiled program. Preserving a behavior is laid on a property called the behavioral inclusion formalizing the fact that the characteristic observational traits of the specified function must be recognized in traces related to the device experiments. In other words, we can exhibit histories consistent with the programed behavior from histories consistent with the device behavior description. The behavioral inclusion is defined from the interpretation of the programs, as a logical consequence (Definition 2).

Definition 2 (Behavioral inclusion).

A program Q behaviorally includes another program P , if and only if the interpretation of the latter is a logical consequence of the interpretation of the former:

P Q ≜ ∀M ∶ M ⊩ ⟦Q⟧ ⇒ M ⊩ ⟦P ⟧ .
The behavioral inclusion is a pre-order2 such that the empty program, denoted by , is a minimum, meaning that a program with no behavior can be observed in all traces. And a program whose interpretation equals , is a maximum. Figure 2 illustrates the behavioral inclusion on a particular model.

Observability. It may arise that no trace would be consistent with some programmed behaviors. For example, the program {Obs ∶∶ g, g ⊙→ g} is not observable in a trace. Indeed, its interpretation yields to the following formula: A((@ Obs g)∧(g → ((⟨ ⟩ -¬g)∧¬g))), false in all models because world

P Q {g 1 ◯→ g 3 , {[k 1 ]{g 0 ◯→ g 1 }, [k 3 ]{g 3 ◯→ g 4 }, [k 2 ]{g 0 ◯→ g 2 }, [k 4 ]{g 3 ◯→ g 5 }, g 1 ◯→ g 3 , [k 6 ]

Functional synthesis

The functional synthesis is the operation whereby biological components of a library are selected and assembled to generate a device behaviorally including the designed function. The behavior of each component is described by a gubs program. At its simplest, the functional synthesis could be considered as a proper substitution of variables by constants. For example, given the following activation {G 1 + → g 2 }, g 2 will be substituted by gene G 2 , providing that component Q describes the activation {G 1 + → G 2 }. However, more complex situations may arise during component selection. For example, if the activation G 1 + → G 2 occurs with another regulation only i.e.,

Q = {G 1 + → G 2 , G 3 + → G 4 } then the selection of Q adds a supplementary regulation.
Formally, a finite substitution is a set of mappings, σ = {v i b i } i , on variables and constants such that a variable can be substituted by a variable or a constant, and a constant can only substituted by itself 3 . For instance, we have:

{Obs::G(l) + b 2 , b 1 ◯→ G(l)}[{b 1 ↦ B 1 , b 2 ↦ B 2 , l ↦ Low}] = {Obs::G(Low) + B 2 , B 1 ◯→ G(Low)}.
Functional synthesis rules. The functional synthesis is defined by rules (Table 3) governing the component assembly. Only the dependences and the attributes will be functionally synthesize.

3 P σ or P [σ] represents its application on program P and identity substitutions are omitted.

The observation spots are considered as annotations used for the compilation process. To insure the correctness, each transform must preserved the seminal behavior. Hence, each program resulting from the application of a rule must behaviorally includes the previous one. Formally, the functional synthesis is modeled by a relation on programs denoted by , i.e., Q σ P where P is the initial program and Q the transformed one, such that each rule insures that: Q σ P is correct with regards to a substitution σ, that is P [σ] Q[σ] and Q[σ] is observable. Also notice that the behavioral inclusion is preserved by substitution (Proposition 2). Proposition 2. For all substitutions σ, we have:

P Q ⇒ P [σ] Q[σ].
Table 3 describes a set of rules and Theorem 1 demonstrates their correctness, Γ is a set of components representing the library. P ⊆ Asm Q denotes the fact that program Q corresponds to an assembly including P i.e., Q = (Q 1 , P, Q 2 ) where Q 1 or Q 2 may be an empty program. Rule (Inst.)

-Instantiation - Q[σ] ⊆ Asm P [σ] obs (Q[σ]) Q ∈ Γ (Inst.) Q σ P -Commutativity, Contraction - Q σ P, P ′ (Com.) Q σ P ′ , P Q σ P (Cont.) Q σ P, P -Assembly - Q σ P Q ′ σ ′ P ′ σ VA(P )∩VA(P ′ ) = σ ′ VA(P )∩VA(P ′ ) obs (Q[σ], Q ′ [σ ′ ]) (Asm.) Q, Q ′ σ∪σ ′ P, P ′
Table 3: Functional synthesis rules describes the fact that an observable instance of a part of a component in the library is functionally synthesized. Rule (Com.) expresses the commutativity of the assembly. Rule (Cont.) contracts the redundant formulation of programs. Finally, Rule (Asm.) details the conditions for an assembly of two components, each representing a functional synthesis of a part of the designed function.

Theorem 1. The functional synthesis rules (Table 3) are correct.

-dependencies -

Q σ S 1 ⊙→ S 2 , S 2 ⊙→ S 3 , ∆ (Trans.) Q σ S 1 ⊙→ S 3 , ∆ Q σ S 1 ⊙→ S 2 , ∆ (N2P.) Q σ S 1 ◯→ S 2 , ∆ Q σ S 1 ◯→ S 2 , ∆ (R2N.) Q σ S 1 ⊕→ S 2 , ∆ -agent states - S 1 + S 2 (SCom.) S 2 + S 1 S + s (SCont.) S + s + s S + s (Incl.) S
Table 4: Rules for dependencies and agent states. S i stands for a collection, s 1 + . . . + s n , of agent states, including negation, and ∆ stands for the rest of the program.

Another set of rules, more specifically devoted to causal relation (Table 4), defines alternate possibilities to express similar behaviors. This table also includes rules for agent sets. They play an essential role in the compilation by proposing alternate possibilities for the design. For example, Rule (Trans.) expands the chain of persistent dependences by adding intermediary dependence to refine a pathway. Rule (N2P.) transforms a normal dependence to a persistent one since the latter is a normal dependence with an additional property. And Rule (R2N.) transforms a remanent dependence to a normal dependence, since normal dependence is also remanent dependence with a repetition of the effect restricted to one step. Notice that, according to these rules, all the dependence chains can be implemented with persistent dependencies.

Example

The compilation process is here exemplified by the design of the Band Detector proposed in [START_REF] Basu | A synthetic multicellular system for programmed pattern formation[END_REF].

The design aims at forming patterns of different colors in a population of bacteria exploiting the quorum sensing phenomenon by staining with fluorescent protein (GFP). The amount of molecules of interest that receives a cell depends on its relative position to tje cell diffusing the molecule of interest: more the cell is far from the source, fewer is the amount of molecules received. Its diffusion is controlled by an external event. The activation or inhibition of the fluorescent protein due to the concentration will distinguish the bands surrounding the source. In the original design, the protein does not fluoresce in an intermediary band. From a computing standpoint, we can assimilate the and Cl, at level 1, the amount of AHL only allows activation of Cl, and finally, at level 0, none are activated.

We show that from the sender-receiver program, we obtain the original design by applying the afore mentioned rules with an appropriate selection of components. The regulations of Figure 3 are described in gubs program (Table 5) translating in term of dependencies and relations on their attributes their regulatory action. We focus here on some illustrative steps of the sender program compilation. The complete functional synthesis is given in Appendix. The compilation consists in finding the appropriate components whose assembly behaviorally includes the sender-receiver program, with the particularity that the diffusive molecule must be the same in both programs. To ease compilation follow-up, we label each dependency of the sender-receiver program (Table 6).

Q 1 ={[Light]{detect ◯→ Tetr}} Q 2 ={Tetr + → LuxL} Q 3 ={AHL:{low ≉ mid ≉ high}, Luxl + → AHL(low), Luxl + → AHL(mid), Luxl + → AHL(high)} Q 4 ={AHL:{low ≉ mid ≉ high}, LuxR:{low ≉ {mid ≺ high}}, AHL(mid) ◯→ LuxR(mid), AHL(high) ◯→ LuxR(high)} Q 5 ={LuxR:{low ≉ {mid ≺ high}}, LuxR(mid) + → Cl, LuxR(high) + → Cl + LaclM1} Q 6 ={Cl - → Lacl} Q 7 ={LaclM1 - → GFP} Q 8 ={Lacl - → GFP}
Table 5: Part of the database dedicated to the Band Detector.

Let us consider P 11 whose compilation is closed to P 12 and P 13 . Notice that P 11 cannot be directly instantiated with any component because, in the one hand, the component Q 1 contains a context like P 11 but applied on gene Tetr instead of AHL, and on the other hand Q 3 has the AHL molecule but no context is defined. So, to fit P 11 with the components Q 1 , Q 2 and Q 3 , first, the normal dependence is converted to persistent one (Rule (N2P.)).

Q 1 , Q 2 , Q 3 σ {[light]{detect ⊙→ AHL(low)}} (N2P.) Q 1 , Q 2 , Q 3 σ P 11
Thereby, the resulting dependence can be separated to match the assembly Q 1 , Q 2 , Q 3 by applying (Trans.) rule twice. v 1 and v 2 are fresh variables.

Q 1 , Q 2 , Q 3 σ P ′ 11 = {[light]{detect ⊙→ v 2 , v 2 ⊙→ v 1 , v 1 ⊙→ AHL(low)} (Trans.) Q 1 , Q 2 , Q 3 σ [light]{detect ⊙→ v 1 , v 1 ⊙→ AHL(low)} (Trans.) Q 1 , Q 2 , Q 3 σ [light]{detect ⊙→ AHL(low)}
Finally, we obtain a new program program P ′ 11 compatible with Q 1 , Q 2 , Q 3 , and each variable is substituted by a constant (biological element) with the application of Rule (Inst.). For P ′ 11 we have:

Q 1 , Q 2 , Q 3 [σ = {light Light, v 1 T etr, v 2 Luxl}] ⊆ Asm P ′ 11 [σ] obs(Q 1 , Q 2 , Q 3 [σ]) (Inst.) Q 1 , Q 2 , Q 3 σ [light]{detect ⊙→ v 1 , v 1 ⊙→ v 2 , v 2 ⊙→ AHL(low)}
By following this scheme for P 12 and P 13 , we respectively obtain P ′ 12 and P ′ 13 . The final assembly corresponds to the functional synthesis of Sender program.

Q 1 , Q 2 , Q 3 σ P ′ 11 ⋮ Q 1 , Q 2 , Q 3 σ P 11 Q 1 , Q 2 , Q 3 σ P ′ 12 ⋮ Q 1 , Q 2 , Q 3 σ ′ P 12 Q 1 , Q 2 , Q 3 σ P ′ 13 ⋮ Q 1 , Q 2 , Q 3 σ ′′ P 13 (Asm.) Q 1 , Q 2 , Q 3 σ∪σ ′ ∪σ ′′ P 11 , P 12 , P 13
In conclusion, the functional synthesis generates the original genetic circuit (Figure 3) from the sender program. A similar approach can be also applied to obtain the receiver program (see the

Towards automated functional synthesis.

A possible algorithm for the assembly could be based on a combinatorial application of the rules. However, such algorithm may reveal inefficient in practice. We investigate the conditions for an efficient algorithm of compilation based on an internal representation of a program, as a set of contextualized dependencies with attributes, {{A, [K]S 1 ⍟→ S 2 }}, such that A, K, S 1 , S 2 are respectively: a set of attributes specification related to the agent involved in the dependency, a set of contexts and sets of agent states. Any program can be encoded under this representation from a normal form of the program (not detailed here). Formally, the problem solved by the compilation algorithm can be defined as follows (Definition 3):

Definition 3 (Functional Synthesis Problem). Let Γ = {Q i } 1≤i≤n be set where each Q i is a set of contextualized dependencies with attributes and P a set of contextualized dependencies with attribute, can we find the smallest observable subset of components C ⊆ Γ, such that there exists a substitution σ so that its application on the components of C form a cover of P [σ],i.e., ∃σ ∶ P

[σ] ⊆ ⋃ Qj ∈C Q j [σ]∧ obs C.
As the set cover problem is reducible to this problem, the problem is NP-complete. Then, the resolution is oriented towards a heuristic algorithm.

Related works

Domain specific languages have been used in systems biology and in synthetic biology. Although they share some common features, their purpose differs: the former aims at defining a framework to model and simulate systems biology whereas the latter is focused on biological device specification. However, a convergence of these two goals is observed in synthetic biology CAD environment [START_REF] Weeding | SynBioSS designer: a web-based tool for the automated generation of kinetic models for synthetic biological constructs[END_REF]. In language for systems biology, several projects have been developed. Based on process-calculus, seminally used to model process concurrency, several rule-based languages model protein interactions by name-passing [START_REF] Priami | Application of a stochastic name-passing calculus to representation and simulation of molecular processes[END_REF][START_REF] Danos | Rule-based modelling of cellular signalling[END_REF][START_REF] Ciocchetta | Bio-PEPA: A framework for the modelling and analysis of biological systems[END_REF]. Another approach is based on logic, such as biocham [START_REF] Calzone | BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge[END_REF] that formalizes the temporal properties of a biological system and validate models with respect to such specifications.

In the field of language for synthetic biology, structural languages [START_REF] Czar | Writing DNA with GenoCAD[END_REF][START_REF] Pedersen | Towards programming languages for genetic engineering of living cells[END_REF][START_REF] Bilitchenko | Eugene-a domain specific language for specifying and constraining synthetic biological parts, devices, and systems[END_REF] is used for a modular and hierarchical description of well-formed genome sequences by grammars. Although the functionality of the devices is not directly addressed during the specification, a model of dynamics is associated to each grammatical construct, postponing its functional validation at simulation phase. Amorphous programming language has been also investigated to specify biological devices at the scale of cell colony, here considered as a possible computing medium for amorphous program. J. Beal [START_REF] Beal | Automatic Compilation from High-Level Biologically-Oriented Programming Language to Genetic Regulatory Networks[END_REF] demonstrates the proof of concept of this approach in proto.

Ultimately, the design in synthetic biology will certainly require different programming layouts based on different paradigms addressing the integration levels of biological systems. In a tower of languages, starting from a language with collective operations on cell colony, as amorphous languages, and ending by a structural description programmed in a grammar based language, as genocad, gubs language occupies the intermediary level dedicated to cell entity behavioral programming. Then, from an amorphous program, a gubs program may be generated, which in turn can be used to generate a sequence processed by a grammar based language environment. In comparison to modeling languages, their goal is not to provide a framework for biological systems modeling, but rather to provide a model abstracting the behavior of cells to make them easily programmable.

Conclusion

In gubs language, we propose to characterize a programming paradigm abstracting the molecular interactions in the context of open system, that differs to an approach dedicated to biological system modeling. Accordingly, the interactions are symbolized by causal dependencies whose interpretation is driven by effect. We have demonstrated the proof-of-concept of the compilation based on rewriting rules, and illustrated it on a realistic example. The perspective of this work is to find an efficient compilation algorithm. Identifying the biological parameters guiding the component selection should be a key issue in this undertaking.

• M, w ⊩ ¬a ⇐⇒ M, w ⊩ ¬a. By definition of the realizability relation, the world ment is equivalent to: M, w ⊮ a ⇐⇒ M, w ⊮ a. By (1), this equivalence holds.

• M, w ⊩ (ψ 1 ∧ ψ 2 )σ ⇐⇒ M, w ⊩ (ψ 1 ∧ ψ 2 )
. By definition of the substitution, we have to prove: M, w ⊩ (ψ 1 σ)∧(ψ 2 σ) ⇐⇒ M, w ⊩ (ψ 1 ∧ψ 2 ). By definition of the realizability relation we can formulate the property equivalently as follows:

M, w ⊩ (ψ 1 σ) ∧ M, w ⊩ (ψ 2 σ) ⇐⇒ M, w ⊩ ψ 1 ∧ M, w ⊩ ψ 2 .
By induction hypothesis, we have: M, w ⊩ (ψ 1 σ) ⇐⇒ M, w ⊩ ψ 1 and M, w ⊩ (ψ 2 σ) ⇐⇒ M, w ⊩ ψ 2 , implying the previous condition.

• M, w ⊩ (ψ 1 ∨ ψ 2 )σ ⇐⇒ M, w ⊩ (ψ 1 ∨ ψ 2 ).
The proof is similar to the proof of the previous item (∧).

• M, w ⊩ (@ a ψ)σ ⇐⇒ M, w ⊩ @ a ψ. By definition of the substitution we have to prove that: M, w ⊩ (@ aσ ψσ) ⇐⇒ M, w ⊩ @ a ψ By definition of the realizability relation, this is equivalent to:

∃w ′ ∈ W ∶ w ∈ V (aσ) ∧ M, w ′ ⊩ ψσ ⇐⇒ ∃w ′′ ∈ W ∶ w ′′ ∈ Ṽ (a)σ ∧ M, w ′′ ⊩ ψ.
By setting w ′ = w ′′ , from (1) we have:

w ′ ∈ V (aσ) ⇐⇒ w ′ ∈ V (a)
. By induction hypothesis, we have: M, w ′ ⊩ ψσ ⇐⇒ M, w ′ ⊩ ψ. The both last properties imply that:

∃w ′ ∈ W ∶ w ∈ V (aσ) ∧ M, w ′ ⊩ ψσ ⇐⇒ ∃w ′ ∈ W ∶ w ′ ∈ Ṽ (a)σ ∧ M, w ′′ ⊩ ψ,
which implies the initial property.

• M, w ⊩ (⟨k⟩ψ)σ ⇐⇒ M, w ⊩ ⟨k⟩ψ. By definition of the substitution we prove that: M, w ⊩ ⟨kσ⟩ψσ ⇐⇒ M, w ⊩ ⟨k⟩ψ. By definition of the realizability relation the condition is equivalent to:

∃w ′ ∈ W ∶ M, w ′ ⊩ ψσ ∧ wR kσ w ′ ⇐⇒ ∃w ′′ ∈ W ∶ M, w ′′ ⊩ ψ ∧ w Rk w ′′ .
By setting w ′ = w ′′ , the following equivalence holds from (2): wR kσ w ′ ⇐⇒ w Rk w ′ . By induction hypothesis, we have: M, w ′ ⊩ ψσ ⇐⇒ M, w ′ ⊩ ψ. The both last properties imply that:

∃w ′ ∈ W ∶ M, w ′ ⊩ ψσ ∧ wR kσ w ′ ⇐⇒ M, w ′ ⊩ ψ ∧ w Rk w ′
which implies the initial property.

• M, w ⊩ ([k]ψ)σ ⇐⇒ M, w ⊩ [k]ψ.
The proof is similar to the previous item.

• M ⊩ (Eψ)σ ⇐⇒ M ⊩ Eψ. By definition of the substitution we prove that: M, w ⊩ E(ψσ) ⇐⇒ M, w ⊩ Eψ.

By definition of the realizability relation, we have:

∃w ∈ W ∶ M, w ⊩ (ψσ) ⇐⇒ M, w ⊩ ψ,
which is directly verified by induction hypothesis.

• M ⊩ (Aψ)σ ⇐⇒ M ⊩ Aψ. The proof is similar to the previous item.

Proposition 2. First, let us remark that when P Q, the property is trivially verified. Besides, under the assumption P Q, if Q[σ] is not observable the property is also verified because an unobservable program includes all programs behaviorally (Definition 2).

In the rest of the proof, we assume that P is behaviorally included in Q and Q[σ] is observable (i.e., P Q and obs Q[σ]). Hence, by definition of the observability there exists a model M such that M ⊩ ⟦Q[σ]⟧. By proposition 3, we deduce that there exists a model M such that: M ⊩ ⟦Q⟧. Moreover, as P Q by hypothesis, there exists S ⊆ Dom M such that: M S ⊩ ⟦P ⟧. By construction of M we deduce that there exists a sub model of M, denoted by M ′ , complying to the properties, (1) and (2) of Proposition 3 which corresponds to M S . By the definition of rules leading to model M, the structure of the models is preserved. Then as M S is a multi-rooted model, M ′ is also a multi-rooted model. Moreover, we have M ′ ⊩ P [σ] by Proposition 3. Then we conclude that:

P [σ] Q[σ].
Theorem 1. First, let us remark that P Q is true whenever M ⊮ Q by definition of the behavioral inclusion (Definition 2). Hence, the proof doesn't consider the trivial verified case but rather the case where M ⊩ Q.

Inst. Directly from the definition of the behavioral inclusion (Definition 2).

Com. By definition of the semantics ⟦P, P ′ ⟧ = A(φ ∧ φ ′ ) = A(φ ′ ∧ φ) = ⟦P ′ , P ⟧ with ⟦P ⟧ P = φ and ⟦P ′ ⟧ P = φ ′ . Thus, for all M we have: M ⊩ ⟦P, P ′ ⟧ ⇐⇒ M ⊩ ⟦P ′ , P ⟧. Hence, if Q P, P ′ we conclude that: Q P ′ , P .

Cont. Similar to the proof of (Com.).

Asm. First let us remark that σ VA(P )∩VA(P ′ ) = σ ′ VA(P )∩VA(P ′ ) means that the substitution of the common variables are the same for σ and σ ′ , leading to,

Q[σ ∪ σ ′ ] = Q[σ] and Q ′ [σ ∪ σ ′ ] = Q ′ [σ ′ ].
Let σ ′′ = σ ∪ σ ′ . Then, we have the following property by definition of the semantics (Table 2.1) and σ ′′ .

∀M ∈ KS(⟦(Q, Q ′ )[σ ′′ ]⟧) ∶ M ⊩ ⟦Q[σ]⟧ ∧ M ⊩ ⟦Q ′ [σ ′ ]⟧ .
Notice that the set of models, KS(⟦(Q, Q ′ )[σ ′′ ]⟧), is not empty since, by hypothesis, obs (Q[σ], Q ′ [σ ′ ]) holds. As Q σ P and Q ′ σ ′ P ′ , any model validating Q (resp. Q ′ ) also validates P , (resp. P ′ ) by definition of the functional synthesis. Then, we deduce that:

∀M ∈ KS(⟦(Q, Q ′ )[σ ′′ ]⟧) ∶ M ⊩ ⟦P [σ]⟧ ∧ M ⊩ ⟦P ′ [σ ′ ]⟧ .
Then, we conclude that: [light]{detect ⊙ → AHL(high)} (N2P.)

∀M ∈ KS(⟦(Q, Q ′ )[σ ′′ ]⟧) ∶ M ⊩ ⟦(P, P ′ )[σ ′′ ]⟧ .

Complete compilation of the Band Detector

-Sender - Q 1 , Q 2 , Q 3 [σ = {detect Detect, light Light, v 1 T etr, v 2 Luxl}] ⊆ Asm P ′ 11 [σ] obs(Q 1 , Q 2 , Q 3 [σ]) (Inst.) Q 1 , Q 2 , Q 3 σ P ′ 11 } Q 1 , Q 2 , Q 3 [σ ′ = {detect Detect, light Light, v 3 T etr, v 4 Luxl}] ⊆ Asm P ′ 12 [σ ′ ] obs(Q 1 , Q 2 , Q 3 [σ ′ ]) (Inst.) Q 1 , Q 2 , Q 3 σ ′ P ′ 12 Q 1 , Q 2 , Q 3 [σ ′′ = {detect Detect, light Light, v 5 T etr, v 6 Luxl}] ⊆ Asm P ′ 13 [σ ′′ ] obs(Q 1 , Q 2 , Q 3 [σ ′′ ]) (Inst.) Q 1 , Q 2 , Q 3 σ ′′ P ′ 13 P ′ 11 = [light]{detect ⊙ → v 1 , v 1 ⊙ → v 2 , v 2
P 13 Q 1 , Q 2 , Q 3 σ P 11 Q 1 , Q 2 , Q 3 σ ′ P 12 Q 1 , Q 2 , Q 3

Figure 1 :

 1 Figure1: The curves represent the typical behaviors of the causal dependencies based on the time evolution of a quantity (q) related to agents c and e (e.g., rna transcript for gene regulation). The symbolic agent states c and e are here both associated to the maximal threshold of the quantity. The symbolic trace (T ) is issued from a periodic sampling of the evolution by identifying whether c or e occur. An history (H) complying to a causal dependence definition is represented below the trace. The first graphic illustrates the normal causality: c ◯→ e, the second the persistent: c ⊙→ e and the third the remanent one: c ⊕→ e.

Figure 3 :Figure 3

 33 Figure 3: The band detector regulatory circuit.

Sender Receiver P 11 =

 11 {[Light]{detect ◯→ AHL(low)}} P 21 = {AHL(low) ◯→ GFP} P 12 = {[Light]{detect ◯→ AHL(mid)}} P 22 = {AHL(mid) ◯→ GFP} P 13 = {[Light]{detect ◯→ AHL(high)}} P 23 = {AHL(high) ◯→ GFP} with {AHL:{low ≉ mid ≉ high}} as attributes of AHL.

  {g 8 ◯→ g 9 }, g 2 ◯→ g 5 , [k 7 ]{g 8 ◯→ g 10 }, [k 3 ]{g 3 ◯→ g 4 }, g 9 ◯→ g 11 , [k 4 ]{g 3 ◯→ g 5 }, g 10 ◯→ g 11 , g 6 ◯→ g 8 , a ∶∶ g 4 } [k 5 ]{g 6 ◯→ g 7 }, [k 6 ]{g 8 ◯→ g 9 }, [k 7 ]{g 8 ◯→ g 10 }, g 9 ◯→ g 11 , g 10 ◯→ g 11 , a ∶∶ g 4 , b ∶∶ g 5 , c ∶ g 11 }

				g0	g6
			k1	k5
				k2
		g1		g7		g8
				g2	k6	k7
		g3		g9		g10
		k3	k4
	a :	g4	b :	g5	c :	g11
	Figure 2: Behavioral inclusion example. Consistent histories of P necessary contains worlds colored
	in gray.

Obs must both satisfies g and ¬g by definition of the persistent dependence. A gubs program is said observable if and only if the formula resulting from its interpretation is validated by one model at least. Hence, the interpretation of an unobservable program is an antilogy. An unobservable program can be assimilated to a programming error. The detection of such errors can be carried out at compile-phase by using tableaux method

[START_REF] Mayer | Two tableau provers for basic hybrid logic[END_REF]

that automatically determines whether a formula is satisfiable in a model. Notice that an observable program always behaviorally includes an observable program (Proposition 1). Proposition 1. A program behaviorally included in an observable program is observable: ∀P, Q ∈ P ∶ obs Q ∧ P Q ⇒ obs P.

Table 6 :

 6 Separation of the dependencies. complete proof in Appendix 5). = {AHL:{low ≉ mid ≉ high}, [Light]{detect ◯→ Tetr}, Tetr

	Sender

+ → LuxL, Luxl + → AHL(low), Luxl + → AHL(mid), Luxl + → AHL(high)}

Table 8 :

 8 Complete band detector compilation.

= ¬⊺, ψ ∨ φ = ¬(¬ψ ∧ ¬φ), ψ → φ = ¬(ψ ∧ ¬φ), [k]φ = ¬⟨k⟩¬φ, Eφ = ¬A¬φ.

A reflexive and transitive relation.

Acknowledgements. The funding for most of this work is granted by the anr synbiotic (anr blan 0307 01) and we would like to thank the colleagues of this project for their fruitful discussions.

Proofs

Proposition 1. By contradiction, assume that P is unobservable, then there does not exist a model satisfying the formula. As Q is observable, we deduce that there exists models satisfying Q, but no restricted model must satisfy P , that contradicts the definition of the behavioral consequence. Proposition 3. Let ψ ∈ F H be a formula, let σ ∶ (NOM ∪ PROP ∪ REL) → (NOM ∪ PROP ∪ REL) be a substitution on nominals, variables and relational symbols, let M = ⟨W, (R k ) k∈τ , V ⟩ be a model, we define the model M = ⟨W, ( Rk ) k∈τ , Ṽ ⟩ from M as follows:

Proof. The proof is defined by induction on the formula: without loss of generality, we assume that ψ is in Negation Normal Form where negation occurs only immediately before variables only. Recall that every formula can be set in Negation Normal Form.

• M, w ⊩ a ⇐⇒ M, w ⊩ a, a ∈ PROP ∪ NOM. By (1), we have w ∈ V (aσ) ⇐⇒ w ∈ Ṽ (a) leading to the equivalence.