Efficient Control Synthesis and Learning in Distributed Cyber-Physical Systems
Abstract:
Scientific challenges: How can multiple cooperative cyber-physical systems communicate and coordinate to accomplish complex high-level tasks within unknown, dynamic and adversarial environments?
Overview: This collaborative project between the University of Delaware (UD) and Boston University (BU) aims at developing a framework unifying temporal logic planning and adaptive reactive synthesis for cyber-physical systems that operate in dynamic and unknown environments. Concrete hybrid dynamical systems admit discrete abstractions that can be identified and analyzed using tools from automata theory, formal language theory, grammatical inference, and model checking. The PIs envision multiple systems learning the dynamics of an unknown environment collectively, and then refine their plans based on models for the environmental dynamics that are inferred during execution.
Results: In this fiscal period we developed a framework that integrates symbolic control synthesis, game theory and grammatical inference to perform adaptive control synthesis for systems operating in unknown, dynamic, and potentially adversarial environments. We show how action model learning and grammatical inference can be jointly utilized for identifying the interactions between a system and its environment. Grammatical inference then operates in parallel, identifying a formal language which describes the environment. This framework accommodates multiple learning paradigms for constructing provably-correct, adaptive control policies in real-time, either using game-theoretic synthesis methods or model-checking tools.
For synthesis, we developed sampling-based temporal logic planning algorithms that combine long- term temporal logic goals with short-term reactive requirements. The mission specification has two parts: (1) a global specification given as a Linear Temporal Logic (LTL) formula over a set of static service requests that occur at the regions of a known environment, and (2) a local specification that requires servicing a set of dynamic requests that can be sensed locally during the execution. The algorithm has three desirable properties. First, it is incremental, in the sense that the procedure for finding a satisfying path at each iteration scales only with the number of new samples generated at that iteration. Second, the underlying graph is sparse, which guarantees the low complexity of the overall method. Third, it is probabilistically complete. We also provide a conditional result showing that the incremental checking procedure has the best possible complexity bound. These synthesis methods can be combined with machine learning methods to identify the dynamics of uncertain aspects of the systems environment. To this end, we are currently working on extending the system-environment interaction to cases where the system consists of multiple agents. In particular, we study systems where the agents are autonomous, interacting concurrently, and trying to achieve individual tasks expressed as LTL formulae. The agents are not necessarily cooperative—their goals and preferences may or may not be perfectly aligned or opposing. We show how to reason about agent behaviors in such systems with concurrent, multi-agent games with infinitely many stages. To enable coordination, we develop negotiation protocols which ensure that under proper designs of preferences and tasks, the mutually accepted plan is a Pareto optimal Nash equilibrium. Integrating this result with the aforementioned synthesis methods and machine learning methods promises to provide a concrete and formal methodology for constructing provably-correct, adaptive heterogeneous cyberphysical systems which can enhance the effectiveness of coordination in emergency response situations.
Broader impacts: This research activity is multidisciplinary, combining expertise from robotics, lin- guistics, cognitive science, and computer science, and in this capacity exposes researchers of different fields to entirely new ideas and ways of thinking. Exploiting a common theoretical foundation provided by formal language theory, we establish new and reinforce existing intellectual links between disparate scientific communities, and educate a new generation of scholars versed in topics of arts, sciences, and engineering. Our own graduate students receive significant interdisciplinary training, and have developed a range of analytical techniques that cross traditional academic boundaries.
Submitted by Herbert Tanner
on
Abstract:
Scientific challenges: How can multiple cooperative cyber-physical systems communicate and coordinate to accomplish complex high-level tasks within unknown, dynamic and adversarial environments?
Overview: This collaborative project between the University of Delaware (UD) and Boston University (BU) aims at developing a framework unifying temporal logic planning and adaptive reactive synthesis for cyber-physical systems that operate in dynamic and unknown environments. Concrete hybrid dynamical systems admit discrete abstractions that can be identified and analyzed using tools from automata theory, formal language theory, grammatical inference, and model checking. The PIs envision multiple systems learning the dynamics of an unknown environment collectively, and then refine their plans based on models for the environmental dynamics that are inferred during execution.
Results: In this fiscal period we developed a framework that integrates symbolic control synthesis, game theory and grammatical inference to perform adaptive control synthesis for systems operating in unknown, dynamic, and potentially adversarial environments. We show how action model learning and grammatical inference can be jointly utilized for identifying the interactions between a system and its environment. Grammatical inference then operates in parallel, identifying a formal language which describes the environment. This framework accommodates multiple learning paradigms for constructing provably-correct, adaptive control policies in real-time, either using game-theoretic synthesis methods or model-checking tools.
For synthesis, we developed sampling-based temporal logic planning algorithms that combine long- term temporal logic goals with short-term reactive requirements. The mission specification has two parts: (1) a global specification given as a Linear Temporal Logic (LTL) formula over a set of static service requests that occur at the regions of a known environment, and (2) a local specification that requires servicing a set of dynamic requests that can be sensed locally during the execution. The algorithm has three desirable properties. First, it is incremental, in the sense that the procedure for finding a satisfying path at each iteration scales only with the number of new samples generated at that iteration. Second, the underlying graph is sparse, which guarantees the low complexity of the overall method. Third, it is probabilistically complete. We also provide a conditional result showing that the incremental checking procedure has the best possible complexity bound. These synthesis methods can be combined with machine learning methods to identify the dynamics of uncertain aspects of the systems environment. To this end, we are currently working on extending the system-environment interaction to cases where the system consists of multiple agents. In particular, we study systems where the agents are autonomous, interacting concurrently, and trying to achieve individual tasks expressed as LTL formulae. The agents are not necessarily cooperative—their goals and preferences may or may not be perfectly aligned or opposing. We show how to reason about agent behaviors in such systems with concurrent, multi-agent games with infinitely many stages. To enable coordination, we develop negotiation protocols which ensure that under proper designs of preferences and tasks, the mutually accepted plan is a Pareto optimal Nash equilibrium. Integrating this result with the aforementioned synthesis methods and machine learning methods promises to provide a concrete and formal methodology for constructing provably-correct, adaptive heterogeneous cyberphysical systems which can enhance the effectiveness of coordination in emergency response situations.
Broader impacts: This research activity is multidisciplinary, combining expertise from robotics, lin- guistics, cognitive science, and computer science, and in this capacity exposes researchers of different fields to entirely new ideas and ways of thinking. Exploiting a common theoretical foundation provided by formal language theory, we establish new and reinforce existing intellectual links between disparate scientific communities, and educate a new generation of scholars versed in topics of arts, sciences, and engineering. Our own graduate students receive significant interdisciplinary training, and have developed a range of analytical techniques that cross traditional academic boundaries.