Open Bisimulation for Quantum Processes
量子过程描述了可能涉及量子信息的并发通信系统。我们提出了一个开放互模拟量子过程的概念，并表明，它提供了一个健全的和完整的证明方法，量子过程之间的自然扩展行为等价。我们还给出了一个模态特征的开放互模拟，通过扩展的Hennessy-Milner逻辑的量子设置。
2012-01-02 cs.LO quant-ph
Proving Linearizability via Branching Bisimulation
线性化和进度属性是并发对象的关键正确性概念。然而，模型检验线性化遭受PSPACE-硬度的微量夹杂物问题。本文提出了利用分支互模拟，一个基本的语义等价关系的进程代数，可以有效地计算，在检查这些属性。一个商的建设提供了巨大的状态空间减少的结果。我们确认所提出的方法的优势，对十几个基准问题。
2016-09-30 cs.LO cs.PL
Nash Equilibrium and Bisimulation Invariance
本文发现标准策略模型下互模拟不保持纳什均衡存在性，提出三种保持该性质的策略模型，为策略推理逻辑提供新语义基础并研究受限场景。
2019-09-19 cs.LO
Theories of Truly Concurrent Processes
本文基于Hennessy的工作，为真正并发过程代数建立测试语义，继承操作语义、公理语义和指称语义的三位一体。
2026-08-20 cs.LO
A Concurrent Calculus with Atomic Transactions
软件事务存储器（STM）模型是一种用于控制对资源的并发访问的原始方法，而不需要显式的基于锁的同步机制。STM的一个关键特性是提供了一种方法来将原子块内的读写操作序列分组，类似于数据库事务，其整个效果应该原子地发生。在本文中，我们调查STM从进程代数的角度来看，定义了一个扩展的异步CCS与原子块的行动。我们的目标是不仅要设置一个正式的推理STM实现的基础，但也要了解这个模型与其他并发控制机制。我们还将此演算视为使用原子事务扩展流程演算的测试平台。这是一个有趣的研究方向，因为在大多数情况下，将事务与进程演算混合在一起的实际工作考虑补偿事务，这是一个缺乏所有众所周知的ACID属性的模型。我们发现，除了原子事务的结果在一个非常富有表现力的演算，足以轻松地编码其他并发原语，如守护选择和多集同步（à la join演算）。我们的编码的正确性证明使用一个合适的概念互模拟等价。然后应用等价性来证明有趣的“交易定律”，并获得交易的简单范式。
2006-10-24 cs.DC cs.LO
Scalable Minimization Algorithm for Partial Bisimulation
Eindhoven University of Technology（埃因霍温理工大学）
提出一种高效算法计算标记迁移系统的部分互模拟预序和等价，通过利用互模拟动作子集实现可扩展的最小化。
2012-07-10 cs.LO cs.SY eess.SY
Approximate Bisimulation Minimisation
我们提出了多项式时间算法，以尽量减少标记马尔可夫链的转移概率是不知道的，已经扰动，或只能通过采样。我们的算法是基于一个新的概念的近似互模拟商，通过集中在一起的状态是完全bisimilarily在一个轻微的扰动系统。我们目前的实验表明，我们的算法是能够恢复未扰动系统的互模拟商的结构。
2021-10-01 cs.FL cs.LO
Symbolic bisimulation for quantum processes
利用文献中提出的互模拟概念，为了检验两个量子过程是否互相似，我们必须用任意量子态实例化它们的自由量子变量，并验证结果组态的互相似性。这使得从算法的角度来看，检查双相似性是不可行的，因为量子态构成了一个连续统。在本文中，我们直接在量子操作层次上引入了一种量子过程的符号操作语义，它允许我们描述量子过程之间的互模拟，而无需求助于量子态。我们表明，这里定义的符号互模拟是等价的开放互模拟量子过程在以前的工作中，当考虑强互模拟。提出了一种符号基双相似性检验算法。基于Hennessy-Milner逻辑对量子过程的扩展，我们给出了量子双相似性的模态逻辑刻画。
2012-02-21 cs.LO
An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
我们提供了一个新的算法来确定口吃等价与时间复杂度$O(m \log n)$，其中$n$是状态的数量和$m$是一个Kripke结构的转换的数量。该算法也可用于确定$O(m(\log |\mathit{Act}|+ \log n))$时间上的分支互模拟，其中$\mathit{Act}$是标记迁移系统中的动作集。从理论上讲，我们的算法大大提高了现有的算法，所有的时间复杂度$O(m n)$在最好的。而且，它具有更好或相等的空间复杂度。实际结果证实了这些发现，表明我们的算法可以优于现有的算法的数量级，特别是当Kripke结构的大小是大的。我们的算法的重要性远远超出了口吃等价和分支互模拟。已知的$O(m n)$算法已经比大多数其他算法更有效（在空间和时间上），以确定行为等价（包括弱互模拟），因此它经常被用作一个必不可少的预处理步骤。这种新的算法使得使用口吃等价和分支互模拟更有吸引力。
2016-01-07 cs.DS cs.LO
Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States
提出了一种基于马尔可夫自动机的弱互模拟判定算法。为此，定义了消失状态的不同概念（从广义随机Petri网领域已知的概念）。消失状态是必不可少的相关概念（基于状态）天真的弱互模拟和（基于分布）弱互模拟。本文提出的互模拟算法遵循划分-细化方案，具有指数时间复杂度。
2014-04-30 cs.FL cs.LO
Distributed Branching Bisimulation Minimization by Inductive Signatures
提出了一种新的状态空间最小化模分支互模拟分布式算法。像它的前身一样，它使用签名进行细化，但细化过程和签名已经过优化，以利用输入图不包含tau循环的事实。细化过程中的优化旨在减少所需的迭代次数和内存需求。在前一种情况下，我们不能证明有改进，但我们的实验表明，在许多情况下，迭代次数较少。在后一种情况下，我们可以证明，新算法的最坏情况下的内存使用是线性的状态空间的大小，而旧算法有一个二次上限。本文包括新算法的正确性证明和一些实验的结果，比较旧的和新的算法的性能。
2009-12-13 cs.DC cs.DM cs.DS
Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs
Puggelli等人最近研究了具有凸不确定性的MDP的PCTL性质的验证。然而，模型检验算法通常遭受状态空间爆炸。在本文中，我们解决概率互模拟，以减少这样的MDP的大小，同时保持PCTL性能，它满足。我们讨论了在文献中研究的模型中的不确定性的不同解释，并导致两种不同的互模拟定义。我们给出了算法来计算这些互模拟的时间多项式的模型的大小和指数的不确定分支的同分性。最后，我们通过一个案例研究表明，在实践中的大型模型可以有小的分支，并通过我们的方法可以实现大量的状态空间减少。
2014-04-10 cs.FL cs.LO
Lowerbounds for Bisimulation by Partition Refinement
本文研究了标号迁移系统上基于划分细化判定互模拟的算法时间下界，证明顺序算法下界为 $Ω((m+n)\log n)$，并行算法为 $Ω(n)$，并指出现有线性技术无法加速通用算法。
2023-05-10 cs.LO
Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods
我们引入多项式耦合，概率耦合的推广，开发一个算法的等价关系的计算，可以被解释为一个提升的概率互模拟多项式微分方程，一个无处不在的模型的动力系统在科学和工程。该算法具有多项式时间的复杂性，并补充了经典的分区细化方法，因为：（a）它实现了系统的本地探索，可能产生的等价，不一定涉及整个系统的检查微分方程;（b）它可以增强技术;（c）它允许规范的对不应该被包括在输出中。使用一个原型，这些优势被证明从系统生物学的应用程序模型简化和比较的案例研究。值得注意的是，我们报告四个数量级较小的运行时间比分区细化方法时反驳马尔可夫链之间的等价性。
2021-04-27 cs.LO
Computing Stuttering Simulations
口吃互模拟是一个著名的行为等价，它保留了CTL-X，即没有下一次操作符X的CTL。相应地，口吃模拟前序诱导了一个更粗糙的行为等价，它保留了存在片段ECTL-{X，G}，即没有下一次X和全局G算子的ECTL。虽然口吃互模拟等价可以通过著名的Groote和Vaandrager的[1990]算法计算，但据我们所知，没有计算口吃模拟前序和等价的算法。本文针对有限状态系统提出了这样一种算法。
2009-04-09 cs.LO
An Operational Petri Net Semantics for the Join-Calculus
我们提出了一个并发操作Petri网语义的连接演算，指定并发和分布式系统的进程演算。在系统规范和实际实现之间经常存在差距，这是由规范方面的同步假设和实现中的异步交互组件造成的。联合演算是有希望的，以减少这一差距，提供一个抽象的规约语言，这是异步分布。经典的过程语义通过交错的方式建立了一个实际上独立的动作的隐式顺序。连接演算的语义也是如此。为了捕获这样的独立动作，基于步骤的语义，例如，如在Petri网上定义的。我们的Petri网语义的连接演算诱导步骤的行为在一个自然的方式。我们证明我们的语义行为等价于原来的连接演算语义的互模拟。我们将讨论如何加入特定的假设影响现有的概念，基于Petri网的可分布性。
2012-08-14 cs.LO
On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics
University of Antwerp（安特卫普大学）
本文研究了鲁棒马尔可夫决策过程在多面体不确定性集下的复杂性，证明了(s,a)-矩形RMDP的鲁棒策略评估在P中，阈值问题在NP中，同时通过将奇偶游戏和马尔可夫过程状态间的仿射度量归约到RMDP阈值问题，建立了下界。
2026-06-25 cs.LO
Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms
本文提出用可见性关系公理化替代线性化点，通过形式化事件间协助请求的分离性质，为Harris等人的RDCSS、MCAS等基于描述符的并发协助算法构造了可复用、声明式的可线性化证明。
2023-07-10 cs.DC cs.LO
Enabling Replications and Contexts in Reversible Concurrent Calculus
现有的形式主义的代数规范和表示网络的可逆代理遭受一些缺点。尽管多次尝试，通信系统演算（CCS）的可逆变格并没有提供令人满意的适应的概念，通常在“向前”的过程代数，如复制或上下文。它们似乎也未能利用源于可逆性的可能的新功能，例如基于它们如何复制允许反向计算的内存机制来区分多个复制的能力。现有的形式主义不允许在也有过去的上下文中执行过程的“热插拔”。最后，它们假设存在“永远新鲜”的键或标识符，如果实现得不好，可能会导致不必要的瓶颈和涉及所有线程的查找。在本文中，我们开始调查这些问题，首先设计了一个进程代数赋予的机制来生成标识符，而不需要咨询其他线程。我们使用这种演算来重铸CCS中的非确定性的可能表示，并作为副产品建立一个简单而直接的并发定义。我们的可逆演算，然后证明满足预期的属性，并允许精确地布局不同的表示复制的过程与内存。我们还观察到，迄今为止定义的可逆互模拟都不是我们的“可逆”上下文概念下的同余。
2021-03-29 cs.LO math.LO
Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence
如果一个给定的配置的下推自动机（PDA）是双相似的一些（未指定）有限状态过程的问题是可判定的。的可判定性证明的框架中的一阶文法，这是由有限的标签规则，重写根的一阶项。该框架相当于PDA，其中也允许确定性（即无选择性）ε-步骤，即Sénizergues展示了一个决定双相似性的复杂过程（1998，2005）的模型。这样的过程在这里被用作算法的黑盒部分。这一结果扩展了Stearns（1967）提出的确定性PDA的正则性问题的可判定性，后来Valiant（1975）在复杂性方面进行了改进。非确定性PDA的可判定性问题，在这里得到了肯定的回答，一直是开放的（如所指出的，例如，作者：Broadbent和Göller，2012年）。
2019-09-23 cs.FL cs.LO
Minimization of Dynamical Systems over Monoids
本文针对交换幺半群上的动力系统提出广义前向互模拟（GFB）及划分细化算法，以计算最粗等价关系，并应用于布尔网络和加权网络，实现非线性约简与分析加速。
2023-05-08 cs.LO q-bio.QM
Visibility Reasoning for Concurrent Snapshot Algorithms
可见性关系是由Henzinger等人提出的，作为一种抽象，用于证明并发算法的线性化，从而获得模块化和可重用的证明。这与基于展示算法的线性化点的常规方法相反。在本文中，我们应用可见性关系开发模块化的证明三个优雅的并发快照算法的Jayanti。证明被签名分成抽象级别增加的组件;更高抽象级别的组件被共享，即，它们同时应用于所有三种算法。重要的是，界面特性在数学上捕捉到了Jayanti最初的直觉，而这些直觉以前只是非正式地给出的。
2021-11-08 cs.LO cs.PL
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
我们提出了一个轻量级的方法，以霍尔式规范的细粒度并发，基于时间戳的历史，抽象捕捉原子的程序状态的变化的概念。我们的关键观察是，历史形成了一个部分交换幺半群，并发资源的表示的基本结构。这种洞察力为我们提供了一种统一的机制，使我们能够像对待分离逻辑中的堆一样对待历史。例如，两者都服从相同的断言逻辑和推理规则（例如，框架规则）。此外，通常适用于堆的所有权转移的概念在历史学中也有对应的概念。它可以用来正式表示帮助-一个并发算法的重要设计模式，一个线程可以代表另一个线程执行代码。历史方面的规范自然地抽象了粒度，在这个意义上，复杂的细粒度算法可以被赋予与简化的粗粒度算法相同的规范，使它们同样方便客户端推理。我们说明了我们的方法上的一些例子，并验证所有的Coq。
2014-10-01 cs.LO
Strategy Improvement for Concurrent Safety Games
我们考虑图上的并发博弈。在每一轮游戏中，每个玩家同时独立地选择一步棋，这些棋步共同决定了向后继状态的过渡。两个基本目标是安全性目标：“永远停留在状态集合F中”，以及它的对偶，可达性目标，“达到状态集合R”。本文提出了一种策略改进算法，用于计算并发安全博弈的值，即参与人1执行安全目标的最大概率。该算法产生一个序列的玩家-1的策略，以确保获胜的概率，单调收敛到安全游戏的值。这一结果的意义是双重的。首先，虽然策略改进算法是已知的马尔可夫决策过程和回合制游戏，以及并发可达性游戏，这是第一个并发安全游戏的策略改进算法。其次，也是最重要的，改进算法提供了一种从下面近似并发安全博弈的值的方法（已知的值迭代算法从上面近似值）。因此，当与值迭代算法，或与可达性游戏的策略改进算法一起使用时，我们的算法导致计算可达性和安全游戏的值的收敛上界和下界的第一个实用算法。
2008-04-29 cs.GT cs.LO
An Epistemic Perspective on Consistency of Concurrent Computations
并发计算的一致性属性，例如，顺序一致性、可线性化性或最终一致性对于设计正确的并发算法是必不可少的。在本文中，我们提出了一个逻辑形式化的一致性属性，是基于一个标准的逻辑知识。我们的形式化提供了一个声明性的角度来看，什么是一致性要求，并提供了一些有趣的统一见解不同的外观属性。
2013-05-10 cs.LO
On the formalization of the notion of a concurrent algorithm
Informatics Institute, Faculty of Science, University of Amsterdam（阿姆斯特丹大学科学学院信息学研究所）
本文旨在形式化并发算法的概念，通过定义并发原算法及其等价关系，探讨并发与非确定性之间的联系。
2025-10-20 cs.CC cs.DS cs.LO
Termination Criteria for Solving Concurrent Safety and Reachability Games
我们考虑图上的并发博弈。在游戏的每一轮，每个玩家同时独立地选择一步棋，这些棋步共同决定了向后继状态的过渡。两个基本目标是永远停留在一组给定状态的安全性目标，以及它的对偶，到达一组给定状态的可达性目标。本文提出了一种计算并发安全对策值的策略改进算法，即局中人1实现安全目标的最大概率。该算法产生一个序列的玩家-1的策略，以确保获胜的概率，单调收敛到安全游戏的值。我们的结果是显着的，因为策略改进算法提供了，第一次，一种方法来近似值的并发安全游戏从下面。由于值迭代算法，或可达性游戏的策略改进算法，可以用来近似相同的值从上面，这两种算法的组合产生一种方法，用于计算收敛序列的上限和下限的并发可达性和安全游戏的值。以前的方法只能从一个方向近似这些游戏的值，并且由于没有已知的收敛速度，它们没有提供解决这些游戏的实用方法。
2008-09-23 cs.GT cs.LO
Learning to Prove Safety over Parameterised Concurrent Systems (Full Version)
我们重新审视了经典的问题，证明安全的参数化并发系统，即，用有限（符号）方法表示的有限状态并发系统的无限族。这样的无限族的一个例子是一个用餐哲学家协议，具有任意数量的n个进程（n是定义无限族的参数）。常规模型检验是一种用于参数化并发系统建模的通用框架，其中无限组的配置（分别为：transitions）由正则集（resp.常规换能器）。虽然在常规的模型检验框架中验证安全属性通常是不可判定的，但是在过去的15年中已经开发了许多复杂的半算法，可以在许多实际情况中成功地证明安全性。在本文中，我们提出了一个简单的解决方案，利用Angluin的经典L* 算法（及其变体）来合成正则归纳不变量。我们提供了一个终止保证时，从一组给定的初始配置可达的配置集是定期的。我们已经测试了L* 算法的标准（以及新的）的例子，在定期的模型检验，包括用餐哲学家协议，用餐密码协议，和几个互斥协议（如面包店，伯恩斯，Szymanski，和德国）。我们的实验表明，尽管我们的解决方案的简单性，它可以执行至少以及现有的半算法。
2017-10-03 cs.FL cs.LO cs.PL
