Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
我们考虑定量扩展的交替时间时序逻辑ATL/ATL称为定量交替时间时序逻辑（QATL/QATL），其中计数器的值可以比较使用等式，不等式和模约束的常数。我们解释这些逻辑在一个计数器的游戏模型，这是无限的持续时间的游戏有限的控制图，每个过渡可以增加或减少一个无界计数器的值。也就是说，这些游戏的状态空间通常是无限的。我们考虑的模型检验问题的逻辑QATL和QATL的一个计数器的游戏模型与VASS语义，我们开发的算法，并提供匹配的下界。我们的算法是基于减少的模型检验问题的模型检验游戏。这种方法使我们很容易处理扩展的逻辑语言以及无限的状态空间。该框架一方面概括了定性问题，如有限状态系统的ATL/ATL模型检验、单计数器过程上的分支时间时序逻辑CTL和CTL的模型检验以及LTL规范的可实现性问题。另一方面，QATL/QATL的模型检验问题推广了定量问题，如能源博弈（在QATL的情况下）和能源平价博弈（在QATL的情况下）的固定初始信用问题。我们的结果是积极的，因为我们表明，泛化是不是太昂贵的复杂性。作为一个副产品，我们获得了新的结果的复杂性模型检验CTL在一个计数器的过程中，并表明，决定赢家在一个计数器的游戏与LTL的目标是2 ExpSpace完成。
2014-09-19 cs.LO
Model Checking Probabilistic Pushdown Automata
我们考虑概率下推自动机（pPDA）的模型检验问题和各种概率逻辑中可表达的属性。我们开始与属性，可以制定为一个广义的随机游走问题的实例。我们证明了定性和定量的模型检验这类性质和pPDA是可判定的。然后，我们证明了模型检验的定性片段的逻辑PCTL和pPDA也是可判定的。此外，我们开发了一个容错的模型检验算法的PCTL和无状态pPDA的子类。最后，我们考虑了一类ω-正则性质，并证明了pPDA的定性和定量模型检验都是可判定的。
2006-03-09 cs.LO
Model Checking Games for the Quantitative mu-Calculus
我们研究了模态逻辑和模态μ演算的定量扩展，并研究了逻辑和游戏之间的紧密联系是否可以从定性逻辑提升到定量逻辑。事实证明，如果以适当的方式定义定量μ演算，尊重逻辑运算符之间的对偶性质，那么它的模型检验问题确实可以通过奇偶博弈的定量变体来表征。然而，这些定量游戏有相当不同的性质比他们的经典同行，特别是他们，在一般情况下，不确定的位置。逻辑和博弈之间的对应是双向的：定量转换系统上的公式的值与相关的定量博弈的值一致，相反，定量平价博弈的值在定量μ演算中是可定义的。
2008-02-20 cs.GT cs.LO
Efficient computation of exact solutions for quantitative model checking
马尔可夫决策过程的定量模型检查器通常使用有限精度算法。如果模型检验过程中的所有系数都是有理数，则模型检验的结果也是有理数，从而可以准确地计算出模型检验结果。然而，精确的技术通常过于昂贵或可扩展性有限。在本文中，我们提出了一种方法，从有限精度算术的近似解开始获得精确的结果。该方法的输入是调度器的描述，其可以通过使用有限精度的模型检查器来获得。给定一个调度程序，我们展示了如何获得相应的基础上的线性规划问题，在这样的方式，该基础是最佳的，每当调度程序达到最坏情况的概率。这种对应关系是已知的折扣MDP，我们展示了如何应用它在未贴现的情况下，提供了一些预处理。利用对应关系，线性规划问题可以从所获得的基开始以精确的算术求解。因此，即使模型检查器提供的调度器不是最优的，该方法也会找到最坏情况的概率。在我们的实验中，从候选调度程序的精确解的计算是显着快于使用单纯形方法从默认的基础上开始精确的算术计算。
2012-07-04 cs.LO
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
定量分离逻辑（QSL）是分离逻辑（SL）的扩展，用于概率指针程序的验证。在QSL中，公式计算为实数而不是真值，例如，在给定的符号堆中，内存安全终止的概率。与\SL一样，使用QSL进行推理时的一个关键问题是\emph{entailment}：公式f是否包含另一个公式g？我们给出了从QSL中的蕴涵检查到SL中的蕴涵检查的一般性约简。这允许利用大量的SL研究来自动验证概率指针程序。我们分析了我们的方法的复杂性，并证明其适用性。特别是，我们得到的第一个可判定性结果，验证这些程序通过应用我们的减少到一个量化的扩展著名的符号堆片段的分离逻辑。
2022-01-27 cs.LO cs.PL
Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking
我们调查的统计模型检验技术分析软件产品线模型的定量属性与概率方面的适用性。为此，我们丰富了面向功能的语言FLan的动作率，它指定的可能性表现出特定的行为或安装功能在特定的时刻或以特定的顺序。丰富的语言（称为PFLan），使我们能够指定模型的软件产品线的概率配置和行为，例如，通过考虑基于离散时间马尔可夫链的PFLan语义。PFLan的Maude实现与分布式统计模型检查器MultiVeStA相结合，对一个简单的产品线案例研究进行定量分析。所提出的分析包括某些感兴趣的行为（例如产品故障）的可能性和产品的预期平均成本。
2015-04-14 cs.LO cs.SE
Pareto Curves for Probabilistic Model Checking
多目标概率模型检验提供了一种方法来验证随机系统的几个可能相互冲突的定量属性。它在控制器综合和组合概率验证中有很好的应用。然而，现有的方法是基于线性规划，这限制了可以分析的系统的规模，并使得验证的时间有界的属性非常困难。我们提出了一种新的方法，解决这两个缺点，基于生成的连续近似的帕累托曲线的多目标模型检验问题。我们说明了一个大的基准集上的效率显着提高，并显示如何可视化帕累托曲线的能力显着提高了从当前的概率验证工具获得的结果的质量。
2012-06-24 cs.LO
A CEGAR-like Approach for Cost LTL Bounds
定性的形式化验证，即寻找关于系统行为的布尔答案，通常不足以满足实际目的。观察定量信息是感兴趣的，例如，用于电池或实时调度器的适当校准。从历史上看，重点一直是在一个连续的领域的数量，但近年来显示了离散的定量域的新的兴趣。代价线性时序逻辑是经典线性时序逻辑的一种定量扩展。它集成到一个很好的理论，在过去几年中，扩展了定性设置，与同行的逻辑，自动机和代数结构。我们提出了一个实际使用的逻辑模型检查的目的。CLTL公式定义了一个从无限单词到整数的函数。在给定的一组单词上找到这样一个函数的边界可以被看作是LTL通用和存在模型检查的扩展。我们提出了一个基于经典LTL模型检验的类CEGAR算法，并使用带计数器的Büchi自动机实现了该算法，为离散定量逻辑的实际应用迈出了第一步.
2015-06-18 cs.LO
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
概率计算树逻辑（PCTL）和连续随机逻辑（CSL）通常分别用于描述离散时间和连续时间的概率属性规范。在PCTL和CSL中，执行满足某些时态性质的可能性可以通过其基本计算树逻辑（CTL）中路径量词的概率扩展来定量表示，但它们的路径公式在CTL中是通过相同的运算符来表示的。由于这个原因，它们都不能表示具有定量时间属性的公式，例如“某些属性在路径上超过80%的时间点（在某个有界区间内）保持不变”的形式。本文引入了一个新的时态算子来表达事件频率的概念，并在CTL \star的基础上定义了概率频率时态逻辑（PFTL）。因此，我们可以很容易地表示概率系统中的行为的时间属性。然而，它是很难开发一个完整的PFTL模型检查，由于丰富的表现力。相应地，我们开发了一个模型检测算法的CTL类片段的PFTL对有限状态马尔可夫链，和一个近似的模型检测算法的有界线性时序逻辑（LTL）类片段的PFTL对可数状态马尔可夫链。
2011-11-14 cs.LO
Statistical Model Checking : An Overview
随机系统的定量属性通常在逻辑中指定，允许将满足某些时间属性的执行度量与阈值进行比较。随机系统的模型检验问题通常是通过数值方法来解决的，该方法迭代计算（或近似）满足相关子公式的路径的精确测量;算法本身取决于被分析的系统类别以及用于指定属性的逻辑。解决模型检验问题的另一种方法是对系统进行多次运行的\emph{simulate}，并使用\emph{hypothesis testing}来推断样本是否提供了满足或违反规范的\emph{statistical}证据。在这篇简短的论文中，我们调查了统计方法，并概述了其在效率，一致性和简单性方面的主要优势。
2010-05-08 cs.LO
A quantitative extension of Interval Temporal Logic over infinite words
Halpern和Shoham的区间时态逻辑HS的模型检验最近已经被系统地研究，并且已知它在三种不同的语义（基于状态、基于迹和基于树的语义）下是可判定的。在这里，我们专注于基于轨迹的语义，其中的主要语义实体是无限的执行路径（轨迹）的给定Kripke结构，假设在另外的同质性的命题估值。我们引入了一个定量的扩展HS的痕迹，称为差异HS（DHS），允许一个表达时间间隔长度（持续时间）之间的差异的限制。一些模态的定量扩展直接导致不可判定性，因此，我们通过考虑DHS的严格语法片段来研究模型检验和可满足性问题的可判定性边界。特别是，我们确定了最大的可判定的片段DHSS的DHS证明，此外，所考虑的问题的片段至少是2EXPSPACE硬。此外，通过利用新的结果，线性时间混合逻辑，我们表明，对于一个同样具有表现力的片段的DHSS，问题是EXPSPACE完全的。最后，我们通过一个新的混合逻辑的单变量片段提供了一个表征HS的痕迹。
2022-07-13 cs.LO
On (Omega-)Regular Model Checking
检查无限状态系统通常通过将无限状态集编码为正则语言来完成。计算这样一个规则的表示，比如说，一个系统的可达状态集需要加速技术，可以计算无限数量的转换的效果。在已经提出的加速技术中，可以找到特定的和通用的技术。特定技术利用被分析的特定类型的系统，例如，操纵队列或整数的系统，而通用技术仅假设转换关系由有限状态转换器表示，其必须迭代。在本文中，我们调查的可能性，使用通用技术的情况下，只有特定的技术已被利用到目前为止。发现现有的通用技术往往是不适用的情况下，很容易处理的特定技术，我们已经开发出一种新的方法来迭代换能器。这种新方法建立在早期工作的基础上，但利用了许多新的概念和算法思想，通常在实验的帮助下诱导，这使其具有广泛的范围以及良好的性能。
2008-09-12 cs.LO
Faster Statistical Model Checking for Unbounded Temporal Properties
针对马尔可夫链的无界时态性质，如可达性和完全线性时态逻辑，提出了一种新的统计模型检验算法。其主要思想是，我们监视每个模拟运行的飞行，以快速检测，如果一个底部强连接的组件是进入高概率，在这种情况下，模拟运行可以提前终止。因此，我们的模拟运行往往比所需的终止边界，计算先验的期望水平的置信度和状态空间的大小短得多。与以前的统计模型检验算法相比，对于给定的置信度，我们的方法不仅在许多情况下更快，而且需要更少的系统信息，即，只有最小的转移概率发生在马尔可夫链，从而使几乎完整的黑盒验证。此外，我们的方法可以推广到无界的定量属性，如平均回报界。
2016-03-03 cs.LO
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
本文针对量子连续时间马尔可夫链，提出结合代数与数值方法的连续随机逻辑模型检验方案，确立了CSL的可判定性并保证计算效率，还给出示例演示方法应用。
2025-11-10 cs.LO
Probabilistic Model Checking for Energy Analysis in Software Product Lines
在软件产品线（SPL）中，软件产品的集合由它们在功能方面的共性定义，而不是一个接一个地明确指定所有产品。几个验证技术进行了调整，以建立时间属性的SPL。符号和基于族的模型检验已被证明是成功的解决组合爆破时出现的推理几个特征组合。然而，大多数形式化验证方法的SPL的文献中提出的重点是静态SPL，其中的产品的功能是固定的，不能改变在运行时。这与动态SPL相反，动态SPL允许在部署后动态地调整产品的功能组合。本文的主要贡献是一个动态SPL的组成建模框架，它支持概率和不确定性的选择，并允许定量分析。我们在基于自动机的协调组件内指定运行时期间的特征变化，从而能够对如何触发动态特征变化以优化各种定量目标的策略进行推理，例如，能源或货币成本和可靠性。对于我们的框架有一个自然的和概念上简单的翻译成输入语言的著名的概率模型检查PRISM。这有利于应用程序的PRISM的强大的符号引擎的动态SPL和他们的家庭为基础的分析对各种定量查询的操作行为。我们证明了我们的方法的可行性，通过案例研究发出的能量感知绑定网络设备。
2013-12-30 cs.LO cs.SE
Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives
模型检验允许人们根据系统行为的形式模型（通常是Kripke结构）自动验证系统预期属性的规范。基于点的时态逻辑，如LTL、CTL和CTL*，描述了系统如何逐状态演化，通常用作规约语言。他们证明自己在各种应用领域相当成功。然而，属性约束的时间顺序的时间扩展的事件，以及涉及时间聚合，这是固有的间隔为基础的属性，不能正确地处理它们。区间时态逻辑（ITLs），以间隔作为其原始的时间实体，原来是非常适合的规范和验证的间隔计算属性（我们解释的所有轨道的Kripke结构作为计算间隔）。研究了Halpern和Shoham的时间区间模态逻辑（HS）的部分片段的模型检验问题。HS的特点是每对区间之间的每种可能的排序关系（所谓的艾伦关系）都有一种模态。首先，我们描述了一个EXPSPACE模型检验算法的HS片段的艾伦的关系满足，满足，开始，开始，和完成，它利用的可能性找到，为每个轨道（无限长），一个等效的有界长度的轨道代表。在检查属性时，它只需要考虑长度不超过给定界限的轨迹。我们证明了这样一个片段的模型检验问题是PSPACE困难的。最后，我们确定了其他表现良好的HS片段，这些片段的表达能力足以捕捉系统的有意义的区间特性，如互斥，状态可达性和非饥饿，其复杂性小于或等于LTL。
2017-09-06 cs.LO
Semiring-based Specification Approaches for Quantitative Security
我们的目标是提供不同的半环为基础的正式工具的规格的安全要求：我们定量地提高了开放系统的方法，根据该系统是部分指定的。因此，我们假设存在一个未知的，可能是恶意的代理，与系统并行交互。两个规范框架沿着两条不同（但仍然相关）的路线设计。首先，通过比较一个系统的行为与预期的，或通过检查这样的系统是否满足一些安全要求：我们研究了一种新的近似行为等价比较进程的行为，从而扩展了广义非演绎成分（GNDC）的方法与分数。作为第二个结果，我们配备了一个模态逻辑与半环值的目的有一个权重相关的满足公式，指定一些要求的属性。最后，我们概括了经典的部分模型检查功能，我们将其命名为定量部分模型检查，以这种方式指出系统必须满足的必要和充分条件，以便被认为是安全的，相对于一个固定的安全/功能阈值。
2015-09-29 cs.CR cs.FL cs.LO
Computing Quantiles in Markov Reward Models
概率模型检验主要集中于推理某些路径属性或某些随机变量的期望值的概率的技术。然而，对于定量系统分析，还有另一种有趣的性能度量，即分位数。一个典型的分位数查询需要输入一个概率下界p和一个可达性属性。然后，任务是计算最小奖励界限r，使得在累积奖励超过r之前，至少有概率p到达目标集。分位数在数理统计中是众所周知的，但据我们所知，到目前为止，模型检验社区还没有解决它们。在本文中，我们研究了在离散时间有限状态马尔可夫决策过程的状态上具有非负回报的直到性质的分位数查询的复杂性。我们表明，定性分位数查询可以在多项式时间内进行评估，并提出了一个指数算法的定量分位数查询的评估。对于马尔可夫链的特殊情况下，我们表明，定量分位数查询可以评估在时间多项式中的链的大小和最大奖励。
2013-01-10 cs.LO
Distributional Probabilistic Model Checking
本文提出概率模型检测的分布式扩展，适用于DTMCs和MDPs，支持方差、风险价值等分布式查询，并开发了计算完整分布及近似最优策略的方法，实验验证了其可扩展性。
2024-03-15 cs.LO
Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)
Universidad Nacional de Córdoba（科尔多瓦国立大学）；CONICET（阿根廷国家科学研究委员会）；University of Twente（特温特大学）；Dresden University of Technology（德累斯顿工业大学）；Centre for Tactile Internet with Human-in-the-Loop (CeTI)（带有人类参与触觉互联网中心）
提出首个基于轻量级策略采样的多目标统计模型检验方法，用于逼近帕累托最优前沿，并实现有限预算下的有效近似。
2026-07-02 cs.LO
Lazy Probabilistic Model Checking without Determinisation
在定量分析的马尔可夫链和马尔可夫决策过程对规范的LTL或作为某种形式的不确定的Büchi自动机的瓶颈是列入一个确定步骤的自动机正在考虑。在本文中，我们表明，完全确定可以避免：子集和断点的建设就足够了。我们已经实现了我们的方法-明确和符号的版本-在一个原型工具。我们的实验表明，我们的原型可以与成熟的工具，如PRISM竞争。
2015-04-24 cs.FL cs.LO
Verifying Reachability Properties in Markov Chains via Incremental Induction
在概率验证和非概率验证之间存在可扩展性差距。概率模型检验工具基于显式引擎或（多端）二元决策图。这些结构在非概率验证领域得到了更可扩展的技术（如IC3）的补充。我们提出了一个符号概率模型检验算法的基础上IC3类增量建设的归纳条款划分的状态空间，交错与增量建设的线性不等式系统。本文比较了我们的实现标准的定量验证的替代方案：我们的实验表明，我们的算法是一个步骤，以更可扩展的符号验证有限状态马尔可夫链中的罕见事件。
2019-09-19 cs.LO
Quantitative Verification of Neural Networks And its Security Applications
National University of Singapore（新加坡国立大学）；University of California, Berkeley（加州大学伯克利分校）
神经网络越来越多地用于安全关键领域。这促使人们对验证或证明神经网络的逻辑编码属性感兴趣。先前的工作主要集中在检查存在属性，其中目标是检查是否存在违反给定属性的任何输入。然而，神经网络训练是一个随机过程，在它们的分析中出现的许多问题需要概率和定量推理，即，估计有多少输入满足给定的属性。为此，我们提出了一个新的和原则性的框架，定量验证的逻辑属性指定的神经网络。我们的框架是第一个提供PAC风格的稳健性保证，因为它的定量估计是在一个可控的和有界的误差从真正的计数。我们通过构建一个名为NPAQ的原型工具来实例化我们的算法框架，该原型工具可以检查二进制神经网络的丰富属性。我们展示了新兴的安全分析如何在3个具体的应用程序中利用我们的框架：量化对抗性输入的鲁棒性，特洛伊攻击的有效性，以及给定神经网络的公平性/偏见。
2019-06-25 cs.AI cs.CR cs.LG
Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
在本文中，我们研究了一个模型的量子马尔可夫链，这是一个量子模拟的马尔可夫链，并得到取代概率的转移矩阵与量子操作。我们表明，这个模型是非常适合描述的混合动力系统，包括一个量子组件和一个经典的，虽然它具有相同的表达能力，另一个量子马尔可夫模型在文献中提出的。事实上，在量子信息处理中经常会遇到混合系统;例如，量子程序和量子协议都可以被视为混合系统。因此，我们进一步提出了一个称为混合量子自动机（HQA）的模型，可以用来描述这些从外部世界接收输入（动作）的混合系统。我们证明了HQA的语言等价问题是多项式时间可判定的。此外，我们将这个结果应用到量子马尔可夫链的迹等价问题，从而它也是多项式时间可判定的。最后，我们讨论了量子马尔可夫链的线性时间性质的模型检验，并表明可以成功地解决正则安全性的定量分析。
2015-06-30 cs.LO quant-ph
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
LIPN CNRS UMR 7030 Université Sorbonne Paris Nord（巴黎北大学国家科学研究中心联合研究实验室）；Pohang University of Science and Technology（韩国科学技术院）；University of Oslo（奥斯陆大学）
本文提出了一种用于参数时间Petri网的形式化分析与参数综合框架，利用重写逻辑与SMT求解器实现精确语义分析，通过符号可达性方法实现参数综合，实验表明方法在多个方面优于现有工具。
2024-09-12 cs.LO
Converting Reconfigurable Petri Nets to Maude
模型检验是理论计算机科学的一个重要研究方向。它可以验证具有一组属性（如活性，死锁或安全性）的模型。典型的建模技术之一是Petri网，它们被很好地理解并且可以用于模型检验。可重构Petri网是基于一组规则的Petri网。这些规则可以动态地用于改变网络。缺少的是验证可重构网络和死锁或活性等属性的可能性。本文介绍了一个转换可重构Petri网Maude，使我们能够填补空白。提出了一种基于Maude方程-重写逻辑和LTLR模型检验器的网变换方法。
2014-11-12 cs.FL cs.LO
Model Checking Matrix Product States against Linear Chain Logic
School of Cryptology, East China Normal University（华东师范大学密码学院）；Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所系统软件重点实验室）
本文提出线性链逻辑(LCL)，用于验证周期性MPS家族在系统尺寸增长时的物理性质，如环上的非平凡性和大尺寸渐进行为，通过完全正映射分析MPS的定量特征，实现高效的模型检查算法。
2026-05-14 cs.LO quant-ph
Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
本文提出信号时空逻辑（SSTL），用于指定和监控线性时间与离散空间模型的时空属性，支持布尔与定量语义，并应用于图灵反应-扩散系统和大型共享单车系统验证。
2018-10-22 cs.LO
From Width-Based Model Checking to Width-Based Automated Theorem Proving
Stockholm University（斯德哥尔摩大学）；University of Bergen（卑尔根大学）
本文提出一个通用框架，将大量基于宽度的模型检验算法转换为用于测试图论猜想在有限宽度图类上有效性的算法，改进了理论上的上界。
2024-09-15 cs.AI cs.DM cs.DS
Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata
各类无穷状态递归概率系统分析和模型检验的中心计算问题（包括拟生灭过程、多类型分支过程、随机上下文无关文法、概率下推自动机和递归马尔可夫链）是{ \em终止概率}的计算，并且计算这些概率又归结为计算对应的{ \em单调多项式系统}（MPS）的方程的{ \em最小不动点}（LFP）解，表示为x=P（x）。Etessami和Yannakakis证明了牛顿方法的分解变体对于任何具有非负解的MPS单调收敛于LFP解。随后，Esparza，Kiefer和Luttenberger得到了牛顿方法对某些类型MPS的收敛速度的上界。最近，更好的上限已获得特殊类的MPS。然而，在本文之前，对于任意（不一定是强连接的）MPS，牛顿方法的收敛速度作为输入MPS的编码大小|P|的函数，x=P（x），根本没有上界。在本文中，我们提供了最坏情况下的上界，作为输入编码大小|P|和Σ> 0的函数，对于具有LFP解q^* 的任何MPS，分解牛顿法（即使有舍入）在q^* 的加性误差Σ> 0内收敛所需的迭代次数。我们的上界基本上是最优的几个重要参数。使用我们的上界，并建立在以前的工作，我们获得了第一个P-时间算法（在标准图灵计算模型）的定量模型检验，在所需的精度，离散时间QBD和（等效）概率1-计数器自动机，相对于任何（固定）ω-正则或LTL属性。
2013-04-26 cs.CC cs.LO
Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems
大多数现有的概率模型检验案例研究是基于很好理解的理论模型和分布。然而，现实生活中的概率系统通常涉及分布参数，其值是通过经验测量获得的，因此受到小扰动。在本文中，我们考虑这些系统的参数模型（即，参数马尔可夫链）配备了绝对距离的范数。我们的主要贡献是一种方法来计算渐近界的形式的条件数的约束可达概率对扰动的分布参数的系统。通过Zeroconf协议和跳蛙问题的实验证明了该方法的有效性。
2013-08-28 cs.LO cs.SE
Efficient Algorithms for Checking Fast Termination in VASS
带状态的向量加法系统（VASS）由配备有d个计数器的有限状态空间组成，其中在每个转换中，每个计数器递增、递减或保持不变。VASS为分析并发进程、参数化系统提供了一个基本模型，也可作为程序的抽象模型用于边界分析。虽然终止是基本的活性属性，它询问给定模型是否总是终止的定性问题，但更一般的定量问题要求终止步骤的数量。在定量界领域的一个基本问题是获得渐近界的终止时间。大的渐近界，如指数或更高的已经表明，要么有一些错误的建模，或模型是没有用的实践。因此，我们专注于VASS的多项式渐近界。虽然一些众所周知的方法（例如，字典排序函数）对于多项式边界既不可靠也不完整，其他方法仅给出了用于上界的可靠方法。在这项工作中，我们的主要贡献如下：第一，对于线性渐近界，我们提出了一个健全的和完整的方法VASS，而且，我们的算法运行在多项式时间。其次，我们根据循环向量的法线对VASS进行分类。我们表明，在正常的奇异性是渐近界，如指数和非小学VASS的关键原因。在没有奇异性的情况下，我们证明了渐近复杂性界总是多项式的形式$Θ(n^k)$，对于一些k $\leq$ d。我们提出了一个算法，时间复杂度多项式的大小的VASS和指数的维数d，计算最佳k。
2017-08-29 cs.CC cs.DS cs.FL
Alternating-Time Temporal Logic with Mean-Payoff Guarantees
Heriot-Watt University（赫瑞-瓦特大学）
本文提出带合取平均收益约束的ATL*扩展ATL*_mp，分析其模型检验复杂度、记忆层级等性质，证明有限记忆策略可实现低于完美记忆上确界的所有阈值，还关联了合作理性验证。
2026-08-05 cs.GT cs.LO cs.MA
Multi-Objective Model Checking of Markov Decision Processes
研究并给出了马尔可夫决策过程多目标模型检验问题的有效算法。给定MDP，M，以及给定多个线性时间（ω-正则或LTL）性质φ i，以及概率ri ε[0，1]，i=1，.，k，我们问是否存在控制器的策略σ，使得对于所有i，由σ控制的M的轨迹满足φ i的概率至少为ri。我们提供了一个算法，决定是否存在这样的策略，如果是这样产生它，并运行在时间多项式中的MDP的大小。这种策略可能需要同时使用随机化和内存。我们还考虑了更一般的多目标ω-正则查询，我们激励与应用的假设保证组合推理的概率系统。注意，在不同属性之间可以存在折衷：以高概率满足属性φ 1可能需要以低概率满足φ 2。将其视为多目标优化问题，我们需要关于“权衡曲线”或帕累托曲线的信息，以最大化不同属性的概率。我们证明了在MDP的大小下，可以计算关于时间多项式中的一组ω-正则性质的近似Pareto曲线。我们的定量上限使用LP方法。我们还研究了定性的多目标模型检验问题，我们表明，这些可以通过纯粹的图论方法进行分析，即使策略可能仍然需要随机化和内存。
2008-11-11 cs.CC cs.GT cs.LO
On Quantitative Algebraic Higher-Order Theories
我们探讨了扩展Mardare等人的可能性。定量代数的结构，自然出现的组合逻辑和微积分。首先，我们证明了该框架确实适用于这些结构，并给出了可靠性和完备性结果。然后，我们证明了一些负面的结果，清楚地描绘到何种程度的度量空间范畴可以这样的理论模型。最后，我们给出了几个例子的非平凡高阶定量代数。
2022-04-28 cs.LO math.LO
Pushdown Model Checking Above the Cubic Bottleneck
Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；University of Warwick（华威大学）
本文从细粒度复杂度理论角度，基于3k-团等假设证明下推模型检测现有算法的时间下界，提出2NPDA(k)假设并通过线性归约网络佐证，解释该问题长期无更优算法的原因。
2026-08-26 cs.CC cs.FL cs.LO
