Probabilistic Weighted Automata
不确定加权自动机是在变迁上具有数值权重的有限自动机。它们定义了数量语言L，给每个词w分配一个实数L（w）。无限词w的值被计算为w上所有游程的最大值，游程的值被计算为最大值、limsup、liminf、极限平均值或转换权重的折扣和。我们引入了概率加权自动机，其中以随机（而不是非确定性）方式选择转换。在几乎肯定语义（分别）。正语义），则单词w的值是最大实数v，使得在w上的游程具有至少为v的值，概率为1（分别为正概率）。我们研究了概率加权自动机的自动机理论的经典问题：空性和普遍性，表达性，以及在各种语言操作下的封闭性。对于数量语言，空性和普遍性被定义为一些（分别）的值是否。每一个）字都超过了给定的阈值。我们证明了这些问题中的一些是可判定的，而另一些是不可判定的。关于表达能力，我们表明，概率使我们能够定义各种各样的新类的定量语言，除了贴现和自动机，概率的选择是没有更多的表达比非确定性。最后，我们给出了一个几乎完整的图片封闭的概率加权自动机的各种类以下逐点操作的定量语言：最大值，最小值，总和，和数值补。
2009-09-09 cs.LO
Minimal witnesses for probabilistic timed automata
见证子系统在概率系统的分析中被证明是一个有用的概念，例如作为关于为什么给定属性成立的诊断信息或作为细化算法的输入。介绍了概率时间自动机（PTA）中可达性问题的见证子系统。使用一个新的操作差界矩阵，它示出了如何法卡斯证书的有限状态互模拟子系统的PTA可以被翻译成见证子系统。我们提出了算法的最小见证子系统的三个概念下的最小性，从不同的角度捕捉的时间行为的计算，并讨论了它们的复杂性。
2020-07-01 cs.LO
Backwards Reachability for Probabilistic Timed Automata: A Replication Report
向后可达性是一种有效的基于区域的概率时间自动机模型检验方法。PTCTL属性。然而，当前的实现仅限于可达性属性的最大概率。在本文中，我们报告我们的新实现的向后可达性的一部分，适度的工具集。它支持直到公式的最小和最大概率，使其成为当今最通用的实现。我们比较其行为的实验结果报告的原始论文提出的向后可达性技术。
2022-08-25 cs.LO
POPACheck: A Model Checker for Probabilistic Pushdown Automata
TU Wien（维也纳工业大学）
POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。
2025-06-04 cs.LO
Model Checking Probabilistic Pushdown Automata
我们考虑概率下推自动机（pPDA）的模型检验问题和各种概率逻辑中可表达的属性。我们开始与属性，可以制定为一个广义的随机游走问题的实例。我们证明了定性和定量的模型检验这类性质和pPDA是可判定的。然后，我们证明了模型检验的定性片段的逻辑PCTL和pPDA也是可判定的。此外，我们开发了一个容错的模型检验算法的PCTL和无状态pPDA的子类。最后，我们考虑了一类ω-正则性质，并证明了pPDA的定性和定量模型检验都是可判定的。
2006-03-09 cs.LO
Compositional Reasoning for Probabilistic Automata with Uncertainty
RWTH Aachen University（亚琛工业大学）
本文提出一种假设-保证框架，用于验证具有不确定转移概率的概率自动机。研究了参数概率自动机和鲁棒概率自动机，建立了不对称、循环和交错证明规则，用于验证多目标查询，如概率可达性和参数期望总奖励。
2026-03-31 cs.LO
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective
本文从余代数视角统一推广公平模拟至非确定性树自动机和概率词自动机，并证明其可靠性以验证语言包含。
2017-09-05 cs.LO
Refinement and Difference for Probabilistic Automata
本文研究了随机系统的差分算子，其规格用抽象概率自动机（APAs）表示。在细化在两个规范之间失败的情况下，该操作符的目标是产生一个规范APA，该规范APA表示该失败的所有见证PA。我们的贡献是一个算法，允许近似的差异，两个APA任意精度。我们的技术依赖于新的定量概念的APA之间的距离，用于评估收敛的近似，以及对APA的细化关系的深入检查。该过程是有效的，并且不比细化检查更复杂。
2014-08-25 cs.LO
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
马尔可夫链有强模拟关系和弱模拟关系，概率自动机有强模拟关系和强概率模拟关系。然而，马尔可夫链上的强模拟和弱模拟以及概率自动机上的强模拟的决策算法并不有效，这使得它们是否可以像它们的非概率对应物那样有效地使用还不清楚。本文提出了大幅改进的算法，以决定是否一些（离散或连续时间）马尔可夫链强或弱模拟另一个，或者是否一个概率自动机强模拟另一个。关键的创新是使用参数最大流技术来分期计算。我们还提出了一种新的算法来决定强概率模拟前序的概率自动机，它具有多项式复杂性，通过减少到LP问题。当概率自动机的算法扩展到连续时间对应，我们保留了相同的复杂性强和强概率模拟。
2008-11-18 cs.LO
A Decidable Probability Logic for Timed Probabilistic Systems
在本文中，我们扩展的谓词逻辑介绍[Beauquier等人。2002]，以处理半马尔可夫过程。我们证明，相对于定性概率性质，模型检验是可判定的这种逻辑应用于半马尔可夫过程。此外，我们将我们的逻辑概率时间自动机考虑经典和紧急语义，并考虑时钟上的谓词。我们证明，半马尔可夫过程的结果也举行概率时间自动机的两个语义考虑。此外，我们证明了马尔可夫过程的结果[Beauquier et al. 2002]是可扩展的概率时间自动机，其中紧急语义被认为是。
2006-03-29 cs.LO
The Decidability Frontier for Probabilistic Automata on Infinite Words
我们认为概率自动机的无限的话，接受定义的安全性，可达性，Büchi，coBüchi，和限制平均条件。我们考虑定量和定性决策问题。我们提出了概率有限自动机的扩展和适应性证明，并提出了一个完整的刻画概率自动机的定量和定性决策问题的可判定性和不可判定性的边界上无限的话。
2011-04-27 cs.FL cs.LO
Convex Language Semantics for Nondeterministic Probabilistic Automata
我们探索语言语义的自动机结合概率和不确定性的行为。我们首先证明了具有非确定性的概率自动机有两种自然语义。对于这两种选择，我们表明，这些自动机是严格的表达比确定性概率自动机，我们证明了检查语言等价性的问题是不可判定的减少从阈值问题。然而，我们提供了一个折扣度量，可以计算到任意高的精度。
2018-05-29 cs.FL cs.LO
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
概率自动机已成功地应用于并发和随机系统的形式化验证。有效的模型检验算法已经被研究，其中最常用的用于表达属性的逻辑是基于概率计算树逻辑（PCTL）及其扩展PCTL^*。提出了各种行为等价物，作为一个强大的工具，抽象和组合最小化的PA。不幸的是，这些等价是众所周知的合理的，但就PCTL或PCTL* 所诱导的逻辑等价而言并不完整。塞加拉在1995年指出了一个既健全又完整的行为等价的愿望，但多年来一直没有定论。在本文中，我们引入了新的概念，强互模拟关系，PCTL和PCTL* 的特点。我们扩展了弱互模拟的特点PCTL和PCTL* 没有下一个运营商，分别。此外，我们还扩展了模拟前序的框架。因此，我们的论文弥合了在这种情况下逻辑和行为等价性和前序之间的差距。
2013-06-21 cs.LO
MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata
马尔可夫自动机将连续时间、概率转移和非确定性结合在一个模型中。它们代表了一种重要而强大的方式来建模各种复杂的现实生活系统。然而，这样的模型往往很大，难以处理，使得抽象和抽象细化成为必要。在本文中，我们提出了一个抽象和抽象细化技术的马尔可夫自动机，基于游戏和菜单的概率自动机的抽象。第一个实验表明，显着减少的大小是可能的使用抽象。
2014-06-09 cs.LO
Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata
本文研究概率自动机及概率一计数器自动机对 PCTL 与 PCTL$^*$ 的模型检测，通过归约空性问题并构造行为等价的一计数器自动机，证明两类问题均不可判定。
2021-08-30 cs.FL cs.LO math.LO
Timed Automata with Polynomial Delay and their Expressiveness
我们考虑以前的模型的时间，概率和随机时间自动机，我们介绍我们的模型的时间自动机与多项式延迟，我们表征这些模型相对于彼此的表现力。
2019-03-17 cs.LO
Lattice structures for bisimilar Probabilistic Automata
本文证明了双相似概率自动机（PA）的某些集合上存在一个深层结构。这些结构的关键先决条件是PA的紧性概念。结果表明，紧双相似PA形成格。这些结果，然后使用，以建立范式不仅为有限自动机，而且为无限自动机，只要他们是紧凑的。
2014-02-27 cs.FL cs.LO
Cost Preserving Bisimulations for Probabilistic Automata
概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象，使弱概率互模拟作为参考概念，总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念，使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性，我们建立组合属性相对于并行组合。此外，多项式时间的决策算法，提出了，可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。
2015-02-16 cs.FL cs.LO
Bisimilarity of Probabilistic Pushdown Automata
研究了概率下推自动机及其子类的双相似性问题。我们的定义pPDA允许概率和非确定性的分支，概括了下推自动机的经典概念（没有ε-转换）。我们的第一个贡献是一个一般的建设，减少检查的概率转换系统的双相似性检查的非确定性转换系统。这种构造直接产生pPDA的双相似性的可判定性，以及概率基本过程代数的子类上的双相似性问题的基本上界，即，单态pPDA。我们进一步表明，通过仔细的分析，一般的减少可以用来证明一个EXPTIME上界的概率可见下推自动机的双相似性。这里我们还提供了一个匹配的下限，建立EXPTIME-完全性。最后，我们证明了概率单计数器自动机（pPDA的另一个子类）的判定双相似性是PSPACE完全的。在这里，我们使用一个更专门的参数来获得最佳的复杂度界限。
2012-10-08 cs.FL cs.LO
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
概率自动机是拉宾在1963年作为语言接受者引入的。两个自动机是等价的，当且仅当它们以相同的概率接受每个单词。另一方面，在过程代数领域，Segala于1995年重新提出了概率自动机，它比Rabin的自动机更具有一般性。互模拟已经提出了Segala的自动机来表征它们之间的等价性。到目前为止，等价的两个概念及其特征是最独立的研究。在本文中，我们考虑Segala的自动机，并提出了一个新的概念，基于分布的互模拟加入现有的等价和双相似。我们的互模拟桥梁社区中的两个密切相关的概念，并提供了一个统一的方式来研究他们的特点。我们通过研究基于分布的互模拟度量证明了我们的定义的实用性，这产生了拉宾自动机的等价性的强大概念。
2014-03-08 cs.FL cs.LO
On Zone-Based Analysis of Duration Probabilistic Automata
我们提出了一个扩展的基于区域的算法分析时间自动机处理系统的时间不确定性被认为是概率，而不是集理论。我们研究持续时间概率自动机（DPA），表示多个并行进程承认内存满连续分布的持续时间。对于这个模型，我们开发了一个扩展的基于区域的前向可达性算法，其后继算子是一个密度Transformer，从而提供了一个解决方案，验证和性能评估问题有关的非循环DPA（或循环DPA的有界时域行为）。
2010-11-01 cs.FL cs.LO
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
概率系统的模型检测问题主要依赖于将LTL转换为确定性Rabin自动机（DRW）。我们最近的Safraless翻译的LTL（F，G）片段产生较小的自动机相比，传统的方法。在这项工作中，而不是DRW，我们认为确定性自动机的接受条件作为广义拉宾对（DGRW）的析取。与DRW相比，LTL（F，G）公式到DGRW的Safraless翻译导致更小的自动机。我们提出了概率模型检测算法以及DGRW条件下的博弈求解。我们的新算法在理论界和实际评价方面都有所改进。我们比较PRISM与我们的新的翻译，并表明，新的翻译导致显着的改善。
2013-04-18 cs.FL cs.LO
An algorithmic approximation of the infimum reachability probability for Probabilistic Finite Automata
给定一个概率有限自动机（PFA），一组状态S和一个错误阈值e > 0，我们的算法近似于自动机到达S的下确界概率（量化所有无限词）。我们的结果对比与已知的结果，近似问题是不可判定的，如果我们考虑的上确界，而不是下确界。由于我们研究的是到达一组状态的概率，而不是以接受状态结束的概率，因此我们的工作与模型检验的关系比与形式语言的关系更大。
2010-09-20 cs.FL cs.LO
Compositional Reasoning for Parametric Probabilistic Automata
本文将概率自动机的假设-保证组合推理框架扩展到参数化概率自动机，支持多种证明规则、多目标属性与期望奖励验证，并提出组合模型的单调性推理规则。
2025-06-10 cs.LO math.PR
Combining Weak Distributive Laws: Application to Up-To Techniques
交替自动机和概率自动机的共代数建模长期以来一直受到阻碍的情况下分配律的幂集单子本身，分别幂集单子的有限分布单子。这可以用弱分配律的框架来解决。我们扩展这个框架的情况下，其中一个单子只是一个函子。我们提供了抽象的组合性结果，广义的确定过程，和系统的健全的技术。一路上，我们将这些结果作为一个激励的例子交替自动机。另一个例子是概率自动机，我们的结果产生的相互模拟的可靠性高达凸包。
2020-10-02 cs.LO
Quantitative Games on Probabilistic Timed Automata
两人零和博弈是一个完善的模型，用于合成优化某些性能标准的控制器。在这样的游戏中，一个玩家代表控制器，而另一个玩家描述（对抗）环境，控制器合成对应于计算控制器在给定标准下的最优策略。Asarin和Maler通过合成控制器来优化到达最终状态的时间，从而开始了对（非概率）时间自动机的定量游戏的研究。他们的方法的正确性和终止性依赖于利用一类特殊的函数的性质，称为简单函数，可以被随机表示。在本文中，我们考虑概率时间自动机上的定量博弈。由于简单函数的概念是不足以解决游戏在这种情况下，我们概括简单的功能，所谓的准简单的功能。然后，利用这类函数，我们证明了在概率时间自动机上求解具有期望可达时间或期望折扣时间准则的博弈问题是在NEXPTIME $\cap$ co-NEXPTIME中。
2010-06-03 cs.GT cs.LO
Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
本文通过博弈刻画概率双模拟，将其归约为非概率情形，并应用于概率下推自动机及其子类，分别得到PSPACE、EXPTIME和2-EXPTIME上界，且下界同样成立。
2018-11-14 cs.FL cs.LO
Profinite Techniques for Probabilistic Automata and the Markov Monoid Algorithm
我们考虑有限词上概率自动机的值1问题：它询问给定的概率自动机是否接受概率任意接近1的词。这个问题被认为是不可判定的。然而，已经提出了不同的算法来部分地解决它;最近已经表明，基于代数的马尔可夫Monoid算法是迄今为止最正确的算法。本文的第一个贡献是给出了马尔可夫么半群算法的一个特征。第二个贡献是发展了一个概率自动机的profinite理论，称为prostochastic理论。这个新的框架给出了一个拓扑帐户的价值1的问题，这在这种情况下是作为一个空问题铸造。上述特征是重新使用prostochastic理论，使我们能够给出一个简单的和模块化的证明。
2017-09-09 cs.FL cs.LO
Model Checking Probabilistic Operator Precedence Automata
TU Wien（维也纳工业大学）；AIT Austrian Institute of Technology（奥地利技术研究院）
本文针对概率下推自动机，引入概率算子优先级自动机，并针对POTLf$\chi$规范开发了最优的EXPTIME/EXPSPACE概率模型检测算法，同时支持LTL规范，为递归概率程序验证提供了首个最优上下文无关逻辑。
2026-09-23 cs.LO cs.PL
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
概率时间自动机（Probably Timed Automata，PTAs）是一种扩展了离散概率分布的时间自动机（Timed Automata，TA），它作为一种数学模型，广泛应用于随机和时间行为。在这项工作中，我们考虑的问题，模型检查的线性\emph{dense-time}性质在{PTA}。特别是，我们研究了线性密集时间属性，可以编码的TA与无限的验收criterion.First，我们表明，模型检查PTA对确定性TA规格的问题可以通过产品建设解决。基于乘积结构，证明了确定性TA规格问题的计算复杂性是EXPTIME-完全的。然后我们证明了当放宽到一般的（非确定性的）TA时，模型检测问题变得不可判定，我们的结果大大扩展了TA的稠密时间特性和非确定性。
2018-06-13 cs.FL cs.LO
High-level Counterexamples for Probabilistic Automata
在模型检验中，为被违反的系统性质提供简洁易懂的反例是一项重要的任务。概率系统的反例到目前为止，现有的工作计算一个大的系统运行或系统的状态的子集，这两者都是有限的使用手动调试。许多概率系统都是用一种保护命令语言来描述的，就像流行的模型检查器PRISM所使用的那样。在本文中，我们描述了如何一个最小的可能的子集的命令可以识别，一起使系统错误。我们还展示了如何进一步简化所选命令，以获得一个易于理解的反例。
2015-03-28 cs.LO cs.SE
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
本文研究概率下推自动机定量界证书与期望终止时间的关系，借助底层多项式方程组 Jacobian 的谱半径等性质，证明正几乎必然终止总存在易验证证书。
2023-04-23 cs.FL cs.LO
Computing Probabilistic Bisimilarity Distances for Probabilistic Automata
本文提出一种基于简单随机博弈的策略迭代算法，用于高效计算概率自动机的概率互模拟距离，并证明该距离可界定状态满足ω-正则性质的概率差。
2021-02-01 cs.FL cs.LO
Decision Questions for Probabilistic Automata on Small Alphabets
研究一元和二元概率有限自动机的空性与$\lambda$-可达性问题，根据歧义度和字母表大小刻画其复杂度，揭示了多项式与有限歧义下的NP困难性及EXPTIME可解性。
2023-12-20 cs.FL cs.LO
Modal Specifications for Probabilistic Timed Systems
模态自动机是一个经典的形式化模型，基于组件的系统，配备了丰富的规范理论支持抽象，细化和组合推理。近年来，模态自动机的定量变量被引入到嵌入式和移动系统的基于组件的设计的说明和推理中。这些分别概括了定时和概率系统的模态规范理论。在本文中，我们定义了一个模态规约语言的组合概率时间系统，称为抽象概率时间自动机，推广现有的形式主义。我们引入适当的语法和语义细化的概念，并讨论我们的规约语言的一致性，也相对于时间发散。我们确定了我们的模型，我们定义的抽象，结合和并行组合的基本操作的子类，并显示几个组合的结果。
2013-06-12 cs.FL cs.LO
Computing Distances between Probabilistic Automata
我们提出了概率自动机（PA）上的模拟和互模拟的宽松概念，允许一些误差epsilon。当λ为零时，我们恢复PA上的互模拟和模拟的通常概念。我们给出了这些概念的逻辑特征，通过选择适当的逻辑，它不同于基本的，L与否定和L没有否定，由模态算子。使用流网络，我们展示了如何计算PTIME中的关系。这允许定义PA的状态之间的有效可计算的非折扣距离。引入了对该距离的自然修改，以获得折扣距离，从而削弱了长期转换的影响。我们比较我们的概念的距离，以前定义的其他人，并说明我们的方法上的各种例子。我们还表明，我们的距离是不膨胀的过程代数算子。虽然没有否定的L是一个合适的逻辑，以确定性PA的双（双）模拟，它不是一般的PA;有趣的是，我们证明，它确实是一个较弱的概念，称为先验双（双）模拟，我们证明是NP-难以决定。
2011-07-06 cs.FL cs.LO
Probabilistic Disjunctive Normal Forms in Temporal Logic and Automata Theory
V.A. Trapeznikov Institute of Control Sciences of Russian Academy of Sciences（俄罗斯科学院控制科学瓦·阿·特拉佩兹尼科夫研究所）
本文提出概率析取范式用于表示和推理不确定性，结合代数证据组合与概率分布，实现逻辑、数值方法和连续概率的融合。
2026-03-11 cs.FL cs.LO math.PR
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
FlexFringe: Modeling Software Behavior by Learning Probabilistic Automata
Department of Software Technology, Delft University of Technology, the Netherlands（软件技术系，代尔夫特理工大学，荷兰）
本研究介绍了FlexFringe中概率确定性有限自动机学习方法的高效实现，通过改进状态合并策略提升性能，实验证明其在软件日志异常检测任务上优于现有神经网络方案。
2025-09-23 cs.LG cs.LO cs.SE
