带标签实时自动机强可检测性的公式化与验证——一种并发组合方法

《Information and Computation》：Formulation and verification of strong detectability for labeled real-time automata — A concurrent-composition method

　　

摘要

实时自动机是一类被广泛使用的实时系统。本文针对带标签实时自动机（LRTA）提出了两个版本的强可检测性定义，其含义是：在经历某种延迟之后（观察到的标签数量或实时延迟），沿着每一条生成的无限运行，都可以通过观察所生成的带时标签序列来确定当前状态及后续状态。借助于作者先前某篇论文中定义并计算的并发合成，给出了这两个强可检测性版本的否命题的必要充分条件。本文还证明了对这两种强可检测性定义的验证问题都属于????????完全问题。作为副产品，我们给出了一个针对LRTA的NP状态估计算法。

引言

部分可观测动态系统的状态检测问题可追溯到计算机科学中1950年代的自动机思想实验（后来被称为摩尔机）[2]，以及控制科学中1960年代线性微分方程的可观测性[3]。该问题涉及刻画这样的性质：能否使用输入序列及其对应的输出序列来确定初始状态。前者衍生出计算机科学中的众多分支，例如基于模型的测试[4]和模型检测[5]；后者则催生了现代控制理论，尤其是各类微分方程中的可观测性研究，涵盖线性系统[3]、[6]、非线性系统[7]、[8]、[9]、切换系统[10]、网络化系统[11]、[12]以及布尔控制网络[13]、[14]、[15]等等。

离散事件系统领域研究的状态检测问题涉及可检测性性质的研究，其含义是能否使用生成的输出（又称标签）序列来确定当前及后续状态[16]、[17]。此类性质为许多相关问题奠定了基础，例如状态估计、观测器设计和控制器综合。离散事件系统广泛使用的数学模型包括有限自动机、Petri网、max-plus系统等。

文献[17]、[18]中提出的带标签有限状态自动机（LFSAs）并发合成方法，通过刻画强可检测性的否命题，提供了一种统一的、目前最高效的验证基于推理性质的方法[19]，例如可检测性、可诊断性和可预测性的强版本。这里的"基于推理的性质"是指：通过观察生成的输出可以推断部分可观测系统的内部信息。此外，并发合成方法能够对任意LFSAs验证基于推理的性质，并去除了过去30多年验证LFSAs中基于推理性质时所使用的两个基本假设：无死锁性（不存在死状态）和无发散性（不会生成不可观测环）。经典且广泛使用的方法——用于验证强可检测性的检测器方法[20]、用于验证可诊断性和可预测性的孪生工厂方法[21]和验证器方法[22]、[23]及其变体（例如[24]、[25]、[26]）——都依赖这两个基本假设。此外，这四种方法的复杂度几乎相同。因此，与另外三种老方法相比，并发合成方法显示出显著优势。这三种老方法及其变体之所以依赖这两个假设，是因为它们是通过验证基于推理性质本身、而不是验证其否命题来提出的，详见[19]。此外，并发合成被扩展到在PSpace中验证LFSAs中可检测性、可诊断性和可预测性的去中心化版本[27]，这些扩展后的性质被称为共同可检测性、共同可诊断性和共同可预测性。共同可检测性的验证问题被证明是????????难的，共同可预测性的验证问题被证明是????????????难的。作为较早的结果，LFSAs中共同可诊断性的验证问题被证明是????????????难的[28]。在[29]中，作者错误地声称：(1) 验证器方法用于验证任意LFSAs的可诊断性时不依赖任何假设；(2) 他们给出了在LFSAs中验证共同可诊断性的多项式时间算法。事实上，作者并未给出任何验证共同可诊断性的算法（算法1中的表达式 GN,1‖GN,2‖GF 并未被完整定义）。验证共同可诊断性的多项式时间算法极不可能存在，因为在LFSAs中验证共同可诊断性是????????????难的[28]。

除了验证基于推理的性质之外，当并发合成与观测器1结合使用时，它提供了一种统一的、目前最高效的验证LFSAs中各类标准版本的状态不透明性和强版本的状态不透明性的方法[19]、[32]。LFSAs中验证标准版本状态不透明性和强版本状态不透明性的不同验证方法的时间复杂度比较见[19, 表4和表5]。此外，文献[33]使用并发合成方法验证了LFSAs中若干类的强初始-终状态不透明性。这类性质在[19]中被称为"隐藏式性质"（concealment-based），因为它们意味着通过观察生成的输出无法推断部分可观测系统的内部信息。

概括而言，并发合成方法从根本上改变了由LFSAs建模的离散事件系统研究现状，因为基于并发合成方法，LFSAs的大量性质可以被归类为两类——基于推理的和基于隐藏的。要验证基于推理的性质，并发合成已足够；要验证基于隐藏的性质，则需将并发合成与观测器结合。源自并发合成方法的验证方法目前是最高效的，并且去除了近30年来一直使用的无死锁性和无发散性这两个基本假设。详见[19]。

在[34]、[35]中，并发合成的定义被非平凡地扩展到了带幺半群上的带标签加权自动机，并基于并发合成给出了强可检测性版本的必要充分条件；特别地，对于在幺半群(???,+)上的此类自动机，并发合成计算问题被证明是????完全的，而强可检测性验证问题被证明是????????完全的。后来在[36]中，并发合成被用于在指数时间内验证有有理半环上的带标签无歧义加权自动机的两个强可检测性版本（但作者错误地声称其算法为多项式时间运行，实际上他们仅考虑了状态对计算复杂度的贡献，而忽视了作为有理数的权重的贡献）。在[37]中，并发合成被扩展到带标签实时自动机（LRTA），LRTA是一类被广泛使用的实时系统，并且基于无限运行提出了可诊断性的概念，基于并发合成对其进行验证。并发合成计算问题被证明是????完全的，可诊断性验证问题被证明是????????完全的。

一般带标签定时自动机中的强可检测性验证问题是????????????完全的[34]、[38]。在这两篇论文中，两个强可检测性版本的否命题是通过使用两个带标签定时自动机的经典并行合成以及定时自动机的区域自动机（region automaton）来验证的，区域自动机提出于[39]。并行合成与区域自动机的组合更早在[40]中被用于在????????????中验证带标签定时自动机的可诊断性否命题。带标签定时自动机中可诊断性的验证问题被证明是????????????完全的[40]。

在本文中，针对LRTA，我们提出了两个强可检测性版本，其含义是：存在一种延迟，使得沿着每一条生成的无限运行，在该延迟之后可以通过观察所生成的带时标签序列来确定当前状态及后续状态，其中标签表示一种输出。在第一个版本中，延迟k是生成的标签数量，即观察到的带时标签序列至少含有k个标签；在第二个版本中，延迟t是实时延迟。然后，它们的否命题意味着：对于每一种延迟，都存在一条无限运行，使得沿着该运行，在该延迟之后无法唯一确定当前状态。基于[37]中给出的并发合成，我们将给出这两个强可检测性版本否命题的必要充分条件（见定理3.1和定理3.5）。第一个版本的刻画较为简单，因为在该版本中延迟k是生成的标签数量（类似于[34]中研究的强可检测性）。如定理3.1所示，为刻画该版本的否命题，只需要一个条件（如定理3.1中的(i)和(ii)），该条件意味着：存在一条CC(??)的运行，它经过某个环2并终止于一个状态，该状态的两个分量（即??的两个状态）是不同的，且从该状态的左分量出发在??中可达一个环。这里CC(??)是LRTA ??与其自身的并发合成。然而，第二个版本的刻画则复杂得多，因为该版本中的延迟是实时延迟。如定理3.5所示，为刻画该版本的否命题，我们需要讨论足够大的实时延迟出现在何处，并得出5个条件（也参见表1作为示意）。此外，我们将证明这两个版本的否命题的必要充分条件都可以借助[37]中提出的并发合成在????内被验证（见定理3.6）；验证这两个版本是????????难的（见定理3.7）。

为刻画LRTA的强可检测性版本，基于在某一时刻观察到的带时标签序列计算状态估计是关键步骤。基于[41]中的先前结果，我们证明如果所有涉及的时刻都属于?，则LRTA的状态估计可以在????内完成（见命题2.1）。我们执行状态估计的流程比[42]中所得到的流程更简单且更高效（[42]中的主要结果——算法2和算法3——为双指数时间）。此外，我们的结果要通用得多，因为[42]中研究的自动机是LRTAs的一个严格子类，其所有时间区间都是单点。针对[42]所给状态估计流程的显式复杂度分析见注释1。

第2节给出我们的研究背景，包括符号约定、文献[41]中证明的LRTAs状态估计的复杂度结果，以及[37]中提出并计算的并发合成，还有为给出本文主要结果所需的进一步结果。第3节展示主要结果，包括一个????状态估计算法、两个强可检测性版本、基于并发合成的必要充分条件，以及验证这两种可检测性版本的复杂度结果。第4节以简短的结论结束全文。

片段章节

符号约定

对于字母表Σ，Σ*和Σω分别表示Σ上的有限字符串集合（包含空字符串?）和无限字符串集合。字母表中的元素称为字母。我们还记Σ+ := Σ*?{??}。对于字符串w ∈ Σ*，|w|表示其长度，即在w中出现的Σ元素（计重复）的个数；wω表示w的无穷多次连接。对于字符串w ∈ Σ*，若存在另一个字符串w″使得??=??′???″，则称字符串w′是w的前缀。

一个????状态估计算法

我们通过以下三个算法实现命题2.1。

三个算法的正确性：算法1可在????内实现，因为其中第4行最多被执行多项式次。算法2可在????内实现，因为其中第4行最多被执行多项式次。再由算法1和算法2，算法3也可在????内实现。

例3

考虑图5中的LRTA ??2。我们用算法3计算 ??(??2,??,6) 和 ??(??2,(??,8))。

记

结论

在本文中，我们为带标签实时自动机（LRTA）提出了两个版本的强可检测性，分别称为强标签可检测性和强时间可检测性。基于[37]中给出并计算的并发合成，我们给出了这两个版本的必要充分条件，并证明了它们的验证问题都属于????????完全问题。

本文中获得的所有结果都可以推广到更一般的一类自动机，其中区间为
CRediT作者贡献声明
Kuize Zhang：撰写—审阅与编辑，撰写—原始草稿，方法论，调查，形式分析，概念化
利益冲突声明
作者声明，他们没有任何已知的可能影响本文所述工作的经济利益或个人关系。
Kuize Zhang