Remyelination is a regenerative process that aims to repair damaged regions of the central nervous system, caused by demyelinating diseases, like multiple sclerosis. This process fails to completely repair the demyelinated lesions in many cases and the causes of the failures are not clear. Since many factors and complex mechanisms regulate the process, it is helpful to use high-level modelling languages to describe it and model checking techniques to perform the analysis. They allow us to describe and simulate this stochastic process, and to analyse its behaviour in different scenarios. This study will support neurologists to reason about the different factors that influence this complex process and to create new hypotheses to test through lab experiments. In this chapter, we introduce a novel process algebra called MELA that we used for modelling the remyelination process. We present a number of MELA models capturing different hypotheses about the functioning of remyelination, and their comparison. We perform the analysis of the spatio-temporal evolution of remyelination using Signal Spatio-Temporal Logic and Statistical Model Checking.
|Title of host publication||Automated Reasoning for Systems Biology and Medicine|
|Editors||Pietro Liò, Paolo Zuliani|
|Number of pages||28|
|Publication status||E-pub ahead of print - 12 Jun 2019|