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.