arXiv 1507.033442015-07cs.LO

Reversible Quantum Process Algebra with Guards

Yong Wang

备注：: 238 pages, 23 figures, 98 tables. arXiv admin note: substantial text overlap with arXiv:1501.05260, arXiv:1404.0665, arXiv:1811.01070

英文摘要：

Truly concurrent process algebras are generalizations to the traditional process algebras for true concurrency, CTC to CCS, APTC to ACP, $π_{tc}$ to $π$ calculus, APPTC to probabilistic process algebra. And we also did some work on reversible process algebra and probabilistic truly concurrent process algebra. In this book, we utilize reversible truly concurrent process algebras APRTC and probabilistic process algebra APPTC to model quantum computing and unify quantum and classical computing.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

带对合的笛卡尔非保护递归

Non-Cartesian Guarded Recursion with Daggers

University of Edinburgh（爱丁堡大学）

本文将对合范畴中的保护递归框架扩展到非笛卡尔环境，通过构造合适的范畴并研究其与对合范畴结构的交互，为高阶可逆编程语言添加保护递归特性。

2026-07-01cs.LOcs.PLmath.CT

On infinite guarded recursive specifications in process algebra

In most presentations of ACP with guarded recursion, recursive specifications are finite or infinite sets of recursion equations of which the right-hand sides are guarded terms. The completeness with respect to bisimulation equivalence of the axioms of ACP with guarded recursion has only been proved for the special case where recursive specifications are finite sets of recursion equations of which the right-hand sides are guarded terms of a restricted form known as linear terms. In this note, we widen this completeness result to the general case.

2020-05-02cs.LO

Truly Concurrent Process Algebra Is Reversible

Based on our previous process algebra for concurrency APTC, we prove that it is reversible with a little modifications. The reversible algebra has four parts: Basic Algebra for Reversible True Concurrency (BARTC), Algebra for Parallelism in Reversible True Concurrency (APRTC), recursion and abstraction.

2018-09-29cs.LO

Truly Concurrent Pi-Calculi with Reversibility, Probabilism and Guards

The well-known process algebras, such as CCS, ACP and $π$-calculus, capture the interleaving concurrency based on bisimilarity semantics. We did some work on truly concurrent process algebras, such as CTC, APTC and $π_{tc}$, capture the true concurrency based on truly concurrent bisimilarities, such as pomset bisimilarity, step bisimilarity, history-preserving (hp-) bisimilarity and hereditary history-preserving (hhp-) bisimilarity. Truly concurrent process algebras are generalizations of the corresponding traditional process algebras. In this book, we introduce reversibility, probabilism, and…

2021-08-24cs.LO

Truly Concurrent Calculi with Reversibility, Probabilism and Guards

2021-08-15cs.LO

An Algebra of Reversible Computation

Process algebra ACP based on the interleaving semantics can not be reversed. We design a reversible version of APTC called RAPTC. It has algebraic laws of reversible choice, sequence, parallelism, communication, silent step and abstraction, and also the soundness and completeness modulo strongly forward-reverse truly concurrent bisimulations and weakly forward-reverse truly concurrent bisimulations.

2018-05-02cs.LO

更多相关论文收起更多论文

Reversible Quantum Process Algebra

Truly concurrent process algebras are generalizations to the traditional process algebras for true concurrency, CTC to CCS, APTC to ACP, $π_{tc}$ to $π$ calculus , APPTC to probabilistic process algebra. And we also did some work on reversible process algebra and probabilistic truly concurrent process algebra. In this book, we utilize reversible truly concurrent process algebras APRTC and APPTC to model quantum computing and unify quantum and classical computing.

2021-08-05cs.LO

Reversible Truly Concurrent Process Algebra

We design a reversible version of truly concurrent process algebra CTC which is called RCTC. It has good properties modulo several kinds of strongly forward-reverse truly concurrent bisimulations and weakly forward-reverse truly concurrent bisimulations. These properties include monoid laws, static laws, new expansion law for strongly forward-reverse truly concurrent bisimulations, τlaws for weakly forward-reverse truly concurrent bisimulations, and congruences for strongly and weakly forward-reverse truly concurrent bisimulations.

2018-05-03cs.LO

Reversible Barbed Congruence on Configuration Structures

A standard contextual equivalence for process algebras is strong barbed congruence. Configuration structures are a denotational semantics for processes in which one can define equivalences that are more discriminating, i.e. that distinguish the denotation of terms equated by barbed congruence. Hereditary history preserving bisimulation (HHPB) is such a relation. We define a strong back and forth barbed congruence using a reversible process algebra and show that the relation induced by the back and forth congruence is equivalent to HHPB, providing a contextual characterization of HHPB.

2015-08-20cs.LO

A complete axiomatisation of reversible Kleene lattices

We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.

2019-02-21cs.FLcs.LO

Reversible monadic computing

We extend categorical semantics of monadic programming to reversible computing, by considering monoidal closed dagger categories: the dagger gives reversibility, whereas closure gives higher-order expressivity. We demonstrate that Frobenius monads model the appropriate notion of coherence between the dagger and closure by reinforcing Cayley's theorem; by proving that effectful computations (Kleisli morphisms) are reversible precisely when the monad is Frobenius; by characterizing the largest reversible subcategory of Eilenberg-Moore algebras; and by identifying the latter algebras as measureme…

2015-05-16cs.LOmath.CT

无跳跃星代数的一般完备性定理

A General Completeness Theorem for Skip-free Star Algebras

本文针对以等式理论T为参数的分支过程代数，在特定条件下公理化双相似性，抽象了早期论证，为概率分支的无跳跃过程代数提供新完备性定理并涵盖已有结果。

2025-01-25cs.LO

效应的语义学：中心性、量子控制与可逆递归

The Semantics of Effects: Centrality, Quantum Control and Reversible Recursion

本文研究程序语义学，通过单子中心刻画效应交换性，为可逆量子语言建立完备指称语义，并利用范畴论为可逆递归提供语义基础，同时探讨高阶量子控制的局限与前景。

2024-06-05cs.LOcs.PLmath.CT

Enabling Replications and Contexts in Reversible Concurrent Calculus

Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions that are usual in ''forward-only'' process algebras, such as replication or context. They also seem to fail to leverage possible new features stemming from reversibility, such as the capacity of distinguishing between multiple replications, based on how they replicate the memory mechanism allowing to reverse the computation…

2021-03-29cs.LOmath.LO

Lambda-calculus and Reversible Automatic Combinators

In 2005, Abramsky introduced various linear/affine combinatory algebras of partial involutions over a suitable formal language, to discuss reversible computation in a game-theoretic setting. These algebras arise as instances of the general paradigm explored by Haghverdi (Abramsky's Programme), which amounts to defining a lambda-algebra starting from a GoI Situation in a traced symmetric monoidal category. We investigate this construction from the point of view of the model theory of lambda-calculus. We focus on the strictly linear and affine parts of Abramsky's Affine Combinatory Algebras, ske…

2018-08-30cs.FLcs.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-18cs.LO

Causal Consistent Replication in Reversible Concurrent Calculi

Reversible computation is key in developing new, energy-efficient paradigms, but also in providing forward-only concepts with broader definitions and finer frames of study.Among other fields, the algebraic specification and representation of networks of agents have been greatly impacted by the study of reversible phenomena: reversible declensions of the calculus of communicating systems (CCSK and RCCS) offer new semantic models, finer congruence relations, original properties, and revisits existing theories and results in a finer light.However, much remains to be done: concurrency, a central n…

2021-10-25cs.DCcs.LO

revTPL：可逆时序进程语言

revTPL: The Reversible Temporal Process Language

本文提出 revTPL，将因果一致可逆性引入带离散时间和超时算子的时序进程语言 TPL，证明其满足因果一致可逆演算性质，并说明其可视为带时间的可逆 CCS 扩展。

2024-01-30cs.LOcs.PL

Secure Process Algebra

Based on our previous work on truly concurrent process algebras APTC, we use it to verify the security protocols. This work (called Secure APTC, abbreviated SAPTC) have the following advantages in verifying security protocols: (1) It has a firmly theoretic foundations, including equational logics, structured operational semantics, and axiomatizations between them; (2) It has rich expressive powers to describe security protocols. Cryptographic operations are modeled as atomic actions and can be extended, explicit parallelism and communication mechanism to modeling communication operations and p…

2021-10-25cs.CRcs.LO