Qualitative Reachability for Open Interval Markov Chains
区间马尔可夫链扩展了经典马尔可夫链，可以使用区间而不是精确值来描述转移概率。虽然区间马尔可夫链的标准公式具有闭区间的特征，但以前的工作也考虑了开区间马尔可夫链，其中的区间也可以是开的或半开的。在本文中，我们专注于定性的可达性问题的开区间马尔可夫链，考虑是否最佳（最大或最小）的概率与某一组状态可以达到等于0或1。我们提出了多项式时间算法，这些问题的标准语义的区间马尔可夫链。我们的方法不依赖于封闭的开区间，与以前的方法开区间马尔可夫链，并能证明的情况下，概率0或1可以达到不完全，但任意接近。
2018-09-22 cs.LO
Verification of Parametric Markov Automata under Time-bounded Reachability
Eindhoven University of Technology（埃因霍温理工大学）
针对参数化马尔可夫自动机（pMA），提出通过离散化为参数化马尔可夫决策过程（pMDP）并分析，解决时间有界可达性概率的合成问题，实现参数空间的满足/违反区域划分。
2026-06-23 cs.LO
Reachability Analysis of Quantum Markov Decision Processes
我们引入量子马尔可夫决策过程（qMDP）的概念作为一个语义模型的不确定性和并发量子程序。通过实例表明，qMDP可用于量子算法和协议的分析。我们研究了各种qMDP的可达性问题的有限地平线和无限地平线。解决了这些问题的（不）可判定性和复杂性，或者澄清了它们与某些长期未决问题的关系。我们还开发了一个算法，找到最佳的调度程序，达到上确界可达概率。
2014-07-09 cs.LO quant-ph
On the Complexity of Reachability in Parametric Markov Decision Processes
本文研究了参数马尔可夫决策过程（pMDP），它是马尔可夫决策过程（MDP）的一种扩展，其中转移概率由有限参数集上的多项式描述。固定所有参数的值会产生MDP。特别是，本文研究了这些参数的值，使诱导MDP满足一些可达性约束的复杂性。我们讨论不同的变体取决于比较运算符的约束和域的参数值。我们改进了该问题的所有已知下界，并特别提供了该问题不同变体的ETR完整性结果。此外，我们提供的见解在功能描述诱导可达性概率，以及如何pMDPs概括并发随机可达性游戏。
2019-04-02 cs.CC cs.LO
QReach: A Reachability Analysis Tool for Quantum Markov Chains
Tsinghua University（清华大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）
QReach是一种基于CFLOBDD的量子马尔可夫链可达性分析工具，通过新的框架和模型检查子过程提升量子电路和算法的验证效率。
2025-12-04 cs.LO quant-ph
A Probabilistic Logic for Verifying Continuous-time Markov Chains
连续时间马尔可夫链（CTMC）执行是状态上连续的一类概率分布。本文提出了一种概率线性时序逻辑，即连续时间线性逻辑（CLL），用于推理CTMC的概率分布执行。我们定义的概率分布的空间上的CLL的语法。CLL的语法包括多相定时直到公式，并且CLL的语义允许时间重置以研究相对时间属性。我们推导出相应的CLL公式的模型检测算法。模型检测算法的正确性依赖于Schanuel猜想，这是超越数论中的一个中心开放问题。此外，我们提供了一个运行的CTMC的例子来说明我们的方法。
2022-04-14 cs.LO
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
Radboud University（拉德堡德大学）；RWTH Aachen University（亚琛工业大学）
本文提出了一种高效计算最优条件可达性的方法，适用于无环马尔可夫决策过程，并在抽象-细化框架中分析大量马尔可夫链，展示了在贝叶斯网络分析、概率程序和运行时监控中的有效性。
2026-05-13 cs.LO
Verifying Global Two-Safety Properties in Neural Networks with Confidence
本文提出首个面向深度神经网络全局鲁棒性与公平性等置信度二安全性性质的自动化验证方法，通过自组合与 softmax 新型抽象实现可靠静态分析，并在 Marabou 上完成基准评估。
2024-09-03 cs.LO
The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
Technische Universität Darmstadt（达姆施塔特工业大学）；Université libre de Bruxelles（布鲁塞尔自由大学）；Departement d’Informatique（计算机系）
研究了具有无限时域可达性目标的马尔可夫决策过程的永不变差关系。如果从p到达目标状态集的最大概率至多与从q到达的最大概率相同，则状态q永远不会比状态p差，而不考虑标记转移的概率。极端概率态、终结分量和本质态都是由NWR导出的等价关系的特例。使用NWR，可以折叠相同等价类中的状态。然后，可以移除导致次优状态的动作。我们证明了与计算NWR相关的自然决策问题是CONP完全的。最后，我们扩展了以前已知的不完全多项式时间迭代算法下近似的NWR。
2018-02-24 cs.AI cs.LO
A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker
由于增加每个CPU插槽的处理单元数量的强烈趋势，因此多线程程序变得越来越重要。我们介绍了一种新的可配置的程序分析验证多线程程序的线程数有限。我们提出了一个简单而有效的实现现有的程序验证框架CPAchecker的组成部分。虽然CPAchecker已经在一个大型的基准集的顺序验证任务的竞争力，我们的扩展增强了框架的整体适用性。我们处理多线程的实现与数据流分析的抽象域是正交的，因此，可以与CPAcchecker中的几种现有分析相结合，如值分析，区间分析和BDD分析。新的分析是模块化的，可以用来，例如，验证可达性属性以及检测程序中的死锁。本文包括一些优化步骤的效益评估（例如，改变可达性算法的迭代顺序或应用偏序约简）以及与用于验证多线程程序的其它现有技术工具的比较。
2016-12-15 cs.LO cs.PL cs.SE
Reachability in Augmented Interval Markov Chains
在本文中，我们提出了增广的区间马尔可夫链（AIMCs）：一个概括的熟悉的区间马尔可夫链（IMCs）的不确定的转移概率是另外允许相互依赖。这种新模型保留了IMC所提供的灵活性，用于描述参数不清楚的随机系统，例如由于测量误差，但也允许我们指定具有已知相同概率的转换，从而提供进一步的表达能力。本文的重点是可达性在AIMCs。我们研究了定性、精确定量和近似可达性问题及其自然子问题，并建立了它们复杂性的上界和下界。我们证明了确切的可达性问题是至少作为著名的平方根和问题一样难，但令人惊讶的是，近似版本在于$\mathbf{NP}$，如果底层图是已知的，而限制的确切问题的不确定边缘的常数是在$\mathbf{P}$。最后，我们表明，在图结构的不确定性影响复杂性证明$\mathbf{NP}$ -完整的定性子问题，与一个容易获得的上限$\mathbf{P}$为同一个子问题与已知的图形结构。
2017-01-11 cs.CC cs.DM cs.LO
Markov Automata with Multiple Objectives
马尔可夫自动机结合了非确定性，概率分支和指数分布延迟。这种连续时间马尔可夫决策过程的组合变体被用于可靠性工程、性能评估和随机调度。到目前为止，它们的核查侧重于单一目标，如（定时）可达性和预期成本。在实践中，这些目标往往是相互依赖的，目的是揭示权衡取舍。我们提出的算法，同时分析几个目标和近似帕累托曲线。这包括，例如，多个（定时）可达性目标或各种预期成本目标。我们还考虑其组合，如在预算内的时间目标-哪些政策保证达到目标状态的最后期限内至少有概率$p$，同时保持允许的平均成本低于阈值？我们采用现有的方法为经典的马尔可夫决策过程。主要的挑战是如何对待利用国家居留时间的政策，即使是为了不定时的目标。实验结果表明了该方法的可行性和可扩展性。
2017-05-10 cs.LO
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
我们重新审视马尔可夫链的符号验证有限时域可达性。流行的方法迭代计算步骤有界状态可达概率。相比之下，概率推理的最新进展建议用符号表示通过马尔可夫链的所有水平长度路径。我们问这种观点是否推进了概率模型检验的最新技术。首先，我们正式描述这两种方法，以突出其主要区别。然后，利用这些见解，我们开发了Rubicon，一个将Prism模型转换为概率推理工具Dice的工具。最后，我们证明了更好的可扩展性相比，概率模型检查器在选定的基准。总之，我们的研究结果表明，概率推理是一个有价值的除了概率模型检验投资组合-与Rubicon作为第一步集成两个角度。
2021-06-30 cs.LO
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes
本文研究Markov决策过程中多目标可达性、不变性与平均收益查询的可验证性，将线性规划方法改造为认证算法，并生成调度器和子系统见证。
2025-01-10 cs.LO
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
我们研究了验证有限连续时间马尔可夫链（CTMC）C对线性实时规范作为一个确定性的时间自动机（DTA）A有限或穆勒接受条件。我们要解决的中心问题是：C的路径集合被A接受的概率是多少，即，C满足A的可能性结果表明，在有限的验收标准，这等于在有限的分段确定性马尔可夫过程（PDP）的可达概率，而Muller验收标准，它符合终端强连通组件在这样的PDP的可达概率。定性验证显示相当于PDP的图形分析。在我们的PDP的可达性概率，然后其特征在于作为第二类Volterra积分方程系统的最小解，并示出近似的偏微分方程系统的解决方案。对于单时钟DTA，该积分方程系统可以被变换成线性方程系统，其中系数是常微分方程的解。由于系数实际上是CTMC中的瞬态概率，因此该结果意味着CTMC分析的标准算法足以验证单时钟DTA规范。
2011-03-27 cs.LO
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
本文讨论了有限状态马尔可夫决策过程（MDP）的整数权重分配给每个状态动作对。提出了新的算法来分类端组件根据其限制行为相对于累积的权重。这些算法被用来提供两种类型的整数加权MDPs的基本问题的解决方案。首先，一个多项式时间算法的经典随机最短路问题，推广已知的结果，特殊类的加权MDPs。其次，定性概率约束的重量有界（重复）的可达性条件的解决。其中，它示出的问题，以决定是否一个析取的重量有界的可达性条件下，几乎肯定持有一些调度属于$\textrm{NP}\cap \textrm{coNP}$，是可解的伪多项式时间，是至少一样难，解决两个球员的平均支付游戏，而相应的问题，泛量化的竞争对手是可解的多项式时间。
2018-04-30 cs.LO
Marimba: A Tool for Verifying Properties of Hidden Markov Models
Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas（应用数学与系统研究所）；University of Bristol（布里斯托尔大学）；Bristol Robotics Laboratory（布里斯托尔机器人实验室）；Universidad Nacional Autónoma de México（墨西哥国立自治大学）
对隐马尔可夫模型（Hidden Markov Models，简称HMM）的性质进行形式化验证，对于保证模型和系统的正确性具有重要意义。HMM验证的一个重要步骤是Zhang等人开发了一系列用于验证HMM的逻辑，称为POCTL* 及其模型检验算法。据我们所知，我们在这里介绍的验证工具是第一个基于张等人。的方法。作为其有效的应用程序的一个例子，我们验证了在人机交互的上下文中的移交任务的属性。我们的工具在Haskell中实现，并使用人形机器人Bert 2进行实验评估。
2015-10-28 cs.LO cs.RO
Farkas certificates and minimal witnesses for probabilistic reachability constraints
本文介绍了Farkas证书的最小和最大可达概率在马尔可夫决策过程（MDP），我们使用的MDP变体的Farkas引理的上下界。所有这些证书的集合被示出为形成多胞形，其点对应于模型和属性的见证子系统。利用这种对应关系，我们可以将寻找最小见证人的问题转化为寻找具有最大数量的零的顶点的问题。虽然计算这样的顶点是计算困难的一般情况下，我们从我们的配方，表现出竞争力的性能相比，最先进的技术，我们得到新的算法。作为一个论点，渐近更好的算法不能希望，我们发现，即使是非循环马尔可夫链的决策版本的最小证人是NP完全的。
2020-02-05 cs.LO math.OC
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
我们解决的问题，验证消息传递程序，定义为一组通过无界FIFO缓冲区通信的并行进程。我们引入了一个有界分析，探讨了一种特殊类型的计算，称为k-同步。这些计算可以被视为交互阶段的（无界）序列，每个阶段允许最多k个发送动作（由不同的进程），然后是对应于同一阶段中发送的接收序列。我们给出了一个判定程序k-同步性的过程，即，每个计算是否等价于（具有相同的happens-before关系）其k-同步计算之一。我们还表明，在k-同步计算的可达性和检查k-同步性都是PSPACE完全的。此外，我们引入了一类程序称为{ \em流有界}的问题，决定是否存在一个k>0的程序是k-同步，是可判定的。
2018-04-18 cs.LO cs.PL
A Comparison of Sequential and GPU Implementations of Iterative Methods to Compute Reachability Probabilities
我们考虑计算可达性概率的问题：给定一个马尔可夫链，马尔可夫链的初始状态，以及马尔可夫链的一组目标状态，从初始状态到达任何目标状态的概率是多少？这个问题可以简化为求解一个线性方程Ax = b，其中A是一个矩阵，b是一个向量。我们考虑两种求解线性方程的迭代法：Jacobi方法和双共轭梯度稳定（BiCGStab）方法。对于这两种方法，顺序和并行版本已经实施。并行版本已在计算统一设备架构（CUDA）上实现，以便它们可以在NVIDIA图形处理单元（GPU）上运行。从我们的实验中，我们得出结论，随着矩阵大小的增加，CUDA实现优于顺序实现。此外，BiCGStab方法比Jacobi方法更好地执行密集矩阵，而Jacobi方法更好地执行稀疏矩阵。由于可达性概率问题在概率模型检验中起着关键作用，我们还比较了从概率模型检验器获得的矩阵的实现。我们的实验支持Bosnacki等人的猜想，即Jacobi方法优于Krylov子空间方法，这是BiCGStab方法所属的一类，用于概率模型检验。
2012-10-24 cs.DC cs.LO
Algorithms for reachability problems on stochastic Markov reward models
我们研究和开发的随机马尔可夫奖励模型（sMRM），它扩展了马尔可夫链的过渡时间/奖励建模为随机变量。技术提出，使计算首次通过时间分布（或奖励分布），只有适度规模的系统时，在一台计算机上解决的高精度。相比之下，朴素模拟技术可以扩展，并且足以解决高精度不成问题的大量问题，但是如果可以精确建模（一个潜在的大警告），当需要非常精确的解决方案时，这项工作可能会很有价值。所提出的工作是交织在一起的时态逻辑理论，虽然不是主要的贡献的工作，实现了这项工作的自动概率分析/验证领域的连接。虽然它的承认确实混淆了算法的细节是主要的，但是。我们提出了计算第一通道奖励密度，期望值问题，和其他可达性问题的方程。重点是寻找严格的数值解的首次通过时间/奖励密度。我们采用线性代数算法，如高斯消去法，和迭代法，如功率法，雅可比和高斯-赛德尔。我们提供了两个离散奖励sMRM的解决方案，其中所有奖励离散（格）随机变量。对于连续奖励sMRM，其中所有奖励都是严格连续随机变量。我们的解决方案涉及使用快速傅里叶变换（FFT）进行更快的计算，我们能够适应现有的卷积求积规则，以获得更准确的解决方案，规则，如梯形规则，辛普森规则和龙伯格的方法。
2022-08-14 cs.LO cs.NA math.NA
Sound Value Iteration
计算可达性概率是概率模型检验的核心。所有模型检查器都使用值迭代以迭代方式计算这些概率。该技术通过确定递增步数的可达性概率，从下向上逼近固定点。为了避免明显偏离的结果，最近提出了从下方和上方收敛的变体。这些程序需要两侧的起始值。我们提出了一种替代方案，不需要先验计算的起始向量，收敛速度更快的许多基准。我们的技术的关键是给紧和安全的界限-其计算是廉价的-可达概率。提升这种技术的预期回报是微不足道的马尔可夫链和MDPs。在大量基准测试上的实验结果表明了该方法的可扩展性和高效性。
2018-04-13 cs.LO
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
本文针对量子连续时间马尔可夫链，提出结合代数与数值方法的连续随机逻辑模型检验方案，确立了CSL的可判定性并保证计算效率，还给出示例演示方法应用。
2025-11-10 cs.LO
Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards
马尔可夫决策过程是并发优化问题的有用模型，但对于穷举验证方法来说往往是棘手的。最近的工作已经引入了轻量级的近似技术，直接从调度空间采样，带来了可扩展的替代标准的数值模型检验算法的前景。到目前为止，重点一直是优化一个属性的概率，但许多问题需要定量分析的回报。因此，在这项工作中，我们提出了轻量级的统计模型检验算法，以优化马尔可夫决策过程的奖励。我们认为标准的定义中使用的奖励模型检验，引入一个辅助的假设检验，以适应可达性奖励。我们证明了我们的方法在一些标准的案例研究的性能。
2015-03-23 cs.LO
Parameter Synthesis for Markov Models: Faster Than Ever
我们提出了一个简单的技术来验证概率模型的转移概率是参数。关键是用极值的非确定性选择来代替参数转换。使用现成的平均值分析所得到的无参数模型产生参数空间中区域概率的（可细化的）下限和上限。该技术优于现有的分析参数马尔可夫链的几个数量级的运行时间和可扩展性。它的美妙之处在于它适用于各种概率模型。它特别提供了第一个健全的和可行的方法进行参数综合的马尔可夫决策过程。
2016-05-26 cs.LO
On Decidability of Time-bounded Reachability in CTMDPs
考虑连续时间马氏决策过程的时间有界可达性问题。我们证明了这个问题是可判定的Schanuel猜想。我们的决策过程依赖于结构的最优政策和条件的可判定性（根据Schanuel的猜想）的理论的实数扩展指数和三角函数在有界域。我们进一步表明，任何无条件可判定性的结果将意味着无条件可判定的有界连续Skolem问题，或等价地，检查的问题，如果一个指数多项式有一个非切零在有界区间。我们注意到，后者的问题也是可判定的Schanuel的猜想，但寻找无条件的决策程序仍然是长期悬而未决的问题。
2020-06-09 cs.LO cs.SY eess.SY
Beyond Decisiveness of Infinite Markov Chains
研究无限状态马尔可夫链验证，证明决断性是统计模型检测几乎必然终止的充要条件，提出结合抽象与重要性采样的方法，用决断性链替代非决断性链以统一数值与统计验证，并在概率下推自动机上完成首次原型实现。
2024-09-27 cs.FL cs.LO
Analyzing Value Functions of States in Parametric Markov Chains
University of Antwerp（安特卫普大学）
本文研究参数马尔可夫链验证，将单调性问题归约为状态间可达性概率比较，利用坍缩同值等价类的高效算法减小模型规模，并加速单调性检查与参数提升，可作为快速预处理步骤。
2025-04-26 cs.AI cs.LO
Q-Learning for Reachability in MEC-Free MDPs
Georgia Institute of Technology（佐治亚理工学院）
本文提出Quasar，首个无模型Q学习算法，用于无最大端分量MDP的可达性，通过时序差分更新实现渐近最优，内存从O(|S|^2|A|)降至O(|S||A|)，样本效率显著优于基于模型方法。
2026-10-02 cs.AI cs.LG cs.LO
Significant Diagnostic Counterexamples in Probabilistic Model Checking
提出了一种新的马尔可夫链和马尔可夫决策过程概率模型检验中的反例生成技术。反例中的（有限）路径在可能向用户提供类似调试信息的证人中被分组在一起。我们列出了五个属性，证人应该满足，以作为调试援助有用：相似性，准确性，独创性，重要性和有限性。我们的见证者包含在强连接组件之外表现相似的路径。本文展示了如何计算这些证人减少的问题，生成反例的一般属性在马尔可夫决策过程中，在几个步骤，生成反例的可达性属性在非循环马尔可夫链的简单问题。
2008-06-06 cs.LO cs.PF
Faster Algorithms for Markov Decision Processes with Low Treewidth
我们考虑两个核心算法的概率验证问题：最大端部分解和几乎确定的可达集计算的马尔可夫决策过程（MDP）。对于MDPs与树宽$k$，我们提出了两个改进的静态算法，分别运行在时间$O(n \cdot k^{2.38} \cdot 2^k)$和$O(m \cdot \log n \cdot k)$的问题，其中$n$是状态的数量和$m$是边缘的数量，显着提高了以前已知的$O(n\cdot k \cdot \sqrt{n\cdot k})$约束低树宽。我们还提出了递减算法，这两个问题的MDPs与恒定的树宽，运行在摊销对数时间，这是一个巨大的改进，以前已知的算法，需要摊销线性时间。
2013-10-30 cs.DS cs.LO
Continuous-Time Markov Decisions based on Partial Exploration
Technical University of Munich（慕尼黑工业大学）；Saarland University（萨尔兰大学）
本文提出一种加速连续时间马尔可夫决策过程时间有界可达性分析算法的框架，通过识别并分析子系统实现高效计算，验证了该方法在多个传统算法中的显著加速效果。
2018-07-25 cs.LO cs.SY eess.SY
Scalable Verification of Markov Decision Processes
Inria Rennes – Bretagne Atlantique（法国国家信息与自动化研究所雷恩－布列塔尼大西洋中心）
马尔可夫决策过程（MDP）是有用的模型并发过程优化问题，但验证它们的数值方法往往是棘手的。现有的近似方法不能很好地扩展，并且仅限于无记忆存储器。在这里，我们提出了MDPS的可扩展性验证的基础上，使用一个O（1）的历史相关的存储器表示。因此，我们促进可扩展的学习技术和大规模并行验证的使用。
2014-09-17 cs.DC cs.DS cs.LG
Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives
University of Colorado Boulder（科罗拉多大学博尔德分校）；Jet Propulsion Laboratory（喷气推进实验室）；California Institute of Technology（加州理工学院）
本文研究无折扣 POMDP 的最大可达性概率问题，提出一种基于试验的启发式搜索值迭代新算法，通过值边界引导信念空间探索并解决循环处理缺陷，提供双侧概率界限，实验证明其在概率保证和计算时间上优于现有方法。
2024-06-05 cs.AI cs.LO cs.RO
