Hybrid seminar at McGill University or Zoom.

Formal analysis of dynamical systems is crucial for improving safety and reducing costs. This talk presents two recent contributions addressing both theoretical and applied aspects of this goal. In the first part, I will introduce a theory-oriented result: a regret-free reinforcement learning framework for infinite-horizon temporal logic specifications. We consider systems modeled as finite-state Markov decision processes (MDPs) with unknown dynamics. Our main contribution is a regret-free algorithm for infinite-horizon reach-avoid problems. For general Linear Temporal Logic (LTL) specifications, we reduce the synthesis problem to a reach-avoid formulation once the underlying graph structure is known. Finally, we provide a separate algorithm to learn this graph structure, assuming a known lower bound on transition probabilities.

In the second part, I turn to an application-oriented topic: the formal analysis of metastability in large-scale server systems. These systems serve as the backbone of modern cloud computing infrastructure. We develop a formal characterization of metastability using a domain-specific modeling language, compiled into continuous-time Markov chains (CTMCs) that approximate program semantics via modeling and data-driven calibration. These CTMCs enable both qualitative and quantitative analysis of global system behavior. Our techniques are implemented in a tool for modeling and analyzing server systems. Using models inspired by real-world failures, we demonstrate the tool’s effectiveness in predicting metastability phenomena observed in practice.

Bio: Mahmoud Salamati is a postdoctoral associate at the Max Planck Institute for Software Systems (MPI-SWS). He received his PhD from MPI-SWS and his MSc from the University of Tehran. His research interests include formal methods in control, verification of probabilistic systems, decidability in dynamical systems, and energy systems. His current work focuses on metastability in server systems and the development of regret-optimal learning algorithms for various classes of dynamical systems. He has published in top-tier conferences and journals spanning control, machine learning, and theoretical computer science, and received the best paper award at QEST'18.