Parametric, Probabilistic, Timed Resource Discovery System

TL;DR

This paper introduces a distributed resource discovery and reservation system modeled with probabilistic timed automata, highlighting the challenges in parameter synthesis for such complex models.

Contribution

It presents a semi-formal, probabilistic, timed model of a distributed resource system, addressing the complexity of parameter synthesis.

Findings

Model is timed, parametric, and probabilistic.

Highlights challenges in parameter synthesis.

Provides a foundation for verifying distributed resource systems.

Abstract

This paper presents a fully distributed resource discovery and reservation system. Verification of such a system is important to ensure the execution of distributed applications on a set of resources in appropriate conditions. A semi-formal model for his system is presented using probabilistic timed automata. This model is timed, parametric and probabilistic, making it a challenge to the parameter synthesis community.