Theories of Truly Concurrent Processes
本文基于Hennessy的工作，为真正并发过程代数建立测试语义，继承操作语义、公理语义和指称语义的三位一体。
2026-08-20 cs.LO
A Calculus for True Concurrency
我们设计了一个演算真正的并发称为CTC，包括它的语法和操作语义。CTC对几种强真并发互模拟和弱真并发互模拟都有很好的模性质，如么半群律、静态律、强真并发互模拟的新展开律、弱真并发互模拟的$τ$律、强、弱真并发互模拟的全同余以及递归的唯一解.
2020-04-22 cs.LO
Truly Concurrent Process Algebra Is Reversible
基于我们以前的进程代数的并发APTC，我们证明了它是可逆的一个小的修改。可逆代数有四个部分：可逆真并发基本代数（BARTC），可逆真并发代数（APRTC），递归和抽象。
2018-09-29 cs.LO
Truly Concurrent Bisimilarities are Game Equivalent
我们设计的游戏真正并发的双相似性，包括强烈真正并发的双相似性和分支真正并发的双相似性，如pomset双相似性，步骤双相似性，历史保存的双相似性和遗传的历史保存的双相似性。
2019-06-27 cs.GT cs.LO
Truly Concurrent Process Algebra to Unifying Quantum and Classical Computing
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。现在，是时候利用真正的并发进程代数APTC和APPTC来建模量子计算并统一量子计算和经典计算了。在这本书中，我们介绍了APTC的原理，利用APTC统一量子和经典计算及其在量子通信协议验证中的应用，利用APPTC统一量子和经典计算及其在量子通信协议验证中的应用。
2021-10-25 cs.LO
Finitary Truly Concurrent Bisimulations
为基于预互模拟预序的过程语言开发完全抽象指称模型，解决无限观察区分问题，定义真正并发预互模拟及其有限形式。
2026-06-09 cs.LO
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
本文证明了（强）全并发互模拟性和i-因果网互模拟性在有限有界Petri网上是可判定的，其核心方法是对Vogler的有序标记证明技术进行推广。
2023-12-20 cs.LO
Actors -- A Process Algebra Based Approach
我们基于真正的并发进程代数来建模Actor，并在以下特征中捕获Actor模型：（1）并发性：所有Actor并发执行;（2）异步性：Actor异步接收和发送消息;（3）唯一性：Actor具有唯一名称和关联的唯一邮箱名称;（4）集中性：参与者专注于处理消息，包括一些本地计算，一些新参与者的创建，以及向其他参与者发送一些消息;（5）通信依赖性：影响参与者的唯一方式是向其发送消息;（6）抽象：除了接收和发送消息以及创建新的角色之外，本地计算被抽象;（7）持久性：角色在处理消息之后不会消失。真并发进程代数具有丰富的表达能力，可以对上述角色的特性进行建模，更重要的是，它是真并发的模型。与其他角色模型相比，基于真并发进程代数的角色模型具有以下优点：（1）真并发进程代数具有丰富的表达能力，可以描述参与者的几乎所有特征，特别是对于异步通信，（2）真并发进程代数和角色都是真并发的模型，具有与生俱来的相似性;（3）真并发进程代数具有坚实的语义基础和强大的证明理论，角色系统的正确性可以很容易地得到证明。
2021-10-27 cs.LO
Probabilistic Process Algebra for True Concurrency
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在这本书中，我们引入概率到真正的并发进程代数，基于概率进程代数的工作。
2021-07-28 cs.LO
Reversible Quantum Process Algebra
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在可逆进程代数和概率真并发进程代数方面也做了一些工作。在本书中，我们利用可逆的真正并发进程代数APRTC和APPTC来建模量子计算，并统一量子和经典计算。
2021-08-05 cs.LO
Reversible Quantum Process Algebra with Guards
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在可逆进程代数和概率真并发进程代数方面也做了一些工作。在这本书中，我们利用可逆的真正并发进程代数APRTC和概率进程代数APPTC来建模量子计算，并统一量子和经典计算。
2021-08-05 cs.LO
An Algebra of Reversible Computation
基于交错语义的进程代数ACP是不可反转的。我们设计了一个可逆版本的APTC称为RAPTC。它具有可逆选择、顺序、并行、通信、静默步和抽象等代数定律，以及模强正逆真并发互模拟和弱正逆真并发互模拟的可靠性和完备性。
2018-05-02 cs.LO
The Nature of Concurrency
本研究基于真并发进程代数的最新成果，阐明交错并发与真并发的关系，给出事件结构、Petri网等真并发模型的进程代数基础。
2023-08-24 cs.LO
Security Analyses of Quantum Communication Protocols
真并发进程代数是对传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在本书中，我们利用真并发进程代数APTC和APPTC来建模量子计算，并统一量子计算和经典计算。
2021-07-28 cs.LO
Structural Operational Semantics for True Concurrency
将结构操作语义扩展到真并发，以偏序多重集取代单动作作为转移基础，并推广LTS、TSS及行为等价等概念。
2026-06-16 cs.LO
An Algebra of Actors Based on True Concurrency
基于异步$π$演算的Actor代数$\textrm{A}π$完全捕获了Actor的属性，但是，它是基于交错互模拟语义的。我们将$\textrm{A}π$调整为$\textrm{A}π_{tc}$，使$\textrm{A}π$具有真正的并发语义。给出了$\textrm{A}π_{tc}$的语法和操作语义，以及$\textrm{A}π_{tc}$的真正并发语义模型和代数定律。
2017-05-06 cs.LO
A Truly Concurrent Semantics for Reversible CCS
本文针对 RCCS 的抽象语义问题，利用 CCS 到 Petri 网的经典编码并引入因果一致可逆性，构造每个 RCCS 项对应的可逆 Petri 网模型。
2024-12-02 cs.IT cs.LO math.IT
Compositional Net Semantics up to Step Net Bisimilarity
步网双相似性\cite{Gor23}是有限Petri网的一个真正并发的行为等价，它是标准步网双相似性\cite{NT84}在Petri网上的光滑推广，但具有关联标记（仅相同大小）产生相同的事件偏序的性质.进程代数FNM \cite{Gor17}真实地表示所有（且仅）有限Petri网，直到同构。我们证明了步网双相似是一个同余w.r.t.这样，我们就为所有的有限Petri网类定义了一个完全尊重因果关系和系统分支结构的合成语义。
2023-01-28 cs.LO
Data refinement for true concurrency
大多数现代系统都表现出复杂的并发行为，其中多个系统组件以细粒度的原子性修改和观察系统状态。许多系统（例如，多核处理器、实时控制器）也表现出真正的并发行为，其中多个事件可以同时发生。本文提出了一个基于区间的框架，其中包括捕获非确定性表达式计算的高级操作符定义的数据细化。通过修改区间的类型，我们的理论可以专门涵盖离散和连续系统的数据细化。我们提出了一个基于区间的编码的前向模拟，然后证明我们的前向模拟规则是健全的，我们的数据细化定义。一些规则分解正向模拟证明顺序和并行组合开发。
2013-05-27 cs.LO
Compositional Semantics of Finite Petri Nets
本文针对有限 Petri 网，证明保结构互模拟关于 FMN 算子为同余，并给出尊重因果性与分支结构的组合语义及可靠公理化基础。
2023-08-17 cs.LO
Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings
本文针对并发可逆系统，基于Degano & Priami证明树方法开发编码，统一推导前向、反向及前向-反向互模拟的展开律，并揭示反向类互模拟编码需扩展反向就绪集。
2024-11-21 cs.LO
Concurrency and Probability: Removing Confusion, Compositionally
针对Petri网中混淆与分布式决策问题，提出基于结构分支单元（s-cells）的静态分解方法，将网转换为无混淆网，使冲突备选方案可概率化，非冲突备选保持并发，且与递归停止配置对应。
2019-12-18 cs.LO
A Process Algebra for Games
使用计算机科学中的形式化工具来描述博弈是一个有趣的问题。我们给游戏，确切地说是两个人的游戏，一个公理化的基础上的进程代数ACP（代数通信过程）。在ACP算法中引入了一个新的算子--对手的选择组合算子（OA），用来描述博弈树和博弈策略，称为GameACP。自然地建立了其健全而完整的公理体系。为了模拟游戏的结果（玩家和对手的共同行动），相应地，在GameACP中，GameACP过程的执行，另一个称为播放操作符（PO）的操作符扩展到GameACP中。我们还建立了一个健全的和完整的公理系统PO。为了克服新出现的不确定性引入GameACP，我们扩展真正的并发进程代数APTC游戏称为GameAPTC。最后给出了博弈结果与GameACP和GameAPTC过程推论之间的正确性定理。
2019-05-08 cs.LO
Secure Process Algebra
基于我们以前对真并发进程代数APTC的工作，我们使用它来验证安全协议。本文的工作（Secure APTC，简称SAPTC）在验证安全协议方面具有以下优点：（1）具有坚实的理论基础，包括等式逻辑、结构化操作语义以及它们之间的公理化;（2）具有丰富的描述安全协议的表达能力。密码操作被建模为原子操作并可扩展，显式的并行性和通信机制用于建模通信操作和通信主体，丰富的计算属性用于描述安全协议中的计算逻辑，包括条件保护、交替组合、顺序组合、并行性和通信、封装和死锁、递归、抽象。(3)特别是通过抽象，可以方便、直观地观察安全协议的输入输出关系，包括无攻击时的关系、各种已知攻击下的关系以及未知攻击下的关系（如果未知攻击可以描述的话）。
2021-10-25 cs.CR cs.LO
