CPS: Breakthrough: Knowledge-Aware Cyber-Physical Systems

该项目解决了网络物理系统（CPS）中知识的基础问题，即结合通信，计算和物理等方面的系统。单个系统通过传感器观察其环境，并通过执行器进行交互。两者都不完美。因此，CPS对世界的内部看法是模糊的，它的行动是不精确的。CPS的分析方法仍然没有区分世界的真相和内部观点，导致理论模型的行为与现实世界的对应行为之间的不匹配。如何信任它们来执行安全关键任务？该项目通过开发CPS中知识和学习的推理方法来解决这一关键不足。该项目致力于开发新的逻辑原则，以验证知识感知的CPS。本项目研究如何使世界与通过传感器的部分感知之间的不匹配明确，以及如何在这种不匹配的情况下在理论和实践中实现可证明的正确控制。通过在不断变化的世界中研究不断变化的知识，该项目为CPS提供了一个基本特征，没有这个特征，CPS就永远不会同时真正安全高效。该项目的广泛意义和重要性是CPS在许多安全关键领域（如航空和汽车工业）获得广泛关注的结果。这种CPS存在安全漏洞的一个原因是，正式的验证技术在很大程度上仍然是知识不可知的，并且可验证的解决方案过于悲观。该项目解决了这些问题，并提供了一些工具，允许将有关环境意图的知识合并到模型中，以派生出可证明正确的，但合理的乐观的，因此有效的行为。根据其逻辑性质，这些技术适用于广泛的CPS，因此对许多应用程序做出了重大贡献。在这个项目中获得的结果将在CPS模型和实验室机器人场景中进行演示，并将在课程和工业合作伙伴中共享。本项目所追求的技术方法是开发一种新的建模语言、逻辑和证明演算，用于验证知识感知的CPS。所使用的知识范式允许CPS控制器无缝地获取关于世界的知识，也可以获取关于系统中其他代理（即其他控制器）的知识。知识是不同主体之间相互作用的关键。该项目研究了一个明确的世界感知和智能体意图模型——以及这些感知和意图的知识——如何允许CPS智能体在多智能体场景中基于更有效但仍可证明安全的控制来行动。这些方法将在验证工具KeYmaera中实现，并在不同的案例研究应用程序（如汽车场景）的正式验证中进行演示。

This project addresses the foundational problem of knowledge within cyber-physical systems (CPS), i.e., systems that combine aspects such as communication, computation, and physics. A single system observes its environment through sensors and interacts through actuators. Neither is perfect. Thus, the CPS's internal view of the world is blurry and its actions are imprecise. CPS are still analyzed with methods that do not distinguish between truth in the world and an internal view thereof, resulting in a mismatch between the behavior of theoretical models and their real-world counterparts. How could they be trusted to perform safety-critical tasks? This project addresses this critical insufficiency by developing methods to reason about knowledge and learning in CPS. The project pursues the development of new logical principles for verifying knowledge-aware CPS. This project investigates how to make the mismatch between the world and the partial perception through sensors explicit and how to achieve provably correct control in theory as well as practice despite this mismatch. By investigating changing knowledge in a changing world, this project contributes to a fundamental feature without which CPS can never be truly safe and efficient at the same time. The project's broader significance and importance are a result of the widespread attention that CPS gain in many safety-critical areas, such as in aviation and automotive industries. One reason for safety gaps in such CPS is that formal verification techniques are still largely knowledge-agnostic, and verifiable solutions overly pessimistic. This project addresses these issues and provides tools that allow for incorporating knowledge about the environment's intentions into the models to derive provably correct, but justifiably optimistic, and thus efficient, behavior. By their logical nature, these techniques are applicable to a wide range of CPS and, thus, contribute significantly to numerous applications. Results obtained within this project will be demonstrated in CPS models and laboratory robot scenarios, and will be shared in courses and with industrial partners.The technical approach that this project pursues develops a new modeling language, logic, and proof calculus for verifying knowledge-aware CPS. The knowledge paradigm used allows CPS controllers to seamlessly acquire knowledge about the world but also about other agents in the system, i.e., other controllers. Knowledge is the key to interactions between different agents. This project investigates how an explicit model of world perception and agent intentions - and knowledge of these perceptions and intentions - allows CPS agents to act, based on more efficient, but still provably safe control in multi-agent scenarios. The methods will be implemented in the verification tool KeYmaera and demonstrated in formal verification on different case study applications such as car scenarios.