理论计算机科学电子笔记154：STS Hierarchy3访问与Lab

理论计算机科学电子笔记154（2006）59-69www.elsevier.com/locate/entcs访问STS Hierarchy3Nathalie Bertrand1和菲利普·施诺贝伦2Lab。 Sp'ecificati o n &V'erification，CNRS&ENSdeCachan，61，av. Pdt. Wilson，94235 Cachan Cedex France摘要由Henzinger、Majumdar和Raskin引入的符号转移系统的层次结构是一个优雅的分类工具，用于一些支持符号“向后闭包”验证算法的变体的无限状态操作模型族。它首先被用于混合动力系统的家庭和说明。在本文中，我们调查是否STS层次结构可以占经典家庭的无限状态系统的时间或混合系统之外保留字：符号转换系统，结构良好的转换系统，STS层次结构。1介绍无限状态系统的验证是一个非常活跃的研究领域，其中研究如何将有限状态系统模型检查成功技术的算法技术扩展到更具表达力的计算模型[3]。人们研究了许多不同的模型，从无限数据模型（如通道系统）到无限控制模型（如过程代数），包括时间自动机和混合系统。一般的不可判定性结果是通过发现特殊的限制子类来解决的，在这些子类中，可判定性可以被恢复用于特定的验证问题，我们对表达性和可处理性之间的妥协的理解定期提高。已经有人试图在现有的过多的分散的结果中带来一些秩序。一种方法是发现(1)支持一些通用的验证算法，（2）可以解释足够丰富的各种模型。 [1，12]中的良构转换系统1 电子邮件地址：bertrand@lsv.ens-cachan.fr2 电子邮件地址：phs@lsv.ens-cachan.fr3.本报告由Pers'ee提供，由法国科学研究部的ACIS'ecurit'e基金提供。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.00760N. Bertrand，P.Schnoebelen/Electronic Notes in Theoretical Computer Science 154（2006）59⊆S是这样的尝试之一，其中的关键概念是存在一个良好的准秩序之间的配置是兼容的过渡。WSTS思想应用广泛，并且实例存在于许多类模型中[12]。[15]的符号转换系统（STS）是另一种尝试。实际上[15]定义了一个五个不同层次的层次结构：STS 1到STS 5。所有级别均定义为同样的方式：一个系统是STSk i，它的配置集产生一个有限的商模k，一个等价关系，将状态与类似的从101到105的等价物越来越粗糙，STSk类中的系统也在STS（k+ 1）中。此外，给出了通用符号闭包算法的五个变体，每个类一个，允许验证从μ演算模型检查（对于类STS 1）到可达性属性（对于类STS 5）的属性STS思想虽然具有启发性，但其缺点是适用范围不广.在文献[15]中，所有给出的STS 1到STS 5类的例子都是混杂系统的一些限制族。并且没有给出STS 4系统的实例。因此，目前尚不清楚这种分类是否会对混合和定时系统产生任何影响。我们的贡献。我们研究了一些著名的模型族，这些模型族存在验证结果，并且与混合系统无关：Petri网，下推系统和通道系统。特别地，我们考虑有损信道系统的几个变体[2，7]。对于这些家族，一个自然的问题是它们是否会产生位于STS层次结构的某个级别内的系统在这里，我们只考虑语义的问题：我们问是否一个给定的系统模型与一组给定的可观察的属性产生STSk过渡系统。我们不关心算法问题和符号验证，即使STS层次满足其目的时，系统可以配备一个工作区域代数[15]。我们研究的一个普遍结果是，只有在[12]意义上结构良好的系统才能适合STS层次结构，在级别STS 5（或者，有时，STS 4）。事实上，[15]使用了“结构良好的系统”的名称我们认为，这两个概念之间的密切联系并不提供完美的配合。2STS层次结构Henzinger，Majumdar和Raskin在[15]中介绍了符号转换系统（STS）。这些是配备了区域代数的标记转移系统。然而，由于我们在本文中不考虑算法问题或符号验证，我们将使用简化的定义。定义2.1标记转移系统（LTS）是一个元组S=S，→，P，其中S是一个（可能是无限的）状态集，→S×S是一个转移关系，P2是一个有限的可观察属性（或可观察量）集，它覆盖了状态空间：S=p∈P p。N. Bertrand，P.Schnoebelen/Electronic Notes in Theoretical Computer Science 154（2006）596112345K观察是一组可观察的状态σ的观测值P（σ）为{p∈P|σ∈ p}。经典上我们写σ→σJ而不是（σ，σJ）∈ →，并且说σJ是σ的后继者之一。如果没有后继者，则σ是死锁状态。 S中的（有限）路是状态序列σ1，···，σn使得对于所有i，σi→σi+1。STS层次结构基于模拟和跟踪的公知概念（参见，例如，[13]）。我们回顾一下模拟的定义。设S=S，→，P，是一个LTS。二元关系R<$S×S是对S的模拟，如果σRτ需要：(i) p∈P，σ∈p惠τ∈p，(ii) σσ→σJ，ττ→τJs. t。σJRτJ。如果R是一个双线性方程，则σ和这样，σRτ.如果两个模型都是模拟的，则通过σ τ = S τ-来表示模拟的等价性R1和R2使得σR1τ和τR2σ.众所周知，双相似和模拟等价是等价关系。现在我们回顾一下痕迹的定义。设S=S，→，P，是一个LTS。来自状态σ的迹是对源自σ的路径的观察。形式上它是一个观测序列P1···Pn，使得存在一条路径σ1···σ n，其中σ1 = σ且Pi= P（σ i），i = 1，. ，n. Pn中的任何p，沿着迹线的最后一个观测值，是被称为数据集的数据集是由数据集和数据集组成的，其中数据集是由数据集组成的，数据集是由数据集组成的。两个状态σ和τ通过σσ是τ的迹线，反之亦然。如果从σ中恢复，则由στ = S τ-确定的时间常数为对于长度n和目标p，存在来自长度n和目标p的τ的迹，反之亦然。亦然本文提出了一种新的求解方法，即用σ τ = S τ -i来表示一个新的定常微分方程σ的长度为n，目标为p，从τ开始的迹线的长度最多为n，目标P，反之亦然。显然，迹等价、距离等价和有界可达等价是等价关系。定义2.2（STS层次）[15]。一个标号迁移系统S=<$S，→，P<$属于STSk（ 1≤k≤ 5）类i =Sha finitein dex（即，induecsafinnitenumberberofequivalenceS中的类）。STS类的一些直接属性是：如果S在STSk中，则它在STS（k+1）中。有限系统：如果S=S，→，P，有有限个S，则S在STS 1中。62N. Bertrand，P.Schnoebelen/Electronic Notes in Theoretical Computer Science 154（2006）590/1JJ平凡观测量：如果S=S，→，P，有P={S}，则S在STS 5中。 如果没有状态是S是死锁状态，则S在STS 1中是偶数关于单调性可观测量：如果S = S，→，P，且SJ= S，→，P，J，仅 差P，j，P，j，（即，S具有比SJ更多的可观察性质），并且S在STSk中，则SJ也在STSk中。3结构良好的变迁系统与STS高层结构在[15]中，STS 5类被认为与结构良好的转换系统相一致，一类支持通用验证算法的无限状态转换系统[10，1，12]。这一主张得到了STS 5系统的另一种表征的支持，使用良好的准序[15，定理5A]。然而，与WSTS的联系并没有更加明确。在这一节中，我们证明了WSTS是在STS 5中，并考虑相反的问题：任何STS 5过渡系统可以通过装备一个我们还记得，良拟序（WQO）是一个自反且传递的关系≤（在某个集合S上）使得对于S中的任意无限序列x0，x1，···，存在下标

下载后可阅读完整内容，剩余1页未读，立即下载