Proof-Theoretic Concepts in the Semantics of Concurrency

该项目旨在研究证明论技术在真(非交织)并发的操作语义问题上的应用。这项研究将探索Petri网和线性逻辑理论之间的一种富有成效的关系，这种关系产生了网令牌游戏和线性证明树之间的对应关系。这种对应关系使得可以看到线性逻辑证明理论中的算法和定理可以应用于网络理论中的问题，反之，关于网络的结果对于线性逻辑片段中的可证明性具有结果。例如，标准的证明论概念，如割消除法，产生了增加网络上执行序列中的并发性的算法。另一方面，网上前向标记的可判断性可用于表示对大量线性逻辑公式集合的可判断性。逻辑理论的解释和保守延拓等概念对于理解网的抽象可能是有用的。此外，希望这种在证明树中理解并发性的想法将导致发现其他有趣的并发性模型。

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.