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.

该项目根据两人游戏的数学思想开发了一种新的编程语言。该项目的影响是，它为在挑战性的对抗环境中建模交互式系统提供了一个强大的新工具，并有助于编写在最坏情况下保持正确的代码。研究人员特别关注该新工具在安全应用程序中的影响，例如一个代理商追求另一个代理商的数学游戏。该项目的新颖性是，它提高了我们将代码和数据建模为单独但互动的事物的能力，并且它首次将尚未取消的逻辑传统转变为一种实用的编程语言，称为动态逻辑和游戏逻辑。技术方法结合了两个良好的想法：逻辑节目的逻辑编程和一种形式上的logics家族。逻辑编程是一种编程方式，其中程序由正式的逻辑规则组成，并且运行程序等同于搜索证明。游戏逻辑是模态逻辑的家族，每个模态操作员在两个玩家之间定义了零和游戏的模型。该项目建立在研究者在游戏逻辑证明和计算之间建立理论联系的发展，从而将其转变为实用联系。这种转换将基于对动态逻辑公式的自动分析和其他丰富的逻辑编程语言（例如答案集编程语言）的先前文献。影响是为在对抗环境中提供一种简洁，表现力的语言，用于建模包括软件，包括软件。由于游戏证明与赢得策略相对应，因此主要的影响是对证明搜索和程序合成之间的界限模糊，为自动搜索程序员游戏模型的获胜策略提供了一种优雅的机制。该奖项反映了NSF的法定任务，并通过使用该基金会的知识优点和广泛的影响来评估NSF的法定任务，并通过评估有价值。