TITLE: Synthesis of Resilient Control Strategies Using Formal Methods
ABSTRACT: The increased adoption and deployment of cyber-physical systems in critical infrastructure in recent years have led to important questions about their functioning. Thus, automated tools are necessary to alleviate the need for manual design and proof of correct behavior of these systems. Signal Temporal Logic (STL) have been recently used to express system behavior under complex temporal requirements. We introduce novel quantitative semantics for STL in order to highlight the frequency of satisfaction of the temporal specifications, and use these semantics to formally verify whether the system execution meets the desired requirements. We next present computational frameworks to synthesize control strategies for discrete-time and continuous-time systems with imposed temporal constraints. Different optimization frameworks are developed to optimize control strategies such that the system execution satisfies a desired temporal specification. Simulation results in biological networks, robot path planning and multi-agent systems control demonstrate the efficacy of the proposed approaches.
Calin Belta, SE/ME; Sean Andersson, SE/ME; Melissa Kemp, BME, Georgia Tech;
Roberto Tron, SE/ME