Open Bisimulation for Quantum Processes
量子过程描述了可能涉及量子信息的并发通信系统。我们提出了一个开放互模拟量子过程的概念，并表明，它提供了一个健全的和完整的证明方法，量子过程之间的自然扩展行为等价。我们还给出了一个模态特征的开放互模拟，通过扩展的Hennessy-Milner逻辑的量子设置。
2012-01-02 cs.LO quant-ph
Bisimulation for quantum processes
在本文中，我们引入了一个新的概念，量子过程的概率互模拟，并证明它是全等的各种进程代数组合子，包括并行组合，即使经典和量子通信。我们还建立了一些基本的代数规律，这种互模拟。特别地，我们证明了量子过程的递归方程的解的唯一性，这为验证复杂的量子协议提供了一个强有力的证明技术。
2013-11-14 cs.LO quant-ph
A New Branching Bisimulation for Probabilistic Processes
College of Computer and Information Science, Southwest University（西南大学计算机与信息科学学院）；Hunan University of Arts and Science（湖南文理学院）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；School of Mathematics and Statistics, Hubei Minzu University（湖北民族大学数学与统计学院）
该研究为概率过程引入新分支双模拟，此双模拟诱导出更精细等价关系，其有根版本对含递归等构造的概率过程语言是同余关系，是一种新的等价关系定义。
2026-07-21 cs.LO
Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes
我们最近定义了一个弱马尔可夫互模拟等价的集成时间设置，它减少了序列的指数定时的内部行动，个人指数定时的内部行动具有相同的平均持续时间和执行概率的相应序列。这种弱马尔可夫互模拟等价是一个同余序列过程的抽象和原来诱导一个确切的CTMC级聚集在稳态所有考虑的过程。然而，它并不是平行合成的一致性。在本文中，我们展示了如何推广的等价性的方式，一个合理的权衡抽象，组合性和精确性之间实现了并发进程。我们将看到，通过增强并行计算中的抽象能力，可以检索关于并行组合的同余属性，所得到的CTMC级聚合仅对于所考虑过程的某个子集在稳定状态下是精确的。
2012-07-04 cs.LO
Bisimulation for Feller-Dynkin Processes
针对演化呈时间流的连续时间随机过程，提出两种等价的互模拟定义，证明其限制到离散时间时涵盖标准离散时间概念，且并非离散概念的直接推广。
2019-04-01 cs.FL cs.LO math.PR
Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending Story
我们已经开发了一个概念的全球互模拟距离的进程之间的某种程度上超越了互模拟距离的概念已经存在于文献中，主要是基于互模拟游戏。我们的建议是基于转换的成本：我们需要修改一个比较的过程来获得另一个。我们最初的定义只覆盖有限的过程，但共归纳的方法允许我们将其扩展到覆盖无限但有限的树。在展示了我们距离的许多有趣性质之后，我们打算证明关于投影的连续性，但不幸的是，这个问题仍然悬而未决。尽管如此，我们已经得到了一些部分的结果，在本文中提出。
2015-12-22 cs.LO
A Trace Based Bisimulation for the Spi Calculus
一个开放互模拟的概念制定的spi演算，一个扩展的pi演算与密码原语。在这个公式中，开放互模拟是由成对的符号迹索引的，符号迹表示环境与被检查的过程对之间的相互作用的历史。符号迹的使用允许在互模拟检查中对约束输入进行符号处理，这避免了对输入值的量化。证明了开放双相似性在等价性检验方面是合理的，并进一步证明了开放双相似性是过程上的等价关系和有限过程上的同余关系。据我们所知，这是第一个制定的开放互模拟的spi演算的全等结果得到证明。
2009-01-15 cs.CR cs.LO
Unprovability of the Logical Characterization of Bisimulation
我们快速审查标记马尔可夫过程（LMP），并提供了一个反例表明，在一般的可测空间，事件双相似性和状态双相似性不同的LMP。这表明，Desharnais [*]中的逻辑在非解析可测空间中不刻画状态互模拟。此外，我们表明，根据目前的数学基础，这样的逻辑特征是不可证明的空间，是一个协分析集的投影。在这个结构的基础上，证明了一般可测空间上的平稳马尔可夫过程不具有半拉回。[1] J. Desharnais，Labelled Markov Processes。计算机科学学院。蒙特利尔麦吉尔大学（1999年）
2010-12-10 cs.LO
Parameterized Metatheory for Continuous Markovian Logic
本文表明，一个经典的元逻辑框架，包括所有的布尔运算符，可以用来支持马尔可夫过程的度量行为理论的发展。以前，只有直觉框架或没有否定和逻辑蕴涵的框架已经被开发来完成这个任务。本文的重点是连续马尔可夫逻辑（CML），一个逻辑的特点是随机互模拟的马尔可夫过程与任意可测的状态空间和连续时间转换。当参数ε>0被解释为观测误差时，我们引入了CML的ε-参数化元理论：定义了ε-可满足性和ε-可证明性的概念，并给出了一系列包含可判定性、弱完备性和有限模型性质的“参数化”元定理.我们还证明了关于不同参数定义的元逻辑概念之间的关系的结果。使用这个框架，我们可以描述随机互模拟关系和各种基于行为伪度量的观测前序。本文的主要贡献是证明了所有这些分析实际上可以使用一个统一的完整的布尔框架。这扩展了该领域的现有技术，因为相关的作品仅提出了限制例如布尔逻辑蕴涵的使用的直觉上下文。
2012-12-17 cs.LO
Finitary Truly Concurrent Bisimulations
为基于预互模拟预序的过程语言开发完全抽象指称模型，解决无限观察区分问题，定义真正并发预互模拟及其有限形式。
2026-06-09 cs.LO
Logical Characterization of Bisimulation Metrics
互模拟度量为研究不确定性概率过程的行为提供了一种鲁棒而精确的方法。在本文中，我们提出了一个简单的概率变化的Hennessy-Milner逻辑的基础上的互模拟度量的逻辑表征。我们的方法是基于新的概念，模仿公式和公式之间的距离。前者是一个弱版本的著名的特征公式，并允许我们也（准备）概率模拟和概率双相似性的特点。后者是一个1-有界伪度量的公式，反映了Hausdorff和Kantorovich提升定义的双相似伪度量。我们证明了两个过程之间的距离等于它们自己的模仿公式之间的距离。
2016-10-26 cs.LO
Sound Bisimulations for Higher-Order Distributed Process Calculus
虽然分布式系统的进程转移已经变得普遍，推理他们的行为的方法是欠发达。在本文中，我们提出了一个互模拟技术证明行为等价的\emph{higher-order $π$-calculus with passivation}（和限制）中建模的系统。以前的研究，这种演算仅限于上下文互模拟和正常的互模拟，这是不切实际的或不健全的。相比之下，我们提供了一个健全的和有用的定义\emph{environmental bisimulations}，与几个非平凡的例子。从技术上讲，我们的互模拟中的一个中心点是并行组合的子句，它必须考虑在执行过程中产生的进程的钝化。
2011-05-06 cs.DC cs.LO cs.PL
Approximate Bisimulation and Discretization of Hybrid CSP
混合通信顺序过程（Hybrid Communicating Sequential Processes，HCSP）是一种功能强大的混合系统形式化建模语言，它是CSP的扩展，通过引入微分方程来建模连续演化，引入中断来建模连续动态与离散动态之间的相互作用。在本文中，我们调查的语义基础HCSP从操作的角度来看，提出了近似互模拟的概念，它提供了一个适当的标准来表征HCSP过程之间的等价性与连续和离散的行为。给出了一个判定两个HCSP过程是否近似双相似的算法。此外，在此基础上，我们提出了一种离散化HCSP的方法，即，给定一个HCSP过程A，我们构造另一个HCSP过程B，它不包含任何连续动力学，使得A和B在给定精度下近似双相似。这提供了一个严格的方法来转换一个验证的控制模型到一个正确的程序模型，这填补了在嵌入式系统的设计空白。
2016-09-08 cs.LO
First-Order Modal $ξ$-Calculus: On the Aspects of Application and Bisimulation
本文提出了一阶模态$ξ$ -演算以及系谱Kripke模型。受模态$μ$ -演算的启发，一阶模态$ξ$ -演算采取了非常相似的形式，并将其归纳表达扩展到不同的维度。我们阐述了几个生动的例子，证明了这种逻辑的深刻的效用，特别是描绘家谱的并发计算机进程。互模拟概念的逻辑也得到了彻底的检查。
2023-01-17 cs.LO math.LO
Globally Governed Session Semantics
本文提出了一种基于多方会话类型的互模拟理论，其中编排规范管理会话类型进程及其观察者的行为。互模拟的定义与观察者与所观察到的进程合作，以形成完整的全局会话场景，并可用于证明全局协调线程和进程的优化的正确性。诱导互模拟比标准会话互模拟严格地更细粒度。只有当存在两个以上的交错多方会话时，受控制的互模拟和标准互模拟之间的差异才会出现。这个独特的功能使得能够在大规模分布式系统中推理真实场景，其中多个编排会话需要交错。通过关于受支配的基于约简的同余的可靠性和完备性，证明了受支配的双相似性的组合性。最后，在一个大规模网络基础架构的实际应用中，通过一个多会话控制下的线程转换演示了该方法的使用。
2015-03-01 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
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
Approximate reasoning for real-time probabilistic processes
我们开发了一个伪度量模拟广义半马尔可夫过程的互模拟。这个伪度量的内核对应于互模拟，因此我们已经扩展了连续时间概率过程的互模拟到比指数分布更广泛的一类分布。这种伪度量在模型中存在数值信息（如概率和时间）的情况下，对近似推理提供了有用的处理。给出了伪度量的不动点刻画。这使得可用于推理距离的共归纳推理原则。我们表明，我们的方法是不敏感的潜在特设关节的距离表明，它是内在的一个基本的均匀性。我们提供了一个逻辑表征这种一致性使用实值模态逻辑。我们表明，几个感兴趣的定量性质是连续的伪度量。因此，如果两个过程在度量上接近，那么感兴趣的可观察的定量性质确实接近。
2006-03-08 cs.LO
Parallel Pushdown Automata and Commutative Context-Free Grammars in Bisimulation Semantics (Extended Abstract)
本文研究了在互模拟语义下，将经典下推自动机与上下文无关文法等价定理扩展至并行下推自动机与带并行性进程代数的情况。
2023-09-13 cs.LO
Cost Preserving Bisimulations for Probabilistic Automata
概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。
2015-02-16 cs.FL cs.LO
Compositional Reasoning for Interval Markov Decision Processes
Puggelli等人最近研究了具有凸不确定性的Markov决策过程的模型检验概率CTL性质，这类模型检验算法通常存在状态空间爆炸问题.在本文中，我们解决概率互模拟，以减少这样的MDP的大小，同时保持概率CTL属性，它满足。特别是，我们讨论的关键成分，建立在运行时组成间隔MDP组件的并行组合操作。更确切地说，我们研究如何并行组合操作的区间MDP可以定义，以便达到一个同余闭包。其结果是，我们表明，概率互模拟区间MDPs是一致的两个方面的并行性，即同步产品和交织。
2016-07-28 cs.LO
Higher-order Processes with Parameterization over Names and Processes
参数化扩展了高阶过程的抽象和应用能力（就像在微积分中的那些）。这个扩展是严格的，即，配备有参数化的高阶过程在计算上更强大。本文研究了高阶过程的两种参数化：一种是关于名称的参数化，另一种是关于过程本身的参数化。我们提出了两个结果。一个是，在参数化的存在下，高阶过程可以以一种非常整洁的方式编码一阶（名称传递）过程，与没有参数化的高阶过程根本不能编码一阶过程的事实相反。在另一个结果中，我们提供了一个更简单的表征（标准）上下文互模拟高阶过程的参数化，在正常的互模拟，源于众所周知的正常表征高阶微积分。这两个结果表明，更本质的参数化方法在高阶范式的表达性和行为等效。
2016-08-10 cs.LO
Two behavioural pseudometrics for continuous-time Markov processes
McGill University（麦吉尔大学）；Heriot-Watt University（赫瑞-瓦特大学）
本文提出连续时间马尔可夫过程的第二种行为伪度量，基于轨迹，并与前一种伪度量进行比较。
2026-10-30 cs.LO
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness
这项工作提出了易于处理的双向模拟高阶π演算会话原语（HOPI），并提供了一个完整的研究其最重要的子演算的表达能力。首先，我们开发了三种类型的互模拟，这是符合上下文对等。这些特征表明，仅观察高阶值的特定有限集合（其存在于会话类型中）作为输入就足以推理HOp过程。接下来，我们确定HO，一个最小的，二阶的HOPI子演算，其中高阶的应用程序/抽象，名称传递和递归是缺席的。我们表明，HO可以编码HOPI扩展高阶应用程序和抽象，一阶会话π演算可以编码HOPI。这两种编码都是完全抽象的。我们还证明了会话π演算与共享名称的传递不能被编码到HOPI没有共享名称。我们表明，HOPI，HO和PI是同样的表达; HO的表达能力，使有效的推理类型等价的高阶过程。
2015-02-10 cs.LO
Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes
Broadbent和Göller（FSTTCS 2012）证明了无ε二阶下推自动机生成的过程的互模拟等价性的不可判定性。我们添加了一些关于所使用的证明技术的注释，称为Defender's forcing，以及具有ε转换的一阶下推自动机的相关不可判定性证明（Jančar and Srba，JACM 2008）。
2013-03-04 cs.FL cs.LO
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report
通常，分布式系统的验证任务是通过计数器抽象来完成的。这种抽象有时可以通过模拟和互模拟来证明。在这项工作中，我们提供的逻辑基础，这种做法，通过一个专门设计的技术，二阶量词消去。我们的方法，一旦应用到规范的验证问题的参数化分布式系统，产生整数变量系统，准备好模型检查当前基于SMT的工具。我们证明了该方法的可行性与原型实现和第一次实验。
2017-12-05 cs.DC cs.LO cs.SE
Bisimilarity and Simulatability of Processes Parameterized by Join Interactions
本文提出连接交互参数化互模拟，作为Larsen参数化互模拟的自然弱化，证明其在确定性环境中与原概念一致，并给出可模拟性版本及模态逻辑刻画。
2025-08-19 cs.LO cs.PL
A behavioural pseudometric for continuous-time Markov processes
本文推广双模拟度量概念，通过泛函不动点与实值逻辑两种等价方法，为连续时间马尔可夫过程（如布朗运动或含跳跃过程）定义行为伪度量。
2025-01-22 cs.LO
On Decidability of the Bisimilarity on Higher-order Processes with Parameterization
具有参数化的高阶过程能够抽象和应用（从微积分迁移而来），因此在计算上更具表现力。对于最小高阶并发性，众所周知，强双相似性（即，强互模拟相等）在没有参数化的情况下是可判定的。相比之下，对于参数化高阶过程，强双相似性是否仍然是可判定的仍然不清楚。在本文中，我们关注这个问题。基本上有两种参数化：一种是关于名称，另一种是关于进程。我们表明，强双相似性确实是可判定的高阶过程配备了这两种参数化。然后，我们展示了如何适应的决策方法来建立一个公理系统的强双相似性。在这些结果的基础上，我们提供了一个算法的双相似性检查。
2021-08-24 cs.LO
Parameterized Model-Checking for Timed-Systems with Conjunctive Guards (Extended Version)
在这项工作中，我们扩展艾默生和Kahlon的截止定理的过程骨架与合取警卫参数化网络的时间自动机，即系统获得的\emph{apriori}未知数量的时间自动机实例化从一个有限的时间自动机模板集$U_1, \dots, U_n$。通过这种方式，我们的目标是提供一个工具，普遍验证软件系统中未知数量的软件组件（即过程）与连续时间的时间约束进行交互。事实上，分布式算法往往表现出异构性，将动态方面与实时方面结合起来。在本文中，我们还将展示如何模型检查协议，使用特殊的变量存储标识符的参与进程（即PID）的时间自动机与合取警卫。这是不平凡的，因为参数化验证问题的解决方案通常依赖于过程是对称的，即不可区分的。另一方面，许多流行的分布式算法使用PID，因此不能直接应用这些解决方案。
2014-07-30 cs.LO
Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems
本文研究了带离散时钟的参数化离散时间系统的模型检测复杂度，通过引入对称广播通信原语，证明了无控制器系统的安全性规范是PSPACE完全的、活性规范在EXPTIME内可判定，并揭示了带控制器系统的活性规范不可判定。
2025-06-23 cs.LO
Parameterized Synthesis for Fragments of First-Order Logic over Data Words
研究了具有参数化进程数的系统的综合问题。在Church的经典案例中，系统根据到目前为止运行的程序选择动作，目的是满足给定的规范。困难在于，与此同时，环境执行系统无法控制的操作。与固定的有限字母表的情况相反，这里我们考虑参数化字母表的情况。字母表反映了静态但未知的进程的数量。综合问题然后问是否有一个有限数量的过程，系统可以满足规范。这种变体对于非常有限的逻辑已经是不可判定的。因此，我们考虑一个一阶逻辑没有顺序的词的位置。我们表明，即使在这种限制的情况下，合成是不可判定的，如果系统和环境都可以访问所有的进程。另一方面，我们证明了问题是可判定的，如果环境只能访问有限数量的进程。在这种情况下，甚至有一个截止值，这意味着它足以检查有限数量的过程架构来解决综合问题。
2019-10-31 cs.FL cs.LO
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
我们介绍了一种用于容错分布式算法（FTDA）的自动参数化验证方法。FTDA由进程数和假定的拜占庭故障进程的最大数目参数化。在我们的技术的中心是一个参数区间抽象（PIA）的区间边界是参数的算术表达式。使用PIA的数据抽象和一种新形式的计数器抽象，我们减少了参数化的问题，有限状态模型检验。我们证明了我们的方法的实际可行性，通过验证Srikanth和Toueg著名的分布式算法的几个变种。我们的半决策程序的补充和动机的不可判定性证明FTDA验证，即使在没有进程间通信。据我们所知，这是第一篇实现拜占庭FTDA参数化自动验证的论文。
2013-02-03 cs.DC cs.LO
Parameterized Verification of Asynchronous Shared-Memory Systems
我们的特点的复杂性的安全验证问题的参数化系统组成的领导者进程和任意多个匿名和相同的贡献者。进程通过共享的有界值寄存器进行通信。虽然寄存器上的每个操作都是原子的，但是没有同步原语来原子地执行操作序列。我们分析了安全验证问题的复杂性时，过程建模的有限状态机，下推机，和图灵机。当所有进程都是有限状态机时，这个问题是coNP完全的;当它们都是下推机时，这个问题是PSPACE完全的。当每个图灵机被允许与寄存器有限制地进行许多交互时，复杂性仍然是coNP完全的。我们的证明使用组合特征的模型中的计算，并在下推系统的情况下，一些独立的利益语言理论的建设。
2013-07-12 cs.FL cs.LO
Reducing Higher Order Pi-Calculus to Spatial Logics
在本文中，我们表明，理论的过程可以减少到理论的空间逻辑。首先，我们提出了一种高阶π演算的空间逻辑SL，并给出了SL的推理系统。证明了SL的可靠性和不完备性。进一步证明了SL公式的结构同余关系和一步转移关系可以用SL公式的逻辑关系来描述。我们还扩展了SL公式的过程的互模拟。然后，我们扩展SL的所有定义和结果，SL的弱语义版本，称为WL。最后，我们在SL中加入了mu算子。这个新逻辑被命名为muSL。我们证明了WL是muSL的一个子逻辑，并且复制算子可以用muSL表示。
2012-11-17 cs.LO
Model Checking Parameterized Asynchronous Shared-Memory Systems
我们描述了参数化系统的活性验证的复杂性，由一个领导者进程和任意多个匿名和相同的贡献者进程。进程通过共享的有界值寄存器进行通信。虽然寄存器上的每个操作都是原子的，但是没有同步原语来原子地执行操作序列。我们分析的情况下，过程中建模的有限状态机或下推机和属性是由一个Büchi自动机的字母表的读取和写入行动的领导者。我们证明了这个问题是可判定的，并且具有令人惊讶的低复杂性：当所有进程都是有限状态机时，它是NP完全的，并且当它们是下推机时，它是PSPACE-hard和NEXPTIME。这种复杂性低于非参数化的情况：多个有限状态机的活性验证是PSPACE完全的，并且对于两个下推机是不可判定的。对于有限状态机，我们的证明使用存在性抽象和半线性约束来表征无限行为。对于下推机，我们展示了如何贡献者计算高栈高可以模拟计算的许多贡献者，每个低栈高。总之，我们的研究结果特征的匿名性和匿名性的假设下，参数化系统的验证的复杂性。
2015-05-25 cs.DC cs.FL cs.LO
Imperative process algebra with abstraction
介绍了一种基于ACP（Algebra of Communicating Processes）的命令式进程代数.像其他命令式进程代数一样，这个进程代数处理由命令式程序的执行引起的进程。它与已经存在的命令式进程代数的区别之一是支持抽象那些被认为不可见的动作。这种抽象的支持打开了进程代数有趣的应用可能性。本文简要地探讨了与机密数据泄漏有关的信息流安全分析的可能性。对于所提出的公理化，健全性和半完全性结果相对于一个概念的分支互模拟等价。
2022-05-21 cs.LO
Sequentializing Parameterized Programs
我们表现出断言保持（可达性保持）的参数化并发共享内存程序的转换，在一个k轮调度的进程，顺序程序。顺序程序的显著特点是它在任何时候只跟踪一个线程的局部变量，并且只使用O（k）个共享变量的副本（它不使用额外的计数器，甚至不使用一个计数器来跟踪线程的数量）。序列化是使用线性接口的概念来实现的，该线性接口捕获了无界进程块对k轮调度中的共享状态的影响。我们的转换利用线性接口来序列化程序，并确保序列程序只探索可达状态并保留局部不变量。
2012-07-18 cs.LO cs.SE
Parameterized Verification of Coverability in Well-Structured Broadcast Networks
针对不同类型的模型和拓扑结构，研究了有限状态过程广播网络可覆盖性的参数化验证。在本文中，我们试图发展一个理论的广播网络中的进程可以是结构良好的过渡系统。由此产生的形式主义被称为结构良好的广播网络。给出了一个在允许节点间链路重构的情况下判定良结构广播网络可覆盖性的算法。此外，对于各种类型的通信拓扑结构，我们也证明了在静态情况下的可覆盖性的可判定性。我们这样做是通过显示，对于这些类型的静态通信拓扑结构，广播网络本身是一个结构良好的过渡系统，从而证明了广播网络的可覆盖性的可判定性。
2018-09-10 cs.DC cs.LO
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
本文研究由任意数量异步进程组成的参数化共享内存系统的验证问题，证明基于轮次模型的存在性可达性质参数化验证是 PSPACE 完全的，而无轮次模型降至 NP 完全，并给出多项式时间可解的限制条件。
2023-07-31 cs.DC cs.FL cs.LO
Parameterized Synthesis with Safety Properties
参数化综合为参数化系统构造正确的、可验证的控制器提供了一种解决方法。这种系统在实践中自然发生（例如，以分布式协议的形式，其中进程的数量在设计时通常是未知的，并且协议必须工作而不管进程的数量）。在本文中，我们提出了一种新的学习为基础的方法来综合反应控制器的参数化系统的安全规格。我们使用的框架，定期模型检验建模的合成问题作为一个无限持续时间的两个玩家的游戏，并显示如何可以利用Angluin的著名的L* 算法学习正确的设计控制器。这种方法的结果是在一个合成过程中，概念上比现有的合成方法更简单的完整性保证，只要一个获胜的策略可以表示为一个正规的集合。我们已经实现了我们的算法在一个工具，称为L*-PSynth，并已证明其性能的基准范围内，包括机器人运动规划和分布式协议。尽管L*-PSynth很简单，但它与用于合成参数化系统的最先进的工具竞争得很好（在许多情况下甚至优于）。
2020-09-28 cs.FL cs.LO
Parameterized Verification of Deterministic MPI Programs
University of Delaware（特拉华大学）
研究确定性MPI程序验证问题，通过用户提供特定函数将程序转换为参数化顺序程序，利用Frama-C/Wp扩展实现该验证方法。
2026-07-21 cs.LO cs.PL
Deciding the existence of cut-off in parameterized rendez-vous networks
我们研究网络的进程，所有执行相同的有限状态协议和通信感谢一个renove-vous机制。给定一个协议，我们感兴趣的是检查是否存在一个称为截止的数字，使得在任何具有更多参与者的网络中，都存在一个所有实体都以某些最终状态结束的执行。我们提供了这个问题的可判定性和复杂性的结果，在各种假设下，如缺席/存在的领导者或对称/非对称的renovation-vous。
2020-07-11 cs.LO
Parameterized safety verification of round-based shared-memory systems
我们考虑分布式算法的参数化验证问题，其目标是开发技术来证明给定算法的正确性，而不管参与进程的数量。受异步二进制共识算法的启发[J. Aspnes，Fast deterministic consensus in a noisy environment. Journal of Algorithms，2002]，我们考虑了基于轮的分布式算法与共享内存通信。这些系统中的一个特殊挑战是：1）进程的数量是无限的，更重要的是，2）每一轮都有一组新的寄存器。因此，验证算法需要管理两个无穷大的来源。在这种情况下，我们证明了安全验证问题，其中包括在决定是否所有可能的执行避免给定的错误状态，是PSPACE完整的。对于安全验证问题的负实例，我们还提供了指数下限和上限的最小数目的过程中所需的错误执行和最小轮上的错误状态可以覆盖。
2022-04-25 cs.DC cs.FL cs.LO
Ordered Counter-Abstraction
我们引入了一个新的符号表示的基础上原来的概括反抽象。与经典的反抽象（用于分析具有无序或非结构化拓扑的参数化系统）不同，新的表示是为证明线性有序参数化系统的性质而定制的，即，系统与任意多个有限进程放置在一个数组中。数组中的相对位置捕获进程的相对优先级。这些系统的子系统是任意长度的有限字。进程使用受其相对优先级约束的全局转换进行通信。直观地说，符号表示的元素有一个基和一组计数器。它表示遵守计数器所施加的约束的配置，并将base作为子字。我们使用新的表示在一个统一的和自动的反例指导的细化计划。我们引入了一个松弛算子，允许一个良好的准序参数的细化循环的每次迭代的终止。我们解释了如何改进松弛以系统地剔除误报。我们实现了一个工具来说明一些参数化系统的方法。
2012-03-31 cs.LO
On Parameterized Verification Over Tree Topologies
LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP（拉布里实验室，波尔多大学，法国国家科学研究中心，波尔多理工学院）
针对树拓扑上有限状态进程的 rendez-vous 同步，研究了深度有界和相位有界两种约束下的安全性检查复杂度，分别得到与快速增长层级相关的复杂度和 EXPSPACE/2EXPSPACE 完备性结果。
2026-06-26 cs.FL cs.LO
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Technical University of Munich（慕尼黑工业大学）；Vali-e-Asr University of Rafsanjan（拉夫桑贾德瓦利阿斯尔大学）；Masaryk University（马萨里克大学）；Institute of Science and Technology（科学技术研究院）
针对参数化MDP的状态空间爆炸问题，提出利用决策树学习将小实例的最优策略泛化至大实例，无需显式探索大型模型状态空间，在远超现有工具处理规模的模型上表现良好。
2025-04-01 cs.AI cs.LG cs.LO
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
本文综述了基于阈值自动机的参数化验证技术，重点介绍拜占庭模型检查器（ByMC）如何自动验证阈值守卫容错分布式算法，确保其在任意进程数和故障数下正确性。
2023-01-16 cs.DC cs.LO
Local Reasoning for Parameterized First Order Protocols
一阶逻辑（FOL）是一种功能强大的程序验证推理工具.最近的工作表明，常春藤FOL是非常适合验证参数化的分布式系统。然而，在FOL中指定许多自然对象（如环形拓扑）出乎意料地不方便。我们提出了一个框架的基础上FOL指定分布式多进程协议在一个进程本地的方式与隐式网络拓扑结构。在规范框架中，我们提供了一个自动主动分析技术，在本地的协议，在一个过程模块化的方式。我们的目标是反映设计人员经常描述和推理协议的方式。通过隐藏FOL结构背后的拓扑结构，我们简化了建模，但使推理复杂化。为了解决这个问题，我们使用一个拓扑的预言来开发一个合理的和相对完整的证明规则，将隐式拓扑的推理减少到纯FOL。这完全避免了将拓扑公理化的需要。使用的规则，我们建立了一个属性，减少验证到一个固定数量的本地邻域的大小为界的过程。我们展示了如何使用框架上的两个例子，包括领导人选举环。
2019-03-07 cs.LO cs.MA
