Event structures have emerged as a foundational model for concurrent
computation, explaining computational processes by outlining the events and the
relationships that dictate their execution. They play a pivotal role in the
study of key aspects of concurrent computation models, such as causality and
independence, and have found applications across a broad range of languages and
models, spanning realms like persistence, probabilities, and quantum computing.
Recently, event structures have been extended to address reversibility, where
computational processes can undo previous computations. In this context,
reversible event structures provide abstract representations of processes
capable of both forward and backward steps in a computation. Since their
introduction, event structures have played a crucial role in bridging
operational models, traditionally exemplified by Petri nets and process
calculi, with denotational ones, i.e., algebraic domains. In this context, we
revisit the standard connection between Petri nets and event structures under
the lenses of reversibility. Specifically, we introduce a subset of contextual
Petri nets, dubbed reversible causal nets, that precisely correspond to
reversible prime event structures. The distinctive feature of reversible causal
nets lies in deriving causality from inhibitor arcs, departing from the
conventional dependence on the overlap between the post and preset of
transitions. In this way, we are able to operationally explain the full model
of reversible prime event structures.

事件结构在并发计算中扮演重要角色，最近将其扩展到可逆性处理，研究了可逆事件结构与 Petri 网之间的联系，引入了可逆因果网络，并从操作层面解释了可逆主事件结构的完整模型。

可逆透视下的 Petri 网和事件结构

A Reversible Perspective on Petri Nets and Event Structures

In a recent paper, new theorems linking apparently unrelated mathematical
objects (event structures from concurrency theory and full graphs arising in
computational biology) were discovered by cross-site data mining on huge
databases, and building on existing Isabelle-verified event structures
enumeration algorithms. Given the origin and newness of such theorems, their
formal verification is particularly desirable. This paper presents such a
verification via Isabelle/HOL definitions and theorems, and exposes the
technical challenges found in the process. The introduced formalisation
completes the verification of Isabelle-verified event structure enumeration
algorithms into a fully verified framework to link event structures to full
graphs.

本篇论文基于 Isabelle-verified 事件结构枚举算法，通过对巨大数据库进行跨站数据挖掘，发现了连接看似不相关的数学对象（并发理论中的事件结构和计算生物学中的完整图）的新定理，并通过 Isabelle/HOL 定义和定理进行了形式验证，完成了 Isabelle-verified 事件结构枚举算法验证的全面验证框架以链接事件结构和完整图。

原有表征定理的 Isabelle 形式化

Isabelle Formalisation of Original Representation Theorems

FASTUS is a system for extracting information from natural language text for
entry into a database and for other applications. It works essentially as a
cascaded, nondeterministic finite-state automaton. There are five stages in the
operation of FASTUS. In Stage 1, names and other fixed form expressions are
recognized. In Stage 2, basic noun groups, verb groups, and prepositions and
some other particles are recognized. In Stage 3, certain complex noun groups
and verb groups are constructed. Patterns for events of interest are identified
in Stage 4 and corresponding ``event structures'' are built. In Stage 5,
distinct event structures that describe the same event are identified and
merged, and these are used in generating database entries. This decomposition
of language processing enables the system to do exactly the right amount of
domain-independent syntax, so that domain-dependent semantic and pragmatic
processing can be applied to the right larger-scale structures. FASTUS is very
efficient and effective, and has been used successfully in a number of
applications.

FASTUS 是一种基于有限状态自动机的信息提取系统，利用多阶段方法从自然语言文本中提取信息，生成数据库条目，并构建事件结构，以能够对领域无关的语法做出准确的处理。