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.
Watson-Crick automata are two-head machines working on a Watson-Crick tape, i.e., the inputs are double-stranded DNA molecules. In 5 '-> 3 ' Watson-Crick automata, the heads start from the two extremes of the input and the process is finished when they meet. In the new model we present in this paper, one of the heads is blind, i.e., it cannot read but it can only count the symbols it advances through in a computation step. We prove that the model is able to accept a language class which is a proper superset of the class of regular languages and, at the same time, is a proper subset of the class of linear context-free languages. Hierarchy of restricted variants is also shown.
The reversibility criterion for one-dimensional radius-1 first-degree cellular automata under null boundary conditions has a useful ring-theoretic interpretation. The nonlinear coefficients allowed by the criterion lie in the nilradical, and therefore disappear after passage to the reduced quotient. Consequently, the reduced dynamics is not an unrestricted nonlinear system: on every residue-field factor it is an affine triangular map whose diagonal entry is the unit coefficient c_5 . We use this observation to clarify the scope of the nonlinear freedom, to formulate a sufficient reversible-by-construction extension to arbitrary finite commutative rings, and to give explicit Chinese remainder theorem and nilpotent-lifting inversion procedures. Finally, we distinguish the number of nilpotent refinement rounds from the spatial range of the inverse. In particular, a finite null-boundary inverse may depend on an entire interval, so the nilpotency index does not provide a uniform inverse-radius bound.
Yield optimisation of a molecular species in a chemical reaction network is of interest in chemistry and biochemistry, especially in the study of metabolic networks. Chemical reaction networks find a natural computational analogue in Petri nets, with places modeling molecular species and transitions modeling the transformation of educts into products. Although molecules are discrete entities, the yield of a molecule from given sources can be semantically-equivalently abstracted by continuous Petri nets (CPNs). Additionally, CPNs benefit from lower computational complexity, reachability being polynomial. We implement the polynomial-time continuous Petri net coverability procedure of Fraca and Haddad and combine it with binary search to approximate the supremal yield of a designated product to a prescribed precision. As a contrasting formal strategy, we also encode the same objective in a mixed-integer linear framework, which trades provable complexity for broader expressiveness. We compare these two formulations on both synthetic examples and chemically inspired networks, alongside a case-study of the non-oxidative part of the pentose-phosphate pathway, highlighting chemically relevant results.
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.
