Dirk Walther

Primary progressive multiple sclerosis (PPMS) shows a highly variable disease progression with poor prognosis and a characteristic accumulation of disabilities in patients. These hallmarks of PPMS make it difficult to diagnose and currently impossible to efficiently treat. This study aimed to identify plasma metabolite profiles that allow diagnosis of PPMS and its differentiation from the relapsing-remitting subtype (RRMS), primary neurodegenerative disease (Parkinson’s disease, PD), and healthy controls (HCs) and that significantly change during the disease course and could serve as surrogate markers of multiple sclerosis (MS)-associated neurodegeneration over time. We applied untargeted high-resolution metabolomics to plasma samples to identify PPMS-specific signatures, validated our findings in independent sex- and age-matched PPMS and HC cohorts and built discriminatory models by partial least square discriminant analysis (PLS-DA). This signature was compared to sex- and age-matched RRMS patients, to patients with PD and HC. Finally, we investigated these metabolites in a longitudinal cohort of PPMS patients over a 24-month period. PLS-DA yielded predictive models for classification along with a set of 20 PPMS-specific informative metabolite markers. These metabolites suggest disease-specific alterations in glycerophospholipid and linoleic acid pathways. Notably, the glycerophospholipid LysoPC(20:0) significantly decreased during the observation period. These findings show potential for diagnosis and disease course monitoring, and might serve as biomarkers to assess treatment efficacy in future clinical trials for neuroprotective MS therapies.

We study the logic of strategic ability of coalitions of agents with bounded memory by introducing Alternating-time Temporal Logic with Bounded Memory (ATLBM), a variant of Alternating-time Temporal Logic (ATL). ATLBM accounts for two main consequences of the assumption that agents have bounded memory. First, an agent can only remember a strategy that specifies actions in a bounded number of different circumstances. While the ATL-formula means that coalition C has a joint strategy which will make φ true forever, the ATLBM-formula means that C has a joint strategy which for each agent in C specifies what to do in no more than n different circumstances and which will make φ true forever. Second, an agent has bounded recall—a strategy can only take the last m states of the system into account. We use the logic to study the interaction between strategic ability, bounded number of decisions, bounded recall and incomplete information. We discuss the logical properties and expressiveness of ATLBM, and its relationship to ATL. We show that ATLBM can express properties of strategic ability under bounded memory which cannot be expressed in ATL.

Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, as long-known, reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context of description logics, and prove that satisfiability is decidable and EXPTIME-complete using an approach based on Büchi tree automata.