Statistical Model Checking in Drug Repurposing for Alzheimer’s Disease

Dementia is a disease that is characterized by the gradual loss of memory and cognition of patients due to the death of neurons. The future perspective is that the number of patients will increase, due to the aging of the population, reaching up to one third of the world population over 65 years. Alzheimer’s disease is the most common form of dementia and there is no medication to prevent or cure the disease. In this sense, the discovery of an efficient treatment for the disease is a real need, and the repositioning of drugs and in silico techniques can contribute to this purpose. Computational methods, such as Statistical Model Checking, which is a formal verification technique, contribute to this field of research, aiding to analyze the evolution of the protein and drugs interactions at a lower cost than the laboratory experiments. In this work, we present a model of the PI3K/AKT/mTOR pathway and we connected it with Tau and A\(\beta \), which are two important proteins that contribute to the evolution of Alzheimer’s disease. We analyzed the effect of rapamycin, an immunosuppressive drug, on those proteins. Our results show that this medicine has the potential to slow down one of the biological processes that causes neuronal death. In addition, we could show the formal model verification technique can be an efficient tool to design pharmacological strategies reducing experimental cost.