Logics and Games for True Concurrency
我们研究了基于过渡系统，Petri网和事件结构的各种偏序模型的并发性的基本数学性质，并表明这些系统的并发行为可以通过两个简单的和一般的对偶局部行为以统一的方式捕获。这种对偶性被用来定义新的μ演算和逻辑游戏，用于分析具有偏序语义的并发系统。这项工作的一些结果是：一些mu-演算的定义，在某些类的系统，诱导相同的标识作为一些最有名的互模拟等价的并发性;和定义（无限）高阶逻辑游戏的互模拟和模型检查，其中的球员的游戏给予（本地）一元二阶权力的一组元素，他们被允许发挥。更具体地说，我们表明，我们的游戏是健全的和完整的，因此，确定;此外，它们是可判定的有限情况下，并支持新的决策程序的互模拟和模型检查。由于这些mu演算和逻辑游戏概括了著名的不动点逻辑和博弈论决策程序的并发系统与交织语义，本文的结果给出了一些基础的设计一个基于逻辑的，博弈论的框架研究，在一个统一的方式，几个并发系统，无论他们是否有交织或偏序语义。
2010-11-04 cs.LO
The Glory of the Past and Geometrical Concurrency
本文有助于对并发的几何模型的一般理解，被命名为高维自动机（HDAs）的普拉特。特别是，我们调查模态逻辑等模型和它们的表达能力方面的互模拟，可以被捕获。并发的几何模型之所以有趣，主要有两个原因：它的通用性和可表达性，以及捕获自动并发和动作细化的自然方式。然而，这种模型的逻辑没有得到很好的研究，其中一个简单的，但足够的，模态逻辑在HDAs只是最近才被引入。由于这种模态逻辑，有两个存在模态，期间和之后，只捕获分裂互模拟，这是相当低的范Glabbeek和Vaandrager的频谱，直接的问题是什么小的扩展，这个逻辑可以捕获更细粒度的遗传历史保持互模拟（hh）？作为回应，本文中的工作提供了几个见解。一个是HDA的几何方面使得可以用于捕获hh互模拟，这是一种不使用事件变量的标准模态逻辑，与我们比较的两种逻辑（在表达性较低的模型上）相反。我们在这里研究的逻辑使用标准的过去模态，并扩展了以前引入的逻辑（称为HDML），只有向前的，动作标记的模态。此外，我们试图通过引入一个相关的模型，我们称之为ST-配置结构，它扩展了van Glabbeek和Plotkin的配置结构，以更好地理解上述问题。我们将这个模型与HDAs联系起来，并根据这个新模型重新定义和证明了以前的结果。这些提供了一个不同的观点，为什么过去的模态和几何并发捕获遗传历史保持互模拟。还获得了其他相关的见解。
2012-06-14 cs.LO
Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
KTH Royal Institute of Technology（皇家理工学院）
提出一种过去时间时态认知逻辑，用于形式化共享内存并发中的基于局部视图的推理，并在Peterson互斥算法上验证其有效性，同时展示该逻辑如何嵌入依赖-保证推理。
2026-06-24 cs.LO
Convolution, Separation and Concurrency
卷积的概念提出的背景下，正式的幂级数连同提升结构表征代数的这种系列，这通常是quantale。一些例子支持了这些构造的普遍性，最突出的例子是分离逻辑，其中卷积是断言Quantale中的分离合取;区间逻辑，其中卷积是斩波操作;和流区间函数，其中卷积用于分析动态或实时系统的轨迹。一个霍尔逻辑是在幂级数Quantale上以通用的方式构造的，它适用于这些例子中的每一个。在许多情况下，卷积的可交换概念具有作为并发操作的自然解释。
2014-10-15 cs.FL cs.LO
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
本文提出ReLoC Reloaded，一种基于Iris框架的机械化关系分离逻辑，用于证明高阶状态与细粒度并发程序的精化关系，并扩展了逻辑原子关系规范，支持预言变量以增强实用性。
2021-07-20 cs.LO cs.PL
Dynamic Epistemic Logic with Communication Actions
这项工作提出了一个动态认知逻辑与通信动作，可以同时进行。与Ditmarsch、Hoek和Kooi提出的并发认知动作逻辑不同，这里的并发机制是所谓的真正并发，这里我们使用的是基于进程演算的方法，如CCS和CSP，以及动作模型逻辑。我们的方法使得证明的可靠性，完整性和可判定性，不同于其他的方法。我们提出了一个公理化，并表明，证明的合理性，完整性和可判定性，可以使用减少的方法。
2019-02-04 cs.LO
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
作为会话的命题（Propositions-as-Sessions）的出现，为消息传递并发奠定了逻辑基础，它是线性逻辑命题与并发进程会话类型之间的Curry-Howard对应。这种方法的核心是由线性逻辑预示的资源消耗范式。在本文中，我们研究了一个新的点，在设计空间的会话类型系统的消息传递并发程序。我们确定O 'Hearn和Pym的逻辑束的影响（BI）作为一个富有成效的基础解释的逻辑作为一个并发程序设计语言。这导致了对非线性资源的处理，这与基于线性逻辑的现有方法完全不同。我们介绍了一个新的$π$ -演算会话，称为$π$ BI，其最显着的特点是一个构造称为产卵，它表达了新的形式的共享，诱导BI的结构原则。我们说明了$π$ BI的表现力，并奠定了其基本理论：类型保存，死锁自由和弱规范化的结果良好的类型化进程;一个操作上健全和完整的仿射$λ$ -演算的类型化编码;和一个非干扰的结果访问资源。
2022-09-12 cs.LO cs.PL
Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
University of Twente（特温特大学）；TU Delft（代尔夫特理工大学）；Eindhoven University of Technology（埃因霍温理工大学）
本文提出在VerCors中编码弱内存并发的方案，通过扩展原子操作支持并引入协议自动机概念，实现基于许可的分离逻辑，用于验证弱内存并发程序的正确性。
2026-04-22 cs.LO
Towards Concurrent Quantitative Separation Logic
本文提出并发定量分离逻辑，将定量分离逻辑与并发分离逻辑结合，用于验证并发、指针和随机化程序实现后置条件的概率下界。
2024-09-30 cs.LO cs.PL
Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics
本卷包含第25届并发表达性国际研讨会和第15届结构操作语义研讨会（EXPRESS/SOS 2018）的会议记录，该研讨会于2018年9月3日在中国北京举行，作为第29届并发理论国际会议CONCUR 2018的附属研讨会。EXPRESS研讨会旨在汇集对各种形式系统和语义概念的表达感兴趣的研究人员，特别是在并发领域。传统上，他们的重点是比较编程概念（如并发、函数、命令、逻辑和面向对象编程）和计算的数学模型（如进程代数、Petri网、事件结构、模态逻辑和重写系统）之间的相对表达能力。SOS研讨会的目的是成为一个论坛的研究人员，学生和从业人员感兴趣的新发展，未来的调查方向，在结构操作语义领域。SOS研讨会系列的具体目标之一是在从事SOS理论和实践工作的并发和程序设计语言社区之间建立协同作用。自2012年以来，EXPRESS和SOS社区组织了一个年度EXPRESS/SOS联合研讨会，讨论计算数学模型的表达能力以及系统和编程概念的形式语义。
2018-08-24 cs.LO cs.PL
The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices
本文的动机是希望研究包管理使用的工具包的语义的函数式语言。正如它所揭示的那样，这与并发计算的语义密切相关。我们制作的模型不仅具有理论意义，而且可以进行分析和计算。这项工作作出了一些相关的贡献。首先，它涉及分支依赖结构的规范，存在于从知识表示到包管理的领域，并发计算的语义规范。其次，它以精确的方式将依赖结构与格相关联，与特定的格子类建立完全对应。然后，它利用这一点作为一个关键的成分，再加上未得到充分重视的Bruns-Lakser完成，在相关的依赖结构，以区域设置-对象配备了拓扑和逻辑属性。然后，它提供了一个例子，说明这种属性的相互作用是如何使用的-使用依赖结构的拓扑属性来为相关区域设置的内部逻辑配备表示收缩关系（即“版本控制”）的模态。这种方法让我们看到链接（或者更确切地说，选择链接的对象，即“解决”）作为一种效果。最后，它讨论了这种结构可能涉及到复杂性理论中的重要问题，包括可满足性问题的解决方案。在此过程中，我们将看到这种方法如何与熟悉的对象相关，例如包版本策略，Merkle树，nix操作系统和分布式版本控制工具，如git。
2020-04-12 cs.LO math.LO
Comparing Session Type Systems derived from Linear Logic
本文严格比较了由线性逻辑的经典与直觉主义表述派生出的并发会话类型系统，开发了涵盖两者的 $π\mathsf{ULL}$ 系统作为参考框架，并基于局部性原则和进程组合形式分析了其差异。
2024-08-22 cs.LO
A proof-theoretic view on scheduling in concurrency
本文阐述了一种新的方法的问题的证明理论研究的并发交互称为“证据的时间表”。观察证明理论是非常适合于描述合流系统，而并发具有非确定性作为一个基本特征，我们开发了一个对应的证明提供了什么是需要并发系统合流，即调度。在我们的逻辑系统中，进程和验证者在证明语言的不同片段中显式地显示为证明，并且它们之间的切割消除确实对应于并发系统的执行。这种角色的分离为过程的指称语义提供了新的见解，也为将π演算转换为无前缀的形式主义（如solos）提供了新的方法，作为证明系统之间转换的操作对应物。
2014-09-13 cs.LO
Bisimulations and Logics for Higher-Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Warsaw（华沙大学）；EPITA Research Lab（EPITA研究实验室）
本文提出Ipomset模态逻辑，用于刻画HDAs中的路径双向模拟，并定义单元双向模拟及其与标准双向模拟的关系。
2024-11-11 cs.FL cs.LO
Concurrency in Boolean networks
布尔网络（BN）被广泛用于生物系统的定性动力学建模。除了确定每个组件相对于其调节器的状态的演变的逻辑规则之外，组件更新的调度可以对预测的行为产生显著影响。在本文中，我们将探讨使用读（上下文）Petri网（RPN）从并发理论的角度来研究动态的BN。在展示了RPN和BN之间的双向转换以及同步灵敏度结果之间的类比之后，我们说明了BN的常用更新模式可能会错过看似合理的行为，即，错误地得出不存在/不可能达到特定配置的结论。我们提出了一个编码的BN资本化的RPN语义，使更多的行为比广义异步更新模式。建议的编码确保了正确的抽象的任何多值细化，因为人们可能会期望实现时，没有假设其时间特征的生物系统建模。
2019-05-31 cs.DM cs.FL cs.LO
Extracting total Amb programs from proofs
Swansea University（斯旺西大学）；Kyoto University（京都大学）
本文提出CFP逻辑系统，用于从证明中提取可证明总正确性的非确定性和并发程序，通过域论语义验证提取程序的正确性，并展示了一个将无限Gray码转换为符号数字表示的非确定性程序。
2026-10-26 cs.LO
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
本文提出Actris 2.0，一种基于会话类型的分离逻辑，用于在混合并发范式下证明消息传递程序的功能正确性，并通过子协议增强异步推理，已在Coq中机械化验证。
2022-06-08 cs.LO cs.PL
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
Quantum Petri Nets with Event Structures semantics
针对量子并发领域缺乏类似经典佩特里网的规范模型问题，本文引入具有量子赋值的量子佩特里网（QPNs），定义局部量子发生网（LQONs）并构建组合框架，为量子并发建立语义基础。
2025-08-20 cs.LO quant-ph
Quantum Petri Nets with Event Structure semantics
针对量子并发缺乏严格语义与展开理论的问题，提出与量子事件结构语义兼容的量子Petri网（QPNs），通过定义局部量子发生网、构建展开语义及组合框架，建立了语义严谨的量子并发模型，桥接了Petri网理论与量子编程。
2025-09-17 cs.LO quant-ph
Around Classical and Intuitionistic Linear Processes
本文通过从CLL到ILL的翻译，基于类型化观察等价性，以完全抽象结果回答了经典与直觉主义线性逻辑并发类型系统之间的关系问题，揭示了它们之间缺失的形式化联系。
2024-07-22 cs.LO
Temporal Planning via Interval Logic Satisfiability for Autonomous Systems
The University of Melbourne（墨尔本大学）；The University of Toronto（多伦多大学）；Monash University（莫纳什大学）
本文提出以 Allen 区间逻辑表达动作与流的区间关系，并构建 CP 规划图处理复杂并发，实验显示其在案例研究中优于 PDDL 2.1 规划器。
2024-06-14 cs.AI cs.LO cs.SY
Foundations of logic programming in hybrid-dynamic quantum logic
本文提出一种简单且富有表达力的混合动态逻辑用于描述量子程序，研究其中的 Horn 子句并证明初始语义定理，进而通过证明 Herbrand 定理变体奠定了该逻辑片段中量子程序逻辑编程的基础。
2024-06-04 cs.LO
A logical analysis of entanglement and separability in quantum higher-order functions
我们提出了一个函数量子计算语言的逻辑可分性分析。这种逻辑的灵感来自于以前的作品的逻辑分析别名的命令式函数程序。这两种分析有着显著的相似之处，因为它们都是高度非组合的。量子设置更难处理，因为它引入了非确定性，从而大大修改了逻辑断言的语义和有效性。这种逻辑是纠缠/可分性分析的第一个建议，处理功能量子程序设计语言与高阶功能。
2008-01-04 cs.LO
A Theory of Computation Based on Quantum Logic (I)
经典计算理论背后的（Meta）逻辑是布尔（二值）逻辑。量子逻辑是由Birkhoff和von Neumann在60多年前提出的量子力学逻辑。布尔逻辑和量子逻辑之间的主要区别是后者一般不享有分配性。近年来量子计算的迅速发展促使我们建立基于量子逻辑的计算理论。本文件是这样一个新的理论的第一步，它侧重于最简单的计算模型，即有限自动机。研究发现，自动机的许多性质的普遍有效性在很大程度上依赖于底层逻辑的分布性。这表明这些性质在量子逻辑领域并不普遍成立。另一方面，我们证明了它们的局部有效性可以通过对所考虑的自动机的（原子）陈述施加一定的可交换性来恢复。这揭示了经典计算理论和基于量子逻辑的计算理论之间的本质区别。
2004-03-29 cs.LO
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
我们提出了一个模型的子结构逻辑聚束的影响（BI），是适合于推理量子态。在我们的模型中，BI的分离合取描述了可分离的量子态。我们开发了一个程序逻辑，其中的前置条件和后置条件是描述量子态的BI公式-程序逻辑可以被看作是命令式量子程序的分离逻辑的对应物。我们练习逻辑证明量子一次性密码本和秘密共享的安全性，我们展示了如何使用程序逻辑来发现Google Cirq的变分量子算法（VQA）教程中的缺陷。
2021-01-30 cs.LO quant-ph
Quantum modal logic
本文形式化了最简形式的基于量子逻辑的模态逻辑，给出其关系语义与矢列演算并证明二者间的可靠性和完全性定理，为构建量子逻辑上的各类模态逻辑提供基础框架。
2025-11-13 cs.LO math.LO
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
抽象解释、霍尔逻辑和不正确（或反向霍尔）逻辑是静态分析计算机程序的强大技术。所有这些都已成功地扩展到量子设置，但在很大程度上是并行开发的。在本文中，我们研究这些技术之间的关系，在验证量子while程序的背景下，其中的抽象域和一组断言的量子状态是结构良好的。特别地，我们证明了任何完全的量子抽象解释都可以导出一个量子霍尔逻辑和一个量子不正确逻辑，这两个逻辑都是合理的和相对完备的。与文献中提出的逻辑不同，诱导逻辑系统是以向前的方式，使它们在某些应用中更有用。相反，任何健全的和相对完整的量子霍尔逻辑或量子不正确逻辑都导出一个完整的量子抽象解释。作为应用，我们证明了当局部子空间元组作为断言时，不存在任何可靠的、相对完备的量子霍尔逻辑或不正确逻辑.
2022-06-28 cs.LO quant-ph
The Third Life of Quantum Logic: Quantum Logic Inspired by Quantum Computing
我们首先讨论量子逻辑的历史，将其分为三个时代或生活。第一个生命与伯克霍夫和冯诺依曼的代数方法在20世纪30年代。第二次生命与试图将量子逻辑理解为始于20世纪50年代末并在20世纪70年代蓬勃发展的逻辑有关。第三次生命与量子逻辑的最新发展有关，这些发展来自于量子逻辑与量子计算的联系。我们讨论了我们自己的工作，将量子逻辑与量子计算联系起来（将量子逻辑视为存储量子比特的量子寄存器的逻辑），并对基于量子原理的数学进行了一些推测。
2013-02-14 cs.LO math.LO quant-ph
Exogenous Quantum Operator Logic Based on Density Operators
虽然量子逻辑已经提出了使用外生方法来推理封闭的量子系统，但从态逻辑的角度来看，基于密度算符而不是单位向量的量子逻辑是值得研究的。为了实现这一点，我们建立了一个基于密度算符的外生量子算符逻辑（EQOL），用于对开放量子系统进行推理。我们表明，这种逻辑是健全的和完整的。与外生量子命题逻辑一样，外生量子命题逻辑也是经典命题逻辑的外生扩展，用于描述基于密度算子的状态逻辑。作为其应用，我们通过推理和逻辑论证证实了贝尔态的纠缠性，并验证了基本BB 84协议存在窃听。作为开放量子系统的一种新的数学形式，我们引入了一个外生量子马尔可夫链（EQMC），它的量子态被标记为EQOL公式。然后，给出了一个例子来说明使用EQMC描述的广义量子回路程序的终止性验证问题。
2015-07-24 cs.LO quant-ph
Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs
需要一个带有量子变量的一阶逻辑作为断言语言，用于指定和推理量子程序的各种属性（例如正确性）。令人惊讶的是，这样的逻辑在文献中缺失，现有的一阶Birkhoff-von Neumann量子逻辑只处理经典变量和它们的量化。在本文中，我们填补了这一空白，通过引入一阶扩展的Birkhoff-von Neumann量子逻辑与泛量词和存在量词的量子变量。给出的例子表明，我们的逻辑特别适合于指定量子计算和量子信息中研究的一些重要性质。我们进一步将此逻辑作为断言逻辑纳入量子霍尔逻辑中，使其能起到类似于经典霍尔逻辑中的一阶逻辑和分离逻辑中的BI-逻辑的作用。特别是，我们展示了它如何可以用来定义和推导量子概括的一些适应规则，已被应用于显着简化验证的经典程序。预计本文中定义的断言逻辑-一阶量子逻辑与量子变量-可以与各种量子程序逻辑相结合，作为一个坚实的逻辑基础上，验证工具可以建立使用证明助手，如Coq和Isabelle/HOL。
2022-05-04 cs.LO cs.PL quant-ph
On Multiplicative Linear Logic, Modality and Quantum Circuits
一个逻辑系统，来自线性逻辑和称为QMLL的介绍，并显示能够捕获所有的酉量子电路。相反，任何证明都表明通过具体的GoI解释计算一些量子电路。通过赋予乘性线性逻辑以量子模态，得到了具有割消的系统QMLL。
2012-10-02 cs.LO quant-ph
Quantum Logic as Classical Logic
我们提出了一个语义表示的标准量子逻辑QL在一个经典的，正常的模态逻辑，这通过一个格嵌入正交模格到布尔代数与一个模态算子。因此，我们的经典逻辑是量子逻辑QL的一个完善。换句话说，我们驳斥了伯克霍夫和冯·诺依曼的经典论点，即量子力学的逻辑（形式特征）将是非经典的，以及普特南的论点，即量子逻辑（他的同类）将是一般命题推理的正确逻辑。量子力学的命题逻辑是模态的，但却是经典的，命题推理的正确逻辑不需要具有外向的量子特征。一个正常的必然模态足以捕捉量子实验中观察的主观性，这要归功于它未能在经典析取上分布。我们结果的关键是把量子否定转化为可观测性的经典否定。
2017-02-07 cs.LO math-ph math.LO
