CAREER: Logical Reasoning of Networks with Partial Knowledge

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

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.