Antichains for the Automata-Based Approach to Model-Checking
我们提出并评估反链算法来解决非确定Buechi自动机的普遍性和语言包含问题，以及交替Buechi自动机的空性问题。为了获得这些算法，我们建立了模拟前序的存在，可以利用这些前序来有效地评估在互补步骤中定义的自动机上的不动点（我们在我们的方法中保持隐式）。我们使用Tabakov和Vardi最近提出的随机自动机模型来评估算法的性能，以检查Buechi自动机的普遍性。我们表明，这种概率模型的困难的情况下，我们的算法优于标准的几个数量级。
2009-03-02 cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Model Checking Markov Chains Against Unambiguous Buchi Automata
本文给出了一个多项式时间算法，用于有限马尔可夫链的模型检验。
2016-03-26 cs.FL cs.LO
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
2014-02-11 cs.LO
Comparison of Algorithms for Checking Emptiness on Buechi Automata
我们重新研究有限状态系统的LTL模型检测问题。典型的解决方案，如Spin，在飞行中工作，将问题简化为Buechi空虚。这可以在线性时间内完成，并且存在具有此属性的各种算法。尽管如此，细微的设计决策可以在实践中对其实际性能产生很大的影响，特别是在动态使用时。我们比较了大量的算法实验上的一个大的基准套件，测量其实际运行时的性能，并提出改进。与Spin中实现的算法相比，我们的最佳算法平均快约33%。因此，我们建议，对于动态显式状态模型检验，嵌套DFS应该被更好的解决方案所取代。
2009-10-20 cs.LO
Real-Time Model-Checking: Parameters everywhere
本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。
2007-02-27 cs.LO
Fly-automata, model-checking and recognizability
可识别性定理指出，如果一组有限图可由一元二阶（Monadic Second Order，MSO）语句定义，则它相对于图代数是可识别的，而图宽度的定义是基于图代数的。可识别性是一个代数概念，用同余来定义，也可以用有限自动机来描述所考虑的图。该定理要求MSO图属性的验证，或者等价地，有限二元关系结构上的MSO逻辑的模型检验问题，对于由表示属性的公式和输入图或结构的树宽度（或树宽度）组成的参数是固定参数可处理的（FPT）。相应的算法可以通过飞行自动机来实现，其转换是在飞行中计算的，而不是列表。我们回顾了两个版本的可识别性，我们目前的苍蝇自动机的例子表明，他们也可以计算值附加到图。我们表明，飞自动机与无限的状态集产生一个简单的证明强版本的可识别性定理。这个证明以前没有发表过。
2014-09-18 cs.LO
Model Checking Constraint LTL over Trees
约束自动机是Büchi自动机的一种改进，它处理来自某种关系结构S的数据字。这样一个自动机的每一个转换都带有S的关系的约束。只有当当前和下一个数据值满足转换的所有约束时，才能触发转换。这些自动机已被用于设置，其中S是一个线性顺序，以确定约束LTL的约束S。在本文中，S是无限分枝的无限阶树T。给出了T-约束自动机空性的PSPACE算法。这一结果暗示了T上约束LTL的可满足性和模型检验问题的PSPACE完备性。
2015-04-23 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
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
Fly-automata for checking MSO 2 graph properties
一个描述性更强但太长的标题是：构造飞行自动机来检查用边量化写的一元二阶公式表示的有界树宽图的性质。这些特性简称为MSO 2。Fly-automata（FA）在表示图的术语上自底向上运行，并“动态”计算必要的状态和转换，而不是查看巨大的，实际上无法实现的表。在以前的工作中，我们已经构造了处理表示有界宽度的图的项的FA，以检查它们的一元二阶（MSO）性质（由没有边量化的公式表示）。在这里，我们适应这些FA的关联图，使他们可以检查MSO 2属性的有界树宽度的图。这是可能的，因为：（1）图的MSO ~ 2性质就是图的关联图的MSO性质;（2）图的关联图的树宽是线性有界的。我们的结构实际上是可实现的和可用的。我们详细介绍了具体的结构自动机在这个角度来看。
2015-12-22 cs.LO
MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
参数时间自动机扩展了时间自动机（Alfrer和Dill，1991），因为它们允许指定时钟值的参数边界。自1993年由Alfred，Henzinger和Vardi提出以来，已知具有一个时钟的参数时间自动机的空性问题是可判定的，而如果自动机使用三个或更多个参数时钟，则是不可判定的。该问题是开放的参数时间自动机与两个参数时钟。度量时态逻辑（Metric Temporal Logic，简称MTL）是一种广泛应用于实时系统的规约语言。时间自动机的MTL-模型检验是可判定的，无论时间自动机中使用多少时钟。本文证明了参数时间自动机的MTL-模型检验是不可判定的，即使该自动机只使用一个时钟和一个参数并且是确定的。
2014-04-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
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 cs.FL cs.LO
Model-Checking of Ordered Multi-Pushdown Automata
我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。
2012-09-19 cs.FL cs.LO
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)
Universidad Nacional de Córdoba（科尔多瓦国立大学）；CONICET（国家科学研究委员会）；University of Twente（特温特大学）
提出一种结合可细化区间抽象与“大时间步”语义的随机自动机模型检测方法，为最大/最小可达概率提供上下界，实验表明对非平凡示例有效。
2026-07-02 cs.LO
Improved Bounded Model Checking of Timed Automata
时间自动机（TA）是一个非常流行的建模形式主义的时间敏感的属性。一个常见的任务是验证TA的网络是否满足给定的属性，通常用线性时态逻辑（LTL）或时间计算树逻辑（TCTL）的子集表示。在本文中，我们建立在TACK有界模型检查TA，它支持基于信号的语义TA和更丰富的度量区间时态逻辑（MITL）。TACK将TA网络和属性编码为LTL的变体，即时钟约束LTL（CLTLoc）。产生的CLTLoc公式然后可以通过诸如Zot的工具求解，该工具将CLTLoc属性转换为可满足性模理论（SMT）求解器的输入逻辑。我们提出了一种新的方法，保留TACK的MITL属性的编码，同时直接到SMT求解器语言编码的TA网络，利用BitVector逻辑和逻辑的实算术。我们还介绍了几个优化，使我们能够显着优于CLTLoc编码在许多实际情况下。
2021-04-26 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
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
Model Checking One-clock Priced Timed Automata
我们考虑定价模型（a.k.a.加权）时间自动机，它是时间自动机的扩展，具有位置和转换的成本信息，我们基于对模态具有成本约束的经典时态逻辑的扩展来研究该模型的各种模型检查问题。我们证明，在假设模型只有一个时钟，模型检查这类模型对逻辑WCTL，CTL成本约束的方式，是PSPACE完全的（虽然它已被证明是不可判定的，只要模型有三个时钟）。我们还证明了模型检查WMTL，具有成本约束模态的LTL，只有当模型中有一个时钟和一个秒表成本变量（即，其斜率位于{0，1}中）。
2008-06-20 cs.CC cs.GT cs.LO
Symbolic Optimal Reachability in Weighted Timed Automata
加权时间自动机在2000年初被定义用于建模实时系统中的资源消耗或分配问题。在加权时间自动机中，最优可达性是可判定的，并提出了一种符号前向算法来解决这一问题。该算法使用所谓的定价区域，即具有成本函数的标准区域的扩展。为了确保终止，该算法要求时钟有界。对于未定价的时间自动机，已经做了很多工作来开发适合于时间自动机的前向探索的合理抽象，确保在不限制时钟的情况下终止模型检查算法。在本文中，我们利用最近的发展抽象的时间自动机，并提出了一个算法，允许符号分析的所有加权时间自动机，而不需要有界的时钟。
2016-02-01 cs.LO
Pumping lemmas for weighted automata
本文为加权自动机片段定义的五类函数提出泵引理，并证明在最小-加和最大-加半环上，无歧义、有限歧义、多项式歧义及完整加权自动机对应的函数层级是严格的。
2021-07-20 cs.LO
Automata-Based Software Model Checking of Hyperproperties
我们开发了时态流逻辑（TSL）和超时态流逻辑（HyperTSL）模理论的模型检验算法。TSL扩展了线性时序逻辑（LTL）的存储单元，功能和谓词，使其成为一个方便的和表达的逻辑推理软件和其他系统的无限数据域。HyperTSL进一步将TSL扩展到hyperproperties的规范-与多个系统执行相关的属性。因此，HyperTSL可以在软件系统中表达信息流策略，如不干涉。我们用理论扩充了HyperTSL，得到了HyperTSL（T），并建立在LTL软件验证的方法上，得到了TSL和HyperTSL（T）的模型检验算法。这导致了一个合理但不一定完整的算法，用于HyperTSL（T）的forall*exists* 片段中包含的规范。我们的方法构成了第一个软件模型检验算法的时间hyperproperties与量词交替，不依赖于有限状态的抽象。
2023-03-26 cs.FL cs.LO
An Automata Theoretic Characterization of Weighted First-Order Logic
本文在多项式模糊条件下，刻画了具有双向导航及鹅卵石或嵌套能力的扩展加权自动机片段，使其精确识别完整加权一阶逻辑，推广了Droste和Gastin的定量代数刻画。
2023-07-27 cs.LO
Verification of Timed Automata Using Rewrite Rules and Strategies
ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。
2009-07-17 cs.LO
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL cs.LO
Stochastic Timed Automata
随机时间自动机是定义在时间自动机上的纯随机过程，其中延迟和离散选择都是随机的。研究了该模型的几乎确定模型检验问题，即给定一个随机时间自动机A和一个性质$Φ$，我们想判定A是否以概率1满足$Φ$.在本文中，我们确定了几类自动机和属性，这可以决定。证明依赖于一个有限的抽象，称为厚图，我们解释为一个有限的马尔可夫链，我们可以决定几乎肯定的模型检查问题的建设。正确的抽象时，自动机几乎肯定公平，我们表明，是两大类系统，单时钟自动机和所谓的弱反应自动机的情况下。本文中使用的技术收集了实时验证和概率验证的工具，以及在时间自动机上进行的拓扑游戏。
2014-12-07 cs.LO
Timed Automata Robustness Analysis via Model Checking
本文针对时间自动机在设计阶段因时间常数不确定及实现扰动导致规范违反的问题，提出了通过模型检查进行鲁棒性分析的概念与技术，以辅助修复模型并确保可达性与安全规范。
2022-07-28 cs.FL cs.LO
Markov Chains and Unambiguous Automata
本文提出一种多项式时间算法，用于对表示为无歧义自动机的ω-正则规范进行离散时间Markov链的模型检测，证明其复杂度属于NC，与确定性自动机界限匹配且更具简洁性。
2023-04-07 cs.FL cs.LO
POPACheck: A Model Checker for Probabilistic Pushdown Automata
TU Wien（维也纳工业大学）
POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。
2025-06-04 cs.LO
Proving Safety with Trace Automata and Bounded Model Checking
循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。
2014-10-21 cs.FL cs.LO cs.PL
Probabilistic Weighted Automata
不确定加权自动机是在变迁上具有数值权重的有限自动机。它们定义了数量语言L，给每个词w分配一个实数L（w）。无限词w的值被计算为w上所有游程的最大值，游程的值被计算为最大值、limsup、liminf、极限平均值或转换权重的折扣和。我们引入了概率加权自动机，其中以随机（而不是非确定性）方式选择转换。在几乎肯定语义（分别）。正语义），则单词w的值是最大实数v，使得在w上的游程具有至少为v的值，概率为1（分别为正概率）。我们研究了概率加权自动机的自动机理论的经典问题：空性和普遍性，表达性，以及在各种语言操作下的封闭性。对于数量语言，空性和普遍性被定义为一些（分别）的值是否。每一个）字都超过了给定的阈值。我们证明了这些问题中的一些是可判定的，而另一些是不可判定的。关于表达能力，我们表明，概率使我们能够定义各种各样的新类的定量语言，除了贴现和自动机，概率的选择是没有更多的表达比非确定性。最后，我们给出了一个几乎完整的图片封闭的概率加权自动机的各种类以下逐点操作的定量语言：最大值，最小值，总和，和数值补。
2009-09-09 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
Refinement Checking for Multirate Hybrid ZIA
混杂系统是一个既有离散分量又有连续分量的动态系统。为了研究混合系统的建模和验证问题，本文首先介绍了一种结合接口自动机、初始化多速率混合自动机和Z语言的规范化方法MZIA。同时，我们提出了一个加细关系MZIA。在此基础上，给出了有限域MZIA之间加细关系的检验算法，并证明了算法的正确性。
2014-10-13 cs.FL cs.LO
Tree Regular Model Checking for Lattice-Based Automata
树规则模型检验（TRMC）是分析无限状态系统的一系列技术的名称，其中状态由项表示，状态集由树自动机（TA）表示。TRMC的核心问题是判断一组坏状态是否可达。计算表示可达状态集合（的过近似）的TA的问题是不可判定的，但是存在基于树换能器的完成或迭代的有效解决方案。不幸的是，TRMC框架无法有效地捕获系统的复杂结构及其某些功能。作为示例，对于JAVA程序，项的结构主要用于捕获系统的状态的结构。相反，Java程序的整数必须用Peano数编码，这意味着任何代数运算都可能由数千个重写规则的应用程序表示。在本文中，我们提出了格树自动机（LTA），树自动机的扩展版本，其叶子配备了格。LTA允许我们表示可能无限的解释术语集。这些术语能够以有效的方式表示复杂的域和相关操作。我们还将经典的布尔运算扩展到LTA。最后，作为一个主要的贡献，我们引入了一个新的基于完成的算法计算可能无限的可达解释条款在有限的时间。
2012-03-07 cs.FL cs.LO
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
Nested Weighted Limit-Average Automata of Bounded Width
虽然加权自动机提供了一个自然的框架来表达定量属性，但许多基本属性，如平均响应时间，不能用加权自动机来表达。嵌套加权自动机是加权自动机的扩展，它由一个主自动机和一组由主自动机调用的从自动机组成。嵌套的加权自动机比加权自动机更严格地表达（例如，平均响应时间可以用嵌套加权自动机来表示），但是基本判定问题具有更高的复杂性（例如，对于确定自动机，嵌套加权自动机的空性问题是PSPACE-困难的，而加权自动机的空性问题的复杂性是PTIME）。我们考虑嵌套加权自动机的一个自然子类，其中在任何一点上，至多有一个有界数量k的从自动机可以是活动的。我们重点研究了主价值函数是极限平均的自动机。我们证明了这些嵌套的有界宽度的加权自动机比加权自动机（例如，没有重叠请求的平均响应时间可以用界限k=1表示，但不能用非嵌套加权自动机表示）。我们表明，基本决策问题的复杂性（即，空性和普遍性）匹配加权自动机的复杂性。此外，当k是一元输入的一部分时，我们建立PSPACE-完备性。
2016-06-11 cs.FL cs.LO
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
Rewrite based Verification of XML Updates
我们考虑XML文档更新的访问控制问题。在XML编程的上下文中，类型可以被视为对冲自动机，静态类型检查相当于验证程序总是将有效的源文档转换为有效的输出文档。给定一组更新操作，我们特别感兴趣的是检查安全属性，例如在任何更新序列中保存文档类型。我们还感兴趣的相关政策的一致性问题，即检测是否授权的操作序列可以模拟禁止的。我们减少这些问题的类型检查问题，解决了计算变种的对冲自动机特征的祖先和后代的初始文档类型的参数化重写规则关闭。
2009-07-29 cs.LO
Revisiting MITL to Fix Decision Procedures
度量区间时态逻辑（Metric Interval Temporal Logic，MITL）是一种具有可判定可满足性和模型检验问题的实时时态逻辑。MITL的决策过程依赖于自动机理论方法，其中逻辑公式被转换为等效的时间自动机。由于时间自动机在互补下不封闭，MITL的决策过程首先将公式转换为否定的范式，然后再转换为时间自动机。我们发现，不幸的是，这些20岁的程序是不正确的，因为它们依赖于一个不正确的语义的R运算符。我们提出了正确的语义R，并给出了新的，正确的决策程序MITL。我们表明，可满足性和模型检验的MITL是EXPSPACE完全的，如前所述。我们还确定了一个片段的MITL，我们称之为MITL_{WI}是丰富的比MITL_{0,\infty}，我们表明，可满足性和模型检验是PSPACE完成。我们的许多结果已经在PVS中得到了形式化的证明。
2019-10-09 cs.LO
A translation of weighted LTL formulas to weighted Büchi automata over ω-valuation monoids
本文在乘积$ω$ -赋值幺半群上引入了一个满足特定性质的加权LTL。我们还引入了带$\varepsilon$ -转移的加权广义Büchi自动机，以及在积$ω$ -赋值幺半群上带$\varepsilon$ -转移的加权Büchi自动机，并证明了这两个模型在表达上是等价的，也等价于文献中已经引入的加权Büchi自动机.我们证明了我们的逻辑的一个句法片段的每个公式可以有效地转化为一个加权的广义Büchi自动机与$\varepsilon$ -转移。对于满足特定性质的广义乘积$ω$ -赋值幺半群，我们定义了加权LTL，带$\varepsilon$ -变迁的加权广义Büchi自动机，带$\varepsilon$ -变迁的加权Büchi自动机，并证明了广义乘积$ω$ -赋值幺半群的上述结果.本文给出了一个带限制的语法片断的加权LTL公式到带$\varepsilon$ -转移的加权广义Büchi自动机的转化。
2022-01-02 cs.FL cs.LO
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
A Note on Fault Diagnosis Algorithms
在本文中，我们审查算法检查离散事件系统和时间自动机的可诊断性。我们指出，在这两种情况下的可诊断性问题减少到空性问题（定时）Büchi自动机。此外，它是已知的，检查是否离散事件系统是可诊断的，也可以减少到检查有界可诊断性。我们建立了一个类似的时间自动机的结果。我们还提供了一个综合的复杂性结果，为不同的故障诊断问题。
2010-04-16 cs.FL cs.LO
Aperiodic Weighted Automata and Weighted First-Order Logic
根据Schützenberger，McNaughton和Papert在1970年代的基本结果，一阶可定义语言和非周期语言的类别是一致的。在这里，我们将这种等价性扩展到定量设置。为此，加权自动机形成了一个通用的和广泛研究的模型。我们定义了一个合适的加权一阶逻辑的概念。然后，我们证明了这种加权一阶逻辑和非周期多项式模糊加权自动机具有相同的表达能力。此外，我们还得到了适当的加权子逻辑和无二义性或无二义性的非周期加权自动机的等价结果。我们的结果适用于一般的重量结构，包括所有半环，平均计算的成本，有界格，和其他。
2019-09-30 cs.FL cs.LO
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
A Nivat Theorem for Weighted Alternating Automata over Commutative Semirings
本文连接了 WAFA、WFTA 和 PA 三类自动机，通过运行语义中的树使用证明交换半环上 WAFA 行为的 Nivat 刻画，揭示了其与 PA 的反转等价性，并证明了有理数权重下 ZERONESS 问题的可判定性。
2023-12-19 cs.FL cs.LO
Certifying Emptiness of Timed Büchi Automata
时间自动机的模型检测器被广泛用于验证安全关键的实时系统。最先进的工具通过复杂的抽象实现可伸缩性。我们的目标是进一步提高他们的验证结果的信任，特别是检查活性属性。为此，我们开发了一种方法提取证书的空时间Büchi自动机从模型检验运行。这些证书可以由我们在Isabelle/HOL中正式验证的认证者进行双重检查。我们在一个抽象的环境中研究活性证书，并表明我们的方法是健全和完整的。为了证明它的可行性，我们提取了几个模型的证书，这些模型由Tandem和Imitator检查，并使用我们经过验证的认证器对其进行验证。
2020-07-08 cs.FL cs.LO
Determinization of Min-Plus Weighted Automata is Decidable
本文证明了最小加加权自动机的确定化问题可判定，解决了长期开放问题，并提出了分析非确定性自动机运行结构的新工具。
2025-03-31 cs.FL cs.LO
Multi-weighted Automata and MSO Logic
加权自动机是一种非确定性自动机，其中的转换都带有权值。它们可以模拟系统的定量方面，如成本或能耗。运行的值可以被计算为例如转变权重的最大值、极限平均值或折扣总和。在多重加权自动机中，转换带有多个权重，并且可以模拟例如奖励和成本之间的比率，或者在二级资源上的某个上限约束下的主要资源的使用效率。在这里，我们介绍了一个一般模型的多加权自动机以及多加权MSO逻辑。在我们的主要结果中，我们表明，这种多加权MSO逻辑和多加权自动机是表示等价的有限和无限的话。翻译过程是有效的，导致我们的多加权MSO逻辑的可判定性结果。
2015-06-19 cs.FL cs.LO
Determinisation and Unambiguisation of Polynomially-Ambiguous Rational Weighted Automata
本文研究有理数域上加权自动机的确定化与去歧义化问题，证明对多项式模糊加权自动机，这两个问题均属于 PSPACE，填补了 Bell 和 Smertnig 可判定性结果中复杂度界限的空白。
2025-05-27 cs.FL cs.LO
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
本文研究一类非常一般的无限秩树的逻辑性质，即由高阶递归方案生成的无限秩树。我们考虑，对于一元二阶逻辑和模态μ演算，三个主要问题：模型检查，逻辑反射（又名全局模型检查，要求公式成立的元素集的有限描述）和选择（要求，如果存在的话，要求具有二阶自由变量的MSO公式成立的元素集的有限描述）。对于每一个问题，我们都提供了有效的解决方案。这是由于高阶递归方案和可折叠下推自动机之间的已知连接，并在以前的工作有关奇偶校验游戏上的过渡图的可折叠下推自动机。
2021-03-02 cs.FL cs.LO
Reducing Clocks in Timed Automata while Preserving Bisimulation
随着时钟数目的增加，模型检验时间自动机变得越来越复杂。因此，人们希望用尽可能少的时钟来构造一个自动机。检查是否存在一个具有较少时钟的时间自动机，使得原始自动机接受的时间语言被保留的问题是不可判定的。在本文中，我们给出了一个结构，它对任何给定的时间自动机产生一个时间双相似自动机与最少数量的时钟。此外，我们表明，这样一个自动机的最小可能数量的时钟可以构建的时间是双指数的原始自动机的时钟的数量。
2015-05-20 cs.FL cs.LO
Stochastic Model Checking for Multimedia
现代分布式系统包括一类非功能性需求很重要的应用程序。特别是，这些应用程序包括多媒体设施，实时约束是至关重要的，他们的正确运作。为了指定这样的系统，它是必要的，以描述事件发生的概率分布和随机自动机已成为一个有用的技术，通过它可以指定和验证这样的系统。然而，随机描述是非常一般的，特别是它们允许使用一般的概率分布函数，因此它们的验证可能是复杂的。在过去的几年里，模型检测已经成为一个有用的验证工具，大型系统。在本文中，我们描述了两个随机自动机的模型检测算法。这些算法考虑如何写在一个简单的概率实时逻辑的属性可以检查一个给定的随机自动机。
2000-02-04 cs.LO cs.MM
