Reasoning about hidden hybrid assumptions in assured temporal missions
File(s)
Accepted version
Author(s)
Perdomo, Juan
Braberman, Victor
Uchitel, Sebastian
Zudaire, Sebastian
Type
Conference Paper
Abstract
Temporal mission specifications, together with efficient controller synthesis techniques, enable the vision of effective and assured adaptation of robotic behaviour to new missions. However, the assurances provided by controller synthesis can be misleading. Temporal mission specifications adopt a discrete view of the world —through propositional variables or discrete events— while the synthesised controllers ultimately rely on lower-level robotic implementation layers, including control feedback loops and hardware, that interact with continuous physical phenomena.
In this paper, we present a specification framework that allows capturing explicitly the hybrid assumptions linking discrete and continuous domains. We also formalize a soundness relation between discrete mission goals, hybrid assumptions, and continuous mission goals which provides a rigorous foundation for end-to-end reasoning about missions. Making hybrid assumption explicit supports pre-deployment validation and runtime monitoring but also mitigation of and recovery from hybrid assumption violations. We apply this specification framework to four case studies from the literature making explicit hidden hybrid assumptions to achieve mission soundness, discuss their validity, and the related adaptation strategies that they can inspire.
In this paper, we present a specification framework that allows capturing explicitly the hybrid assumptions linking discrete and continuous domains. We also formalize a soundness relation between discrete mission goals, hybrid assumptions, and continuous mission goals which provides a rigorous foundation for end-to-end reasoning about missions. Making hybrid assumption explicit supports pre-deployment validation and runtime monitoring but also mitigation of and recovery from hybrid assumption violations. We apply this specification framework to four case studies from the literature making explicit hidden hybrid assumptions to achieve mission soundness, discuss their validity, and the related adaptation strategies that they can inspire.
Date Acceptance
2026-01-13
Publisher
ACM
Copyright Statement
Subject to copyright. This paper is embargoed until publication. Once published the Version of Record (VoR) will be available on immediate open access.
Source
21st International Conference on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2026)
Publication Status
Accepted
Start Date
2026-04-13
Finish Date
2026-04-14
Coverage Spatial
Rio de Janeiro, Brazil