Invited Lecture at ICTAC 2023

Next 7th of December, Pedro D'Argenio will give one of the invited lectures of the 20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023. The event will take place in Lima, Peru, between the 4th and 8th of December, 2023.

Title: Optimal Route Synthesis in Space DTN using Markov Decision Processes.
Abstract: Delay-tolerant networks (DTN) are time-evolving networks that do not provide continuous and instantaneous end-to-end communication. Instead, the topological configuration of DTN changes continuously: connections are available only during some time intervals and thus the network may suffer from frequent partitions and high delay. In this sense, the DTN paradigm is fundamental to understand deep-space and near-Earth communications. A particular characteristic of space networks is that, due to the orbital and periodic behavior of the different agents (e.g. satellites and terrestrial or lunar stations), contact times and durations between nodes can be accurately predicted. This type of DTNs is called scheduled and expected contacts can be imprinted in a contact plan that exhaustively describes the future network connectivity. In addition, the contacts may suffer of some quantifiable failure that can be included in the contact plan. Thus, this behavior can be encoded in a Markov decision process (MDP) where the non-determinism corresponds precisely to the routing decisions. With this model at hand, we have developed and studied several offline techniques for deriving optimal and near-optimal routing solutions that ensure maximum likelihood of end-to-end message delivery. In particular, we have devised an analytical solution that exhaustively explores the MDP very much like probabilistic model checking does, and have also explored simulation-based techniques using lightweight scheduler sampling (LSS). The objective of this presentation is to report this research as well as current ongoing developments for multi-objective routing optimization on space DTN.

The research presented here have been the result of the cooperation with Juan Fraire, Arnd Hartmanns, Fernando Raverta, Ramiro Demasi, Jorge Finochietto, and Pablo Madoery.

In addition, he will also lecture at the ICTAC 2023 Training School on Applied Formal Methods on the 4th of December, giving the following 3 hours mini-course:

Title: Probabilistic Model Checking.
Abstract: Model checking is a powerful tool to verify automatically if a model satisfies a given property. They normally provide a Boolean answer to a qualitative question. However, probabilistic features normally appear in systems of usually crucial characteristics. For example, it is common to use randomized protocols to solve contention situations in networks or to understand fault models through the stochastic behaviors of faults. In this last case, for instance, the statement "the system does not fail" might be impossible to verify while rather the appropriate question could be "99% of the time the system does not fail". In this tutorial, we will introduce the fundamentals and algorithms to address the verification of this type of quantitative properties. In particular, we will discuss the verification of quantitative and qualitative properties on discrete-time Markov chains as well as on the more versatile setting of Markov decision process.