Sampling Distributed Schedulers for Resilient Space Communication

Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)
2 Downloads (Pure)


We consider routing in delay-tolerant networks like satellite constellations with known but intermittent contacts, random message loss, and resource-constrained nodes. Using a Markov decision process model, we seek a forwarding strategy that maximises the probability of delivering a message given a bound on the network-wide number of message copies. Standard probabilistic model checking would compute strategies that use global information, which are not implementable since nodes can only act on local data. In this paper, we propose notions of distributed schedulers and good-for-distributed-scheduling models to formally describe an implementable and practically desirable class of strategies. The schedulers consist of one sub-scheduler per node whose input is limited to local information; good models additionally render the ordering of independent steps irrelevant. We adapt the lightweight scheduler sampling technique in statistical model checking to work for distributed schedulers and evaluate the approach, implemented in the Modest Toolset, on a realistic satellite constellation and contact plan.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings
EditorsRitchie Lee, Susmit Jha, Anastasia Mavridou
Number of pages20
ISBN (Electronic)978-3-030-55754-6
ISBN (Print)978-3-030-55753-9
Publication statusPublished - 10 Aug 2020
Event12th NASA Formal Methods Symposium, NFM 2020 - Virtual Conference
Duration: 11 May 202015 May 2020
Conference number: 12

Publication series

NameLecture Notes in Computer Science


Conference12th NASA Formal Methods Symposium, NFM 2020
Abbreviated titleNFM 2020
Internet address


  • 22/2 OA procedure


Dive into the research topics of 'Sampling Distributed Schedulers for Resilient Space Communication'. Together they form a unique fingerprint.

Cite this