Verification of Reaction Systems Processes

Reaction Systems (RSs) are a computational framework inspired by biological systems. A RS is formed by a set of entities together with a set of reactions over them. Entities can enable or inhibit each reaction and are produced by reactions. The interaction of a RS with the environment can be modelled by means of an external context sequence. RSs can model several computer science frameworks as well as biological systems. However, the basic computational mechanism of RSs abstracts from several features of biochemical systems which reduces somewhat their expressivity. In some previous works, we have defined semantics of RSs based on process algebras and SOS rules. This allowed us to introduce a flexible framework for extending the basic features of RSs. We implemented our framework in Prolog, as our declarative interpreter makes easier the modifications necessary to accommodate new extensions. In this paper, we give an overview of the basic framework and some extensions and of a methodology for verifying properties of (extended) RSs, and we briefly present our implementation. We discuss the open problems of verification of RSs and the corresponding challenges, with the final aim to realize an expressive integrated framework easily accessible to computer scientists and biologists.