Reasoning About Hidden Hybrid Assumptions in Assured Temporal MissionsFull Paper
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 im- plementation 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 be- tween 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 sup- ports 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.