Compositional synthesis of abstractions for infinite networks

点击翻译按钮获取中文摘要

Recent advances in computing, cheap distributed sensing and large-scale data management have created the potential for new applications, in which large numbers of dispersed agents need to be regulated for a common objective. In the domain of Smart Cities, for instance, city-wide traffic control based on cheap personal communication, car-to-car communication and the deployment of numerous sensors can provide a major step towards energy-efficient and environmentally friendly traffic concepts. The vision of efficiently controlling such large, dispersed systems requires scalable tools that are capable of handling uncertain and time-varying numbers of participating subsystems, limited communication, as well as stringent safety specifications. The costs of incorrect configuration as well as safety and security concerns require automated and provably correct techniques for the verification and synthesis of complex systems. Moreover, emergent applications necessitate sophisticated control objectives, which go well beyond standard goals pursued in classic control theory. For instance, a complex objective is to adjust the traffic lights such that congestion is minimized and freeway throughput is ensured to remain above a minimum threshold. The complex nature of control objectives, number of participating agents, and the complexity of the problem call for methods on systematic, automated synthesis of provably correct controllers by merging ideas from computer science and control theory. In particular, correct-by-construction automated verification and synthesis, which were originally developed for specifying and verifying the correct behavior of software and hardware systems, provide a rigorous framework to efficiently address the above issues.The study of automated controller synthesis based on symbolic models (or finite abstractions) has seen major advances in recent years. However, an efficient approach to the large-scale and possibly infinite-dimensional case is missing. As the computational complexity of constructing symbolic models often scales exponentially with the dimension of the state space, a brute force approach to large-scale systems is not feasible. Instead, we propose to use system structure to derive methods for large-scale systems based on dissipativity or small-gain arguments.This project aims to develop a rigorous mathematical framework for distributed symbolic control of systems composed of a countably infinite number of dynamically coupled subsystems. Our proposed methods will preserve the structure of the network in order to facilitate distributed control design. The effectiveness of the theoretical results will be verified by applications to trafficnetworks.