PSMaude is a probabilistic extension of Maude that provides an expressive probabilistic strategy language to quantify the nondeterminism in probabilistic rewrite theories, allowing the user to specify different probabilistic strategies on top of a base model. In this paper we use PSMaude to define a formal, executable real-time model of the aggregation and interneuronal propagation of the alpha-synuclein (alpha-syn) protein causing Parkinson's disease (PD). To the best of our knowledge, this is the first effort to formally model the spatial, multicellular aspect of alpha-syn accumulation in detail, i.e., the propagation of the pathogenic aggregates through a neural network that is dynamically changing as a consequence of aggregation-induced neuronal death. We then define different probabilistic strategies on top of our model to formalize the aggregation and propagation of alpha-syn in three different scenarios: (i) in a healthy individual, (ii) in a predisposed individual with either the sporadic or the familial form of PD, and (iii) in a predisposed individual that is given some treatment with rapamycin. The strategies are time-dependent, since the brain becomes more predisposed to PD with aging. We then use PSMaude to simulate our model in these different scenarios.