Reaction systems in Stark

Reaction systems (RS) are a model of computation that was inspired by biochemical reactions in living cells. RS are open dynamical systems: while the computation of the next state is deterministic, the conditions triggering the computation depend on the behaviour of an external (uncontrollable) environment. Moreover, although RS have been introduced as a qualitative modelling framework, recent algebraic formalisation have made it possible to extend their expressiveness with quantitative information, like duration of reactions and linear dependencies between the quantities of entities. However, no formal framework for the analysis of such quantitative information is available in the literature. The Stark tool has been introduced to model and analyse the behaviour of dynamical systems interacting with an unpredictable environment. Thanks to its simplicity and versatility, Stark has been successfully applied in a variety of studies, including establishing safety guarantees for autonomous driving systems, ensuring the effectiveness of digital twins, and verifying robustness properties of biochemical systems. In this paper we show how we can implement (quantitative) RS in Stark and exploit the tool to automate their analysis. We apply our approach to three case studies: lac operon expression and synaptic transmission between two and three neurons.