Samuel Buchet
email: samuel.buchet@ec-nantes.fr

Morgan Magnin

Olivier Roux

Proving Unreachability in Automata Networks by Mixing Static Analysis and Bounded Model Checking

Keywords: Static Analysis, Reachability, Bounded Model Checking, Discrete models, Automata Networks, Systems Biology, b2 -→ b1 :: b1 -→ b2 :: a0 b2 -→ b1 :: c0 b2 -→ b1 :: c0

Discrete models have been widely used in the field of bioinformatics, more especially in Systems Biology. Automata Network is a powerful modeling framework which can represent different dynamics on complex systems. The study of its dynamical properties has multiple purposes. Among these properties, reachability is of crucial interest for many real life applications (e.g. in biological regulatory networks). For example, it can give interesting insights about the behavior of the biological system. Additionally, it can be used to validate a model regarding the biological literature. In the last decade, some approaches have been shown of interest to address instances with hundreds of components. They are based on approximations that however lead to non-conclusiveness on some examples that may appear in practical biological examples. In this work, we present an approach combining static analysis with Bounded Model Checking to decide about the unreachable case. The originality of our method lies in the computation of a sufficient bound on the length of execution sequences, derived from previous works using static analysis.

Introduction

Biological systems such as genetic regulatory networks have been widely studied through discrete dynamical models. Indeed, representing biological species as discrete variables can give interesting insights in the dynamics of the system. Over the years, several discrete modeling frameworks have been proposed to capture and understand the behaviors of these networks. One benefit of studying these systems through discrete models is the possibility to perform formal analysis on models, since its state space is discrete and can usually be abstracted as a finite system.

In this paper, we focus on a discrete dynamical framework which can be seen as a generalization of Boolean Networks: Asynchronous Automata Networks (AAN) ( [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF], Paulevé, 2018]). This qualitative approach is based on three key concepts: (1) Biological components (e.g. genes) are abstracted in the form of what we have called automata. The different local states (that are not restricted to Boolean values) of each automaton correspond to the different discrete qualitative levels of the components represented by the automaton. (2) Interaction between biological components is modeled in an atomic way by local transitions on the automata, conditioned by a set of required local states in different automata. (3) In the modeling task, such a representation makes it possible to build the largest possible dynamics, and then to proceed by successive refinements to restrict the possible behaviors. For this latter point, the asynchronous semantics seems suitable due to the large scope of behaviors that are covered. Although there are biological justifications for both the asynchronous and the synchronous semantics, the asynchronous semantics can be justified from the fact that the probability that several biological phenomena occur simultaneously is low. The flexibility of Asynchronous Automata Networks makes them useful to represent various systems, including biological regulatory networks (which can also be modeled as Boolean Networks [START_REF] Taou | Investigating the use of boolean networks for the control of gene regulatory networks[END_REF])). The formal study of the dynamics of biological systems, especially the reachability problem, represent a main challenge because of its difficulty. In addition, reachability analysis is strongly linked to the computation of attractors, which is an important property of biological systems. Attractors are long-term structures in which any dynamics eventually falls into, thus capturing either the long-term behavior of a component or being interpreted as cell types [START_REF] Shen-Orr | Cell type-specific gene expression differences in complex tissues[END_REF]). This kind of properties is also crucial when refining a model of a living system, that is one way to remove inconsistencies or to predict missing information in biological models consisting in comparing the reachabilities/unreachabilities of the model with the experimentally observed behaviors.

In recent years, Bounded Model Checking and especially SAT encoding have been shown as an efficient way to verify temporal properties on dynamical models ( [START_REF] Biere | Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications[END_REF]). In this work, we investigate an approach based on static analysis which, combined with Bounded Model Checking, can be used to tackle reachability analysis in Asynchronous Automata Networks. More especially, this approach can be useful to prove the unreachability cases. To do so, we first introduce the Asynchronous Automata Networks -abbreviated hereafter as Automata Networks (AN) -. Second we describe the associated reachability problems and existing methods to tackle them. Third, we present in more details existing static analysis tools used for these problems. Finally, we introduce our main contribution, which is a new approach based on the computation of a completeness threshold (denominated bound) to prove unreachability. This bound represents a sufficient length for the sequences that solve reachability instances, and can be used as the length of encoded execution sequences to make unreachability proofs with a Bounded Model Checking approach. The computation of the bound relies on the existing static analysis approach, and we show that our new result strengthen the link between the existing properties based on static analysis and the set of solutions to a reachability problem, thus opening the door to further extensions. We also present the current limitations of our approach on specific instances, and we provide additional perspectives to its generalization.

Notations

Integer ranges are noted [m; n] = {m, m + 1, ..., n}. |A| represents the cardinality of a set A. A sequence of elements x is noted x = (x 1 :: x 2 :: .. :: x |x|-1 :: x |x| ) where |x| denotes the length of the sequence. The empty sequence is denoted as ε, thus |ε| = 0.

Automata Networks and related works

In this section, the Asynchronous Automata Networks and their associated reachability problems are introduced. Then, multiple approaches and related works about the reachability problem are covered.

Asynchronous Automata Networks and reachability analysis

Automata Networks are discrete dynamical models which can be used to represent various real world systems. Their use has been focused on the study of biological networks, for example through the static analysis tool Pint ( [Paulevé, 2017]), from the Colomoto framework ( [START_REF] Naldi | The CoLoMoTo Interactive Notebook: Accessible and Reproducible Computational Analyses for Qualitative Biological Networks[END_REF]). Automata Networks are composed of several automata, linked together through their transitions. Each automaton has a limited number of local states and a global state of the model is a vector composed of local states for each automaton. Practically speaking when local states represent the discrete qualitative levels of a biological component, the number of such states is assumed to be relatively limited (often ≤ 3). Indeed, the benefits of discrete modeling is to make abstractions of the system so that its behavior is easier to analyse and interpret. A limited number of local states leads to simpler models that can be exhaustively analyzed.

Definition 1 Automata Network (AN) An Automata Network is a tuple M = (Σ, S, T ) where:

• Σ = {a, b, ..} is the finite set of automata To describe the dynamics of Automata Networks, it is also necessary to specify the semantics. The semantics indicates which transitions can be played simultaneously from any global state. In this work, we focus on the asynchronous semantics, which means that, from one global state, only one transition can be played at a moment, among all the playable transitions. The asynchronous semantics has been preferably used for qualitative modeling in systems biology ( [START_REF] Assmann | Discrete Dynamic Modeling with Asynchronous Update, or How to Model Complex Systems in the Absence of Quantitative Information[END_REF]). Indeed, qualitative models are focused on the representation of the transitions from different discrete states in the species of a biological system [START_REF] Chatain | Boolean Networks: Beyond Generalized Asynchronicity[END_REF]). In the asynchronous update mode, it is assumed that the transitions in the local states of two different species will not happen at the same time.

2 -→ a1, a1 b 1 ,c 2 ---→ a2}. For the transition τ = a1 b 1 ,c 2 ---→ a2, orig(τ ) = a1, dest(τ ) = a2 and enab(τ ) = {b1, c2}.
The asynchronous semantics makes the model non-deterministic in the sense that each transition that is playable from one state leads to a different global state. Note that since transitions between the same local state (i.e. xi c -→ xi) are not considered here, self loops will not appear in the global reachability graph of the Automata Network.

Definition 2 Transition playability (asynchronous semantics) Given an Asynchronous Automata Network M = (Σ, S, T ):

• A transition τ ∈ Tx is playable from a global state s ∈ S if s(x) = orig(τ ) and ∀yi ∈ enab(τ ), yi = s(y). We define the playable predicate such that playable(s, τx) = ⊤ if and only if τ is playable from s.

• The playability operator, denoted •, is defined as s • τ = s ′ where s ′ (y) = s(y) ∀y ∈ Σ \ {x} and

s ′ (x) = dest(τ ) if playable(s, τ ) = ⊤. If playable(s, τ ) = ⊥, s • τ is not defined.
• A sequence π of transitions of size n is denoted as π = (π 1 :: π 2 :: .. :: π n ) with π i ∈ T ∀i and playing π (when possible) is denoted as

s • π = s • π 1 • π 2 • .. • π n , with s ∈ S.
Example 2 In the Automata Network of Fig. 1, from the local state s = (a0, b2, c0), the transitions

τ1 = a0 b 2 -→ a1 and τ2 = c0 b 2 -→ c1 are playable and the transition τ3 = b1 -→ b2 is not playable. In this model, s • τ1 = (a1, b2, c0). For the sequence π = (c0 b 2 -→ c1 :: b2 -→ b1), s • π = s • π 1 • π 2 = (a0, b1, c1).
From these definitions, the reachability problem is defined as questioning the existence of a transition sequence that makes the model evolve from a global initial state to some state which verifies the presence of certain local states. This problem can also be reduced to the reachability of only one local state, by using an additional automaton in the model, as explained in [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF]. For this reason, we will only consider the reachability of a single local state in this work. Regarding the complexity, this problem can be proved PSPACE-Complete through a transformation to bounded Petri nets [START_REF] Cheng | Complexity results for 1-safe nets[END_REF], Paulevé, 2018]). Indeed, the number of (global) states of an Automata Network is finite and exponential in the number of automata and the reachability problem can be seen as finding a path between two states in the state transitions graph of the model. • Issue: Is there a sequence of transitions π = (π 1 :: π 2 :: .. ::

π n ) such that s0 • π = s ′ with s ′ (x) = xi ?
From this latter definition, solutions are formalized by sequences of transitions. However, when a reachability instance admits a solution, this instance may admit an infinite number of solution sequences. Indeed, it can be possible for example to insert arbitrarily long loops inside a solution. The corresponding notion of solution in [Paulevé, 2018] has been refined (as sub-traces and minimal traces) in order to represent only canonical solutions. For this reason, we introduce in this work the equivalent notions of subsolutions and minimal solutions. A sub-solution corresponds to a sub-sequence of a solution (containing only transitions of the original sequence, with a conservation of their order) and that is also a solution to the reachability instance. A minimal solution is a solution which does not admit any sub-solution. It is also worth noting that solutions and minimal solutions may contain multiple occurrences of the same transition.

Definition 4 Solutions, sub-solutions and minimal solutions for reachability Let R = (s0, xi) be a reachability instance.

-A sequence π1 of transitions is a solution to the reachability instance R if

[s0 • π1] (x) = xi.
-A sequence π2 of transitions is a sub-solution of a solution π1 if π2 is a solution and if there exists an injection ϕ :

[1; |π2|] → [1; |π1|] such that ∀i ∈ [1; |π2|], π

Related works

Several approaches have been used to solve the reachability problem in Automata Networks. For example, one can use static analysis techniques, which consist in verifying some properties without any execution of the system ( [START_REF] Wichmann | Industrial perspective on static analysis[END_REF]). A method based on static analysis has been employed in [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF]. This method is based on necessary and sufficient conditions on reachability. The verification of these conditions is usually computationally efficient and, depending on the result, it can be possible to conclude if the reachability is true or not. However, there exists reachability instances for which the result on the verification of the conditions cannot be used (when the necessary conditions are verified and the sufficient conditions are not verified). Nonetheless, it has been observed in the study that, on some biological models, this method is mostly conclusive.

The reachability problem also falls into the category of Model Checking. Formally, Model Checking consists in checking a temporal property on a mathematical model ( [Clarke, 2008]). Several techniques have been created to verify exhaustively large scale systems. This field has applications in various domains such as software verification, parallel systems and systems biology. For instance, model checking has been employed in [ Česka et al., 2014] for the verification of biochemical networks, ( [START_REF] Heath | Probabilistic model checking of complex biological pathways[END_REF]) for the analysis of biological pathways.

Explicit approaches have been applied in Model Checking to biological systems ( [Klarner et al., 2012a, Klarner et al., 2012b, Gallet et al., 2014]). The use of symbolic methods such as Binary Decision Diagrams (BDD) was also originally popular in Model Checking ( [START_REF] Burch | Symbolic model checking: 10 20 states and beyond[END_REF]). Several general symbolic model checking tools such as NuSMV1 or ITS-tools2 can be used to encode the dynamics of Automata Networks. However some of these symbolic methods have not been proven efficient on large scale models ( [Bryant, 1986]) and some instances can be difficult to verify with state of the art approaches, as we can see in the benchmarks from [Paulevé, 2017].

The Bounded Model Checking framework became widely used in Model Checking to study dynamical properties like reachability ( [START_REF] Biere | Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications[END_REF]). This framework consists in encoding execution sequences of a dynamical system using a logic programming language. Then, a dedicated solver is used to exhaustively search among all the sequences of fixed length and look for specific temporal properties. This approach has been used to solve various problems in biological networks ( [START_REF] Dubrova | [END_REF]Teslenko, 2011, Nabli et al., 2016]). For example, solvers for SAT problems have been used to solve reachability problems in Petri nets ( [START_REF] Ogata | SAT-based verification of safe Petri nets[END_REF]), and to compute attractors in asynchronous boolean networks ([Van Giang and Hiraishi, 2020], where the methodology slightly diverges from classical Bounded Model Checking). An encoding have been proposed for reachability analysis in synchronous Gene Regulatory Networks with SMT solving in ( [START_REF] Giacobbe | Model checking the evolution of gene regulatory networks[END_REF]). An Answer Set Programming encoding has also been developed for the computation of attractors in Automata Networks ([Ben Abdallah et al., 2017]).

Although Bounded Model Checking has demonstrated its efficiency to verify properties on large scale systems, proving unreachability still remains difficult as it requires a sufficient length for the encoding of execution sequences. For a finite state model, it is for instance possible to take the number of states of the system but this number is usually exponential in the size of the model. More generally, Bounded Model Checking also offers techniques to determine a completeness threshold of the system (i.e. a bound on the sufficient length of reachability sequences) through the encoding of inductive formula (k-induction techniques, [START_REF] Biere | Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications[END_REF]). For example, it is possible to encode the computation of the longest shortest path that reaches the goal state. However, this type of bound remains very general and its computation can be particularly difficult, as it is explained in appendix B.

In this paper, a bound dedicated to Automata Networks is derived from the existing static analysis approaches. This work aims at combining the bound with a Bounded Model Checking approach to tackle unreachability cases. Indeed, an exhaustive search on execution sequences of the model, combined with a reasonable bound on the reachability instance, can be used to efficiently make unreachability proofs.

Static analysis and Local Causality Graph

As mentioned previously, our approach to solve the reachability problem in Automata Networks relies on existing work using static analysis, that is introduced in [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF]. This approach is based on the consideration of local reachability problems (i.e. a reachability problem within an automata). In this section, we introduce notions from this work that will be used thereafter. The definitions given here are not exactly identical with the definitions in the previous works. However, they are equivalent and the known results still hold.

Local Causality Graph

The main element presented in this section is a graph called the Local Causality Graph. This graph represents local reachabilities (automaton reachabilities), which are defined through objectives and local solutions. Indeed, solving a reachability problem on the whole Asynchronous Automata Network can be seen equivalently as solving a local reachability in one automaton (from the goal local state), which leads to sub reachabilities on the other automata (depending on the conditions of transitions). An objective represents a local reachability problem (i.e. in one automaton) and a local solution is an acyclic sequence of transitions from this automaton, that locally solves the corresponding objective (all the local states are reached at most once).

. :: η n ) (with η i ∈ Tx ∀i ∈ [1; n]) such that orig(η 1 ) = xi, dest(η n ) = xj and dest(η k ) = orig(η k+1 ) ∀k ∈ [1; n -1] and ∀i, j ∈ [1; n], j > i =⇒ orig(η i ) ̸ = dest(η j )
• -→ c2). The objective b0 ⇝ b0 admits only a trivial solution η3 = ε since the local reachability is already satisfied.

In practice, the objectives are solved through an exhaustive search. The number of local states for each automaton is in fact relatively small, as mentioned in subsection 2.1. Note that each transition does not appear more than once in a local solution, which makes the set of local solutions finite. Although some solutions of a reachability instance may contain duplicates of transitions, it will be shown in the following that decomposing a minimal solution into local solutions is always possible. Then, local solutions can be used as additional information to solve a reachability problem. Indeed, the local solutions of an objective may require some states to be realized, depending on the conditions of the transitions. These local states lead to intermediary objectives that needs to be solved, as the conditions of the transitions are not necessarily satisfied in the initial state. This recursive definition results in the construction of a graph, which is called the Local Causality Graph.

Note that the definition of the Local Causality Graph presented here slightly differs from the definition in [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF]. Indeed, the transitions of the automata were not exhibited in the original Local Causality Graphs. In this paper, we show that adding the transitions reveals interesting information about the reachability problem. This alternative Local Causality Graph still contains the information from the original graph and a translation between the two definitions is possible.

Definition 6 Local Causality Graph (LCG) Given an Automata Network M = (Σ, S, T ) and a reachability instance R = (s0, xi), a Local Causality Graph associated with M and R is a digraph G = (VG, EG) with VG = L ∪ O ∪ Q ∪ T ′ such that : • L ⊂ y∈Σ Sy (local states) • O ⊂ y∈Σ Sy × Sy (objectives) • Q = y i ⇝y j ∈O lpaths(yi ⇝ yj) (local solutions) • T ′ = o∈O {η i | i ∈ [1; |η|], η ∈ lpaths(o)} (transitions) • EG ⊂ VG × VG (directed edges)
And which satisfies the following conditions:

1. xi ∈ L (overall objective) 2. (yi, s0(y) ⇝ yi) ∈ EG ∀yi ∈ L (objectives from initial state) 3. (yi ⇝ yj, η) ∈ EG ∀η ∈ lpaths(yi ⇝ yj), ∀yi ⇝ yj ∈ O (all local solutions) 4. (yj, yi ⇝ yj) ∈ EG ∀yi, yj ∈ L (saturation) 5. ∀η ∈ Q, (η, η i ) ∈ EG ∀i ∈ [1; |η|] (transitions of the local solutions) 6. ∀τ ∈ T ′ , ∀yi ∈ enab(τ ), (τ, yi) ∈ EG (required local states)
The construction of the Local Causality Graph starts from the goal local state (from the reachability problem) and one associated objective, from the initial state to this local state (conditions 1 and 2). Then, the different conditions of the definition are applied to the graph, and vertices and edges are added until all the conditions are satisfied. Each time a local state appears in the graph, the objective from the initial state of this automaton to this local state has to be added (condition 2). However, it is not easy to predict which objective would be used for the reachability of a local state, since it depends on the previous local reachabilities that have been solved. That is why all the objectives from any local state of the graph from the same automaton to this local state are added to the graph (condition 4). When an objective is added, all its local solutions are automatically added to the graph (condition 3) with their corresponding transitions (condition 5) and the associated local states required to play these transitions (condition 6).

It is useful to mention that the local solutions vertices "•" in a Local Causality Graph correspond to subsets of transitions, to which they are connected according to condition 4. The presence of a local solution vertex is justified by the fact that it is interesting to distinguish between the different local solutions of an objective in order to solve a reachability. Besides, all vertices appear only once in the graph. For example, if a local state xi ∈ Sx is in the condition of more than one transition, there will be only one vertex xi ∈ VG in the graph. All these transitions will be then connected to this single vertex. Thanks to this, the size of the graph is polynomial in the size of the Automata Network (assuming the number of local solutions for each objective is small). On the other side, this potentially induces the presence of cycles, which will be discussed later.

Example 5 The graph in Fig. 2 is a Local Causality Graph associated with the reachability problem R = ((a0, b0, c0), a2) for the Automata Network of Fig. 1. The numbers labeling some of the vertices are explained later. In this graph, the objectives of the form xi ⇝ xi have not been added since they do not bring additional information for the solution. The local state b1 has two predecessors, because it appears in the conditions of two transitions and as explained above, the vertices must appear only once in the graph. Finally, the sufficient conditions mentioned in subsection 3.2 are satisfied in this graph, which implies that reachability of a2 is possible from (a0, b0, c0).

Necessary and sufficient conditions for reachability

As already mentioned, the Local Causality Graph has been created and used to solve reachability problems in a static way. Necessary conditions for reachability relying on the Local Causality Graph are introduced in [Paulevé, 2018]. These conditions are defined from an incomplete Local Causality Graph, which contains only objectives starting from the local states of the initial state. The necessary conditions state that given an initial state, if there is no local solution to an objective starting from a local state in the initial global state, then its reachability is not possible (i.e. there is no local path to solve the objective within the automaton). This property can be propagated to the successors of the local solution in the graph to prove that some reachabilities are not possible. The verification can be done with an algorithm that is polynomial in the size of the Automata Network.

a 2 a 0 ⇝ a 2 • a 0 b2 -→ a 1 a 1 b1,c2 --→ a 2 b 2 b 0 ⇝ b 2 b 1 ⇝ b 2 • b 1 - → b 2 • b 0 - → b 1 b 1 c 2 b 0 ⇝ b 1 b 2 ⇝ b 1 • • b 2 - → b 1 c 0 ⇝ c 2 • • c 0 b2 -→ c 1 c 1 b1 -→ c 2 c 0 b1 -→ c 2 1 1 2 2 1 3
These conditions have been used in the study to reduce the size of a Local Causality Graph by proving that some objectives (if not all) are impossible. In addition, it can be shown that if a reachability is true, then the transitions of the minimal solutions for this reachability all belong to the Local Causality Graph. In other words, the transitions of the Local Causality Graph are sufficient to solve the reachability, and other transitions may be discarded for this specific instance. This property has been used in the study to reduce the computational cost of solving reachability with Model Checking tools. This property can also be used to remove unreachable local states and automata from the model in some cases.

Sufficient conditions for reachability are introduced in [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF]. These conditions can be used to prove, in some cases, that the reachability is true. The idea behind these conditions is that if every objective of some local state in the graph has at least one solution, its reachability must be true. Indeed, if all objectives admit some solution, it means that the local state can be reached from any other local state of the same automaton in the graph, which slackens the possibilities of the Automata Network (the local states can be reached in any order). This condition can be propagated to the successors of the local state in the Local Causality Graph. It results as a verification that is again polynomial in the size of the Automata Network. Moreover, when the conditions are verified, a solution sequence can be computed. Although these conditions have been successfully applied on large biological models, the sufficient conditions represent an under-estimation of the solutions to a reachability instance. Thus, there are still simple examples for which the verification fails, as it is explained in Example 6.

a 0 1 b 0 1 c 0 1 b 1 , c 0 c 1 b 0 d 0 1 e 0 1 f 0 1 e 1 , f 0 f 1 M 1 , R 1 = ((a 0 , b 0 , c 0 ), a 1 ) M 2 , R 2 = ((d 0 , e 0 , f 0 ), d 1 )
Figure 3: Two Automata Networks illustrating where the necessary conditions are verified and where the sufficient conditions are not verified.

Example 6 The two Automata Networks M1 and M2 in Fig. 3 illustrate simple cases where the verification of the reachability by the necessary and the sufficient conditions fails.

-In the network M1 (on the left), the reachability R1 = ((a0, b0, c0), a1) is possible and the following transition sequence is a solution:

(c0 b 0 -→ c1 :: b0 c 1 -→ b1 :: c1 -→ c0 :: a0 b 1 ,c 0 ---→ a1
). However sufficient conditions verification fails at proving that the reachability is true because, in the corresponding Local Causality Graph, the objective b1 ⇝ b0 has no local solutions (see appendix D.1). The sufficient conditions ensure that the local states from the Local Causality Graph are reachable in any order, and this is not verified in this example because b1 cannot be reached from b0 (no local solutions for b1 ⇝ b0). This objective is practically useless for the reachability of a1 since b0 does not need to be reached when b1 is activated. But it appears in the Local Causality Graph because b1 and b0 are both present.

-Regarding the network M2, the reachability instance R2 = ((d0, e0, f0), d1) is not possible. Indeed, e1 and f0 are required to play the transition from d0 to d1, but f1 needs to be activated in order to activate e1 and f0 cannot be activated afterward. In this example, the necessary conditions are yet verified since every local state of the associated Local Causality Graph is still locally reachable from its local state in the initial state (appendix D.2). Indeed, the necessary conditions consist in verifying that the all objectives starting from the local states in the initial state have at least one solution. Intuitively, for an objective, the absence of local solutions from the local state in the initial state implies the absence of local paths solving the local state in a global solution.

Proofs of unreachability and computation of a bound

This paper focuses on the unreachability case in Asynchronous Automata Networks. From a biological point of view, proving unreachability is much more important than proving that reachability is true. Indeed, the guarantee that a state is accessible remains dummy since unobserved conditions related to the environment will always possibly prevent actually reaching this state. Unfortunately, as explained before, the necessary conditions presented in section 3.2 are not able to tackle all unreachability cases. Our approach to prove unreachability consists in taking advantage on the ability of Bounded Model Checkers to perform exhaustive search over execution sequences of large scale models. However, a completeness threshold (i.e. a bound on the length of reachability sequences) remains necessary to formally prove the unreachability case.

In this work, we propose a method to compute a dedicated bound for Automata Networks. The originality of our approach lies in the use of the Local Causality Graph. This section introduces our bound, named the Local Causality Bound. The Local Causality Bound aims to be specifically adapted to the Asynchronous Automata Networks and we expect this bound to be smaller than more generic completeness thresholds, as it is developed in appendix B. We assume that a smaller bound will help the Model Checkers to give more efficiently an answer. In this part, the first subsection introduces the main definition and property about the Local Causality Bound. Then, the outline of its proof is detailed in subsection 4.2. Complete proofs of intermediary results can be found in appendix C. Some specific cases of the computation of the bound are investigated in subsection 4.3. Subsection 4.4 shows some practical examples of the Local Causality Bound. Finally, the general application of the bound is discussed in subsection 4.5.

Local Causality Bound

Local Causality Graphs aim to over-approximate the solutions of a reachability problem, by linking multiple local reachability problems. Here we investigate how this over-approximation could be exploited to derive a sufficient length on the number of transitions necessary to solve the reachability, and its use to formally prove unreachability. Indeed, the Local Causality Graph can also be computed when the associated reachability instance has no solution. Unfortunately, not all solutions can be represented by a Local Causality Graph since some of them may be arbitrarily long, or they may contain useless transitions, that are not captured by the graph. For this reason, it will be shown that the minimal solutions introduced in Definition 4 can be used to characterize all solutions that are captured by a Local Causality Graph.

Locally, the number of transition necessary to solve an objective can be over-estimated by the length of the longest local solution for that objective. This number may be used to build a bound, but it would not cover the transitions from other automata that are necessary to form a complete solution. Nevertheless, the structure of the Local Causality Graph can be used since the transitions of a local solution are connected to the local states of its conditions. If the bounds of sub-objectives associated with the local states are already known, one can recursively compute a bound for the initial objective.

Since the computation of the bound for one vertex of the Local Causality Graph would depend on its successors in the graph, the next definition proposes a possible computation of the bound as a function of any vertex of the graph. The function is recursive because the bound of one vertex depends on the bounds of the vertices that are connected to it. However, this definition does not directly allow the computation of the bound in a cyclic Local Causality Graph, as it will be discussed afterwards.

-B(τ ) = 1 + y i ∈enab(τ ) B(yi) ∀τ ∈ T ′ -B(η) = k∈[1;|η|] B(η k ) ∀η ∈ Q -B(o) = max η∈lpaths(o) B(η) ∀o ∈ O -B(yj) = max y i ⇝y j ∈O B(yi ⇝ yj) ∀yj ∈ L
Intuitively, the bound function relies on both necessary and the sufficient aspects of the Local Causality Graph. The number of transition associated with a local state is sufficiently approximated by the maximum bound of the corresponding objectives of the graph, and the number of transitions of an objective is sufficiently approximated by the maximum bound of all the local solutions. Indeed, in both cases, it is not possible to decide which objective/local solution would be used in a minimal solution to the reachability. On the contrary, since all transitions are necessary in a local solution and since all their conditions need to be satisfied to play the transitions, their associated bounds take into account all the vertices that are successors in the Local Causality Graph. As it will be proved in subsection 4.2, the bound function, applied to the goal local state of the reachability instance indeed gives a completeness threshold for the reachability. This property is formalized in the following proposition: -For all transition sequences π such that π is a minimal solution of R, |π| ≤ B(xi)

The next example illustrates how the bound can be computed in practice, with an acyclic Local Causality Graph.

Example 7 Fig. 2 shows the bounds computed for the Local Causality Graph of the reachability instance ((a0, b0, c0), a2) of the Automata Network in Fig. 1. For clarity, some of the bounds have been discarded. We can see that the bound B(a2) = (2 + 1) + (5 + 1 + 1) = 3 + 7 = 10 correctly overestimates the length of the solution (= 6) given in Example 3.

As mentioned above, the computation of a bound is useful as soon as one is able to exhaustively check the sequences of a fixed length, with the use of a Bounded Model Checking approach for example. Although this type of encoding have already been proposed for various logical models, a SAT encoding specifically dedicated to Asynchronous Automata Network has been implemented in this work. The SAT encoding is detailed in appendix A. An implementation of the bound computation and the SAT encoding are also available online3 .

Proof of the Local Causality Bound

To formally prove that the Local Causality Bound is able to over-estimate the length of all minimal solutions to a reachability instance, we propose an association between each minimal solution and the Local Causality Graph, that shows precisely how the graph is actually able to over-approximate the minimal solutions. This association consists in decomposing the minimal solution into multiple objectives. These objectives are identified from the conditions of the transitions in the solution and they are associated to sub (local) transition sequences forming local solutions. Since the same objective may be solved several times in a solution, the identification is based on the index of the transition having the condition. We also show that the identified objectives can be associated between each other to form a structure that is similar to the Local Causality Graph. From this association, it is possible to prove by induction on this structure that the Local Causality Bound correctly overestimates the number of transitions of any minimal solution. This subsection shows all the steps that are necessary to build this association. The last part of the proof consists in two lemmas that are demonstrated in appendix C.

In this part, the following notations are used: M = (Σ, S, T ) denotes an Asynchronous Automata Network. R = (s0, xi) represents a reachability instance, assuming s0(x) ̸ = xi and π is a minimal solution to that instance (s0 The next definition, relying on these sequences of indices, aims to identify sequences of objectives locally for each automaton. These objectives correspond to objectives that are solved through local solutions in the minimal solution π. They also correspond to objectives of the Local Causality Graph. If an automaton does not have any identified condition in the minimal solution, the corresponding sequence of objectives would be empty. For the goal local state xi of the reachability instance, one additional objective is identified. Indeed, this local state does not appear in the conditions of the transitions.

• π(x) = xi). G = (VG, EG) is a Local Causality Graph associated with R, with VG = L ∪ O ∪ Q ∪ T ′ ,
Definition 9 Objectives associated with a minimal solution Oπ, are the sequences of objectives of each automaton that are exactly solved by a minimal solution in π. i.e. the local states of these objectives correspond to the conditions for these automata on the other transitions. For all z ∈ Σ \ {x} such that Iπ,z = ε, we have: -Oπ,z = ε For all y ∈ Σ \ {x} such that Iπ,y ̸ = ε, we have |Oπ,y| = |Iπ,y| and |Oπ,x| = |Iπ,x| + 1 For y ∈ Σ such that Iπ,y ̸ = ε (including x), we have: -O 1 π,y = s0(y) ⇝ yj with yj ∈ enab(π I 1 π,y ) ∩ Sy -O i π,y = yj ⇝ y k with yj ∈ enab(π I i-1 π,y ) ∩ Sy and y k ∈ enab(π I i π,y ) ∩ Sy if 1 < i ≤ |Iπ,y| For x, the automaton of the goal local state, we have also:

-O |Iπ,x|+1 π,x = s0(x) ⇝ xi if Iπ,x = ε x k ⇝ xi, x k ∈ enab(π I |Iπ,x| π,x
) ∩ Sx otherwise

The next definition creates an association between the objectives previously identified and the transitions of the minimal solution. It is possible to show that these transitions also correspond to minimal solutions of the associated Local Causality Graph.

Definition 10 Transitions associated with the objectives Let Oπ,y be the sequence of objectives associated with y in the minimal solution π, with y ∈ Σ (including x). When Iπ,y ̸ = ε, the transitions associated with each objective O i π,y , i ∈ [1; |Iπ,y|] of Oπ,y are the (multi)sets defined as:

tr(O i π,y ) = {π j | π j ∈ Ty, j < I 1 π,y } if i = 1 {π j | π j ∈ Ty, I i-1 π,y < j < I i π,y } if i ∈ [2; |Iπ,y|]
and set of transitions associated with

O |Oπ,x| π,x
is defined as:

tr(O |Oπ,x| π,x ) = {π j | π j ∈ Tx, j > I |Iπ,x| π,x } if Iπ,x ̸ = ε {π j | π j ∈ Tx} otherwise
Finally, the next definition introduces the objective tree that aims to connect the identified objectives with each other to reveal their dependencies, and form a structure similar to the Local Causality Graph. The main property of the bound can then be proved on this recursive structure through structural induction.

Definition 11 Objective tree associated with a minimal solution -The objective tree of a minimal solution π is a digraph

H = (VH, EH) with VH ⊂ {O i π,y | i ∈ [1; |Oπ,y|], y ∈ Σ} and EH ⊂ V 2 H , verifying (O i π,y , O j π,z ) ∈ EH ⇐⇒ π I j π,z ∈ tr(O i π,y ) (i.e.
the transition having the condition on z finishing the objective is a transition associated with the parent objective)

It will be shown that H corresponds to a tree (it has no cycles and it is connected). Indeed, H is finite since it contains the finite set of objectives identified from the minimal solution. Moreover, each objective can only be connected to an objective that was solved earlier in the solution, which does not allow the formation of cycles. Last, but not least, each objective has one predecessor except O |Oπ,x| π,x which can be identified as the root of H. We also introduce the notation ≺H defined as: o ′ ≺H o if there exists a path from o to o ′ in H, i.e. if o ′ is a successor of o (direct or not direct).

The following example shows step by step the construction of the objective tree previously defined, from a minimal solution of a reachability instance.

Example 8

In this example, the previous definitions are applied to the rechability instance R = ((a0, b0, c0), a2) on the Automata Network from Fig. 1, with its associated Local Causality Graph from Fig. 2 and with the minimal solution π2 = (b0 -→ b1 :: b1 -→ b2 :: a0

-tr(O 1 π 2 ,a ) = {a0 b 2 -→ a1, a1 b 1 ,c 2 ---→ a2} -tr(O 1 π 2 ,b ) = {b0 -→ b1, b1 -→ b2} ; tr(O 2 π 2 ,b ) = {b2 -→ b1} ; tr(O 3 π 2 ,b ) = ε -tr(O 1 π 2 ,c ) = {c0 b 1
-→ c2} Which leads to the construction of the following objective tree H = (VH, EH):

-VH = {O 1 π 2 ,a , O 1 π 2 ,b , O 2 π 2 ,b , O 3 π 2 ,b , O 1 π 2 ,c } -EH = {(O 1 π 2 ,a , O 1 π 2 ,b ), (O 1 π 2 ,a , O 3 π 2 ,b ), (O 1 π 2 ,a , O 1 π 2 ,c ), (O 1 π 2 ,c , O 2 π 2 ,b )}.
For the following, Iπ,y and Oπ,y (y ∈ Σ) denote the lists of indexes and objectives that are constructed from the minimal solution π defined earlier. H = (VH, EH) denotes an objective tree associated with π. The next lemma gives some properties from the previous definitions that are useful for the proof. The proof of these properties can be found in appendix C.

Lemma 1 The next lemma is used to associate the bound function with the objectives identified in the minimal solution. This property is recursive (the bound of an objective is characterized with respect to the bounds of sub-objectives in the tree) and its application to the root of the objective tree gives an overestimate for all the transitions of the minimal solution. Its proof can also be found in appendix C.

1. ∀y ∈ Σ, ∀i ∈ [1; |Oπ,y|], ∃η ∈ lpaths(O i π,y ) such that {η j | j ∈ [1; |η|]} = tr(O i π,y ) (tr(o) corresponds to a local solution of o) 2. o∈V H tr(o) = {π i | i ∈ [1, |π|]} (
Lemma 2 -∀o ∈ VH, B(o) ≥ |tr(o)| + o ′ ≺ H o |tr(o ′ )|
The proof of lemma 2 can be done by structural induction on H. Its base case corresponds to objectives that do not have any successor in H. The transitions associated with these objectives simply correspond to local solutions. The inductive case occurs when an objective has some successors. In this case, it can be shown that the direct successors are also linked to the objectives in the Local Causality Graph, through the transitions of its local solutions (lemma 1.5). Assuming that the property is recursively true, it is possible to show that the bound of the objective takes into account the transitions associated to all its direct and not direct successors in the tree. This lemma, when applied to the root of the tree (which is O ) is able to overestimate |π|.

Bound computation in cyclic Local Causality Graphs

Proposition 1 can be applied to any Local Causality Graph, but the bound function is recursive: the bound of a vertex of the graph depends on the bounds of its direct successors. Thus, in a cyclic graph, this definition does not lead to a concrete bound since the vertices of the cycles are mutually dependent and no base case can be applied.

a 0 1 b 0 1 b 1 a 1 a 1 a 0 ⇝ a 1 • a 0 b1 -→ a 1 b 1 b 0 ⇝ b 1 • b 0 a1 -→ b 1 b 1 ⇝ b 1 • a 1 ⇝ a 1 • Figure 4: An Automata Network illustrating a simple cycle.
Intuitively, one would think that a cycle implies that the reachability is not possible. Indeed, a cycle in the Local Causality Graph means that a local state needs itself in order to be reached. The following example shows how intuitively such simple cycles may be removed in order to compute the Local Causality Bound.

Example 9 Let M be the Automata Network of Fig. 4, R = ((a0, b0), a1) be a reachability instance and G the Local Causality Graph associated with R, also represented in Fig. 4. In this example, there is no solution to R. More precisely, a1 cannot be obtained from a0 since the only local transition realizing this change requires b1, which requires a1 (to be reached from b0). This mutual dependence creates the following cycle in the associated local causality graph:

(a1, a0 ⇝ a1, •a 0 ⇝a 1 , a0 b 1 -→ a1, b1, b0 ⇝ b1, • b 0 ⇝b 1 , b0 a 1 -→ b1).
Thus, the local causality bounds of all these vertices are not computable, including the reachability goal a1. However, the absence of solution in this case allows to remove some vertices of the cycle. Since a0 ⇝ a1 and b0 ⇝ b1 are both in the cycle, it is possible to assume that a1 cannot be reached from (a0, b0), and similarly b1 cannot be reached from (a0, b0). Thus, we can safely remove the local solution • b 0 ⇝b 1 regarding R for this Local Causality Graph. This leads to a sub graph G ′ of G where the local causality bound of a1 can be computed, and equals 1. Since no solution exists for R, 1 is indeed a correct overestimation. Besides, it is important to notice that the bound computed from the sub graph G ′ is only valid for R. Indeed, in G ′ , the bound of b1 equals 0 but b1 can be reached in one transition from (a1, b0). Since the objective a1 ⇝ a1 is present in G, G is presumably valid for this alternative reachability instance but G ′ is not.

The previous example shows that it is possible in some situations to safely remove vertices from a Local Causality Graph while having the guarantee that the Local Causality Bound remains correct for a given reachability instance. Formalizing these cases is possible by identifying properties on the objective trees made from the minimal solutions of a reachability instance. For example, it is not possible to obtain an objective tree where an objective x0 ⇝ x1 has itself as a descendent, and where at the same time there is no objective of the form x * ⇝ x0. With these properties, it would be possible to identify sub parts of a Local Causality Graph that cannot be associated to any objective tree, proving that no minimal solutions exist for some objective.

However in some cases, removing any of the vertices inside a cycle automatically breaks the proposition 1 for the main reachability goal. Indeed, although simple cycles cannot form a minimal solution, in some more complex examples cycles may appear because of the combinatorial order of reachabilities between several automata. We illustrate this in the next example, where the automata b, c and d are mutually dependant in such a way that the only minimal solution to reach a1 from (a0, b0, c0, d0) uses all the vertices in the cycle of the associated Local Causality Graph, and where some of the vertices (local transitions) from the cycle are used twice.

Example 10 Let M = (Σ, S, T ) be the Automata Network of Fig. 5 and R = (s0, a1) with s0 = (a0, b0, c0, d0). Let G = (VG, EG) be the Local Causality Graph associated with M and R represented in Fig. 6. The solution π = (c0

d 0 -→ c1 :: d0 c 1 -→ d1 :: c1 -→ c0 :: b0 c 0 ,d 1 ---→ b1 :: d1 b 1 -→ d0 :: c0 d 0 -→ c1 :: d0 c 1 -→ d1 :: a0 b 1 ,c 1 ,d 1 -----→ a1) is a minimal solution to R.
This solution contains two duplicated transitions: c0

a 1 a 0 ⇝ a 1 • a 0 b1,c1,d1 ----→ a 1 b 1 b 0 ⇝ b 1 • b 0 c0,d1 ---→ b 1 d 1 c 0 d 0 ⇝ d 1 • d 0 c1 -→ d 1 c 1 ⇝ c 0 • c 1 - → c 0 c 0 ⇝ c 0 • d 1 ⇝ d 1 • c 1 c 0 ⇝ c 1 • c 0 d0 -→ c 1 d 0 d 1 ⇝ d 0 • d 0 b1 -→ d 1 b 1 ⇝ b 1 • c 1 ⇝ c 1 •
EH = {(O 1 π,a , O 2 π,b ), (O 1 π,a , O 4 π,c ), (O 1 π,a , O 4 π,d ), (O 4 π,d , O 3 π,c ), (O 3 π,c , O 3 π,d ), (O 3 π,d , O 1 π,b ), (O 1 π,b , O 2 π,c ), (O 1 π,b , O 2 π,d ), (O 2 π,d , O 1 π,c ), (O 1 π,c , O 1 π,d )}.
This objective tree is represented in Fig. 7. Now let us focus on the bound of c1. Assuming it is possible to cut the cycle in G, one would remove the edge (d0 c 1 -→ d1, c1), which would lead to a bound of 0 for d1 (only the trivial solution remains valid). Then, the bound of c1 would be equal to 4. However, according to the Local Causality Bound, we should have

B(c0 ⇝ c1) ≥ |tr(c0 ⇝ c1)| + o≺ H c 0 ⇝c 1 |tr(o)|, i.e. B(c0 ⇝ c1) ≥ |tr(c0 ⇝ c1)| + |tr(d1 ⇝ d0)| + |tr(b0 ⇝ b1)| + |tr(c1 ⇝ c0)| + |tr(d0 ⇝ d1)| + |tr(c0 ⇝ c1)| + |tr(d0 ⇝ d0)| =⇒ B(c0 ⇝ c1) ≥ 6.
This means that the association between the Local Causality Graph and the minimal solution is not possible if the cycle is cut.

This last example shows that in some instances where several automata are linked in a complex way trough their transitions, cycles appear in the Local Causality Graph, and at the same time duplicated transitions occur in the minimal solutions. This can also be seen on the objective tree made from the solution π, in Fig. 10. Indeed, while the objective tree remains acyclic, the objectives d0 ⇝ d1 and c0 ⇝ c1 are duplicated, indicating the multiple use of the vertices from the cycle of the Local Causality Graph. Thus cycles in the Local Causality Graphs may not be directly safely removed in these instances.

a 0 ⇝ a 1 d 0 ⇝ d 1 b 1 ⇝ b 1 c 1 ⇝ c 1 c 0 ⇝ c 1 d 1 ⇝ d 0 b 0 ⇝ b 1 c 1 ⇝ c 0 d 0 ⇝ d 1 c 0 ⇝ c 1 d 0 ⇝ d 0 Figure 7:
The objective tree for the solution π for R = ((a 0 , b 0 , c 0 , d 0 ), a 1 ) in the example 10 However, we suggest that it is possible to refine (unfold) the Local Causality Graph by duplicating some vertices. The duplicates would allow to refine the objectives by partially re-ordering the reachability of the sub-goals, thus revealing simpler cases where the cycles can be removed. Besides, it is important to note that this particularity occurs only when the Local Causality Graphs have cycles and when the minimal solutions contain duplicates at the same time. The instances with duplicated transitions in the minimal solution and with an acyclic Local Causality Graph can still be directly treated with the bound.

Practical examples

To illustrate a practical application of proposition 1, we show here some examples that can be tested with the implementation of the bound computation and the SAT encoding mentioned in section 4.1 (see text file readme.md ). The Automata Network models used in these examples can be found in the implementation. Each example shows a reachability instance with its answer, and the Local Causality Bound is given when it can be computed. It also shows the answer of the static analysis tool Pint4

The first reachability holds and the second reachability is false. For both of these examples, the computation of the Local Causality Bound is possible and Pint is not able to provide an answer.

Discussion

As previously seen, the computation of the Local Causality Bound is very fast. Indeed, the construction of a Local Causality Graph can be done with a polynomial algorithm in the number of automata in the model, and each vertex of the graph needs to be processed only once in order to compute the bound. However, the examples introduced in subsection 4.3 show that the approximation induced by the Local Causality Graph may be too rough for the computation of the bound, especially when the graph contains cycles.

On the first hand, example 9 shows that some cycles can be treated by removing vertices when certain conditions are satisfied. Such modifications lead to an alternative Local Causality Graph, in which the Local Causality Bound remains correct. We suggest that the conditions allowing to remove some vertices can be elaborated by reasoning on the shape of the objective trees (i.e. not all objective trees can be associated to minimal solutions). For instance, in example 9 we could see that an objective a0 ⇝ a1 cannot be an undirect successor of itself, unless there is at least one other objective a1 ⇝ a * .

On the second hand, example 10 shows a more difficult graph where removing any vertex from the cycle does not lead to a correct bound. We saw that in this example, the minimal solution contains multiple occurences of several transitions, which explains why all the vertices of the Local Causality Graph are mandatory to create the association with the objective tree (thus preventing the possibility to break the cycle). In this situation, refinements can still be considered by duplicating some vertices, in order to reveal simpler cycles that can be removed from the graph. Besides, we may also assume that these latter cases would not be frequent in practice. Indeed, as we saw in example 10, a very particular combination of several automata is necessary to obtain this configuration. Although such a configuration may be theoretically possible with a larger number of automata, this requires a strong connectivity between them, complicating the reachability at the same time. Moreover, we may assume that Automata Networks from biological applications remain sparse, which can be justified by the fact that the necessary and sufficient conditions previously proposed were already successful on concrete examples [START_REF] Folschette | Sufficient conditions for reachability in automata networks with priorities[END_REF]. For these reason, we do not expect a duplication strategy to significantly increase the size of a Local Causality Graph in practice.

Conclusion

To conclude, we have presented in this work a new approach combining static analysis and Bounded Model Checking to prove unreachability in Automata Networks. We have introduced our main result which is a property on a sufficient length of solution sequences of the reachability problem. This property can be used to compute a completeness threshold in acyclic Local Causality Graphs. We have also suggested how to put this property into practice through a SAT encoding presented in appendix A. Thanks to this property and to the encoding, the bound can be used to prove unreachability. We also provide an implementation online of the bound computation from the Local Causality Graph and of the SAT encoding. This implementation has been illustrated through simple examples. Some specific cases with cyclic Local Causality Graphs have also been presented. These examples show the current limitations of our method and bring a new understanding about the reachability instances and the Local Causality Graphs in Asynchronous Automata Networks. Indeed, additionally to the elaboration of the bound, our property helps to strengthen the link between the static analysis techniques already developed and the solutions of the reachability instances, thus opening the door to various extensions. Further improvements will now require to refine the Local Causality Graph by deriving additional properties on its structure. This will imply some trade-off between the computational efficiency of LCGbased methods and the coverage of all possible instances of Automata Networks.

Competing interests: The authors declare none

A SAT encoding for Automata Networks

Bounded Model Checking can be used to verify temporal logic properties on transition systems. In Bounded Model Checking, properties are verified through the execution of the model up to some k transitions. This approach has been used successfully on large scale systems ( [START_REF] Biere | Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications[END_REF]) and has overcome the use of Binary Decision Diagrams. In this section, an encoding of the dynamics of Asynchronous Automata Networks into a propositional logic formula is presented.

The goal is to use solvers for the SAT problems, which consists in deciding if there is an assignment which makes such a logic formula satisfiable. Indeed, the growing efficiency of these solvers makes them useful to tackle all type of combinatorial problems and they have been widely used for Bounded Model Checking ( [START_REF] Balint | Overview and analysis of the SAT challenge 2012 solver competition[END_REF]).

A.1 Global states and execution sequence

To encode the execution of an Automata Network, logic variables should be defined to represent the global states. In this encoding, local states of an automaton are represented with one variable per local state. If a local state is active, the corresponding variable will be equal to true and if it is not, the variable will be equal to false.

Definition 12 Global state encoding Given an Automata Network M = (Σ, S, T ), a local state of an automaton x ∈ Σ is represented as a tuple vx = (vx 1 , vx 2 , .., vx n ) with: (vx, vy, .., vz) with one group of variables for each automaton.

vx i = ⊤ if xi is active ⊥ otherwise and verifying (vx i = ⊤) =⇒ (vx j = ⊥) ∀j ̸ = i A global state s ∈ S is represented as a tuple v =
To use Bounded Model Checking on Automata Networks, it is necessary to represent a sequence of global states of the model. To do so, the variables which represent the global states are duplicated and ordered. The sequence (s0, s1, .., sn) is then represented by the sequence of variables: (v1 = (vx,1, .., vz,1), v2 = (...), .., vn).

A.2 Transition constraints

In order to perform Bounded Model Checking with SAT, the dynamics of Asynchronous Automata Networks has to be encoded as a propositional logic formula. To do so, constraints are used to link the global states of the sequence between each other. These constraints force the logic variables to take only valid values, according to the dynamics of Automata Networks.

Every change between two global states means that one (and only one) transition has been played. Then, if an automaton is modified, the expression must verify that a transition has been played. To do so, the following verifications are necessary:

• there is a transition corresponding to the change • all the conditions of this transition are verified on the origin global state

• only one local state variable per automaton is true in the next global state

• only one automaton is modified between the two states (asynchronicity)

In this encoding, the playability of a transition is checked for every local state of every automaton. This verification is encoded through an implication: if a local state is activated, then a corresponding transition has been played (or this local state was already activated). The formulation used in this encoding is based on a weak constraint, which means that every change must be verified but the absence of change between two consecutive states of a sequence is also valid. However, it does not complicate the search of reachability sequences since a valid sequence can be obtained from the encoded sequence. -ϕ τ,k := v x i ,k ∧ ∧

y i ∈enab(τ ) v y i ,k ∧ ∧ x l ̸ =x j ¬v x l ,k+1
To ensure that there is no change in an automaton, the following expression is used:

-ψ z,k := ∧ z i ∈Sz (v z i ,k → v z i ,k+1 )
The encoding of the playability of any transition to activate xj is made by:

-

ϕ x j ,k := v x j ,k+1 → ( ∨ τ :dest(τ )=x j ϕ τ,k ) ∧ ψ x,k ∨ v x j ,k
The expression ϕ τ,k is used to check that a transition τ can be played between the two global states s k and s k+1 . The expression ψ z,k is additionally used to check that the local state of an automaton y has not changed between the global states s k and s k+1 , which is necessary for the asynchronicity. Finally, the overall constraint ϕ x j ,k check that if a local state xj is activated at step k + 1, then either a transition τ has been played (and the other automata has not changed) or this local state was already active at step k. The overall constraint between two global states combine these constraints for every local states, for every automata.

Definition 14 Constraint between s k and s k+1 Given an Automata Network M = (Σ, S, T ) and an encoding variable sequence v, the global constraint between s k and s k+1 is:

-

Φ k := ∧ x j ∈Sx,x∈Σ ϕ x j ,k
In practice, one can notice that there is a lot of duplication of the ψ z,k constraints. Indeed, with these definitions, the asynchronicity constraint of an automaton z will be duplicated in every local state of every automaton x ̸ = z. Instead, it is possible to encode this constraint in a variable and then make a reference to this variable wherever this constraint is necessary. This makes the logic expression shorter.

A.3 Reachability analysis

In order to verify the reachability we need a final constraint. If we want to check the activation of a local state xi in the last state of the sequence, we only need to check if the corresponding variable is true. This can be done by a simple conjunction on the formula: Φ ∧ vx i ,n. Thanks to this procedure, it is possible to check the reachability not only at step n of the sequence but also for the other global states. Indeed, the constraints let the formula be satisfiable even if there is no change between two consecutive global states. So, if the tested reachability has only solution sequences of size k < n, then some global states would be identical at least n -k times in the SAT solution.

In general, SAT solvers take as input a Conjunctive Normal Form expression. To transform the logic expression into this form, we proceeded as in [START_REF] Plaisted | A structure-preserving clause form translation[END_REF]. This transformation changes the size of the formula by adding variables. However, the size of the new formula remains polynomial in the size of the original one.

B Bounded Model Checking and completeness threshold

In Bounded Model Checking, properties are usually verified for fixed length execution sequences of the models. However, extensions have been introduced in order to provide completeness. These extensions are presented in [START_REF] Biere | Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications[END_REF]. Some completeness bounds can be directly derived from a Bounded Model Checking encoding. For example, the k-induction bound can be computed by adding few modifications to the encoding proposed above. In this section, we discuss about the relevance of the Local Causality Bound regarding the k-induction bound.

B.1 k-induction in Bounded Model Checking

As seen in appendix A, the encoding can be used to check properties in fixed length execution sequences of the model. By creating logic variables vi for each state i of the execution sequence and by linking them with the logic expressions ϕ k , one is able to represent the evolution of an Automata Network.

Some additional constraints can also be used to find a completeness threshold. To do so, it is possible to remove the constraint of the initial state. The resulting sequence is able to check the existence of a path from any state of the model to the state verifying the reachability. If the SAT solver returns UNSAT for this sequence, it proves that no sequence of that length, or longer, can reach the goal state. Indeed, the sequence will remain unsatisfiable after adding another state, since the new sequence contains the same clauses as the first one. In particular, a sequence starting from the initial state to the goal state cannot be satisfiable, which proves the unreachability of the initial problem. Thus, the computation of the bound can be done by increasing the length of that sequence until it is not satisfiable. Unfortunately, execution sequences can contain infinite loops. An alternative is the verification of the shortest longest sequence to the goal state. The shortest sequence means a sequence with no loops, which can be done by checking that all the states in the sequence are different. The definition 15 shows how to compute such a constraint. This constraint makes sure that at least one automaton is different between two global states.

Definition 15 State inequality (si ̸ = sj)

To check the inequality of two states, the following constraint is used:

-

ψi,j := ∨ x∈Σ ∧ x l ∈Sx (vx l ,i → ¬vx l ,j )
This additional constraint increases the length of the sequence, which complicates the search of a satisfiable assignment. Another constraint can be added to facilitate the search. Indeed, the goal state should not be activated along the sequence, since its activation is the goal of the reachability. Then, it is possible to check it all along the sequence by adding constraints like: ¬vx i ,j ∀j.

B.2 Comparison with the Local Causality Bound

The computation of the Local Causality Graph and the Local Causality Bound is essentially driven by the initial state of the reachability instance. Indeed, the first objectives added in the Local Causality Graph start from the initial state of the automaton. On the contrary, the initial state is not taken into account for the computation of the k-induction bound since the initial state constraint is removed from the sequence, which makes the solver search for every sequence that reaches the goal. By the definition of the Automata Networks, we can expect the Local Causality Bound to be shorter than the k-induction bound because the initial state is a strong constraint. If this constraint is removed, additional paths that reach the goal state may be found.

To briefly illustrate this difference, we have generated few random Automata Networks of limited size. To obtain a Local Causality Bound, reachability instances associated to acyclic Local Causality Graphs have also been computed thanks to random generations. These instances can be found in the file README.md from the implementation mentioned in section 4.1. In these examples, we can see that the k-induction bound is at least twice the length of the Local Causality Bound. The difference also seems to become bigger as the size of the Automata Network increases. However, random instances may not totally reflect the difference on actual biological models. Thus, more detailed comparisons with additional experiments are necessary.

C Proof of the Local Causality Bound

This section shows the detailed proofs of lemma 1 and lemma 2 for the Local Causality Bound. These results rely on the following property, already proved in [Paulevé, 2018]. This property states that the transitions of a minimal solution necessarily belong to any Local Causality Graph associated with the reachability instance. In other words, transitions of the Local Causality Graph are sufficient to any minimal solution. The proof of proposition 2 from [Paulevé, 2018] does not correspond completely to Asynchronous Automata Networks. Indeed, their framework considers the generalized semantics: several transitions can be played at the same time in an execution sequence of the model. Moreover, the model authorizes synchronized transitions, that make a change in more than one automaton. Thus, the definition of the Local Causality Graph is slightly different, in order to take into account local states of transitions that do not correspond to the bounds of an objective. However, the proof remains the same. It consists in showing that, from any solution sequence to a reachability instance, it is always possible to remove the transitions that do not belong to the Local Causality Graph. This can be done by identifying loops around these transitions. The proposition is used in the next proof, which contains all the sub-proofs of lemma 1.

Proof 1 Proof of Lemma 1 1. Let y ∈ Σ, i ∈ [1; |Oπ,y|].
From definition 10, the transitions of tr(Oπ,y) form a local path in y. Let assume that tr(Oπ,y) does not form a local solution, this implies from definition 5 that there exists π j , π l ∈ tr(Oπ,y), j ̸ = l, such that dest(π j ) = dest(π l ). Then by removing the loop between j and l from π, the remaining solution is still playable since ∀k ∈ [j + 1; l -1], enab(π k ) ∩ Ty = ∅. This would imply that π is not minimal, which is a contradiction.

2. From definition 10,

o∈V H tr(o) ⊂ {π i | i ∈ [1; |π|]}. Now let us show that {π i | i ∈ [1; |π|]} ⊂ o∈V H tr(o) . Let us assume that there exists i ∈ [1; |π|] with π i ∈ Ty, such that ∀k ∈ [1; |Oπ,y|], π i / ∈ tr(O k π,y
). Since π is minimal, this implies that ∃j ∈ [i + 1; |π|] such that enab(π j ) ∩ Ty ̸ = ∅ (otherwise, it would be possible to remove π i and keep a playable sequence). Let us assume that j is the smallest index greater than i such that enab(π j ) ∩ Ty ̸ = ∅. enab(π j ) ∩ Ty ̸ = ∅ implies that ∃k ∈ [1; |Iπ,y|] such that I k π,y = j. From definition 10, this implies that π i ∈ tr(O k π,y ), which is a contradiction.

D Examples with necessary and sufficient conditions D.1 Sufficient conditions

Sufficient conditions allow to prove that the reachability is possible when additional constraints are verified on the set of solutions to a reachability instance. More especially, the conditions pass if the sub-goals required to solve the instance can be reached in any order, which is ensured when all objectives have at least one local solution. When an objective does not have any local solution, the corresponding parent local state is invalidated and the information is propagated to the parents vertices. Fig. 9 shows the Local Causality graph for the instance R1 of the example 6. In this Local Causality Graph, we can see that the objective b1 ⇝ b0 does not have any local solution. This invalidates all the local states, including the goal a1. The absence of local solution for b1 ⇝ b0 means that b0 cannot be reached from b1. However, in the example 6, solving this objective is not necessary to reach a1 since c1 is reached before b1, justifying that the reachability is actually possible.

D.2 Necessary conditions

The necessary conditions aims at verifying that at least, there exists local paths in each automata allowing to reach all the sub-goals (local states in the transitions). Thus, this verification relies on a sub Local Causality Graph that contains only objectives starting from the local states of the initial state. When no local path exists for an objective, the objective is considered as unsolvable and this information can be propagated to the parents vertices in the graph. Fig. 9 shows the sub Local Causality Graph for the example 6. In this graph, it can be noticed that every objective has a solution, meaning that the necessary conditions are verified. However, no solution exists for the reachability of d1 since f0 needs to be reached from f1 after activating e1, no transition allows to perform this change. -→ e 1

a 1 a 0 ⇝ a 1 a 0 b1,c0 ---→ a 1 b 1 c 0 b 1 ⇝ b 1 b 0 ⇝ b 1 • • b 0 c1 -→ b 1 c 0 ⇝ c 0 c 1 ⇝ c 0 • • c 1 - → c 0 c 1 c 1 ⇝ c 1 c 0 ⇝ c 1 • • c 0 b0 -→ c 1 b 0 b 1 ⇝ b 0 b 0 ⇝ b 0 •
f 0 ⇝ f 0 • f 1 f 0 ⇝ f 1 • f 0 - → f 1

•

  ∀x ∈ Σ, Sx = {x0, x1, ...} is the finite set of local states of automaton x • S = x∈Σ Sx is the set of global states of M • Tx ⊂ {(xi, xj, l) | xi, xj ∈ Sx, xi ̸ = xj, l ⊂ y∈Σ\{x} Sy and |l ∩ Sy| ≤ 1 ∀y ∈ Σ \ {x}} is the finite set of transitions of automaton x ∈ Σ • T = x∈Σ Tx is the set of all transitions of the network For a global state s ∈ S, the corresponding local state of an automaton x is given by s(x). If s(x) = xi, then xi is said active for the state s and the states {xj : xj ̸ = xi} are said inactive for s. A transition τ ∈ Tx is a tuple (xi, xj, {y k , z l , ...}) with xi the origin state of the transition (denoted orig(τ )), xj the destination state of the transition (denoted dest(τ )) and a set of local states {y k , z l , ...} which are necessary to play the transition (denoted enab(τ )). The notation xi y k ,z l ,.. ----→ xj is used for the transitions. In this work, self loop transitions (i.e. transitions of the form xi → xi) are not considered. Indeed, transitions in Automata Networks aim at representing a modification in the dynamics of a biological system. Example 1 Fig. 1 shows an Automata Network with three automata. In this Automata Network, Σ = {a, b, c} and S = {(ai, bj, c k ) | i, j, k ∈ [0; 2]}. For the automaton a, Sa = {a0, a1, a2} and Ta = {a0

  b

Figure 1 :

 1 Figure 1: An Automata Network with 3 automata.

Definition 3

 3 Reachability in Asynchronous Automata Networks • Input: An Automata Network M = (Σ, S, T ), a reachability tuple R = (s0, xi) with s0 ∈ S an initial global state and xi ∈ Sx a goal local state • Output: ⊤ or ⊥

Definition 5

 5 Objective and local solution Given an Automata Network M = (Σ, S, T ): • A local reachability problem of an automaton x ∈ Σ is represented by tuple (xi, xj) ∈ Sx × Sx called objective and denoted xi ⇝ xj • A local solution to an objective xi ⇝ xj is a sequence of transitions η = (η 1 :: .

  The finite set of all local solutions associated with xi ⇝ xj is denoted as lpaths(xi ⇝ xj) • lpaths(xi ⇝ xi) = {ε} ∀xi ∈ Sx, ∀x ∈ Σ Example 4 In the Automata Network of Fig. 1, the objective c0 ⇝ c2 has two solutions. There is one solution η1 = (c0 b 2 -→ c1 :: c1 b 1 -→ c2) and a second solution η2 = (c0 b 1

Figure 2 :

 2 Figure 2: A Local Causality Graph associated with the reachability problem of Example 3. In this representation, boxed vertices correspond to local states and local transitions. Objectives are represented with the same notation introduced previously and • vertices represent local solutions (i.e. sequences of local transitions solving an objective).

Definition 7

 7 Bound function Let M = (Σ, S, T ) be an Automata Network, R = (s0, xi) a reachability problem, and G = (VG, EG) a Local Causality Graph associated with M and R. Following definition 6, VG is defined as VG = L ∪ O ∪ Q ∪ T ′ with L ⊂ y∈Σ Σy, O ⊂ y∈Σ Σy × Σy, Q = o∈O lpaths(o) and T ′ = o∈O {η i | i ∈ [1; |η|], η ∈ lpaths(o)}. The bound function associated with G is a function B : VG → N with:

Proposition 1

 1 Local Causality Bound for a reachability instance Let M = (Σ, S, T ) be an Automata Network, R = (s0, xi) a reachability instance, G = (VG, EG) a Local Causality Graph associated with M and R, and B the bound function associated with G.

  and B is the bound function previously defined.The following definition introduces sequences of ordered transition indexes from the minimal solution π, for each automaton of the model. These sequences intend to catch all transitions of a local solution having a condition on this specific automaton. The corresponding local state (from the condition) will be associated with an objective afterwards.Definition 8 Transitions conditioned on y Let π = (π 1 :: .. :: π n ) be a minimal solution for the reachability instance R = (s0, xi). ∀y ∈ Σ, Iπ,y is the sequence of ordered indexes of all transitions having a condition on y: -enab(π I j π,y ) ∩ Sy ̸ = ∅ ∀j ∈ [1; |Iπ,y|] (all referred transitions have a condition on y) -I j π,y < I j+1 π,y ∀j ∈ [1; |Iπ,y| -1] (the indexes are ordered) -enab(π k ) ∩ Sy = ∅ ∀k / ∈ Iπ,y (there is no other transition having a condition on y in the solution)

b 2 -

 2 → a1 :: b2 -→ b1 :: c0 b 1 -→ c2 :: a1 b 1 ,c 2 ---→ a2) from Example. 3. The sequences of indices for each automaton are: -Iπ 2 ,a = ε ; I π 2 ,b = (3 :: 5 :: 6) ; Iπ 2 ,c = (6) The associated sequences of objectives are: -O π 2 ,b = (b0 ⇝ b2 :: b2 ⇝ b1 :: b1 ⇝ b1) ; Oπ 2 ,c = (c0 ⇝ c2) ; Oπ 2 ,a = (a0 ⇝ a2) Their corresponding transitions are:

  tr forms a partition of π) 3. ∀y ∈ Σ, ∀i ∈ [1; |Oπ,y|], O i π,y ∈ VG (all the objectives identified belongs to the Local Causality Graph) 4. H is a tree (acyclic and connected) 5. ∀o ∈ VH, ∃η ∈ lpaths(o) such that ∀y * ⇝ yj : (o, y * ⇝ yj) ∈ EH, ∃k ∈ [1; |η|] such that (η k , yj) ∈ EG (all successors in the objective tree are (indirect) successors in the Local Causality Graph)

  that the bound function applied to xi in the Local Causality Graph is able to overestimate the length of the minimal solution π. Indeed, lemma 1.2 implies that o∈V G |tr(o)|= |π|. Also, since all objectives identified from the minimal solution belong to the Local Causality Graph, the root of H is a successor of xi in G. Thus, B(xi) ≥ B(O |Oπ,x| π,x

Figure 5 :

 5 Figure 5: An Automata Network associated with cyclic Local Causality Graphs.

Figure 6 :

 6 Figure 6: A Local Causality Graph with a cycle.

•

  Model: example 1.an • Initial state: (a0, b0, c0, d0) • Goal state: a3 • Reachability: Yes • Local Causality Bound: 29 • Sufficient length: 11 (shortest sequence) • Pint's answer: Inconclusive Example 2: • Model: example 3.an • Initial state: (a0, b0, c0) • Goal state: a2 • Reachability: No • Local Causality Bound: 8 • Pint's answer: Inconclusive In the third example, the corresponding Local Causality Graph has cycles, thus the Local Causality Bound cannot be computed. Yet, the reachability is true and a solution can be found with the SAT encoding, by manually choosing the length of the sequence encoded. Example 3: • Model: example 2.an • Initial state: (a0, b0, c0, d0, e0) • Goal state: a1 • Reachability: Yes • Local Causality Bound: Not computable (cyclic Local Causality Graph) • Sufficient length: 8 (shortest sequence) • Pint's answer: Inconclusive

Definition 13

 13 Transition constraint for local state xj Given an Automata Network M = (Σ, S, T ), an encoding variable sequence v and a transition τ = xi c -→ xj ∈ T ∈ M, the validity of the transition τ played to activate xj is encoded by the logic expression:

Proposition 2

 2 Sufficient transitions for reachability Let M = (Σ, S, T ) be an Automata Network, R = (s0, xi) a reachability instance, G = (VG, EG) a Local Causality Graph associated with M, with VG = L ∪ O ∪ Q ∪ T ′ and R and let π be a minimal solution to R. -∀k ∈ [1; |π|], π k ∈ VG, i.e. all the transitions of a minimal solution belong to the Local Causality Graph.

)

  o ∈ VH an objective of H. By using lemma 1, let ηo ∈ lpaths(o) be the local solution corresponding to tr(o). From definition 6, (o, ηo) ∈ EG and (η, η i ) ∈ EG ∀i ∈ [1; |η|]. Moreover, from definition 11, for each objective y * ⇝ yj ∈ VH such that (o, y * ⇝ yj) ∈ EH, ∃k such that π k ∈ tr(o) and yj ∈ enab(π k ). Then (η, π k ) ∈ EG which implies (π k , yj) ∈ EG.These results can be used for the proof of lemma 2. The following proof is performed by structural induction on the objective tree (lemma 1.4), i.e. we show that given o ∈ VH, if ∀o′ : o ′ ≺H o, B(o ′ ) ≥ |tr(o ′ )| + o ′′ ≺ H o ′ |tr(o ′′ )|, then B(o) ≥ |tr(o)| + o ′ ≺ H o |tr(o ′ )|. Proof 2 Proof of Lemma 2 -Let P (o) the property: B(o) ≥ |tr(o)| + o ′ ≺ H o |tr(o ′ )|, with o ∈ VH. -Base case: let o ∈ VH such that ∄(o, o ′ ) ∈ EH. From lemma 1.3, o ∈ VG.By using lemma 1.1, let ηo ∈ lpaths(o) be the local solution corresponding to tr(o). From definition 7, we have B(ηo) ≥ k∈[1;|ηo|] 1 + y j ∈enab(η k o ) B(yj) ≥ |ηo|, which implies that B(o) ≥ |ηo|. Thus, since o has no successors, P (o) holds. -Inductive case: let o ∈ VH and let assume that ∀o ′ : o ′ ≺H o, P (o ′ ) holds. Similarly to the base case, lemma 1.3 implies that o ∈ VG. Let ηo ∈ lpaths(o) be the local solution corresponding to tr(o). From definition 7, According to lemma 1.5, ∀(o, y * ⇝ yj) ∈ VH, ∃k ∈ [1; |ηo|] such that (η k o , yj) ∈ EG. This implies B(ηo) ≥ |ηo| + y j :(o,y * ⇝y j )∈E H B(yj) Moreover, from definition 7: -B(yj) ≥ B(y * ⇝ yj) ∀y * ⇝ yj ∈ VG, and -B(o) ≥ B(η) ∀η ∈ lpath(o), ∀o ∈ VG. This leads to B(o) ≥ |ηo|+ o ′ :(o,o ′ )∈E H B(o ′ ). Then P can be applied inductively to all objectives descendant of o in H. This leads to:B(o) ≥ |ηo| + o ′ :(o,o ′ )∈E H |tr(o ′ )| + o ′′ ≺ H o ′ |tr(o ′′ )| .H being a tree, we have:{o ′ | o ′ ≺H o} = o ′ :(o,o ′ )∈E G {o ′ } ∪ {o ′′ : o ′′ ≺H o ′ } , which implies B(o) ≥ |ηo| + o ′ :o ′ ≺ H o |tr(o ′ )|. Since |ηo| = |tr(o)|, this concludes that P (o) is also verified.Lemma 2 can then be used to prove proposition 1 when applied to the root of the objective tree, i.e. O |Oπ,x| π,x . Indeed, from lemma 1.2, the objectives of H are able to capture all the transitions of π through their corresponding local solutions. Moreover, since H is a tree we have {O |Oπ,x| π,x } ∪ {o ′ | o ′ ≺H O |Oπ,x| π,x } = VH. Then, applying the inductive property P to O ≥ |π|. Finally, since from definition 7, B(xi) ≥ B(x * ⇝ xi) ∀x * ⇝ xi ∈ VG, this leads to B(xi) ≥ |π|, concluding the proof of proposition 1.

Figure 8 :

 8 Figure 8: The Local Causality Graph for the verification of the sufficient conditions for the example 6.

Figure 9 :

 9 Figure 9: The Local Causality Graph made for the verification of the necessary conditions for the example 6.

  3. From proposition 2, ∀i ∈ [1; |π|], π i ∈ VG. This implies from definition 6 that ∀yj ∈ enab(π i ), yj ∈ VG. Then from definition 9, ∀y ∈ Σ, ∀k ∈ [2; |Iπ,y|], O k π,y ∈ VG. Moreover, since yj ∈ VG =⇒ s0(y) ⇝ yj ∈ VG, then O 1 π,y ∈ VG. Lastly, xi ∈ VG =⇒ O From definition 11, and since any transition of π belongs to exactly one identified objective, all objectives except O have exactly one predecessor. Thus, |EH| = |VH| -1. Let us assume that H contains a cycle, and let(O i π,x , O i ′ π,y ), (O i ′ π,y , O i ′′ π,z ) ∈ EH be two consecutive edges of the cycle, implying that O i π,x ≺H O i ′′ π,z . From definition 10, k > I i ′ π,y ∀π k ∈ tr(O i ′ π,y ). In particular, from definition 11, I i ′′ π,z > I i ′ π,y . Similarly, (O i ′ π,y , O i ′′ π,z ) ∈ EH =⇒ k > I i ′′ π,z ∀π k ∈ tr(O i ′′ π,z ). By reasoning on consecutive objectives in the cycle, it can be shown by induction thatI i ′′ π,z < k ∀π k ∈ tr(o) if o ≺H O i ′′ π,z . In particular, O i π,x ≺H O i ′′ π,z =⇒ I i ′′ π,z < I i ′ π,y . Thus, we have I i ′ π,y < I i ′′ π,z and I i ′′ π,z < I i ′ π,y, which is a contradiction. So H has no cycle, and since |EH| = |VH| -1, it is then a tree with O

	|Oπ,x| π,x	∈ VG.
	4. |Oπ,y |
	π,x

http://nusmv.fbk.eu/NuSMV/

https://lip6.github.io/ITSTools-web/index.html

The implementation can be found at https://github.com/smbct/AAN-reach

An implementation of Pint is available at https://loicpauleve.name/pint/. Pint is indeed able to provide a conclusion for unreachability without the use of a bound and it has already been compared to several Model Checking tools on biological models ([Paulevé, 2017]).