CAREER: Logical Reasoning of Networks with Partial Knowledge

在过去的十年里，逻辑推理在计算机网络中取得了巨大的进步，确保了许多不同网络上各种类型的理想行为。这样的成就依赖于一个重要的假设：在一个完全已知的网络上的推理过程总是得出一个决定性的结论。但是，现代网络的庞大规模和复杂性使得很难（如果不是不可能的话）获得目标网络的完整知识，即使缺少一些知识，仍然需要执行一些（可能较弱的）推理。本项目挑战逻辑推理必须完整的假设，开发仅部分已知的网络技术。为了实现具有不确定事件和有限可见性的网络的逻辑推理，本项目计划开发（1）无损失建模，其中明确处理网络不确定性，而不破坏查询能力;以及（2）相对于可获得的信息水平的完全验证，其仅在需要更多信息时才达到不确定的结果。这一愿景的实现是围绕知识表示和部分推理构建的，从而为不确定和缺失的信息提供了一种简单而强大的逻辑语言，通过部分评估，程序包含，谓词实例化，等等。作为朝向其中不可能有全知视图并且最受欢迎的部分推理的真实世界网络的逻辑推理的一步，该项目在计算机网络的持续增长和发展中发挥着独特的作用。与此同时，网络的超大规模作为一个驱动性的挑战，使知识推理社区能够修改和推进早期的复杂性结果，从而在网络中产生更引人注目的用途。借由本计划中不完整的知识表示与归纳推理的数值方法之间的联系，本计划亦可促进未来发展定量网络行为的概率推理。本计划将维持网站https://ravel-net.org/，以公布计划的进展。支持工具将开放源代码;源代码也将在github服务器https://github.com/ravel-net上提供，并提供在线文档，以促进独立验证和重用;网络跟踪，基准和真实世界的数据集将被收集并公开。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

Logical reasoning has made tremendous progress in computer networks in the past decade, assuring desirable behaviors of various types on many different networks. Such achievement relies on an important assumption: the reasoning process on an entirely known network always reaches a decisive conclusion. But the sheer size and complexity of modern networks make it hard, if not impossible, to obtain complete knowledge of the target network, and even when some knowledge is missing, it is still desirable to perform some (perhaps weaker) reasoning. This project challenges the assumption that logical reasoning must be complete and develops techniques for networks only partly known.To achieve logical reasoning of networks with uncertain events and limited visibility, this project plans to develop (1) loss-less modeling in which network uncertainty is explicitly handled without corrupting the querying capability; and (2) complete verification relative to the level of information available, which reaches an inconclusive result only when more information is needed. A realization of this vision is built around knowledge representation and partial reasoning, resulting in a simple yet powerful logical language for uncertain and missing information, enabling a rich set of semantics-based manipulation of partial networks by partial evaluation, program containment, predicate instantiation, etc.As a step towards logical reasoning of real-world networks in which an omniscient view is unlikely and partial reasoning is most sought-after, this project plays a unique role in the continued growth and evolution of computer networks. Simultaneously, the hyper-scale of networks as a driving challenge engages the knowledge reasoning community to revise and advance earlier complexity results, producing a more compelling use in networking. By leveraging the connection between the incomplete knowledge representation in this project and the numerical methods of inductive reasoning, this project may also facilitate future development of probabilistic reasoning for quantitative network behaviors.The project website https://ravel-net.org/ will be maintained to disseminate the progress of the project. Supporting tools will be made open-source; source code will also be available on the github server https://github.com/ravel-net with online documentation to facilitate independent validation and reuse; networking traces, benchmarks, and real-world dataset will be collected and made public.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.