Multiple Sclerosis is an inflammatory demyelinating disorder of the Central Nervous System. It is an autoimmune disease that its causes are still not clarified. The demyelization of the neural axons leads to the physical and cognitive disability of the patient. It is important to model the pathophysiology of Multiple Sclerosis in order to obtain an insight of the problem. Formal methods help in this direction by providing concepts and disciplines that are applicable to biological systems, too. Such formal methods are Process Algebra, Petri Nets, Automata and Binary Decision Diagrams. In our case study we chose to use Stochastic Petri Nets, considering it to be a consistent, robust and dynamic formalism that can cope with the complexity and diversity of this disease. Taking as aetiology the recruitment of lymphocytes at inflammatory brain vessels, we modelled the procedure based on data on mice affected by experimental autoimmune encephalomyelitis. The latter is the analogous of Multiple Sclerosis in human beings. We estimated the probability of adhesion and the number of bound molecules as measures to evaluate the acuteness of Multiple Sclerosis. The results were pretty high and actually should be as we are talking about mice suffering from this disease. The use of interferon beta (IFN-β-1b), a medication that reduces the concentration of chemokine, showed some significant reduction in the probability of adhesion and in the number of bound molecules. We ran the simulation for 3-month, 6-month and 12-month therapy. A reduction in adhesion probability of 2.9% is observed by the 12-month therapy compared to the baseline execution. This is quite optimistic for patients suffering from Multiple Sclerosis. Interferon beta is the predominant medication provided to the Multiple Sclerosis patients. Stochastic Petri Nets formalism is quite easy to learn and use and it is recommended to biologists to use it for their biological simulations. Along with the use of Mobius tool, Stochastic Petri Nets can give powerful perspective to researchers that are interested in nondeterministic phenomena. Biological Systems are such phenomena and should be treated so.

Thesis (Master) -- University of Cyprus, Faculty of Pure and Applied Sciences, Department of Computer Science, 2011.