About DISCOVER Lab

The research goal of Distributed Cooperative System Research (DISCOVER) Laboratory is to build foundations for a provably correct design theory for distributed cooperative systems. We aim to derive a scalable formal design theory and algorithms to enable the engineering of large-scale distributed cyber-physical systems (CPSs) that can function reliably in uncertain and dynamic environments. Our motivation comes from the fact that large-scale, distributed, and networked CPSs have been increasingly prevalent in our daily life. Examples include but not limited to intelligent transportation systems, edge-centric computing, smart grids, and water/gas distribution networks. These systems are safety-critical and their reliable operations are of great national interest.

Existing design methods for distributed engineering systems can be broadly divided into two classes: bottom-up and top-down design. In the bottom-up design methods, complicated behaviors are built upon simple control actions, called primitives. These primitives are usually implemented as simple reactive programs, following pre-defined rules and responding to local changes. However, complicated global behaviors could emerge from a large collection of components executing such simple programs. As the executions of these primitives only involve local sensing and reaction, bottom-up approaches therefore scale well but generally lack formal performance guarantees as it is hard to predict the global emergent behavior. On the other hand, the top-down design methods follow a “divide-and-conquer” philosophy, and decompose a global team mission into local individual tasks or distribute a global cost function into local utilities for each agent based on their individual sensing and actuating capabilities. Different from bottom-up approaches, in the top-down design we synthesize physical control laws and coordination mechanisms by solving the decomposed local design problems. Top-down design therefore can provide performance guarantees, but does not handle efficiently complex physical dynamics or uncertain environments as the design usually depends on an abstracted transition model of the system in a finitely partitioned environment. 

This motivates us to combine the top-down and bottom-up design methods in a unified architecture. For this, we need to overcome two major challenges – scalability and uncertainty. To deal with scalability, we propose to decompose the overall system specification into local specifications for individual components so to distribute the whole design process. To tackle uncertainties, we propose to combine machine learning with formal verification so to achieve verifiable adaptation/reconfiguration in uncertain and dynamic environments. Accordingly, we pursue multi-disciplinary approaches combining methods from control theory, reactive synthesis, computational verification, and machine learning for a scalable formal design theory of distributed CPSs.

Our research will result in deriving a combined top-down and bottom-up formal design theory for high-confidence, large-scale distributed CPSs. Through the proposed design theory, a new perspective to addressing the complexity of large-scale distributed CPSs is developed. Besides of the robotic systems used in our lab as typical design examples, the proposed framework is applicable to the formal design of other CPSs consisting of distributed and coordinated subsystems, such as the national power grid, ground/air traffic networks, and manufacturing systems.

(Group photo taken in May, 2019. From left to right : Armin Maleki, Zihao Song, Tongjia Zheng, Hai Lin, Honghui Wu, Yuxuan Kuang, Fahimeh Orvati Nia and Zahra Hashemi.)

Number of pageloads: