Proof-Theoretic Concepts in the Semantics of Concurrency

并发语义中的证明理论概念

• 批准号: 8912778
• 负责人: Carl Gunter
• 金额: $ 11.81万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-03-15 至 1993-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8912778&HistoricalAwards=false
• 关键词: Proof; Theoretic; Concepts; Semantics; Concurrency

This project aims to investigate the application of proof-theoretic techniques to problems in the operational semantics of true (non- interleaving) concurrency. The research will explore a fruitful relationship between Petri nets and linear logic theories which gives rise to a correspondence between net token games and linear proof trees. This correspondence makes it possible to see that algorithms and theorems from the proof theory of linear logic can be applied to problems in net theory and, conversely, that results about nets have consequences for provability in fragments of linear logic. For example, standard proof-theoretic concepts such as cut elimination give rise to algorithms for increasing the concurrency in an execution sequence on a net. On the other hand, the decidability of forward markings on nets can be used to show decidability for a significant collection of linear logic formulas. Concepts such as the interpretation of logical theories and conservative extension may be useful in understanding abstraction for nets. Moreover, it is hoped that this idea for understanding concurrency in proof trees will lead to the discovery of other interesting models of concurrency.

本项目旨在研究证明理论技术在真（非交错）并发的操作语义问题中的应用。该研究将探索Petri网与线性逻辑理论之间富有成效的关系，从而产生网络令牌博弈与线性证明树之间的对应关系。这种对应关系使我们有可能看到，线性逻辑证明理论中的算法和定理可以应用于网络理论中的问题，相反，关于网络的结果对线性逻辑片段的可证明性有影响。例如，标准的证明理论概念，如割消，产生了用于增加网络上执行序列的并发性的算法。另一方面，网络上前向标记的可判决性可以用来显示线性逻辑公式的重要集合的可判决性。逻辑理论的解释和保守扩展等概念可能有助于理解网络的抽象。此外，我们希望这种在证明树中理解并发性的想法将导致发现其他有趣的并发性模型。