SHF: Small: Game Logic Programming

SHF：小：游戏逻辑编程

• 批准号: 2346619
• 负责人: Rose Bohrer
• 金额: $ 59.6万
• 依托单位: Worcester Polytechnic Institute
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-05-01 至 2027-04-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2346619&HistoricalAwards=false
• 关键词: SHF; Small; Game; Logic; Programming

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.

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