Structural Operational Semantics for True Concurrency
将结构操作语义扩展到真并发，以偏序多重集取代单动作作为转移基础，并推广LTS、TSS及行为等价等概念。
2026-06-16 cs.LO
On the Parallel Composition for True Concurrency
为了深入了解真正的并发并行组合，我们回顾了公理化的并行组合模真正并发的行为等价的真正并发进程代数APTC的侧记。我们证明：（1）不需要任何辅助算子，并行复合模pomset、step和hp-互模拟都有一个有限的可靠的完备公理化。(2)不存在一个有限的声音和完整的公理化的并行复合模hhp-互模拟，没有任何辅助操作。(3)有一个有限的声音和完整的公理化的并行复合模pomset，步骤，hp-。和HHP-互模拟，具有辅助的左并行合成和通信合并。
2020-10-15 cs.LO
The Nature of Concurrency
本研究基于真并发进程代数的最新成果，阐明交错并发与真并发的关系，给出事件结构、Petri网等真并发模型的进程代数基础。
2023-08-24 cs.LO
True Concurrency Can Be Easy
步网互模拟是有限Petri网上的一种共归纳行为关系，它是标准步网互模拟\cite{NT84}定义在有限Petri网上的光滑推广.它的诱导等价提供了一个替代的，更简单的表征因果网双相似性\cite{G15,Gor22}，因为它不诉诸于任何因果结构，和结构保持双相似性\cite{G15}，因为它不需要双射映射之间的相关标记。我们表明，步骤网双相似性可以通过一个合适的模态逻辑，称为NML（网络模态逻辑的缩写）的逻辑特征：两个标记是步骤网双相似的当且仅当它们满足相同的NML公式。
2023-01-28 cs.LO
Truly Concurrent Process Algebra Is Reversible
基于我们以前的进程代数的并发APTC，我们证明了它是可逆的一个小的修改。可逆代数有四个部分：可逆真并发基本代数（BARTC），可逆真并发代数（APRTC），递归和抽象。
2018-09-29 cs.LO
Data refinement for true concurrency
大多数现代系统都表现出复杂的并发行为，其中多个系统组件以细粒度的原子性修改和观察系统状态。许多系统（例如，多核处理器、实时控制器）也表现出真正的并发行为，其中多个事件可以同时发生。本文提出了一个基于区间的框架，其中包括捕获非确定性表达式计算的高级操作符定义的数据细化。通过修改区间的类型，我们的理论可以专门涵盖离散和连续系统的数据细化。我们提出了一个基于区间的编码的前向模拟，然后证明我们的前向模拟规则是健全的，我们的数据细化定义。一些规则分解正向模拟证明顺序和并行组合开发。
2013-05-27 cs.LO
Concurrency, Causality and Conflict via Independence in Reversible Calculi
Augusta University（奥古斯塔大学）；Imperial College London（伦敦帝国学院）；IAR Nagoya University（名古屋大学国际学术研究院）；AGH University of Kraków（克拉科夫AGH科技大学）；University of Leicester（莱斯特大学）
本文在可逆演算中引入独立性概念，证明预可逆系统具有唯一独立性及真并发关系，给出因果与冲突的独立性刻画，并通过Beluga验证两个演算中独立性与依赖性的性质，最后探讨其扩展应用。
2026-09-18 cs.LO
Logics and Games for True Concurrency
我们研究了基于过渡系统，Petri网和事件结构的各种偏序模型的并发性的基本数学性质，并表明这些系统的并发行为可以通过两个简单的和一般的对偶局部行为以统一的方式捕获。这种对偶性被用来定义新的μ演算和逻辑游戏，用于分析具有偏序语义的并发系统。这项工作的一些结果是：一些mu-演算的定义，在某些类的系统，诱导相同的标识作为一些最有名的互模拟等价的并发性;和定义（无限）高阶逻辑游戏的互模拟和模型检查，其中的球员的游戏给予（本地）一元二阶权力的一组元素，他们被允许发挥。更具体地说，我们表明，我们的游戏是健全的和完整的，因此，确定;此外，它们是可判定的有限情况下，并支持新的决策程序的互模拟和模型检查。由于这些mu演算和逻辑游戏概括了著名的不动点逻辑和博弈论决策程序的并发系统与交织语义，本文的结果给出了一些基础的设计一个基于逻辑的，博弈论的框架研究，在一个统一的方式，几个并发系统，无论他们是否有交织或偏序语义。
2010-11-04 cs.LO
Theories of Truly Concurrent Processes
本文基于Hennessy的工作，为真正并发过程代数建立测试语义，继承操作语义、公理语义和指称语义的三位一体。
2026-08-20 cs.LO
Structured Parallel Programming
基于我们以前对真并发代数律的研究，我们设计了一种结构化真并发并行程序设计语言PPL，与大多数程序设计语言不同的是，PPL有一个显式的并行操作符作为基本操作符，包括它的操作语义、指称语义和公理语义。PPL可以构造一个真正的并发图的范式，这意味着它是可能的，以实现一个编译器的PPL。
2021-11-09 cs.LO
Current-State Opacity in Safe Partially Observed Quantum Petri Nets: True-Concurrency Semantics and Exact Symbolic Verification
Institute of Systems Engineering, Macau University of Science and Technology（澳门科技大学系统工程研究所）
本文提出在安全部分观测量子Petri网中使用真正的并发语义来定义当前状态模糊性，并通过精确符号验证算法评估量子后状态泄漏，解决了传统离散事件系统中无法捕捉混合架构安全漏洞的问题。
2026-04-20 cs.LO quant-ph
Truly Concurrent Pi-Calculi with Reversibility, Probabilism and Guards
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在本书中，我们将可逆性、概率论和保护引入真正的并发演算$π_{tc}$。
2021-08-24 cs.LO
Truly Concurrent Calculi with Reversibility, Probabilism and Guards
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在这本书中，我们将可逆性，概率论和警卫引入真正的并发演算CTC。
2021-08-15 cs.LO
Truly Concurrent Process Algebra with Localities
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在这本书中，我们引入地方到真正的并发进程代数，工作的基础上进程代数与地方。
2021-09-10 cs.LO
Formal Relationships Between Geometrical and Classical Models for Concurrency
在过去的几十年中，已经提出了各种各样的并发程序模型，每一个专注于计算的各个方面：跟踪等价性，事件之间的因果关系，冲突和时间表，由于资源访问等最近，模型与几何风味已被引入，基于立方集的概念。这些模型非常丰富和富有表现力，因为它们可以表示任何一组事件之间的交换，从而概括了真正的并发性原则。虽然他们似乎是非常有前途的-因为他们有可能使用的技术，从代数拓扑，以研究并发计算-他们还没有被精确地与以前的模型，本文的目的是填补这一空白。特别是，我们描述了Petri网和立方集之间的附加扩展以前已知的附加Petri网和异步过渡系统之间的尼尔森和Winskel。
2012-06-11 cs.DC cs.LO
Petri Nets and Higher-Dimensional Automata
本文重新审视Petri网的高维自动机语义，将翻译扩展至带抑制弧的网和广义自修改网，并提供了实现该翻译的工具。
2025-02-04 cs.LO
An Event Structure Model for Probabilistic Concurrent Kleene Algebra
给出了概率并发Kleene代数的一个新的真并发模型。该模型基于概率事件结构，结合了Katoen的概率并发工作和Varacca的概率主事件结构的思想。的事件结构进行了比较，与一个真正的并发版本的Segala的概率模拟。最后，该模型的代数属性进行了总结的程度，他们可以用来推导技术，如概率依赖/保证推理规则。
2013-10-09 cs.LO
Security Analyses of Quantum Communication Protocols
真并发进程代数是对传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在本书中，我们利用真并发进程代数APTC和APPTC来建模量子计算，并统一量子计算和经典计算。
2021-07-28 cs.LO
Reversible Quantum Process Algebra
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在可逆进程代数和概率真并发进程代数方面也做了一些工作。在本书中，我们利用可逆的真正并发进程代数APRTC和APPTC来建模量子计算，并统一量子和经典计算。
2021-08-05 cs.LO
An Algebraic Characterisation of Concurrent Composition
我们给出了一种形式的同步并行组合允许真正的并发性的代数表征，使用基于彼得·兰丁的“程序-机器对称自动机理论”的想法。
2014-06-08 cs.LO
Reversible Quantum Process Algebra with Guards
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在可逆进程代数和概率真并发进程代数方面也做了一些工作。在这本书中，我们利用可逆的真正并发进程代数APRTC和概率进程代数APPTC来建模量子计算，并统一量子和经典计算。
2021-08-05 cs.LO
Probabilistic Rely-guarantee Calculus
Jones的可靠保证演算共享变量并发扩展到包括概率行为。我们使用的代数方法，结合和适应概率Kleene代数并发Kleene代数。稳健的代数相对于一般的概率事件结构语义。本文的主要贡献是建立在语义之上的可靠保证规则的集合。特别是，我们展示了如何获得的概率范围内的真实并发指称语义的可靠保证规则。这些规则的使用说明了一个简单的概率并发程序的详细验证：一个错误的Eratosthenes筛。
2015-06-02 cs.LO
Concurrent Kleene Algebra of Partial Strings
并发Kleene代数（CKA）是Hoare等人最近提出的一种代数结构，它统一了并发编程的规律。CKA的统一力量主要依赖于所谓的交换定律，该定律描述了并发和顺序组合操作符如何互换。本文在前人对真并发性理论研究的基础上，利用最小不动点算子扩展了Gischer的pomset模型，并利用Ésik的单调双射态射形式化了程序精化关系，构造了CKA的偏序模型.当我们想证明和反驳带有循环的并发程序的性质时，这种模型的存在是相关的。特别是，它提供了一个基础的分析程序，同时访问放松的内存中所示的后续工作。
2014-10-17 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
Verification of Distributed Quantum Protocols
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数、APTC到局部进程代数的推广。在量子过程代数中，有几个著名的工作，我们曾经在ACP \cite{ACP}和概率过程代数的框架下做过一些工作，将量子计算和经典计算统一起来。现在，是时候利用真正的具有局部性的并发进程代数来建模量子计算并在本书中统一量子计算和经典计算了。由于这项工作是局部性的，因此适合于验证量子通信协议的分布。
2021-10-25 cs.LO
