Compositional synthesis of abstractions for infinite networks
Final Report Abstract
Recent advancements in computing, distributed sensing, and data management have opened up possibilities for novel applications involving a large number of dispersed agents operating towards a common objective. In domains like Smart Cities, leveraging affordable personal communication, car-to-car communication, and extensive sensor deployment can revolutionize energy-efficient and environmentally friendly traffic management on a city-wide scale. However, efficiently regulating such expansive and distributed systems poses challenges, including handling uncertain and time-varying participation, limited communication, and stringent safety requirements. To ensure correctness, automated techniques for verifying and synthesizing complex systems are indispensable, considering the risks associated with incorrect configurations, safety, and security. Moreover, emerging applications necessitate sophisticated control objectives that surpass traditional goals in control theory. For example, a complex objective might involve optimizing traffic light adjustments to minimize congestion and maintain a minimum freeway throughput. Due to the complexity of control objectives, the number of participating agents, and the intricacy of the problem, a systematic and automated synthesis approach is crucial, combining principles from computer science and control theory. Correct-by-construction automated verification and synthesis techniques, initially developed for ensuring the correct behavior of software and hardware systems, provide a rigorous framework to effectively address these challenges. In recent years, substantial progress has been made in automated controller synthesis based on symbolic models or finite abstractions. However, an efficient approach to handle large-scale and potentially infinite-dimensional systems is still lacking. Constructing symbolic models often faces exponential computational complexity, making a brute-force approach unfeasible for large-scale systems. Instead, we propose utilizing system structure and employing dissipativity or small-gain arguments to develop methods tailored for large-scale systems. By preserving the network’s structure, our project establishes a rigorous mathematical framework for distributed symbolic control in systems composed of a countably infinite number of dynamically coupled subsystems. The methods we have developed enable distributed control design by harnessing the inherent system structure, leading to more efficient and scalable control solutions.
Publications
-
A Lyapunov-Based Small-Gain Theorem for Infinite Networks. IEEE Transactions on Automatic Control, 66(12), 5830-5844.
Kawan, Christoph; Mironchenko, Andrii; Swikir, Abdalla; Noroozi, Navid & Zamani, Majid
-
ISS small-gain criteria for infinite networks with linear gain functions. Systems & Control Letters, 157, 105051.
Mironchenko, Andrii; Noroozi, Navid; Kawan, Christoph & Zamani, Majid
-
Symbolic models for infinite networks of control systems: A compositional approach. Nonlinear Analysis: Hybrid Systems, 43, 101097.
Liu, Siyuan; Noroozi, Navid & Zamani, Majid
-
A small-gain theorem for set stability of infinite networks: Distributed observation and ISS for time-varying networks. European Journal of Control, 67, 100634.
Noroozi, Navid; Mironchenko, Andrii; Kawan, Christoph & Zamani, Majid
-
Compositional construction of abstractions for infinite networks of discrete-time switched systems. Nonlinear Analysis: Hybrid Systems, 44, 101173.
Sharifi, Maryam; Swikir, Abdalla; Noroozi, Navid & Zamani, Majid
-
A Lyapunov-Based ISS Small-Gain Theorem for Infinite Networks of Nonlinear Systems. IEEE Transactions on Automatic Control, 68(3), 1447-1462.
Kawan, Christoph; Mironchenko, Andrii & Zamani, Majid
-
A Lyapunov-Based Small-Gain Theory for Infinite Networks via Infinite-Dimensional Gain Operators. SIAM Journal on Control and Optimization, 61(3), 1778-1804.
Kawan, Christoph & Zamani, Majid
