Automated generation of dynamics-based runtime certificates for high-level control

摘要: This paper addresses the problem of synthesizing controllers for reactive missions carried out by dynamical systems operating in environments known physical geometry but consisting uncontrolled elements that system must react to at execution time. Such problems have value semi-structured industrial automation settings, especially those which robots behave collaboratively yet safely with their human counterparts. The proposed synthesis framework cases where there exists no satisfying controller mission, given and environment's assumed behaviors. We introduce an approach leverages information about abstraction automatically generate a concise set revisions such specifications. provide graphical visualization tool as design aid, allowing be conveyed user interactively added specification user's discretion. Any accepted statements become certificates that, if satisfied runtime, guarantees current mission on dynamics. Our is cast into general works various discrete representations (i.e. abstractions) present case studies illustrate application our two example robotic employing different abstractions system.