SHF: Small: Game Logic Programming

该项目基于两人游戏的数学思想开发了一种新的编程语言。该项目的影响是，它提供了一个强大的新工具，用于在具有挑战性的对手环境中对交互系统进行建模，并帮助高效地编写在最糟糕的环境中仍然正确的代码。调查人员特别关注这种新工具在安全应用中的影响，例如一个代理追求另一个代理的数学游戏。该项目的创新之处在于，它提高了我们将代码和数据建模为独立的、但又相互作用的事物的能力，并且它首次将尚未开发的逻辑传统转换为一种实用的编程语言，称为动态逻辑和游戏逻辑。该技术方法结合了两个成熟的想法：逻辑编程范例和称为游戏逻辑的形式逻辑系列。逻辑编程是一种编程风格，其中程序由形式化的逻辑规则组成，运行程序相当于寻找证据。博弈逻辑是一族模态逻辑，其中每个模态算子定义了两个参与者之间的零和博弈模型。这个项目建立在研究人员发展博弈逻辑证明和计算之间的理论联系的基础上，将其转化为实践联系。这种转换将建立在先前关于动态逻辑公式的自动分析和其他丰富的逻辑编程语言(如答案集编程语言)的文献的基础上。其影响是提供一种简明、富有表现力的语言，用于在对抗性环境下对交互系统(包括软件)进行建模。由于游戏证明对应于获胜策略，因此主要影响将是证明搜索和程序合成之间的界限变得模糊，为自动搜索程序员游戏模型的获胜策略提供了一种优雅的机制。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

The project develops a new programming language based on the mathematical idea of a two-player game. The project's impacts are that it provides a powerful new tool for modeling interactive systems in challenging adversarial environments and also helps productively write code that remains correct in worst-case environments. The investigator especially focuses on the impacts of this new tool in security applications, such as mathematical games where one agent pursues another. The project's novelties are that it improves our ability to model code and data as separate, yet interacting things, and that, for the first time, it transforms a yet-unexploited logical tradition into a practical programming language, called dynamic logics and game logics.The technical approach combines two well-established ideas: the paradigm of logic programming and a family of formal logics called game logics. Logic programming is a style of programming where programs are made up of formal logical rules and running a program is equivalent to searching for proofs. Game logic is a family of modal logics where every modal operator defines a model of a zero-sum game between two players. This project builds on the investigator's development of a theoretical connection between game logic proofs and computation, transforming it into a practical connection. This transformation will build upon prior literature on both automated analysis of dynamic logic formulas and on other rich logic programming languages such as answer-set programming languages. The impact is to provide a concise, expressive language for modeling interactive systems, software included, with adversarial environments. Because game proofs correspond to winning strategies, a major impact will be the blurring of lines between proof search and program synthesis, providing an elegant mechanism for automatically searching for the winning strategies of the programmer's game models.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.