Compositional synthesis of abstractions for infinite networks

无限网络抽象的组合综合

• 批准号: 407680529
• 负责人: Professor Dr. Majid Zamani, since 12/2021
• 金额: --
• 依托单位: Lehrstuhl Dynamische Systeme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2018
• 资助国家: 德国
• 起止时间: 2017-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/407680529?language=en
• 关键词: Compositional; synthesis; abstractions; 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.

计算、廉价分布式传感和大规模数据管理的最新进展为新的应用创造了潜力，在新的应用中，需要为一个共同的目标对大量分散的代理进行监管。例如，在智能城市领域，基于廉价个人通信、车对车通信和部署大量传感器的全市交通控制可以为实现节能和环保的交通概念迈出重要一步。 有效控制这样的大型分散系统的愿景需要可扩展的工具，这些工具能够处理参与子系统的不确定和时变数量，有限的通信以及严格的安全规范。不正确配置的成本以及安全和安保问题需要自动化和可证明正确的技术来验证和综合复杂系统。 此外，紧急应用程序需要复杂的控制目标，这远远超出了经典控制理论追求的标准目标。 例如，一个复杂的目标是调整交通信号灯，使拥堵最小化，并确保高速公路吞吐量保持在最小阈值以上。 控制目标的复杂性，参与代理的数量，以及问题的复杂性，要求通过合并来自计算机科学和控制理论的思想，系统地，自动地合成可证明正确的控制器的方法。 特别是，correct-by-construction自动验证和综合，这最初是为指定和验证软件和硬件系统的正确行为而开发的，提供了一个严格的框架来有效地解决上述问题。然而，一个有效的方法来大规模的，可能是无限维的情况下失踪。 由于构造符号模型的计算复杂度通常与状态空间的维数成指数关系，因此对大规模系统的蛮力方法是不可行的。 相反，我们建议使用系统结构来推导基于耗散性或小增益arguments.This项目的大规模systems的方法，旨在开发一个严格的数学框架，分布式符号控制系统组成的可数无限数量的动态耦合子系统。我们提出的方法将保留网络的结构，以方便分布式控制设计。 理论结果的有效性将通过在交通网络中的应用得到验证。