Reasoning About Hybrid Assumptions in Assured Temporal Missions

Authors: Juan Felipe Perdomo, Victor Braberman, Sebastián Zudaire, Sebastián Uchitel.

Abstract: Temporal mission specifications, together with efficient controller synthesis techniques, enable the vision of effective and assured adaptation of robotic behavior 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.

More information: https://dl.acm.org/doi/10.1145/3788550.3794878