ccReact: a rewriting framework for the formal analysis of reaction systems

Reaction Systems (RSs) are a computational framework inspired by biochemical systems, where entities produced by reactions can enable or inhibit other reactions. RSs interact with the environment through a sequence of sets of entities called the context. In this work, we introduce ccReact, a novel interaction language for implementing and verifying RSs. ccReact extends the classical RS model by allowing the specification of recursive, nondeterministic, and conditional context sequences, thus enhancing the interactive capabilities of the models. We provide a rewriting logic (RL) semantics for ccReact, making it executable in the Maude system. We prove that our RL embedding is sound and complete, thereby offering a robust tool for analyzing RSs. Our methods enable various formal analysis techniques for RSs, including simulation of RSs interacting with ccReact processes, verification of reachability properties, model checking of temporal (LTL and CTL) formulas, and exploring the system evolution through a graphical tool to better understand its behavior. We apply our methods to analyze RSs from different domains, including computer science and biological systems. Notably, we examine a complex breast cancer case study, demonstrating that our analysis can suggest improvements to the administration of monoclonal antibody therapeutic treatments in certain scenarios.