Reaction Mining for Reaction Systems

Abstract Reaction systems are a formal model for computational processing in which reactions operate on sets of entities (molecules) providing a framework for dealing with qualitative aspects of biochemical systems. This paper is concerned withr eaction systems in which entities can have discrete concentrations, and so reactions operate on multisets rather than sets of entities. The resulting framework allows one to deal with quantitative aspects of reaction systems, and a bespoke linear-time temporal logic allows one to express and verify a wide range of key behavioural system properties. In practical applications, a reaction system with discrete concentrations may only be partially specified, and the possibility of an effective automated calculation of the missing details provides an attractive design approach. With this idea in mind, the current paper discusses parametric reaction systems with parameters representing unknown parts of hypothetical reactions. The main result is a method aimed at replacing the parameters in such a way that the resulting reaction system operating in a specified external environment satisfies a given temporal logic formula. This paper provides an encoding of parametric reaction systems in SMT, and outlines a synthesis procedure based on bounded model checking for solving the synthesis problem. It also reports on the initial experimental results demonstrating the feasibility of the novel synthesis method.