BioResolve (http://www.di.unipi.it/~bruni/LTSRS/) is a Prolog interpreter for Reaction Systems that offers a flexible playground for their analysis. BioReSolve has been designed by exploiting a process algebraic version of Reaction Systems, which allowed to seamlessly enhance basic Reaction Systems with additional features, like delays, duration, monitoring, dynamic slicing and various kinds of contexts (guarded, nondeterministic and recursive). The talk will provide an overview of the many facets of BioReSolve related to the simulation, analysis and verification of Reaction Systems.

This work presents a formal methodology to analyse and refine clinical treatment guidelines for patients with multiple chronic conditions (a.k.a. multimorbidities). Reaction systems are used as the core modelling framework to capture the dynamic and context-sensitive behaviour of clinical guidelines. By extending standard reaction systems with guarded and recursive contextual processes, we capture the complex interplay of treatment choices and drug interactions. In turn, the GROOVE graph transformation analysis toolset allows us to explore the automatic detection of potentially harmful medication combinations and, more crucially, identify early-stage decisions that may lead to adverse outcomes. All in all, we argue that this combination of approaches supports the development of safer and more personalised care strategies.

We introduce a process algebraic approach to describing, simulating, and analysing DRSs. This allows designing complex models by re-using modular components in a well-structured and compositional way and analysing them with the BioReSolve modelling software. We demonstrate our approach by experimenting with distributed Lotka-Volterra models, where multiple agents evolve according to their own periodic dynamics, but can also synchronise their cycles through diverse communication topologies.

We propose a new variant of reaction systems that incorporates several quantitative aspects relevant to modelling biological reactions, features that have been largely overlooked or only briefly addressed in the literature. Our approach is designed to make reaction systems more applicable to biological models. First, we modify the threshold principle by representing the environment as a multiset in which resources are available in limited quantities. This allows us to capture competition for resources, a key feature of biochemical dynamics. Second, we revise the permanency principle: resources not involved in a reaction may persist in the next state. This reflects natural resource decay in biochemical systems, a concept that has appeared in prior work but remains underexplored in quantitative settings. Third, we introduce the principle of selective inhibition, where the effect of an inhibitor depends on both its type and the substrate it targets. This flexibility is crucial in biochemistry, where inhibitors often exhibit substrate-specific effects that influence regulatory pathways.

We propose an extension to the classical notion of reaction systems, assigning a role to the environment which goes beyond providing context to states. We envisage the possibility of equipping an environment with a valence function assigning valences to the entities in a background set. Then, a reaction immersed in such an environment can be applied only if the total valence of its reactants is greater than the total valence of its inhibitors. This notion stems from the observation that entities can appear to be inactive or with limited activity when immersed in different environmental conditions, for example under extreme temperatures, whether in the cold or in the heat, or under various levels of pollution. On the contrary, the effect of other entities can be amplified under the same or other conditions, e.g., in phase-transition situations or under intense lighting. While such conditions can be qualitatively represented by suitable entities, their being put on a par with entities representing actual resources might lead to more complicated models.

In this talk, we address the problem of model checking temporal and epistemic properties in reaction systems — a computational model inspired by the biochemistry of living cells. We introduce two dedicated temporal logics: rsCTL and rsLTL, counterparts of Computation Tree Logic (CTL) and Linear Temporal Logic (LTL), and discuss the complexity of their model checking procedures. We also present a synthesis method for rsLTL applied to partially defined reaction systems. To incorporate reasoning about knowledge and interaction, we extend the formalism toward distributed reaction systems with agency. This leads to the development of rsCTLK, an epistemic extension of rsCTL, and its corresponding model checking algorithm. We report on experimental results using a biological benchmark and demonstrate the effectiveness of our ReactICS toolkit, comparing it with the MCMAS model checker for multi-agent systems.

We will discuss four distinct Petri net encodings for basic reaction systems that operate independently of the external environment. We begin by exploring a straightforward encoding, which is based solely on the behavior of a given reaction system R, translating its transition system into a Petri net represented as a marked graph. However, this approach leads to an exponential increase in the number of places and transitions. In the following encodings, we address the issue of exponential growth, ultimately arriving at a modular solution that scales polynomially with respect to the size of the original reaction system. The main result is the theorem proving the correctness of the polynomial encoding. Furthermore, we demonstrate how this polynomial encoding can be adapted to accommodate reaction systems that interact with contexts provided by context automata.

Natural computing explores models inspired by nature’s information-processing mechanisms. In bio-molecular computation, reaction systems represent cellular behavior via interactions governed by facilitation and inhibition. We present an extension of ReactICS, a tool for model checking reaction systems, to support distributed reaction systems (DRS) with both synchronous and asynchronous multi-agent interactions. The tool provides temporal model checking methods (for logics such as CTL, LTL and their derivatives specialized for reaction systems) and implements SMT-based bounded model checking methods. Our extension uses a temporal epistemic logic (rsCTLK) and implements a symbolic model checking method using binary decision diagrams.

In contrast to Chemical Reaction Automata, there are recent developments, such as Chemical Pure Reaction Automata, where the system evolves by only considering the products of reactions, discarding any unconsumed reactants after each step. This approach also allows for the modeling of chemical systems in a maximally parallel manner, where multiple reactions can occur simultaneously. Three-way decision models, as introduced in the context of probabilistic rough sets, provide a principled approach to classification and decision-making under uncertainty. In this framework, objects or states are classified into three regions: the positive region (acceptance), the negative region (rejection), and the boundary region (abstention). While chemical reaction automata and three-way decision models are from different fields, they share a common structure of partitioning states/objects into three distinct categories. We would like to explore this structural similarity and the possibilities that ideas and techniques from one domain could potentially be adapted to another.