Goal-Oriented Reduction of Automata Networks

Abstract

We consider networks of finite-state machines having local transitions conditioned by the current state of other automata. In this paper, we introduce a reduction procedure tailored for reachability properties of the form “from global state ${s}$, there exists a sequence of transitions leading to a state where an automaton g is in a local state $\top$”. By analysing the causality of transitions within the individual automata, the reduction identifies local transitions which can be removed while preserving all the minimal traces satisfying the reachability property. The complexity of the procedure is polynomial with the total number of local transitions, and exponential with the maximal number of local states within an automaton. Applied to Boolean and multi-valued networks modelling dynamics of biological systems, the reduction can shrink down significantly the reachable state space, enhancing the tractability of the model-checking of large networks.

Appendices

A Proof of Minimal Traces Preservation

We assume a global AN $(\varSigma ,S,T)$ where $g\in \varSigma$, $g_\top \in S(g)$, and ${s}\in S$ with ${s}(g)\ne g_\top$.

From Property 1 and Definition 7, any trace reaching first $a_i$ and then $a_j$ uses all the transitions of at least one local path in ${\text {local-paths}}_{{s}}({{a}_{i}}\!\leadsto \!{{a}_{j}})$.

We first prove with Lemma 2 that the last transition of a minimal trace $\pi$ for $g_\top$ reachability, of the form $\pi ^{|\pi |}=\{{g}_{i} \rightarrow {g}_{\top }\}$, is necessarily in ${\text {tr}}(\mathcal B)$. Indeed, by definition of $\mathcal B$, ${{g}_{0}}\!\leadsto \!{{g}_{\top }}\in \mathcal B$; and by Lemma 1, ${g}_{i} \rightarrow {g}_{\top }\notin {\text {local-paths}}_{{s}}({{g}_{0}}\!\leadsto \!{{g}_{\top }})$ implies that reaching $g_i$ requires to reach $g_\top$ beforehand.

Lemma 1

Given ${a}_{j} \rightarrow {a}_{i}\in T$, if ${a}_{j} \rightarrow {a}_{i} \notin {\text {tr}}({\text {local-paths}}_{{s}}({{a}_{0}}\!\leadsto \!{{a}_{i}}))$, then for any trace $\pi$ from ${s}$ with $a_j\in \pi ^v {}^\bullet$ and $a_i\in \pi ^w {}^\bullet$ for some $v,w\in [1;|\pi |]$, there exists $u<v$ with $a_i\in \pi ^u {}^\bullet$.

Proof

Let $\eta \in {\text {local-paths}}_{{s}}({{a}_{0}}\!\leadsto \!{{a}_{j}})$ be an acyclic local path such that $\forall n\in [1;|\eta |]$, $a_i\ne {\text {dest}}(\eta ^n)$. The sequence $\eta \!::\!{a}_{j} \rightarrow {a}_{i}$ is then acyclic and, by definition, belongs to ${\text {local-paths}}_{{s}}({{a}_{0}}\!\leadsto \!{{a}_{i}})$, which is a contradiction.    $\square$

Lemma 2

If $\pi$ is a minimal trace for $g_\top$ reachability from state ${s}$, then, necessarily, $\pi ^{|\pi |}\subseteq {\text {tr}}(\mathcal B)$.

Proof

As $\pi$ is minimal for $g_\top$ reachability, without loss of generality, we can assume that $\pi ^{|\pi |} = \{{g}_{i} \rightarrow {g}_{\top }\}$. By definition, ${\text {tr}}({\text {local-paths}}_{{s}}({{g}_{0}}\!\leadsto \!{{g}_{\top }}))\subseteq {\text {tr}}(\mathcal B)$. By Lemma 1, if ${g}_{i} \rightarrow {g}_{\top }\notin {\text {tr}}({\text {local-paths}}_{{s}}({{g}_{0}}\!\leadsto \!{{g}_{\top }}))$, then there exists $u < |\pi |$ such that $g_\top \in \pi ^u {}^\bullet$; hence, $\pi$ would be non minimal.    $\square$

The rest of the proof of Theorem 1 is derived by contradiction: if a transition of $\pi$ is not in ${\text {tr}}(\mathcal B)$, we can build a sub-trace of $\pi$ which preserves $g_\top$ reachability, therefore $\pi$ is not minimal.

Given a transition ${a}_{i} \rightarrow {a}_{j}$ in the q-th step of $\pi$ that is not in ${\text {tr}}(\mathcal B)$, removing ${a}_{i} \rightarrow {a}_{j}$ from $\pi ^q$ would imply to remove any further transition that depend causally on it. Two cases arise from this fact: either all further transitions that depend on $a_j$ must be removed; or ${a}_{i} \rightarrow {a}_{j}$ is part of loop within automaton a, and it is sufficient to remove the loop from $\pi$.

Lemma 3 ensures that if ${{a}_{z}}\!\leadsto \!{{a}_{k}}$ is in $\mathcal B$ and if $a_z$ occurs before the q-th step and $a_k$ after the q-th step of $\pi$, then ${a}_{i} \rightarrow {a}_{j}\notin {\text {tr}}({\text {local-paths}}_{{s}}({{a}_{z}}\!\leadsto \!{{a}_{k}}))$ only if ${a}_{i} \rightarrow {a}_{j}$ is part of a loop, i.e., there are two steps surrounding q where the automaton a is in the same state before their application.

Lemma 3

Given $a\in \varSigma$ and $u,q,v\in [1;|\pi |]$, $u\le q< v$, with $a_z \in {}^\bullet \pi ^u$, $a_k \in {}^\bullet \pi ^v \cup \pi ^v {}^\bullet$, and ${a}_{i} \rightarrow {a}_{j}\in \pi ^q\setminus {\text {tr}}(\mathcal B)$, if ${{a}_{z}}\!\leadsto \!{{a}_{k}}\in \mathcal B$ then $\exists m,n\in [u;v]$, $m\le q\le n$ such that $(\pi ^{1..m-1}) {}^\bullet \cap S(a) = (\pi ^{1..n}) {}^\bullet \cap S(a)$; and $a_k\in {}^\bullet \pi ^v \Rightarrow n <v$.

Proof

If ${a}_{i} \rightarrow {a}_{j}\notin {\text {tr}}(\mathcal B)$ and ${{a}_{z}}\!\leadsto \!{{a}_{k}}\in {\text {tr}}(\mathcal B)$, necessarily ${a}_{i} \rightarrow {a}_{j}\notin {\text {tr}}({\text {local-paths}}_{{s}}({{a}_{z}}\!\leadsto \!{{a}_{k}}))$. Therefore ${a}_{i} \rightarrow {a}_{j}$ belongs to a loop of a local path from $a_z$ (at index u in $\pi$) to $a_k$ (at index v in $\pi$). Hence, $\exists m,n\in [u;v]$ with $m \le q \le n$ and $a_h,a_x,a_y\in S(a)$ such that ${a}_{h} \rightarrow {a}_{x}\in \pi ^m$ and ${a}_{y} \rightarrow {a}_{h}\in \pi ^n$; therefore $(\pi ^{1..m-1}) {}^\bullet \cap S(a) = (\pi ^{1..n}) {}^\bullet \cap S(a) = a_h$. In the case where $a_k\in {}^\bullet \pi ^v$, $a_k\ne a_h$, hence $n < v$.    $\square$

Intuitively, Lemma 3 imposes that $\pi$ has the following form:

given that ${{a}_{z}}\!\leadsto \!{{a}_{k}}\in \mathcal B$.

The idea is then to remove the transitions forming the loop within automaton a. However, transitions in other automata may depend causally on the transitions that compose the local loop in automaton a within steps m and n, following the notations in Lemma 3.

Lemma 4 establishes that we can always find m and n such that none of the transitions within these steps with an enabling condition depending on automaton a are in ${\text {tr}}(\mathcal B)$. Indeed, if a transition in ${\text {tr}}(\mathcal B)$ depends on a local state of a, let us call it $a_p$, the objectives ${{a}_{0}}\!\leadsto \!{{a}_{p}}$ and ${{a}_{p}}\!\leadsto \!{{a}_{k}}$ are in $\mathcal B$, due to the second and third condition in Definition 8. Lemma 3 can then be applied on the subpart of $\pi$ that contains the transition ${a}_{i} \rightarrow {a}_{j}$ not in ${\text {tr}}(\mathcal B)$ and that concretizes either ${{a}_{0}}\!\leadsto \!{{a}_{p}}$ or ${{a}_{p}}\!\leadsto \!{{a}_{k}}$ to identify a smaller loop containing ${a}_{i} \rightarrow {a}_{j}$.

Lemma 4

Let us assume $a\in \varSigma$ and $q\in [1;|\pi |]$ with ${a}_{i} \rightarrow {a}_{j}\in \pi ^q\setminus {\text {tr}}(\mathcal B)$. There exists $m,n\in [1;|\pi |]$ with $m\le q\le n$ such that $\forall t\in {\text {tr}}(\pi ^{m+1..n})$, ${\text {enab}}(t)\cap S(a)\ne \emptyset \Rightarrow t\notin {\text {tr}}(\mathcal B)$, and, if $a=g$ or $\exists t\in {\text {tr}}(\pi ^{n+1..|\pi |})\cap {\text {tr}}(\mathcal B)$ with ${\text {enab}}(t)\cap S(a)\ne \emptyset$, then $(\pi ^{1..m-1}) {}^\bullet \cap S(a) = (\pi ^{1..n}) {}^\bullet \cap S(a)$.

Proof

First, let us assume that $a\ne g$ and for any $t\in \pi ^{q+1..|\pi |}$, ${\text {enab}}(t)\cap S(a)\ne \emptyset \Rightarrow t\notin {\text {tr}}(\mathcal B)$: the lemma is verified with $m=q$ and $n=|\pi |$.

Then, let us assume there exists $v\in [q+1;|\pi |]$ such that $\exists t\in {\text {tr}}(\pi ^v)\cap {\text {tr}}(\mathcal B)$ with $a_k\in {\text {enab}}(t)$. By Definition 8, this implies ${{a}_{0}}\!\leadsto \!{{a}_{k}}\in \mathcal B$. By Lemma 3, there exists $m,n\in [1;v-1]$ with $m\le q\le n$ such that $(\pi ^{1..m-1}) {}^\bullet \cap S(a) = (\pi ^{1..n}) {}^\bullet \cap S(a)$.

Otherwise, $a=g$, and by Lemma 3 with $a_k=g_\top$, there exists $m,n\in [1;|\pi |]$ with $m\le q\le n$ and $m\ne n$ such that $(\pi ^{1..m-1}) {}^\bullet \cap S(a) = (\pi ^{1..n}) {}^\bullet \cap S(a)$. Remark that it is necessary that $n < |\pi |$: if $n=|\pi |$, $g_\top \in (\pi ^{1..m-1}) {}^\bullet$, so $\pi$ would be not minimal.

In both cases, if there exists $r\in [m+1;n]$ such that $\exists a_p\in S(a)$ and $\exists t\in \pi ^r$ with $a_p\in {\text {enab}}(t)$, then $t\in {\text {tr}}(\mathcal B)$ implies that ${{a}_{0}}\!\leadsto \!{{a}_{p}}\in \mathcal B$ and ${{a}_{p}}\!\leadsto \!{{a}_{k}}\in \mathcal B$ (Definition 8). If $r > q$, by Lemma 3 with $a_k=a_p$ and $v=r$, there exists $m',n'\in [m+1;n]$ such that $m' \le q \le n' < r\le n$ with $(\pi ^{1..m'-1}) {}^\bullet \cap S(a) = (\pi ^{1..n'}) {}^\bullet \cap S(a)$. If $r \le q$, by Lemma 3 with $a_0=a_p$ and $u=r$, there exists $m',n'\in [m+1;n]$ such that $r \le m' \le q \le n'$ with $(\pi ^{1..m'-1}) {}^\bullet \cap S(a) = (\pi ^{1..n'}) {}^\bullet \cap S(a)$. Therefore, by induction with Lemma 3, there exists $m,n\in [1;|\pi |]$ such that $\forall t\in {\text {tr}}(\pi ^{m+1..n})$, ${\text {enab}}(t)\cap S(a)\ne \emptyset \Rightarrow t\notin {\text {tr}}(\mathcal B)$.    $\square$

Using Lemma 4, we show how we can identify a subset of transitions in $\pi$ that can be removed to obtain a sub-trace for $g_\top$ reachability. In the following, we refer to the couple (m, n) of Lemma 4 with ${\text {cb}}(\pi ,a,q)$ (Definition 9).

Definition 9

( ${\text {cb}}(\pi ,a,q)$ ). Given $a\in \varSigma$, $q\in [1;|\pi |]$ with $t\in \pi ^q\setminus {\text {tr}}(\mathcal B)$ and $\varSigma (t)=a$, we define ${\text {cb}}(\pi ,a,q) = (m,n)$ where $m,n\in [1;|\pi |]$ such that:

• $\forall t\in {\text {tr}}(\pi ^{m+1..n})$, ${\text {enab}}(t)\cap S(a)\ne \emptyset \Rightarrow t\notin {\text {tr}}(\mathcal B)$;

• $a=g\vee \exists t\in {\text {tr}}(\pi ^{n+1..|\pi |})\cap {\text {tr}}(\mathcal B)$ with ${\text {enab}}(t)\cap S(a)\ne \emptyset$ $\Longrightarrow$ $(\pi ^{1..m-1}) {}^\bullet \cap S(a) = (\pi ^{1..n}) {}^\bullet \cap S(a)$. Moreover, if $a=g$, then $n<|\pi |$.

We use Lemma 4 to collect the portions of $\pi$ to redact according to each automaton. We start from the last transition in $\pi$ that is not in ${\text {tr}}(\mathcal B)$: if ${\text {tr}}(\pi )\not \subseteq {\text {tr}}(\mathcal B)$, there exists $l \in [1;|\pi |]$ such that $\pi ^l\not \subseteq {\text {tr}}(\mathcal B)$ and $\forall n>l, \pi ^n\subseteq {\text {tr}}(\mathcal B)$. By Lemma 2, we know that $l < |\pi |$. Let us denote by ${b}_{i} \rightarrow {b}_{j}$ one of the transitions in $\pi ^l$ which is not in ${\text {tr}}(\mathcal B)$.

We define $\varPsi \subseteq \varSigma \times [1;|\pi |]\times [1;|\pi |]$ the smallest set which satisfies:

• $(b,m,n) \in \varPsi$ if ${\text {cb}}(\pi ,l,b) = (m,n)$

• $\forall (a,m,n)\in \varPsi$, $\forall q\in [m+1;n]$, $\forall t\in \pi ^q$, ${\text {enab}}(t)\cap S(a)\ne \emptyset \Longrightarrow (\varSigma (t),m',n') \in \varPsi$ where ${\text {cb}}(\pi ,q,\varSigma (t)) = (m',n')$.

Finally, let us define the sequence of steps $\varpi$ as the sequence of steps $\pi$ where the transitions delimited by $\varPsi$ are removed: for each $(a,m,n)\in \varPsi$, all the transitions of automaton a occurring between $\pi ^m$ and $\pi ^n$ are removed. Formally, $|\varpi |=|\pi |$ and for all $q\in [1;|\pi |]$, $\varpi ^q \mathop {=}\limits ^{\varDelta }\{ t \in \pi ^q\mid \not \exists (a,m,n)\in \varPsi : a=\varSigma (t) \wedge m\le q\le n \}$.

From Lemma 4 and $\varPsi$ definition, $\varpi$ is a valid trace. Moreover, by Lemma 4, there is no $q\in [1;|\pi |]$ such that $(g,q,|\pi |)\in \varPsi$, hence $g_\top \in \varpi {}^\bullet$. Therefore, $\pi$ is not minimal, which contradicts our hypothesis. $\square$

Example 2

Let us consider the reachability of $c_2$ in the AN of Fig. 1 from state $\langle {A_0,b_0,c_0,d_0}\rangle$. The transitions ${\text {tr}}(\mathcal B)$ preserved by the reduction for that goal are listed in Fig. 2.

Let $\pi$ be the following trace in the AN of Fig. 1:

The latest transition not in ${\text {tr}}(\mathcal B)$ is ${b}_{1} \xrightarrow {\{a_0\}} {b}_{0}$ at step 4. One can compute ${\text {cb}}(\pi ,4,b)=(2,4)$, and as there is no transition involving b between steps 3 and 4, $\varPsi = \{(b,2,4)\}$; therefore, the sequence

$$\begin{aligned} \varpi =\{ {a}_{0} \xrightarrow {\{b_0\}} {a}_{1}\}\!::\!\{ {c}_{0} \xrightarrow {\{a_1\}} {c}_{1}\}\!::\!\{ {a}_{1} \xrightarrow {\emptyset } {a}_{0}\}\!::\!\{\}\!::\!\{ {c}_{1} \xrightarrow {\{b_0\}} {c}_{2}\} \end{aligned}$$

is a valid sub-trace of $\pi$ reaching $c_2$, proving $\pi$ non-minimality.

In conclusion, if $\pi$ is a minimal trace for $g_\top$ reachability from state ${s}$, then, ${\text {tr}}(\pi )\subseteq {\text {tr}}(\mathcal B)$.

B Experiments with Partial Reduction

The goal-oriented reduction relies on two intertwined analyses of the local causality in ANs: (1) the computation of potentially involved objectives (Sect. 3.2) and (2) the filtering of objective that can be proven impossible (Sect. 3.1). The second part can be considered optional: one could simply define the predicate ${\mathbf {valid}}_{{s}}$ to be always true. In order to appreciate the effect of this second part, we show here the intermediary results of model reduction without the filtering of impossible objectives. It is shown in table below, in the lines in italic. As we can see, for some models it has no effect on the reduction, for some others the filtering parts is necessary to obtained important reduction of the state space (e.g., MAPK, TCell-r (94), TCell-d).

Model	# tr	# states	|unf|
EGF-r (20)	68	4,200	1,749
	43	722	336
	43	722	336
Wnt (32)	197	7,260,160	KO
	134	241,060	217,850
	117	241,060	217,850
TCell-r (40)	90	$\approx 1.2\cdot 10^{11}$	KO
	46	25,092	14,071
	46	25,092	14,071
MAPK (53) profile 1	173	$\approx 3.8\cdot 10^{12}$	KO
	147	$\approx 9\cdot 10^{10}$	KO
	113	$\mathbf {\approx 4.5\cdot 10^{10}}$	KO
MAPK (53) profile 2	173	8,126,465	KO
	148	1,523,713	KO
	69	269,825	155,327
VPC (88)	332	KO	KO
	278	$\approx 2.9\cdot 10^{12}$	185,006
	219	$\mathbf {1.8\cdot 10^9}$	43,302
TCell-r (94)	217	KO	KO
	112	KO	KO
	42	54.921	1,017
TCell-d (101) profile 1	384	$\approx 2.7\cdot 10^8$	257
	275	$\approx 1.1\cdot 10^8$	159
	0	1	1
TCell-d (101) profile 2	384	KO	KO
	253	$\approx 2.4\cdot 10^{12}$	KO
	161	75,947,684	KO
EGF-r (104) profile 1	378	9,437,184	47,425
	120	12,288	1,711
	0	1	1
EGF-r (104) profile 2	378	$\approx 2.7 \cdot 10^{16}$	KO
	124	$\approx 2\cdot 10^9$	KO
	69	62,914,560	KO
RBE2F (370)	742	KO	KO
	56	2,350,494	28,856
	56	2,350,494	28,856