Article: DeCastro, J; Ehlers, R; Rungger, M; Dagger, A; Kress-Gazit, H; “Automated Generation of Dynamics-Based Runtime Certificates for High-Level Control”, Discrete Event Dynamic Systems-Theory and Applications, 27 (2):371-405
Abstract: This paper addresses the problem of synthesizing controllers for reactive missions carried out by dynamical systems operating in environments of known physical geometry but consisting of uncontrolled elements that the system must react to at execution time. Such problems have value in semi-structured industrial automation settings, especially those in which robots must behave collaboratively yet safely with their human counterparts. The proposed synthesis framework addresses cases where there exists no satisfying controller for the mission, given the dynamical system and the environment’s assumed behaviors. We introduce an approach that leverages information about an abstraction of the dynamical system to automatically generate a concise set of revisions to such specifications. We provide a graphical visualization tool as a design aid, allowing the revisions to be conveyed to the user interactively and added to the specification at the user’s discretion.
Any accepted statements become certificates that, if satisfied at runtime, provide guarantees for the current mission on the given dynamics. Our approach is cast into a general framework that works with various discrete representations (i.e. abstractions) of the system dynamics. We present case studies that illustrate application of our approach to controller synthesis for two example robotic missions employing different abstractions of the system.
Funding Acknowledgement: NSF Expeditions in Computing project ExCAPE: Expeditions in Computer Augmented Program Engineering [CCF-1138996]
Funding Text: This work was supported by the NSF Expeditions in Computing project ExCAPE: Expeditions in Computer Augmented Program Engineering [grant number CCF-1138996]