弱双Kleene代数的等价性检查

确定性时间有限状态机：等价性检验和表达能力

Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power

人们对定义随时间而丰富的自动机模型越来越感兴趣。例如，时间自动机被引入作为用时钟扩展的自动机。在本文中，我们研究了时间有限状态机（TFSMs）的模型，即，用时间丰富的FSM，它接受定时输入单词并生成定时输出单词。在这里，我们讨论了具有单个时钟的TFSM的一些模型：具有定时保护的TFSM、具有超时的TFSM以及具有定时保护和超时的TFSM。我们解决了所有三个模型的等价性检查的问题，我们比较他们的表达能力，特征的TFSM的子类定时警卫和TFSM的超时是等价的。

Equivalence Checking of Quantum Finite-State Machines

In this paper, we introduce the model of quantum Mealy machines and study the equivalence checking and minimisation problems of them. Two efficient algorithms are developed for checking equivalence of two states in the same machine and for checking equivalence of two machines. As an application, they are used in equivalence checking of quantum circuits. Moreover, the minimisation problem is proved to be in $\textbf{PSPACE}$.

关于确定性自顶向下树自动机的等价判定问题

On the Equivalence Checking Problem for Deterministic Top-Down Tree Automata

针对自顶向下确定性有限树自动机（DFTAs）的状态语言等价判定问题，提出将其转化为语言理论方程系统可解性检查的高效算法，通过代入与冲突检测开发判定程序，并证明其正确性、终止性及$O(n^2)$最坏时间复杂度。

符号交替有限自动机的符号判定过程

A Symbolic Decision Procedure for Symbolic Alternating Finite Automata

我们引入符号交替有限自动机（S-AFA）作为一个表达，简洁，可判定的模型，用于描述任意字母表上的有限序列集。s-AFA上的布尔运算具有线性复杂度，这与非交替符号自动机的交和并的二次成本形成鲜明对比。由于这种简洁性，空性和等价性检查是PSpace困难的。我们介绍了一种算法，用于检查两个s-AFA的等价性的基础上互模拟同余。该算法允许我们利用SAT和SMT求解器的能力来有效地搜索s-AFA的状态空间。我们评估我们的决策过程中的两个验证和安全应用：1）检查可满足性的线性时序逻辑公式在有限的痕迹，2）检查等价的布尔组合的正则表达式。我们的实验表明，我们的技术往往优于现有的技术，它可以在这两个应用程序中是有益的。

用导数判定KAT和霍尔逻辑

Deciding KAT and Hoare Logic with Derivatives

带测试的Kleene代数（KAT）是布尔代数（BA）和正则表达式代数Kleene代数（KA）的结合，是一个用于程序验证的方程系统。特别地，KAT包含了霍尔逻辑（PHL）的命题片段，该逻辑是用于程序的规范和验证的形式化系统，并且是当前大多数用于检查程序正确性的工具的基础。KAT的方程理论和PHL在KAT中的编码都是可判定的。在本文中，我们提出了一个新的决策过程的基础上的概念偏导数的两个KAT表达式的等价性。我们还介绍的概念，衍生模特定的方程组。有了这个，我们扩展了以前的程序来决定PHL。最后给出了一些实验结果。

基于PRES +模型的嵌入式系统设计验证中的等价性检查

Equivalence Checking in Embedded Systems Design Verification using PRES+ model

本文主要研究嵌入式系统的建模和形式化验证。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。因此，作为第一步，我们寻求设计一种算法来将PRES+模型转换为FSMD模型，并且我们寻求在现实生活中的示例上手动执行我们的算法，并且我们必须将两个版本的PRES+模型转换为FSMD模型。然后使用现有的等价性检查器，我们已经检查了两个FSMD模型之间的等价性。

嵌入式系统设计验证中的等价性检查

Equivalence Checking in Embedded Systems Design Verification

在这份报告中，我们专注于嵌入式系统的建模和形式化验证相关的一些方面。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。作为第一步，因此，我们试图设计一个算法，将PRES+模型FSMD模型。

Kleene代数中FMP的初等证明

An Elementary Proof of the FMP for Kleene Algebra

本文通过变换自动机的方法，给出了Kleene代数有限模型性质的初等证明，并推导出Kozen和Pratt定理。

Direct Construction of Program Alignment Automata for Equivalence Checking

The problem of checking whether two programs are semantically equivalent or not has a diverse range of applications, and is consequently of substantial importance. There are several techniques that address this problem, chiefly by constructing a product program that makes it easier to derive useful invariants. A novel addition to these is a technique that uses alignment predicates to align traces of the two programs, in order to construct a program alignment automaton. Being guided by predicates is not just beneficial in dealing with syntactic dissimilarities, but also in staying relevant to t…

并发系统的组合模型检验，用Petri网

Compositional model checking of concurrent systems, with Petri nets

组合性和进程等价性都是进程代数的标准概念。复合性意味着一个复合系统的行为只依赖于其组成部分的行为，即没有涌现行为。过程等价意味着系统的显式状态空间让位于其交互模式：环境可以通过交互获得的信息。Petri网是一个经典的，但被广泛使用和理解的并发模型。然而，它们经常被描述为非组合模型，并且工具倾向于处理整体的、全局指定的模型。本教程论文集中在Petri网与边界（PNB）：1-安全网的合成，图形代数，以及其应用程序中的可达性检查工具彭罗斯。该算法的特点是使用组合性和进程等价，一个强大的组合，可以利用，以提高性能的检查可达性和覆盖性在几个常见的例子，其中Petri网模型现实的并发系统。

基于广义时间自动机与新活性算法的MITL模型检测

MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

本文提出将MITL翻译为广义时间自动机（GTA）的新方法，对时间直到模态实现指数级改进，并设计新的基于区域的Büchi非空性算法以解决GTA活性检查问题。

确定性加权实时单计数器自动机的等价性

Equivalence of Deterministic Weighted Real-time One-Counter Automata

本文引入了确定性加权实时单计数器自动机（DWROCA），并为其等价性问题提供了更简证明与更优多项式时间算法。

概率自动机等价问题的复杂性

On the Complexity of the Equivalence Problem for Probabilistic Automata

检验两个概率自动机的等价性已被证明是有效地建立概率系统的各种行为和匿名性的关键问题。在最近的实验中，基于多项式同一性测试的随机等价性测试优于确定性算法。在本文中，我们表明，多项式身份测试产生有效的算法，各种概括的等价问题。首先，我们提供了一个随机NC程序，也输出一个反例跟踪的情况下，不等价。其次，我们将展示如何检查等价性两个概率自动机（累积）奖励。我们的算法运行在确定性的多项式时间，如果奖励计数器的数量是固定的。最后，我们证明了概率可见下推自动机的等价问题是对数空间等价的算术电路同一性测试问题，这是决定由算术电路表示的多项式是否为同零。

加权 GKAT：完备性与复杂性

Weighted GKAT: Completeness and Complexity

本文提出了配备分支、条件和循环的非解释型加权编程语言 wGKAT，利用加权自动机变体给出其操作语义，引入了可靠且完备的公理化体系，并提供了互模拟等价的多项式时间判定过程。

利用虚拟时钟检查定时双射性

Checking Timed Bisimilarity with Virtual Clocks

本文提出了一种扩展区图的虚拟时钟表示法，用于解决定时自动机的双射性检查问题，该方法在平均情况下比区域图更小，并通过实验验证了其有效性。

一阶文法的互模拟等价是ACKERMANN-完全的

Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete

Sénizergues（1998，2005）证明了两个具有限制静默动作的下推自动机是否弱双相似。我们提供了第一个已知的复杂性上界这个著名的问题，在等效设置的一阶文法。这ACKERMANN上限是最佳的，我们还表明，强双相似性是连续递归的自动机的状态数是固定的。

高维模态μ演算的模型检验

Model-Checking the Higher-Dimensional Modal mu-Calculus

高维模态μ演算是μ演算的扩展，其中公式被解释为标记转换系统的状态元组。在这种逻辑中可以表达的每个属性都可以在多项式时间内进行检查，相反，每个具有互模拟不变编码到标记转换系统中的多项式时间可判定问题也可以在高维模态μ演算中定义。我们通过给出几个决策问题的例子来证明后一种联系，这些决策问题归结为对某些固定公式的高维模态μ演算的模型检验。通过这种方式，用于逻辑的通用模型检验算法然后可以经由部分评估来使用，以便获得用于这些问题的算法，这些算法可以受益于在程序验证领域中良好建立的改进，即运行中（on-the-fly）和符号技术。这项工作的目的是将这种技术扩展到其他领域，以及，在这里示例性地做了过程等价，自动机理论，解析，字符串问题，和游戏。

从有限自动机到正则表达式再返回--描述复杂性研究综述

From Finite Automata to Regular Expressions and Back--A Summary on Descriptional Complexity

有限自动机和正则表达式的等价性可以追溯到1956年Kleene关于神经网络和有限自动机中的事件的开创性论文。在本文中，我们参观了一个片段的文献和总结结果的上限和下限的有限自动机转换为正则表达式，反之亦然。我们还简要地回顾了已知的边界上去除自发跃迁（ε-跃迁）的非无干扰的非确定性设备。此外，我们报告最近的结果的平均情况下的复杂性边界的转换正则表达式有限自动机和全新的发展的状态消除算法，转换有限自动机正则表达式。