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.
Ballis, D., Brodo, L., Falaschi, M., Olarte, C. (2024). Process Calculi and Rewriting Techniques for Analyzing Reaction Systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp.1-18). Cham : Springer [10.1007/978-3-031-71671-3_1].
Process Calculi and Rewriting Techniques for Analyzing Reaction Systems
Falaschi M.;
2024-01-01
Abstract
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11365/1275915