The Complexity of Satisfiability Checking for Symbolic Finite Automata
本文研究符号有限自动机的可满足性问题，通过将其分解为输入字符理论与接受单词索引的单子二阶理论，获得了该自动机类及其线性算术约束扩展的紧计算复杂度界限。
2023-06-30 cs.LO
Model Checking for a Class of Weighted Automata
在过去的十年中，已经提出了大量不同的模型检验方法。不同的方法适用于不同的模型类型，包括不定时，定时，概率和随机模型。本文提出了一种新的模型检验技术框架，其中包括一些已知的方法，但扩大了可将模型检验应用于一般加权自动机类的模型类别。该方法允许一个简单的适应模型检验的模型，尚未考虑为此目的。可以应用模型检验的那些新模型类型的例子是max/plus或min/plus自动机，它们是描述不同形式的动态系统和优化问题的良好建立的模型。在这种情况下，模型检验可用于验证系统的时间或定量属性。本文首先简要介绍了我们的类加权自动机，作为一个非常一般的模型类型。然后给出了值计算树逻辑（CTL）的$) is introduced as a natural extension of the well known branching time logic CTL. Afterwards, algorithms to check a weighted automaton according to a CTL$公式。最后，给出了加权自动机和CTL$的互模拟。
2003-04-15 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
Bounded Model Checking of an MITL Fragment for Timed Automata
时间自动机（TA）是一种常见的建模时间系统的形式。有界模型检验（BMC）是一种使用SAT或SMT求解器搜索违反属性的运行的验证方法。MITL是线性时间逻辑LTL的实时扩展。最初，MITL被定义为非重叠时间间隔的轨迹，而不是“超密集”时间轨迹，允许时间间隔重叠在单个点上，这些点被当今常见的时间自动机语义所采用。在本文中，我们扩展的MITL片段的语义超密集的时间轨迹，并设计了一个有界的模型检验编码的片段。我们证明了正确性和完整性的意义上说，使用一个足够大的范围内的反例，任何给定的非控股property.We可以找到实现建议的有界模型检验方法和实验研究的效率和可扩展性的实现。
2013-04-26 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
Antichains for the Automata-Based Approach to Model-Checking
我们提出并评估反链算法来解决非确定Buechi自动机的普遍性和语言包含问题，以及交替Buechi自动机的空性问题。为了获得这些算法，我们建立了模拟前序的存在，可以利用这些前序来有效地评估在互补步骤中定义的自动机上的不动点（我们在我们的方法中保持隐式）。我们使用Tabakov和Vardi最近提出的随机自动机模型来评估算法的性能，以检查Buechi自动机的普遍性。我们表明，这种概率模型的困难的情况下，我们的算法优于标准的几个数量级。
2009-03-02 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 memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Beyond Language Equivalence on Visibly Pushdown Automata
我们研究了（双）模拟类的前序/等价性检查的类可见下推自动机及其自然子类可见BPA（基本进程代数）和可见一计数器自动机。我们描述了通用的方法来证明复杂性的上限和下限的一些研究前序和等价物，如模拟，完成模拟，准备模拟，2嵌套模拟前序/等价物和互模拟等价。我们的主要结果是，所有提到的等价和前序是EXPTIME-完全的可见下推自动机，PSPACE-完全的可见一计数器自动机和P-完全的可见BPA。我们的PSPACE下界明显的一计数器自动机也提高了以前已知的DP-硬度结果为普通的一计数器自动机和一计数器网。最后，我们研究了可见下推自动机的正则性检验问题，证明了它们可以在多项式时间内判定。
2009-01-26 cs.CC cs.LO
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 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
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
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 Probabilistic Operator Precedence Automata
TU Wien（维也纳工业大学）；AIT Austrian Institute of Technology（奥地利技术研究院）
本文针对概率下推自动机，引入概率算子优先级自动机，并针对POTLf$\chi$规范开发了最优的EXPTIME/EXPSPACE概率模型检测算法，同时支持LTL规范，为递归概率程序验证提供了首个最优上下文无关逻辑。
2026-09-23 cs.LO cs.PL
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
Parity Games and Automata for Game Logic (Extended Version)
Parikh的游戏逻辑是一个类似PDL的不动点逻辑，它在单调邻域框架上解释，表示玩家在确定的两人游戏中的战略力量。博弈逻辑转化为单调$μ$ -演算的一个片段，而单调模式自动机又在表达上等价于单调模式自动机。奇偶博弈和自动机是处理模态不动点逻辑（如模态$μ$ -演算）中嵌套不动点的组合复杂性的重要工具。本文（1）讨论了邻域结构上博弈逻辑的奇偶博弈语义a，（2）利用这些博弈得到了对应于博弈逻辑的单调$μ$ -演算片段的自动机理论刻画。我们的证明广泛使用的结构，我们称之为语法图，结合了易于使用的语法树的公式与自动机的灵活性和简洁性。它们本质上是一个基于图的观点的交替树自动机，介绍了威尔克在研究模态$μ$ -演算。
2017-09-03 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
Proving Safety with Trace Automata and Bounded Model Checking
循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。
2014-10-21 cs.FL cs.LO cs.PL
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。
2012-07-04 cs.FL 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
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 Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
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
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
On MITL and alternating timed automata over infinite words
单时钟交替时间自动机（OCATA）已被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义。在本文中，我们认为OCATA的模型检查和可满足性的问题MITL（MTL的语法片段），解释了无限的话。我们的方法是基于扩展到无限词的区间语义（最近在[BEG13]中介绍了有限词的情况）。我们提出了基于区域和基于区域的算法，基于这种语义，MITL模型检查和可满足性。我们报告的原型工具实现这些算法的性能。
2014-06-17 cs.LO math.LO
Towards Approximate Model Checking DC and PDC Specifications
DC已被证明是一个很有前途的工具，用于规范和验证硬实时系统设计的功能需求。许多工作致力于开发有效的技术来检查模型的硬实时系统对直流规格。DC模型检验理论仍在不断发展，但由于微积分的高度不可判定性和模型检验的高度复杂性，目前还没有可用的工具支持实际验证。PDC模型检验的现状远不如DC模型检验。鉴于迄今为止取得的成果，它是可取的DC和PDC规格开发近似的模型检验技术。这项工作的动机是开发近似技术检查DC和PDC规格的硬实时系统的自动机模型。不同于以往的作品，只处理可判定的公式，我们要发展的近似技术，涵盖整个DC和PDC公式。我们的工作，即近似技术检查实时自动机模型的系统LDI和PLDI规范的第一个结果，本文中描述。
2012-12-16 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
On MITL and alternating timed automata
单时钟交替时间自动机OCATA最近被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义（Ouaknine，Worrell 2005）。我们考虑OCATA的应用问题的模型检查MITL公式（MTL的语法片段）对时间自动机。我们引入了一个新的语义OCATA，直观地说，时钟估值的间隔，而不是单一的真实值。由于这种新的语义，我们表明，我们可以绑定的时钟副本的数量是必要的，让OCATA识别模型的MITL公式。配备了这种技术，我们提出了一个新的算法来翻译的MITL公式到一个时间自动机，我们勾勒出几个想法来定义新的模型检验算法的MITL。
2013-04-09 cs.FL cs.LO
Verification of Timed Automata Using Rewrite Rules and Strategies
ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。
2009-07-17 cs.LO
A Note on Fault Diagnosis Algorithms
在本文中，我们审查算法检查离散事件系统和时间自动机的可诊断性。我们指出，在这两种情况下的可诊断性问题减少到空性问题（定时）Büchi自动机。此外，它是已知的，检查是否离散事件系统是可诊断的，也可以减少到检查有界可诊断性。我们建立了一个类似的时间自动机的结果。我们还提供了一个综合的复杂性结果，为不同的故障诊断问题。
2010-04-16 cs.FL cs.LO
Stochastic Timed Automata
随机时间自动机是定义在时间自动机上的纯随机过程，其中延迟和离散选择都是随机的。研究了该模型的几乎确定模型检验问题，即给定一个随机时间自动机A和一个性质$Φ$，我们想判定A是否以概率1满足$Φ$.在本文中，我们确定了几类自动机和属性，这可以决定。证明依赖于一个有限的抽象，称为厚图，我们解释为一个有限的马尔可夫链，我们可以决定几乎肯定的模型检查问题的建设。正确的抽象时，自动机几乎肯定公平，我们表明，是两大类系统，单时钟自动机和所谓的弱反应自动机的情况下。本文中使用的技术收集了实时验证和概率验证的工具，以及在时间自动机上进行的拓扑游戏。
2014-12-07 cs.LO
Linear-Time Model Checking Branching Processes
（多类型）分支过程是生成随机无限树的自然和充分研究的模型。分支过程具有非确定性和概率性分支，推广了转移系统和马尔可夫链（但不是一般的马尔可夫决策过程）。我们研究了模型检验分支过程对线性时间ω-正则规范的复杂性：它是几乎肯定的情况下，由分支过程随机生成的树的每个分支满足ω-正则规范？主要结果是，对于LTL规格这个问题是在PSPACE，包含经典的结果，分别为过渡系统和马尔可夫链。底层的一般模型检查算法是基于自动机理论的方法，使用明确的Büchi自动机。
2021-07-04 cs.FL cs.LO
Certifying Emptiness of Timed Büchi Automata
时间自动机的模型检测器被广泛用于验证安全关键的实时系统。最先进的工具通过复杂的抽象实现可伸缩性。我们的目标是进一步提高他们的验证结果的信任，特别是检查活性属性。为此，我们开发了一种方法提取证书的空时间Büchi自动机从模型检验运行。这些证书可以由我们在Isabelle/HOL中正式验证的认证者进行双重检查。我们在一个抽象的环境中研究活性证书，并表明我们的方法是健全和完整的。为了证明它的可行性，我们提取了几个模型的证书，这些模型由Tandem和Imitator检查，并使用我们经过验证的认证器对其进行验证。
2020-07-08 cs.FL cs.LO
POPACheck: A Model Checker for Probabilistic Pushdown Automata
TU Wien（维也纳工业大学）
POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。
2025-06-04 cs.LO
Bisimilarity of Probabilistic Pushdown Automata
研究了概率下推自动机及其子类的双相似性问题。我们的定义pPDA允许概率和非确定性的分支，概括了下推自动机的经典概念（没有ε-转换）。我们的第一个贡献是一个一般的建设，减少检查的概率转换系统的双相似性检查的非确定性转换系统。这种构造直接产生pPDA的双相似性的可判定性，以及概率基本过程代数的子类上的双相似性问题的基本上界，即，单态pPDA。我们进一步表明，通过仔细的分析，一般的减少可以用来证明一个EXPTIME上界的概率可见下推自动机的双相似性。这里我们还提供了一个匹配的下限，建立EXPTIME-完全性。最后，我们证明了概率单计数器自动机（pPDA的另一个子类）的判定双相似性是PSPACE完全的。在这里，我们使用一个更专门的参数来获得最佳的复杂度界限。
2012-10-08 cs.FL cs.LO
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
本文研究一类非常一般的无限秩树的逻辑性质，即由高阶递归方案生成的无限秩树。我们考虑，对于一元二阶逻辑和模态μ演算，三个主要问题：模型检查，逻辑反射（又名全局模型检查，要求公式成立的元素集的有限描述）和选择（要求，如果存在的话，要求具有二阶自由变量的MSO公式成立的元素集的有限描述）。对于每一个问题，我们都提供了有效的解决方案。这是由于高阶递归方案和可折叠下推自动机之间的已知连接，并在以前的工作有关奇偶校验游戏上的过渡图的可折叠下推自动机。
2021-03-02 cs.FL 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
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
Model-checking real-time systems: revisiting the alternating automaton route
本文提出了一种基于区域方法的1-ATA空性算法，改进了MTL到1-ATA的转换，并研究了在特定条件下模型检验实时系统的方法。
2026-01-06 cs.FL cs.LO
Convex Language Semantics for Nondeterministic Probabilistic Automata
我们探索语言语义的自动机结合概率和不确定性的行为。我们首先证明了具有非确定性的概率自动机有两种自然语义。对于这两种选择，我们表明，这些自动机是严格的表达比确定性概率自动机，我们证明了检查语言等价性的问题是不可判定的减少从阈值问题。然而，我们提供了一个折扣度量，可以计算到任意高的精度。
2018-05-29 cs.FL cs.LO
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
Revisiting Reachability in Timed Automata
我们重新审视了实时验证的一个基本结果，即给定的时间自动机的配置之间的二进制可达性关系是可定义的整数和实数的线性算术。在本文中，我们给出了一个新的和更简单的证明这一结果，建立在著名的可达性分析的时间自动机涉及差分界矩阵。利用这个新的证明，我们给出了一个指数空间过程的模型检验的可达性片段的逻辑参数TCTL。最后我们证明了后一个问题是NEXPTIME困难的。
2017-04-18 cs.LO
Finding Minimum and Maximum Termination Time of Timed Automata Models with Cyclic Behaviour
本文提出了一种计算具有循环行为的时间自动机模型的最佳和最坏执行时间（BCET/WCET）的新算法。该算法可以工作在任何任意的对角线自由TA，可以处理更多的情况下比以前现有的算法BCAT/WCET计算，因为它可以处理TA中的周期，并决定他们是否导致一个无限的WCET。我们证明了所提出的算法的合理性，并研究其复杂性。据我们所知，这是第一个模型检验算法，全面解决系统的循环行为的BCET/WCET问题。Behrmann等人提供了一种算法，用于计算在定价时间自动机（PTA）中达到目标状态的最小成本/时间。该算法已在著名的模型检验工具UPPAAL中实现，用于计算自动机的最小终止时间。然而，我们表明，在某些情况下，当无限循环存在，在UPPAAL中实现的算法可能不会终止，我们提供的例子，UPPAAL未能验证。
2016-10-31 cs.FL cs.LO
