单计数器自动机上的有记忆线性时间逻辑的模型检验

一类加权自动机的模型检验

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$的互模拟。

时间自动机MITL片段的有界模型检验

Bounded Model Checking of an MITL Fragment for Timed Automata

时间自动机（TA）是一种常见的建模时间系统的形式。有界模型检验（BMC）是一种使用SAT或SMT求解器搜索违反属性的运行的验证方法。MITL是线性时间逻辑LTL的实时扩展。最初，MITL被定义为非重叠时间间隔的轨迹，而不是“超密集”时间轨迹，允许时间间隔重叠在单个点上，这些点被当今常见的时间自动机语义所采用。在本文中，我们扩展的MITL片段的语义超密集的时间轨迹，并设计了一个有界的模型检验编码的片段。我们证明了正确性和完整性的意义上说，使用一个足够大的范围内的反例，任何给定的非控股property.We可以找到实现建议的有界模型检验方法和实验研究的效率和可扩展性的实现。

基于自动机的模型检验方法中的反链

Antichains for the Automata-Based Approach to Model-Checking

我们提出并评估反链算法来解决非确定Buechi自动机的普遍性和语言包含问题，以及交替Buechi自动机的空性问题。为了获得这些算法，我们建立了模拟前序的存在，可以利用这些前序来有效地评估在互补步骤中定义的自动机上的不动点（我们在我们的方法中保持隐式）。我们使用Tabakov和Vardi最近提出的随机自动机模型来评估算法的性能，以检查Buechi自动机的普遍性。我们表明，这种概率模型的困难的情况下，我们的算法优于标准的几个数量级。

无自动机约束LTL可满足性检验

Constraint LTL Satisfiability Checking without Automata

本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。

基于无约束Buchi自动机的Markov链模型检验

Model Checking Markov Chains Against Unambiguous Buchi Automata

本文给出了一个多项式时间算法，用于有限马尔可夫链的模型检验。

Buechi自动机空性检测算法的比较

Comparison of Algorithms for Checking Emptiness on Buechi Automata

我们重新研究有限状态系统的LTL模型检测问题。典型的解决方案，如Spin，在飞行中工作，将问题简化为Buechi空虚。这可以在线性时间内完成，并且存在具有此属性的各种算法。尽管如此，细微的设计决策可以在实践中对其实际性能产生很大的影响，特别是在动态使用时。我们比较了大量的算法实验上的一个大的基准套件，测量其实际运行时的性能，并提出改进。与Spin中实现的算法相比，我们的最佳算法平均快约33%。因此，我们建议，对于动态显式状态模型检验，嵌套DFS应该被更好的解决方案所取代。

实时的模型检验：参数无处不在

Real-Time Model-Checking: Parameters everywhere

本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。

飞行自动机、模型检验与可识别性

Fly-automata, model-checking and recognizability

可识别性定理指出，如果一组有限图可由一元二阶（Monadic Second Order，MSO）语句定义，则它相对于图代数是可识别的，而图宽度的定义是基于图代数的。可识别性是一个代数概念，用同余来定义，也可以用有限自动机来描述所考虑的图。该定理要求MSO图属性的验证，或者等价地，有限二元关系结构上的MSO逻辑的模型检验问题，对于由表示属性的公式和输入图或结构的树宽度（或树宽度）组成的参数是固定参数可处理的（FPT）。相应的算法可以通过飞行自动机来实现，其转换是在飞行中计算的，而不是列表。我们回顾了两个版本的可识别性，我们目前的苍蝇自动机的例子表明，他们也可以计算值附加到图。我们表明，飞自动机与无限的状态集产生一个简单的证明强版本的可识别性定理。这个证明以前没有发表过。

树上的模型检验约束LTL

Model Checking Constraint LTL over Trees

约束自动机是Büchi自动机的一种改进，它处理来自某种关系结构S的数据字。这样一个自动机的每一个转换都带有S的关系的约束。只有当当前和下一个数据值满足转换的所有约束时，才能触发转换。这些自动机已被用于设置，其中S是一个线性顺序，以确定约束LTL的约束S。在本文中，S是无限分枝的无限阶树T。给出了T-约束自动机空性的PSPACE算法。这一结果暗示了T上约束LTL的可满足性和模型检验问题的PSPACE完备性。

用于MSO 2图性质检验的飞行自动机

Fly-automata for checking MSO 2 graph properties

一个描述性更强但太长的标题是：构造飞行自动机来检查用边量化写的一元二阶公式表示的有界树宽图的性质。这些特性简称为MSO 2。Fly-automata（FA）在表示图的术语上自底向上运行，并“动态”计算必要的状态和转换，而不是查看巨大的，实际上无法实现的表。在以前的工作中，我们已经构造了处理表示有界宽度的图的项的FA，以检查它们的一元二阶（MSO）性质（由没有边量化的公式表示）。在这里，我们适应这些FA的关联图，使他们可以检查MSO 2属性的有界树宽度的图。这是可能的，因为：（1）图的MSO ~ 2性质就是图的关联图的MSO性质;（2）图的关联图的树宽是线性有界的。我们的结构实际上是可实现的和可用的。我们详细介绍了具体的结构自动机在这个角度来看。

稠密时间系统的符号仿真检验

Symbolic Simulation-Checking of Dense-Time Systems

直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。

概率自动机与概率一计数器自动机的分支时间性质模型检测

Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata

本文研究概率自动机及概率一计数器自动机对 PCTL 与 PCTL$^*$ 的模型检测，通过归约空性问题并构造行为等价的一计数器自动机，证明两类问题均不可判定。

单时钟参数时间自动机的MTL-不可判定模型检验

MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable

参数时间自动机扩展了时间自动机（Alfrer和Dill，1991），因为它们允许指定时钟值的参数边界。自1993年由Alfred，Henzinger和Vardi提出以来，已知具有一个时钟的参数时间自动机的空性问题是可判定的，而如果自动机使用三个或更多个参数时钟，则是不可判定的。该问题是开放的参数时间自动机与两个参数时钟。度量时态逻辑（Metric Temporal Logic，简称MTL）是一种广泛应用于实时系统的规约语言。时间自动机的MTL-模型检验是可判定的，无论时间自动机中使用多少时钟。本文证明了参数时间自动机的MTL-模型检验是不可判定的，即使该自动机只使用一个时钟和一个参数并且是确定的。

用于概率模型检验和LTL综合的广义Rabin对自动机

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与我们的新的翻译，并表明，新的翻译导致显着的改善。

单计数器自动机上平坦冻结线性时序逻辑的模型检测

Model Checking Flat Freeze LTL on One-Counter Automata

本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。

有序多下推自动机的模型检验

Model-Checking of Ordered Multi-Pushdown Automata

我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。

通过区间抽象的有效随机自动机模型检测（扩展版）

Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

提出一种结合可细化区间抽象与“大时间步”语义的随机自动机模型检测方法，为最大/最小可达概率提供上下界，实验表明对非平凡示例有效。

Improved Bounded Model Checking of Timed Automata

Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solve…

符号树自动机非空性检验的复杂度

The Complexity of Checking Non-Emptiness in Symbolic Tree Automata

该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。

概率算子优先级自动机的模型检测

Model Checking Probabilistic Operator Precedence Automata

本文针对概率下推自动机，引入概率算子优先级自动机，并针对POTLf$\chi$规范开发了最优的EXPTIME/EXPSPACE概率模型检测算法，同时支持LTL规范，为递归概率程序验证提供了首个最优上下文无关逻辑。

具有连接保护的定时系统的参数化模型检验（扩展版）

Parameterized Model-Checking for Timed-Systems with Conjunctive Guards (Extended Version)

在这项工作中，我们扩展艾默生和Kahlon的截止定理的过程骨架与合取警卫参数化网络的时间自动机，即系统获得的\emph{apriori}未知数量的时间自动机实例化从一个有限的时间自动机模板集$U_1, \dots, U_n$。通过这种方式，我们的目标是提供一个工具，普遍验证软件系统中未知数量的软件组件（即过程）与连续时间的时间约束进行交互。事实上，分布式算法往往表现出异构性，将动态方面与实时方面结合起来。在本文中，我们还将展示如何模型检查协议，使用特殊的变量存储标识符的参与进程（即PID）的时间自动机与合取警卫。这是不平凡的，因为参数化验证问题的解决方案通常依赖于过程是对称的，即不可区分的。另一方面，许多流行的分布式算法使用PID，因此不能直接应用这些解决方案。

单时钟定价时间自动机的模型检验

Model Checking One-clock Priced Timed Automata

我们考虑定价模型（a.k.a.加权）时间自动机，它是时间自动机的扩展，具有位置和转换的成本信息，我们基于对模态具有成本约束的经典时态逻辑的扩展来研究该模型的各种模型检查问题。我们证明，在假设模型只有一个时钟，模型检查这类模型对逻辑WCTL，CTL成本约束的方式，是PSPACE完全的（虽然它已被证明是不可判定的，只要模型有三个时钟）。我们还证明了模型检查WMTL，具有成本约束模态的LTL，只有当模型中有一个时钟和一个秒表成本变量（即，其斜率位于{0，1}中）。

DC和PDC规范的近似模型检验

Towards Approximate Model Checking DC and PDC Specifications

DC已被证明是一个很有前途的工具，用于规范和验证硬实时系统设计的功能需求。许多工作致力于开发有效的技术来检查模型的硬实时系统对直流规格。DC模型检验理论仍在不断发展，但由于微积分的高度不可判定性和模型检验的高度复杂性，目前还没有可用的工具支持实际验证。PDC模型检验的现状远不如DC模型检验。鉴于迄今为止取得的成果，它是可取的DC和PDC规格开发近似的模型检验技术。这项工作的动机是开发近似技术检查DC和PDC规格的硬实时系统的自动机模型。不同于以往的作品，只处理可判定的公式，我们要发展的近似技术，涵盖整个DC和PDC公式。我们的工作，即近似技术检查实时自动机模型的系统LDI和PLDI规范的第一个结果，本文中描述。

用自动机模态重新审视时间逻辑

Revisiting Timed Logics with Automata Modalities

众所周知，（定时的）$ω$ --诸如“p在每个偶数位置保持”和“p在接下来的10个时间单位内至少出现三次”的规则属性不能在度量间隔时间逻辑（$\mathsf{MITL}$）和事件时钟逻辑（$\mathsf{ECL}$）中表达。一个标准的补救措施，这一缺陷是扩展这些与模态定义的自动机。在本文中，我们表明，逻辑$\mathsf{EMITL}_{0,\infty}$（添加非确定性的有限自动机模式到片段的$\mathsf{MITL}$只有下限和上限的约束）和$\mathsf{EECL}$（添加自动机模式到$\mathsf{ECL}$）已经表现为$\mathsf{EMITL}$（完整的$\mathsf{MITL}$与自动机模式）。特别地，$\mathsf{EMITL}_{0,\infty}$和$\mathsf{EECL}$的可满足性和模型检查问题是PSPACE完全的，而$\mathsf{EMITL}$的相同问题是EXPSPACE完全的。我们还提供了一个简单的翻译，从$\mathsf{EMITL}_{0,\infty}$对角自由时间自动机，这使得实际的可满足性和模型检验的基础上，现成的工具。

Automata-Based Software Model Checking of Hyperproperties

We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory cells, functions and predicates, making it a convenient and expressive logic to reason over software and other systems with infinite data domains. HyperTSL further extends TSL to the specification of hyperproperties - properties that relate multiple system executions. As such, HyperTSL can express information flow policies like noninterference in software systems. We augment HyperTSL with theories, resulting in Hype…

基于重写规则和策略的时间自动机验证

Verification of Timed Automata Using Rewrite Rules and Strategies

ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。

随机时间自动机

Stochastic Timed Automata

随机时间自动机是定义在时间自动机上的纯随机过程，其中延迟和离散选择都是随机的。研究了该模型的几乎确定模型检验问题，即给定一个随机时间自动机A和一个性质$Φ$，我们想判定A是否以概率1满足$Φ$.在本文中，我们确定了几类自动机和属性，这可以决定。证明依赖于一个有限的抽象，称为厚图，我们解释为一个有限的马尔可夫链，我们可以决定几乎肯定的模型检查问题的建设。正确的抽象时，自动机几乎肯定公平，我们表明，是两大类系统，单时钟自动机和所谓的弱反应自动机的情况下。本文中使用的技术收集了实时验证和概率验证的工具，以及在时间自动机上进行的拓扑游戏。

混杂系统HyLTL模型检验的改进

Improving HyLTL model checking of hybrid systems

混合系统的模型检测问题是科学界长期面临的挑战。大多数现有的方法和工具要么是有限的，他们可以验证的属性，或限于简化类的系统。为了克服这些限制，最近提出了一种称为HyLTL的时序逻辑。该逻辑的模型检验问题已通过将公式转换为等效的混合自动机来解决，该混合自动机可以使用现有的工具来分析。最初的构造采用了一个声明性过程，它会预先生成指数级的许多状态，当涉及复杂的公式时，效率可能非常低。在本文中，我们解决了一个技术问题的建设，没有考虑在以前的作品，并提出了一个新的算法，将HyLTL到混合自动机，利用优化技术来自离散LTL社区建立更小的自动机。

UPPAAL-SMC：定价时间自动机的统计模型检验

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

本文介绍了实时验证工具uppaal的主要扩展uppaalsmc。UPPAALSMC允许在自然随机语义下对定价时间自动机的网络的性能特性进行有效分析。特别是，uppaalsmc依赖于统计模型检验方法的一系列扩展，该方法被推广用于处理实时系统和估计不可判定的问题。UPPAALSMC与友好的用户界面结合在一起，该用户界面允许用户以有效的方式指定复杂的问题，以及以概率分布的形式获得反馈，并比较概率以分析系统的性能方面。调查的重点是该工具的演变-包括建模和规范形式主义以及应用技术-连同该工具的应用案例研究。

POPACheck：概率下推自动机的模型检查工具

POPACheck: A Model Checker for Probabilistic Pushdown Automata

POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。

通过模型检查进行时间自动机鲁棒性分析

Timed Automata Robustness Analysis via Model Checking

本文针对时间自动机在设计阶段因时间常数不确定及实现扰动导致规范违反的问题，提出了通过模型检查进行鲁棒性分析的概念与技术，以辅助修复模型并确保可达性与安全规范。

Markov链与无歧义自动机

Markov Chains and Unambiguous Automata

本文提出一种多项式时间算法，用于对表示为无歧义自动机的ω-正则规范进行离散时间Markov链的模型检测，证明其复杂度属于NC，与确定性自动机界限匹配且更具简洁性。

基于时间自动机规范的连续时间马尔可夫链的模型检验

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规范。

用迹自动机和有界模型检验证明安全性

Proving Safety with Trace Automata and Bounded Model Checking

循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。

多速率混合ZIA的精化检测

Refinement Checking for Multirate Hybrid ZIA

混杂系统是一个既有离散分量又有连续分量的动态系统。为了研究混合系统的建模和验证问题，本文首先介绍了一种结合接口自动机、初始化多速率混合自动机和Z语言的规范化方法MZIA。同时，我们提出了一个加细关系MZIA。在此基础上，给出了有限域MZIA之间加细关系的检验算法，并证明了算法的正确性。

格自动机的树正则模型检验

Tree Regular Model Checking for Lattice-Based Automata

树规则模型检验（TRMC）是分析无限状态系统的一系列技术的名称，其中状态由项表示，状态集由树自动机（TA）表示。TRMC的核心问题是判断一组坏状态是否可达。计算表示可达状态集合（的过近似）的TA的问题是不可判定的，但是存在基于树换能器的完成或迭代的有效解决方案。不幸的是，TRMC框架无法有效地捕获系统的复杂结构及其某些功能。作为示例，对于JAVA程序，项的结构主要用于捕获系统的状态的结构。相反，Java程序的整数必须用Peano数编码，这意味着任何代数运算都可能由数千个重写规则的应用程序表示。在本文中，我们提出了格树自动机（LTA），树自动机的扩展版本，其叶子配备了格。LTA允许我们表示可能无限的解释术语集。这些术语能够以有效的方式表示复杂的域和相关操作。我们还将经典的布尔运算扩展到LTA。最后，作为一个主要的贡献，我们引入了一个新的基于完成的算法计算可能无限的可达解释条款在有限的时间。

满足Ω-正则稠密时间性质的概率时间自动机

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的稠密时间特性和非确定性。

基于重写的XML更新验证

Rewrite based Verification of XML Updates

我们考虑XML文档更新的访问控制问题。在XML编程的上下文中，类型可以被视为对冲自动机，静态类型检查相当于验证程序总是将有效的源文档转换为有效的输出文档。给定一组更新操作，我们特别感兴趣的是检查安全属性，例如在任何更新序列中保存文档类型。我们还感兴趣的相关政策的一致性问题，即检测是否授权的操作序列可以模拟禁止的。我们减少这些问题的类型检查问题，解决了计算变种的对冲自动机特征的祖先和后代的初始文档类型的参数化重写规则关闭。

重新审视MITL以修复决策程序

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中得到了形式化的证明。

再论时间自动机的可达性

Revisiting Reachability in Timed Automata

我们重新审视了实时验证的一个基本结果，即给定的时间自动机的配置之间的二进制可达性关系是可定义的整数和实数的线性算术。在本文中，我们给出了一个新的和更简单的证明这一结果，建立在著名的可达性分析的时间自动机涉及差分界矩阵。利用这个新的证明，我们给出了一个指数空间过程的模型检验的可达性片段的逻辑参数TCTL。最后我们证明了后一个问题是NEXPTIME困难的。

模型检验正则语言约束

Model Checking Regular Language Constraints

即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。

关于MITL和无限词上的交替时间自动机

On MITL and alternating timed automata over infinite words

单时钟交替时间自动机（OCATA）已被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义。在本文中，我们认为OCATA的模型检查和可满足性的问题MITL（MTL的语法片段），解释了无限的话。我们的方法是基于扩展到无限词的区间语义（最近在[BEG13]中介绍了有限词的情况）。我们提出了基于区域和基于区域的算法，基于这种语义，MITL模型检查和可满足性。我们报告的原型工具实现这些算法的性能。

参数线性动态逻辑

Parametric Linear Dynamic Logic

我们介绍参数线性动态逻辑（PLDL），它扩展了线性动态逻辑（LDL）的时间运营商配备参数，约束其范围。LDL是作为线性时序逻辑（LTL）的扩展而提出的，它能够表达所有$ω$ -正则规范，同时仍然保持LTL的许多理想属性，如直观的语法和转换为指数大小的非确定性Büchi自动机。但是LDL缺乏表达时间约束的能力。通过添加参数化的运营商LDL，我们得到一个逻辑，能够表示所有的$ω$ -正则性质，并包含参数化LTL和PROMPT-LTL LTL的参数化扩展。我们的主要技术贡献是翻译PLDL公式到非确定性Büchi字自动机的指数大小通过交替自动机。这就产生了一个PSPACE模型检验算法和一个具有双指数运行时间的可实现性算法。此外，我们给出了紧的上限和下限的最优参数值为这两个问题。这些结果表明，PLDL模型检验和可实现性并不比LTL模型检验和可实现性难。

Logics Meet 2-Way 1-Clock Alternating Timed Automata

In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to read in both forward and backward direction, the 2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that subclass of 2-Way 1-ATA with reset free loops (2-Way 1-ATA-rfl) is expressively equivalent to MSO[<] extended with Guarded Metric Quantifiers (GQMSO). Emptiness Checking problem for 2-Way 1-ATA-rfl (and hence GQMSO) is undecidable, in general. We propose a "non-punctuality" like restriction, called non-adjacency, for 2-Way 1-ATA-rfl, and also for GQMSO, for which the emptines…

Backwards Reachability for Probabilistic Timed Automata: A Replication Report

Backwards reachability is an efficient zone-based approach for model checking probabilistic timed automata w.r.t. PTCTL properties. Current implementations, however, are restricted to maximum probabilities of reachability properties. In this paper, we report on our new implementation of backwards reachability as part of the Modest Toolset. Its support for minimum and maximum probabilities of until formulas makes it the most general implementation available today. We compare its behaviour to the experimental results reported in the original papers presenting the backwards reachability technique…

可视下推自动机上的超越语言等价性

Beyond Language Equivalence on Visibly Pushdown Automata

我们研究了（双）模拟类的前序/等价性检查的类可见下推自动机及其自然子类可见BPA（基本进程代数）和可见一计数器自动机。我们描述了通用的方法来证明复杂性的上限和下限的一些研究前序和等价物，如模拟，完成模拟，准备模拟，2嵌套模拟前序/等价物和互模拟等价。我们的主要结果是，所有提到的等价和前序是EXPTIME-完全的可见下推自动机，PSPACE-完全的可见一计数器自动机和P-完全的可见BPA。我们的PSPACE下界明显的一计数器自动机也提高了以前已知的DP-硬度结果为普通的一计数器自动机和一计数器网。最后，我们研究了可见下推自动机的正则性检验问题，证明了它们可以在多项式时间内判定。

A Linear-Time Nominal $μ$-Calculus with Name Allocation

Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Ba…

关于MITL和交替时间自动机

On MITL and alternating timed automata

单时钟交替时间自动机OCATA最近被引入作为（单时钟）时间自动机的自然扩展来表达MTL的语义（Ouaknine，Worrell 2005）。我们考虑OCATA的应用问题的模型检查MITL公式（MTL的语法片段）对时间自动机。我们引入了一个新的语义OCATA，直观地说，时钟估值的间隔，而不是单一的真实值。由于这种新的语义，我们表明，我们可以绑定的时钟副本的数量是必要的，让OCATA识别模型的MITL公式。配备了这种技术，我们提出了一个新的算法来翻译的MITL公式到一个时间自动机，我们勾勒出几个想法来定义新的模型检验算法的MITL。

关于故障诊断算法的注记

A Note on Fault Diagnosis Algorithms

在本文中，我们审查算法检查离散事件系统和时间自动机的可诊断性。我们指出，在这两种情况下的可诊断性问题减少到空性问题（定时）Büchi自动机。此外，它是已知的，检查是否离散事件系统是可诊断的，也可以减少到检查有界可诊断性。我们建立了一个类似的时间自动机的结果。我们还提供了一个综合的复杂性结果，为不同的故障诊断问题。

Linear-Time Model Checking Branching Processes

(Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing both transition systems and Markov chains (but not generally Markov decision processes). We study the complexity of model checking branching processes against linear-time omega-regular specifications: is it the case almost surely that every branch of a tree randomly generated by the branching process satisfies the omega-regular specification? The main result is that for LTL specifications this pro…

单调多项式系统上牛顿法的上界及概率单计数器自动机的P-时间模型检验

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属性。

Certifying Emptiness of Timed Büchi Automata

Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model checking runs. These certificates can be double-checked by a certifier that we formally verify in Isabelle/HOL. We study liveness certificates in an abstract setting and show that our approach is sou…

用树自动机判定归纳分离逻辑的蕴涵

Deciding Entailments in Inductive Separation Logic with Tree Automata

具有归纳定义的分离逻辑（SL）是用于指定复杂递归数据结构的自然形式主义，用于操作此类结构的程序的组合验证。任何基于SL的自动验证过程的关键要素是蕴涵问题的可判定性。在这项工作中，我们减少了蕴涵问题的一个非平凡的子集SL描述树（和超越）的语言包含树自动机（TA）。我们的减少提供了严格的复杂性界限的问题，并表明在我们的片段的蕴涵是EXPTIME完成。出于实用的目的，我们利用自动机理论的最新进展，如包含检查非确定性TA避免明确的确定性。我们实现了我们的方法，并提出了有前途的初步实验结果。

关于代数积构造的不可行定理

A No-go Theorem for Coalgebraic Product Construction

本文提出关于代数积构造的不可行定理，并展示MC与MFAs的代数积构造作为新实例，解决多项式时间内的模型检查问题。