Formal Synthesis of Uncertainty Reduction Controllers

TL;DR

This work targets uncertainty management in self-adaptive systems by introducing Parley, a two-tier control paradigm that separates uncertainty-reduction decisions (URC) from standard adaptation (UAC). It delivers a formal synthesis workflow that augments DTMC models into pDTMCs and uses probabilistic model checking, aided by EvoChecker, to generate Pareto-optimal URC policies with guarantees on reliability and performance. The approach is instantiated in a running mobile-robot navigation example and validated in mobile robotics and server infrastructure scenarios, showing improved effectiveness and significantly richer policy diversity compared with a baseline. While scalability remains a challenge due to exponential growth in state and policy spaces, Parley demonstrates practical applicability through automated tooling and real-world-like experiments, suggesting substantial impact for robust, cost-aware adaptive systems.

Abstract

In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our paper proposes a more nuanced, adaptive approach to SAS uncertainty reduction. To that end, we introduce a SAS architecture comprising an uncertainty reduction controller that drives the adaptive acquisition of new information within the SAS adaptation loop, and a tool-supported method that uses probabilistic model checking to synthesise such controllers. The controllers generated by our method deliver optimal trade-offs between SAS uncertainty reduction benefits and new information acquisition costs. We illustrate the use and evaluate the effectiveness of our approach for mobile robot navigation and server infrastructure management SAS.

Figures (5)

• Figure 1: Parley self-adaptive system architecture: an uncertainty reduction controller drives the adaptive reduction of epistemic uncertainty through the invocation of uncertainty reduction "services" provided by the managed system, its environment, or a combination thereof.
• Figure 2: A sample map for our running example. The robot starts in the lower left corner and its mission is to traverse to the destination in the upper right corner without crashing into static obstacles. Red arrows denote move commands.
• Figure 3: Policy selection for the robotic example.
• Figure 4: Gain in (a) Hypervolume and (b) Spread of Parley compared to baseline across different maps in requirement setting $min\_success \geq 70\%$ and $max\_cost \leq 80$.
• Figure 5: Pareto-fronts for different applications.