因果可逆束事件结构的迁移系统
Transition Systems from Causal Reversible Bundle Event Structures
AI总结：
本文针对用于研究类CCS和类π系统可逆扩展的因果可逆束事件结构，开发了其到两种迁移系统语义的映射，证明了语义同构并给出了范畴论刻画。
AI中文摘要：
可逆计算是一种新兴范式，它在传统仅正向计算的基础上扩展了反向执行能力，使计算既能正向运行也能反向运行。事件结构是并发理论中的基础模型，通过描述发生的事件及其之间的关系为理解计算过程提供了一种方式。文献中区分了两种将迁移系统语义与事件结构模型关联的结构不同的方法：一种基于构型，即已执行事件的集合；另一种基于模型残差，即模型尚未执行的片段。基于构型的迁移系统主要用于语义表示，而基于残差的迁移系统则被积极用于证明并发进程演算的操作语义与指称语义之间的一致性，以及可视化模型的动态性。本文聚焦于因果可逆束事件结构，这类结构用于研究类CCS和类π系统的可逆扩展；本文开发了从可逆事件结构模型到上述两种迁移系统语义的映射，该映射使得证明两种语义的同构成为可能；本文还提供了这些映射的范畴论刻画。
英文摘要：
Reversible computing is a novel paradigm that has recently emerged and extends traditional forwards-only computation with the capability to execute in the reverse direction, making it possible for computation to run backwards as well as forwards. Event structures are a foundational model in concurrency theory, providing a way to understand computational processes by describing the events that occur and the relationships between them. In the literature, two structurally different approaches to associating transition system semantics with event structure models have been distinguished. One approach is based on configurations, which are sets of already executed events. The other approach is based on model residuals, which are not yet executed fragments of the model. Configuration-based transition systems appear to be primarily used for semantic representations. Residual-based transition systems are actively applied to demonstrate the consistency between operational and denotational semantics of concurrent process calculi, as well as to visualize the dynamics of models. The present paper focuses on bundle event structures with causal reversibility, which are used in the study of reversible extensions of CCS- and π-like systems. Mappings from the reversible event structure model to the two transition system semantics are developed, which made it possible to prove the isomorphism of the semantics. A category-theoretic characterization of the mappings is provided.
