A framework for monitored dynamic slicing of reaction systems

Reaction Systems (RSs) (Ehrenfeucht and Rozenberg 2007b; Brijder et al. 2011a) are a computational framework inspired by systems of living cells. Their constituents are a finite set of entities and a finite set of reactions. Each reaction is a triple that consists of: a set of entities whose presence is needed to enable the reaction, called reactants; a set of entities whose absence is needed to enable the reaction, called inhibitors; and a set of entities that are produced when the reaction takes place, called products. RSs have shown to be a general computational model whose application ranges from the modelling of biological phenomena (Azimi et al. 2014; Corolli et al. 2012; Azimi 2017; Barbuti et al. 2016) to molecular chemistry (Okubo and Yokomori 2016). The classical semantics of RSs is defined as a reduction system whose states are sets of entities (those produced at the previous step, possibly joined with others provided by an external context, thus modelling the interaction with the environment). Notably, as reactions exploit facilitation and inhibition mechanisms, the behaviour of RSs is generally non-monotonic, i.e., a computational effect, like the production of a given entity, is not necessarily preserved when more entities are present in the source state.

The theory of Reaction Systems (RSs) was born in the field of Natural Computing to model the qualitative behaviour of biochemical reactions in living cells. We briefly account here for the main concepts as introduced in the classical set theoretic presentation of RSs (Brijder et al. 2011a). In the following, we use the term entities to denote generic molecular substances (e.g., atoms, ions, molecules) that may be present in the states of a biochemical system.

Let S be a (finite) set of entities; we call a state any subset \(W\subseteq S\). A reaction in S is a triple \(r = (R,I,P)\), where \(R, I, P\subseteq S\) are finite, non empty sets and \(R \cap I = \emptyset \). The sets R, I, P are the sets of reactants, inhibitors, and products, respectively. We let \( rac (S)\) denote the set of all reactions over S.

Given a state \(W\subseteq S\), the result of a reaction \(r = (R,I,P)\in rac (S)\) on W, denoted by \( res _r(W)\), is defined as follows, where \( en _r(W)\) is called the enabling predicate of r:From the above definition it follows that all reactants have to be present in the current state for the reaction to take place, while the presence of any of the inhibitors would block the reaction. Products are the outcome of the reaction, to be released in the next state.

A Reaction System is a pair \(\mathcal{A} = (S, A)\) where S is the set of entities, and \(A \subseteq rac (S)\) is a finite set of reactions over S. Given \(W\subseteq S\), the result of the reactions A on W, denoted \( res _A(W)\), is just the lifting of \( res _r\), i.e., \( res _A(W) \triangleq \cup _{r \in A} res _r(W)\).

Since living cells are seen as open systems that react to environmental stimuli, the behaviour of a RS is formalised in terms of an interactive process. Let \(\mathcal{A} = (S, A)\) be a RS and let \(n \ge 0\). An \((n+1)\)-steps interactive process in \(\mathcal{A}\) is a pair \(\pi = (\gamma , \delta )\) s.t. \( \gamma =\{C_i\}_{i\in [0,n]}\) is the context sequence and \(\delta =\{D_i\}_{i\in [0,n]} \) is the result sequence, where \( C_{i}, D_{i} \subseteq S\) for any \(i\in [0,n]\), \(D_0 = \emptyset \), and \(D_{i+1} = res _{A}(D_{i} \cup C_{i})\) for any \(i \in [0,n-1]\). The context sequence \(\gamma \) represents the environment, while the result sequence \(\delta \) is entirely determined by \(\gamma \) and the set of reactions A. We call \(\tau = W_{0}, \ldots , W_{n}\) the state sequence, with \(W_{i} \triangleq C_{i} \cup D_{i}\) for any \(i \in [0, n]\). Note that each state \(W_{i}\) in \(\tau \) is the union of the context \(C_{i}\) at step i and the result set \(D_i= res _{A}(W_{i-1})\) from step \(i-1\). Note also that the result of a computation step does not depend on the order of application of the reactions.

In order to define our automatic slicing technique, we find it convenient to exploit the algebraic syntax for RSs introduced in Brodo et al. (2021a). Inspired by process algebras such as CCS (Milner 1980), simple SOS inference rules define the behaviour of each operator. This induces a LTS semantics for RSs, where states are terms of the algebra, each transition corresponds to a step of the RS and transition labels retain some information on the entities involved at each step. Transition labels and SOS rules will allow us to pair RSs with monitors and to easily enrich state information with histories, respectively.

While in principle reactions, entities and contexts could be seen as components to be handled separately (and in the implementation is more convenient to do so), we mix them together to provide a compositional account of their interactions. A RS process \(\textsf{P}\) embeds a mixture process \(\textsf{M}\) obtained as the parallel composition of some reactions (R, I, P), some set of current entities D (possibly the empty set), and some context processes \(\textsf{K}\). We write \(\prod _{i\in I} \textsf{M}_i\) for the parallel composition of all \(\textsf{M}_i\) with \(i\in I\).

A context process \(\textsf{K}\) is a possibly non-deterministic and recursive system: the nil context \(\textbf{0}\) stops the computation; the prefixed context \(C.\textsf{K}\) makes the entities C available to the reactions at the current step, and then leaves \(\textsf{K}\) be the context offered at the next step; the non-deterministic choice \(\textsf{K}_1+\textsf{K}_2\) allows the context to behave as either \(\textsf{K}_1\) or \(\textsf{K}_2\); X is a process variable, and \(\textsf{rec}~X.~\textsf{K}\) is the usual recursive operator of process algebras. Choice and recursion can combine in-breadth (different evolutions) and in-depth (evolutions of different length, possibly infinite) analysis. The ability to compose contexts in parallel is useful, e.g., to handle different entities with different strategies or to reduce combinatorial explosion at the specification level. For example, letting \(\textsf{K}^?_{\textsf{a}} \triangleq \textsf{rec}~X.~\textsf{a}.X + \emptyset .X\) be the context that can recursively offer \(\textsf{a}\) or not at any step, the process \(\textsf{K}^?_{\textsf{a}} | \textsf{K}^?_{\textsf{b}} | \textsf{K}^?_{\textsf{c}}\) can recursively offer any combination of entities \(\textsf{a}\), \(\textsf{b}\) and \(\textsf{c}\).

We say that \(\textsf{P}\) and \(\textsf{P}'\) are structurally equivalent, written \(\textsf{P} \equiv \textsf{P}'\), when they denote the same term up to the laws of commutative monoids (unit, associativity and commutativity) for parallel composition \(\cdot | \cdot \), with \(\emptyset \) as the unit, and the laws of idempotent and commutative monoids for choice \(\cdot +\cdot \), with \(\textbf{0}\) as the unit. We also assume \(D_1 | D_2 \equiv D_1\cup D_2\) for any \(D_1,D_2\subseteq S\).

A transition label \(\ell \) is a tuple \(\langle (D,C)\vartriangleright R,I,P\rangle \) with \(D,C,R,I,P\subseteq S\). The sets D, C record the entities available in the current state of the system, where C is provided by the context and D is the result from the previous step; the set R records entities whose presence is assumed (either acting as reactants or as inhibitors); the set I records entities whose absence is assumed (either acting as inhibitors or as missing reactants); and the set P records the products of enabled reactions.

The operational semantics of RS processes is defined by the SOS rules in Fig. 1.

The process \(\textbf{0}\) has no transition. The rule \((\textit{Ent})\) makes available the entities in the (possibly empty) set D, then reduces to \(\emptyset \). The rule \((\textit{Cxt})\) says that a prefixed context process \(C.\textsf{K}\) makes available the entities in the set C and then reduces to \(\textsf{K}\). The rule \((\textit{Rec})\) is the classical rule for recursion. The rules \((\textit{Suml})\) and \((\textit{Sumr})\) select a move of either the left or the right component, resp., discarding the other process. The rule \((\textit{Pro})\) executes the reaction (R, I, P) (its reactants, inhibitors, and products are recorded in the label), which remains available at the next step together with newly produced entities P. The rule \((\textit{Inh})\) applies when the reaction (R, I, P) should not be executed; its label records the causes for which the reaction is disabled: possibly some inhibiting entities \((J \subseteq I)\) are present or some reactants \((Q \subseteq R)\) are missing, with \(J \cup Q \ne \emptyset \), as at least one cause is needed. The rule \((\textit{Par})\) puts two processes in parallel by pooling their labels and joining all the set components of the labels. The sanity check \(\ell _1\frown \ell _2\) is required to guarantee that reactants and inhibitors are consistent (see definition below, where we let \(W_i \triangleq D_i \cup C_i\) for brevity):In the conclusion of rule \((\textit{Par})\) we write \(\ell _1\cup \ell _2\) for the component-wise union of labels (see definition below, where the notation \(X_{1,2} \triangleq X_1 \cup X_2\) is used):Finally, the rule \((\textit{Sys})\) requires that all the processes of the systems have been considered, and also checks that all the needed reactants are actually available in the system (\(R \subseteq D \cup C\)). In fact this constraint can only be met on top of all processes. The check that inhibitors are absent (\(I\cap (D \cup C) = \emptyset \)) is embedded in rule \((\textit{Par})\). In the following we assume transitions \(\textsf{P}\xrightarrow {\langle (D,C)\vartriangleright R,I,P\rangle } \textsf{P}'\) guarantee that any instance of the rule \((\textit{Inh})\) is applied in a way that maximises the sets J and Q (see Brodo et al. 2021a).

The following theorem from Brodo et al. (2021a) shows how the set-theoretic dynamics of a RS matches the SOS semantics of its RS process.

Dynamic slicing is a technique that helps to debug a program by simplifying a partial execution trace, thus depurating it from parts which are irrelevant to finding the bug. It can also help to highlight parts of the program which have been wrongly ignored by the execution.

In this section we show how to check a biological model by our slicing methodology. The implementation is available on-line,⁶ with a small manual to use it. It extends the tool BioReSolve,⁷ which already provided a friendly environment for simulation, analysis and verification of RSs. The tool has been developed and tested under SWI-Prolog and exploits a few library predicates for efficiency reasons. DCG Grammar rules are used to ease the writing of RS specifications. Its features include the possibility to simulate single traces or generate the whole graph of the LTS (where user defined predicates can be used to color each node depending on its content so to improve readability), to verify modal logic formulas, to check bisimulation based equivalences between different RSs, to deal with quantitative aspects of RSs, such as delays and duration for produced entities and linear handling of concentration levels (see Brodo et al. 2021a, c for more details).

The interpreter will show the corresponding trace \(\frac{D_0}{C_0}\xrightarrow {N_1} \cdots \xrightarrow {N_m}\frac{D_m}{C_m}\), emphasizing the elements \(D_i, C_i, N_i\). Then the users have to provide the entities that they wantsto mark in \(D_m\). Finally, the interpreter will compute the corresponding sliced computation and present it. Let us see one example for illustrating our tool.

In this section we try to further automate the slicing process whenever the user can describe a property to be checked along a computation: the computation is stopped as soon as the current state S does not satisfy the property. Then slicing starts from S, which is automatically marked.

To specify properties we reuse the simple assertion language introduced in Brodo et al. (2021a), which is tailored on the labels of the LTS generated by SOS semantics in Sect. 3. Then, we rely on a fragment of the recursive extension of the Hennessy-Milner Logic, called sHML (Aceto et al. 2021a), to formally express properties to be verified along a RS process execution. We exploit the monitor technique from Aceto et al. (2020) to check if the current state of the RS process execution respects or not the required property. To this aim, we apply the translation from sHML formula to monitors given in Aceto et al. (2021a). Some modifications are required as in the original proposal sHML logic works on action names, whereas we work with logic assertions.

Reaction Systems have been designed as a qualitative model. In fact, their theory is based on assumptions such as no permanency, i.e., any entity vanishes unless it is sustained by a reaction in the same way as a living cell would die for lack of energy, without chemical reactions; no counting, i.e., the quantity of entities that are present in a cell is not taken into account; and threshold nature of resources, i.e., we assume that either an entity is available for all reactions, or it is not available at all.

More recently, different versions of RSs were also studied in several papers (Ehrenfeucht and Rozenberg 2007a; Brijder et al. 2011b; Meski et al. 2016; Ehrenfeucht et al. 2017; Bottoni et al. 2019, 2020; Koutny et al. 2021) to account for certain aspects of biological system in a more accurate way and increase their predictive power about natural phenomena. In particular, the work in Brodo et al. (2021c, 2023b) show that the process algebraic approach described in Sect. 3 allows to enhance RS models with several quantitative features in a modular way.

In this section we show that the basic slicing algorithm can be rather naturally extended to deal with quantitative extensions of RSs, like those including delays and linear processes. The extension is rather direct in the case of delays. Linear processes require some more elaborate changes due to the peculiarity of this type of RSs.

Dynamic program slicing has been applied to several programming paradigms, for instance to imperative programming (Korel and Laski 1988), functional programming (Ochoa et al. 2008), Term Rewriting (Alpuente et al. 2011), functional logic programming (Alpuente et al. 2014, 2016), and Constraint Concurrent Programming (Falaschi et al. 2020). RSs use term rewriting and sets manipulation for its basic computation mechanism. Thus, Alpuente et al. (2011, 2016) have a similarity with our work in the adoption of a backward style of computation of the slicer and Alpuente et al. (2016) uses assertions to stop the computation and to start the slicing process. However our framework and the one in Alpuente et al. (2011, 2016) are quite different: the former is oriented towards functional computations, while the latter considers the Maude language. In the language that they consider there are neither inhibitors, which introduce a kind of non-monotonic behaviour in the rewriting rule, nor a notion of interactive context. We tried to apply the framework in Alpuente et al. (2011, 2016) on some examples, but we were losing too much information, and the resulting simplified computations were not informative. We have instead defined a framework which is totally specialised and suitable for RSs, we use different logics specific for RSs and we are the first to consider monitors for checking the verification process in a slicer. The automatization of the slicing has been inspired by the recent work by Aceto et al. (2020, 2021a, b), here extended to exploit assertions over labels and the explicit marking of entities that are primary responsible for the fault detection. Azimi et al. (2016) defines a framework for model checking RSs. There is some similarity with our system, in the sense that both frameworks use a logic for checking properties of the underlying model. However our system considers set oriented properties specific for RSs, and analyzes one computation per execution, while the specifications considered in model checking can be more general. Slicing does not consider the full set of possible states in all possible execution traces as model checking do. The strategy is different. Model checking aims to prove if a property holds considering all possible computation states, and it provides a counterexample if it does not. Slicing returns a simplified trace for one specific computation which will help the users in their analyses. In Brodo et al. (2019, 2021b) we derived a similar LTS to the one in this paper by encoding RSs into cCNA, a multi-party process algebra (a variant of the link-calculus defined in Bodei et al. 2019; Brodo and Olarte 2017). In comparison with the encoding of RS in cCNA, here the SOS semantics is extended to traces and tailored for RSs, without relying on an ad hoc translation.

Our implementation introduces several novel features not covered in the literature and has been designed as a tool for verification, for slicing, as well as for rapid prototyping extensions of RSs, not just for their simulations. For ordinary interactive RSs there are already some performant simulators, such as brsim, written in Haskell (Azimi et al. 2015) or such as HERESY which is a GPU-based simulator of RSs, written using CUDA (Nobile et al. 2017). Using Prolog has had the advantage of a more flexible, safe and rapid prototyping.

Ehrenfeucht and Rozenberg (2007a) define the notion of event for “extended reaction systems" (which are not standard RSs), which roughly consists of considering a computation \(W_0, \ldots , W_n\) in RS taking a subsequence of states generated by the RS, starting from a set \(U \subseteq W_i\), with \(0 \le i < n\). The sets which are in the event sequence are called modules. Ehrenfeucht and Rozenberg (2007a) consider that two different events can merge, when one event generates one module of state \(W_k\) which is a subset of the corresponding module in the other event. The notion of event can remind our notion of sliced sequence. However there are many differences. An event corresponds to a forward computation, while we compute a slice backwards. We focus on a set of marked entities, a notion which is not considered in Ehrenfeucht and Rozenberg (2007a). Thus, we look for “a minimal module" which includes the entities of our interest and try to determine the sliced subsequence which is responsible for their introduction. On the other hand, the notion of event and of module do not make a clear separation of the role of the context for deriving the marked entities, which is essential for our framework.

The quantitative enhancements or RSs based on delays and linear processes were first studied in Brodo et al. (2021c, 2023b). Some previous work Ehrenfeucht and Rozenberg (2009) introduced a notion of time in RSs with the purpose of computing the time distance between two different states in a single state sequence. Thus, the authors define, when it exists, a positive and strictly increasing time function, called universal time function, for a RS that assigns a value to each state and it determines how many time units elapse between two consecutive states in an interactive process for that RS. In our approach, the passing time between two consecutive states is alway a time unit. We define a duration for each reactant as a value indicating how many time units it will be active, and a delay value n is associated to each reaction whose effect is to make available the produced reagents only after n time units. We believe that the concept of delay as we defined in Brodo et al. (2021c, 2023b) is novel in the literature on RSs.

The work in Brijder et al. (2011b) introduces a time duration for each entity that indicates how many steps the entity lasts, instead of decaying in the next step time; the authors point out that this mechanism can also be formalised as an interacting context. The entity duration function is then applied to define entity concentrations and to formalise some theoretical results. Later on, Salomaa (2017) introduced a time duration definition for each entity similar to the one in Brijder et al. (2011b). The duration function is then exploited to state a theoretical result. As in Brijder et al. (2011b), Salomaa (2017), we specify a time duration for each entity by assigning a value indicating how many time steps it will be active. As a difference to Brijder et al. (2011b), Salomaa (2017) we define a delay value n associated with each reaction whose effect is to make available the produced reagents only after n time steps. Thus, we make explicit the time duration of each entity and the time delay each reaction takes to be completed. We also remark that in Brijder et al. (2011b), Salomaa (2017) the duration is fixed for each entity, while in our work we can define a different duration for each reaction, leading to different durations depending on the enabled reactions. We believe that our framework for slicing is a good basis to be extended also to the works in Brijder et al. (2011b), Salomaa (2017), even if they mainly seem devoted to the development of theoretical results. In Meski et al. (2016) the authors introduce an extension of RSs by considering discrete concentrations and introducing some quantitative modelling. There, ‘bags’ are used to count the number of each entity which are necessary to enable a reaction. However as a difference to our system they do not consider a concept of multiplicity like us. Thus, whenever they apply a reaction, the number of produced entities is the one indicated explicitly by the bags of the products of the reaction. Similarly to us Meski et al. (2016) takes the maximum number of entities produced by the reactions, and the maximum considering also the contribution of the context. We believe that our slicing algorithm for linear processes might be easily instantiated to the case of the system in Meski et al. (2016).

We have presented the first framework for dynamic slicing of RSs. We have defined a slicing algorithm which has been applied first to standard RSs: both closed systems or interactive (context depending) ones can be dealt with. Then we have shown that the slicer can be applied also to several quantitative extensions of RSs by defining some natural modifications of the basic algorithm. This way we have been able to define a slicer for analysing RSs which consider notions of reaction speed and delays in the activation of the entities, as well as for treating discrete concentration levels in reactions (Brodo et al. 2021c, 2023b).

The main advantage of the slicer is the possibility to automatically extract a simplified computation, with the minimal amount of information that is relevant to explain the production of marked entities. Monitors help to identify states which violate a property and to automate marking of such states, using a flexible language to specify assertions over computations. We have implemented the slicer (Algorithm 1) for RSs, including the monitors, in our working environment called BioResolve¹¹, in Prolog, and have applied our tool to some bioinformatic examples. We are currently working to expand our implementation to the quantitative extensions (Algorithms 3 and 4).

As future work, we plan to add forward slicing to our interpreter, and explore the advantages of combining the information that we can derive by proceeding in the two directions (backward and forward), making the analysis more precise. We also want to extend our slicing algorithm to keep trace of inhibitors, which are essential for the computation. This would provide the user with a fully detailed information about the entities which are involved in the computation of the marked elements.