Towards Scalable Modeling of Biology in Event-B

Biology offers many examples of large-scale, complex, concurrent systems: many processes take place in parallel, compete on resources and influence each other's behavior. The scalable modeling of biological systems continues to be a very active field of research. In this paper we introduce a new approach based on Event-B, a state-based formal method with refinement as its central ingredient, allowing us to check for model consistency step-by-step in an automated way. Our approach based on functions leads to an elegant and concise modeling method. We demonstrate this approach by constructing what is, to our knowledge, the largest ever built Event-B model, describing the ErbB signaling pathway, a key evolutionary pathway with a significant role in development and in many types of cancer. The Event-B model for the ErbB pathway describes 1320 molecular reactions through 242 events.

Identifying efficient controls of complex interaction networks using genetic algorithms

Control theory has seen recently impactful applications in network science, especially in connections with applications in network medicine. A key topic of research is that of finding minimal external interventions that offer control over the dynamics of a given network, a problem known as network controllability. We propose in this article a new solution for this problem based on genetic algorithms. We tailor our solution for applications in computational drug repurposing, seeking to maximise its use of FDA-approved drug targets in a given disease-specific protein-protein interaction network. We show how our algorithm identifies a number of potentially efficient drugs for breast, ovarian, and pancreatic cancer. We demonstrate our algorithm on several benchmark networks from cancer medicine, social networks, electronic circuits, and several random networks with their edges distributed according to the Erd\H{o}s-R\'{e}nyi, the small-world, and the scale-free properties. Overall, we show that our new algorithm is more efficient in identifying relevant drug targets in a disease network, advancing the computational solutions needed for new therapeutic and drug repurposing approaches.

Matrix Insertion-Deletion Systems

In this article, we consider for the first time the operations of insertion and deletion working in a matrix controlled manner. We show that, similarly as in the case of context-free productions, the computational power is strictly increased when using a matrix control: computational completeness can be obtained by systems with insertion or deletion rules involving at most two symbols in a contextual or in a context-free manner and using only binary matrices.