Process Calculi and Rewriting Techniques for Analyzing Reaction Systems

Reaction Systems (RSs) are a successful computational framework inspired by biological systems, where entities are produced by reactions and can be used to enable or inhibit other reactions. In RSs interaction with the environment is modeled by a linear sequence of sets of entities called context. In this paper, we present a new interaction language, called ccReact  for implementing and specifying RSs. ccReact extends the classic RS computational model by allowing the specification of possibly recursive, nondeterministic conditional context sequences, enhancing the interactive capabilities of the models. We provide a rewriting logic semantics for ccReact, making it executable in the Maude system. This enables the simulation and the verification of (reachability) properties, and model checking temporal (LTL and CTL) formulas for our extended RSs. We analyze a breast cancer case study and show that our model checking analyses can in some cases improve the administration of monoclonal antibodies therapeutic treatments.