基于交替自动机的有界模型检测编码及其在多功能机器人中的应用研究.

理论计算机科学电子札记119（2005）83-101www.elsevier.com/locate/entcs基于SNF、AlternatingAutomata和BuchiAutoma的有丹尼尔·谢里登1英国爱丁堡大学信息学院摘要LTL的现代化改造对于多功能机器人来说是一个很大的挑战，因此在这一领域有大量的研究，包括最近的一些关于使用 交替自动机作为中间表示。有界模型检查直到最近才与此分开，通常使用从LTL到命题逻辑的直接转换。本文给出了一种新的基于交替自动机的有界模型检测编码，并重点讨论了交替自动机与SNF之间的关系。本文从理论和实验两个方面探讨了SNF、alternating和Bu？ch ia toma关键字：Bound edmodelchheck i n g，SN F，LTL，Bu？chiaut o m at a，Alterm at i ng aut o m at a ta1介绍在1999年引入有界模型检验之前，LTL模型检验通常通过将公式转换为表达公式的自动机，与模型自动机形成乘积，然后检查结果是否为空来执行。对给定LTL公式产生最小自动机的研究是广泛而多样的。有文献对原始的“GPVW”转换算法[ 12 ]进行了改进，最近的一些工作[10，11]1电子邮件：d. j. sms.ed.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.12.02484D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83建议使用交替自动机（AA）作为中间表示的公式。LTL到AA的转换是线性空间，因此在指数空间转换到Bu？hi自动机之前，可以很容易地进行简化。有界模型检验（BMC）传统上采取了不同的方法：原文[1]给出了一种从LTL直接到命题逻辑的编码。在公式的结构上递归地定义，这（天真地）似乎是状态数的指数大小，尽管经过仔细处理[5]，结果是多项式大小。一种直接基于LTL算子定点特征的替代编码[9使用LTL来自动转换作为有界模型检查的一部分首先由de Joula等人明确提出。唯一的实验比较[5]非常简短，主要是练习许多自动机转换程序中可用的LTL简化虽然有理由将直接到命题的转换与通过自动机的转换区分为“句法”与“语义”[ 5 ]，但本文证明了SNF与交替自动机之间的密切对应关系以及它们从LTL的我们将Bu hi自动机用于BMC，并给出了一种新的可直接使用的交替自动机。这使我们能够更密切地比较SNF编码的使用与自动机的使用，以探索每种方法的优点和缺点我们通过一系列的实验证明了其中的一些2背景2.1有界模型检验BMC通过观察有限数量的状态k来解决LTL模型检查问题。 无穷反例可以用abω形式的路径表示：k = 1的k-l-loop路径|AB|和l =|一|.我们约束一个有限序列，通过假设lLk=stec（π（k）=π（l））2，将π设为k -1 - 100。Alternatively对于某些LTL性质，我们可以给出有限个反例作为k-prefix路径特别是，不可能证明给出Ff的反例，通常，我们通过检查被解释为前缀或循环的k个状态π的序列来验证模型;我们在k个可能的解释上写一个析取，测试路径类型的所有选项2注意，我们给出了π（k）和π（l）之间的等价性，而不是原始文献[1]D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）8385→→→B→ ⊆⊆和l的值。2.2分离范式SNF [8]是基于Gabbay分离定理的类子句范式，具有一般形式Gi（Pi Fi），其中Pi Fi，称为规则被限制为（写作p和f为命题公式）形式为startf的初始规则，其中start仅在每条路径不含时态算子的全局不变规则p→f全局步长规则p→Xf全局不测规则p→Ff从NNFf中的LTL公式到一组SNF规则的转换是通过将图1中的转换函数重复应用于初始公式集{start→f}[9]来实现的。转换引入了新的变量，由语法x标识，x表示变量的直观含义我们把不受变换约束的公式集记为Γ，把NNF中任意LTL公式集记为λ和λ，把命题公式集记为f和g我们也写<$（Gf）来表示Gf出现在<$1中，而<$1（g）代表通过将Gf的每次出现替换为g而获得的公式;类似地对于其他时间算子。2.3BuéchiAutomata我们在这里只简单地讨论了Bu？chi自动机;我们直接参考了Wolper的教程论文[17]。定义2.1布吕克希自动机由元组Q，，δ， I， T定义，其中Q是状态集;是转换标签的字母表; δ是转换函数Q22×Q; IQ是初始状态集; TQ是接受状态集。请注意，我们在定义转换关系时使用2个变量来代替1个变量，以便收集仅通过其动作而不同的转换-这可能是一个重要的优化。一个Bu？chia tomaton的运行是通过这个atomaton来实现的;它是一个假设，如果T中的状态被访问了无限次。也就是说，定义2.2一个运行的布契自动机B，它的hresecto a wordu0u1. .∈ω是状态sinq0q1的 一 个 序 列 。 . ∈Qω，其中hq0∈I且<$i<$α i<$αi，qi+1<$∈86D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83⎧⎫⎨ ⎬∪TSNF[X]（{n→n（Xf）}nr）=stecSNF（{n→n（Ff）}nr）=stec⎧ϕ→ψ(Xf)⎫ΓXf→Xf⎨ϕ→ψ(Ff)⎬∪Γ[F]SNF（{ε→ε（Gf）}εr）=stecFf→Ff⎧⎨ϕ→ψ(f∧XGf)⎫⎬∪Γ[G]<$XGf→X（f<$X Gf）<$⎧⎪⎨SNF[U]（{→（fUg）}r）=stec→⎫⎪⎬ ∪Γ⎩⎪ϕ→Fg⎪⎭SNF[R]（{n→n（fRg）}nr）=stec⎧⎨ϕ→ψ(g∧(f∨X(fRg)))⎫⎬∪Γ<$X（fRg）→X（g<$（f<$X（fRg）<$Fig. 1. SNF的转换函数δ（qi）使得ui∈αi.一个游程是可接受的，如果游程中有无限多个状态是T的成员。一个相对论和Bu？chiaut omaton（GBA）具有一个接受集2Q;每一组都必须经常访问才能接受。一个GBA可以被简化为一个classic的Bu？hi自动机，但不会导致O（|不|）.2.4交替自动机交替自动机（英语：Alternatingautomata）是一种树自动机（运行被描述为树而不是线性轨迹），它结合了确定性和非确定性行为：在非确定性自动机中的转换导致一组状态，从中选择一个;在确定性树自动机中的转换导致一个后继集。交替自动机展示了这些存在和普遍行为的组合虽然我们下面采用的演示是一个状态的连接之间的非确定性选择，它可以推广到任意命题formulae上的numerical，numerical和状态。交替自动机的一个例子是比布希自动机更成功的自动机。LTL到自动机的转换有两种表示，X（fUg）→X（g<$（f<$X（fUg）D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）8387∀ ∈ ∀ ⟨ ⟩ ∈±±∈∧J¯定义2.4 VWAA在单词u0u1上的游程σ. ∈ ω是一个标记的自动机我们遵循Gastin和Oddoux [11]的稍微非传统的介绍：转换是从一个状态到一个状态的结合;每个状态可以有多个转换，非确定性地选择。这有效地编码了从给定状态到达的状态的合取的析取Fritz和Wolper [10]给出的表示是等价的，但是定义中的差异导致自动机的表示更大。另外，Gastin和Oddou使用了一个共同的Buchi接收条件，而Fr则使用了一个Buchi条件。 我们讨论：对于所考虑的交替自动机，一个Bu？hi条件F？Q等价于一个Co-Bu？hi条件Q\F.定义2.3Analternatingco-BuüchiautomatonAisdefinedbythetuple其中，Q是状态集;是转换标签的字母表;δ是转换函数Q→22<$×2Q;I<$2Q是状态的初始组合集;F<$Q是最终状态至于布契自动机定义above，transitionl abel是从 2ω开始的;接受的词仍然是从ω开始的。交替自动机表示LTL公式已知是非常弱的，这意味着在由跃迁确定的状态（Q，）上存在偏序，使得q Q，α，qJδ（q），qJ Q. 也就是说，仅允许从状态到较低或相等状态的转换。这一限制的结果是：在每一个弱循环中，只有循环是自循环。DAGV，E，λ，带V 划分为水平V i，V =i∈NV i和Ei∈NVi×Vi+1。λ：V→Q用au的状态标记图的顶点番茄。Vi可以看作是Q的元素的多重集合。图与词和自动机的关系是λ（V0）∈I和v∈Vi，vλ（v），α，SJ∈δ（λ（v））uiα s=λ（E（v））一个游程是可接受的，如果σ的每一个无限分支只有有限个标号在F中的节点。2.4.1LTL到VWAA的转换我们在这里报告Gastin和Oddoux给出的转换过程集合运算符构造两组析取范式转换的合取：X|∈X，∈Y}。 overbar运算符将req转换为集合风格的析取范式表示：原子命题或时态子公式的合取集合。对于原子命题P上的LTL公式，VWAAA =由下式给出：88D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83G（p→Fq）**东凤企业股份有限公司*不联系我们{\fnMicrosoftYaHei\fs20\2cHFFFFFF\b0}→<$p qG（p→Fq）FqG（p→Fq）FqG（p→Fq）FqFqG（p→Fq）T TG（p→Fq）图二、示例交替自动机（左）和在输入σ=p p pq上运行的一部分（右）。 * 指示无约束的过渡。• Q是Q的时间子公式集（以LTL算子作为主要连接符的子公式集，并原子命题集）• f=2P;I=f;F是形式f1Uf2或Ff1的多个元素的集合• δ定义为δ（T）={\ displaystyle\mathbb {T}δ（p）={{a ∈ |p∈a}，T <$}δ（<$p）={<${a∈<$|p∈/a}，T<$}δ（X<$）={\displaystyle\，e\，}|e∈}δ（F）=（）（{，F}）δ（G）=（）{，G}）δ（，}）δ（1R2）=（2）（（1）{，1R2}）其中，δ是δ的扩展以包括δ的命题子公式：如果θ∈Q，则θ（θ）=δ（θ）（（我们给出了一个示例VWAA，对应于图2中的LTL公式G（pFq）以及一个样本运行。D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）8389∈ ∧ ⊆∈⊆×∀ ∈ ∃ ⟨ ⟩ ∈∈⊆.Σ2.4.2n的紧表示将VWAA的运行表示为DAG是有问题的，因为每个级别的顶点数量无限制地增长。我们可以通过将每个级别限制为一个集合而不是一个多集合来减少运行我们称连续集合构形为CiQ。一个词u 0 u 1上的配置序列. 如果存在的话，将一组边E划分为E i，CiCi+1，使得 QCiα，qJδ（q）。uiαqJEi（q）anddeverypathq0q1. . . 苏chthatqi+1Ei（qi）可以表示F的成员只出现有限次。例如，考虑图2中的运行。相应的配置顺序是{G（p→Fq）}{Fq，G（p→Fq）}{Fq，G（p→Fq）}{Fq，G（p→Fq）}{G（p→Fq）}这明显弱于最初的表述，但我们可以证明所接受的语言是等价的。首先，具有由边E i描述的接受度的配置C i的每个接受序列可以被直接转换成DAGi∈NCi，i∈NEi，I其中I是恒等函数关于国家。在相反的方向上，可以减少每个接受DAG到由Ci=v∈Viλ（v）给出的可接受的配置运行。 我们通过调用接受的路径：它们都是左追加和sunix闭合的-也就是说，接受路径的sunix也是接受的，因为接受路径预先固定了有限数量的附加状态。这意味着接受条件可以在配置上被简化为存在从每个Ci的每个元素开始的接受路径。这是通过检查DAG来保证的，因为每个Vi的每个元素后面都必须跟随一个接受的边缘序列。2.4.3超集性质两种游程公式都描述了每个时间点上状态的最小元素（或多集）我们可以在不改变已接受的语言的情况下，用Ci的超集（类似于Vi）代替Ci，只要连续的配置（树的层次）可以被修改以适应额外状态的演化，同时保持与游程的定义一致。这对于下面描述的编码是至关重要的：我们只需要约束电流90D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83（Ⅲ）k-l -循环，但我们忽略了0≤1 k<$1Lk非循环约束，如[3]所建议的配置是由转换描述的任何超集3有界模型检测编码在讨论了适合于模型检查的LTL公式的三种表示之后，我们现在转向这些表示可以用于有界模型检查的方式。Moura等人[6]和Clarke等人[5]对Bu？hi自动机的nc编码进行了使用SNF进行有界模型检查是Frisch等人的一篇论文的主题。[9]。我们在这里将编码结合在一起的方法是将规范的编码成分分离为三个部分：在所有情况下约束路径的部分;仅当路径是有限路径前缀时约束路径的部分;以及仅当路径是k-循环时约束路径的部分。在原始方法[1]中添加第一个约束有可能大大简化所得公式3<$M，f）k：=<$M） kc（f，k）.encn（f，k）Kl=零（lLk =l（f，k，l））其中encc、 encn和encl表示如下所述的公共、有限和循环编码。3.1BoundedModelCheckingwithBüchiAutomata我们提出了一种de Rexia等人[6]编码的变体，使状态的表示显式化，以避免对状态强制互斥的开销与其他演示文稿相比，我们使用广义的布希自动机：复杂性的chechinggmultipleeaceptancesetsismucchlowtheorantheoverheadofconversiontoclasical布希自动机。所有由布吕克希自动机所接收的都是一个具有有限反例（如Fφ）的有限环-f或多个有限环，它们用一个平凡的有限环编码。因此，有限前缀的情况永远不会被接受，我们推导出enc n（f，k）= n。给出了一个表示LTL的广义dBuéchi自动机，其中Bf=<$Q，<$N，δ，I，T <$N，我们将当前状态q∈Q编码为范围0. |− 1：存在一对一映射Q ×{ i| 0≤i| Q<|− 1 }。|− 1}.对于每个状态i，我们有一组命题变量q n（i），0 ≤n<[log 2（|Q|）|我们写Q1，用于断言比特模式Q0Q1.3给出的公式源自Biere等人给出的常用BMC配方[1]的文件。我们写M）k 对于模型的编码，lLk 对于路径是一个D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）8391（Ⅲ）FF（k，l）=（s）B是ε（q）的最佳表示。对于表示LTL的Buéchi自动机a， A是该模型中的命题集合;元素a∈A的编码是给出 ai作为标准编码。转换关系被编码为对原始状态、目标状态和标签的一组约束。如果转移关系是全的，我们可以写TBf（i，k）=. （分）（a）（b）i iJi+1s，α，sJ < $∈δa∈α初始集合被直接编码为I的成员上的析取：IB（k）=<$s）0s∈I最后，我们决定了一个概念。Buchiacept ancendition是T的每个成员被无限频繁地访问。由于我们已经排除了有限路径前缀，我们知道所有被考虑的路径都是abω的形式。如果我们断言作为循环编码的一部分，在Bu？hi自动机中的相应路径遵循一个me模式，我们可以暗示要求来自每个接受集的代表出现在循环中（即，在b中）：K我F我这样T∈Ti=l s∈Tk−1encc c（f，k）=IBf（k）<$TBf（i，k）i=0时encn（f，k）=nencl（f，k，l）=FBf（k，l）[日志2]|Q|）|− 1i=0时qi（l）参与方qi（k）虽然LTLtoBu？chi自动机编码在公式的大小上是整数，但上述编码仅引入了线性数量的变量。结果公式是线性大小的产品的数量的转变和k，除了FB f是二次的：O（|不|k2）。3.2基于交替自动机的有界模型检测交替自动机的ncding与Bu？hi自动机非常相似。由于运行是一系列配置而不是状态，因此我们使用一个状态变量，92D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83（2）（Ⅲ）∈一个{∈|∈}{∈|∈}F能够表示每一个状态;配置然后由状态的组合表示。给定一个表示LTL公式f的VWAA，f= Q，δ，I，F，我们通过变量q（i）对第i个配置中a a状态q的存在进行编码。一个配置被编码为它的成员的合取：我们写Ci= q∈Cq（i），其中i=。注意，这限制了必要的，但不足够的，配置的成员，所以描述了最小描述运行的配置，如第2.4.3节所述。转换的目标可以被看作是配置的子集，因此以相同的方式编码。对于从上述LTL公式推导出的VWAAs，转换被标记为一组原子命题的集合：命题的允许分配集合。这些可以用文字的合取来表示，其中p q表示aΣp一一ΣQa. 我们写α i表示表示α的文字的合取2、特别方便因为LTL到VWAA转换的实现[11]直接产生这些合取。如前所述，过渡关系被给出为一系列约束TAf（i，k）=.q（i）.<$a）i<$sJ）i+1q∈Q<$α，qJ <$∈δ（q）初始配置集被编码IA（k）=C0）0C0∈I如果没有分支包含F元素的无限次出现，则VWAA运行是接受的。这可以在k-prefix路径上得到保证，如果在任何点达到空配置：非常弱的性质意味着所有连续的配置也是空的，因此没有状态被无限频繁地访问。这也意味着我们可以将检查减少到空的第k个配置：即使第一个空配置在k之前，这也将保持。PAf（k）=<$q（k）q∈Q对于循环的情况，我们不能简单地检查F的出现次数是否无限，因为Co-Bu？hi条件是在穿过构形空间的路径上也就是说，接受运行可以由无限大组成，4参见Gastin和Oddoux的注释2 [11]D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）8393.我iJi+1→路径的数量，每个路径具有有限数量的接受状态的出现。在这种情况下，接受状态将出现在循环中的一个配置中，表明该状态被无限频繁地访问。事实上，我们必须再次利用非常弱的条件：VWAAs中唯一的循环是自循环，因此唯一的路径，访问一个状态的无限经常必须这样做，总是采取自循环转换。通过接受路径的左附加和前缀闭合属性，我们可以推断，如果可以从接受状态进行非自循环转换，那么该状态必须是接受路径的一部分。FAf（k，l）=K<$q）→.<$α）β<$q）β我这样i=l<$α，qJ<$∈δ（q）q∈/qJk−1encc c（f，k）=IAf（k）<$TAf（i，k）i=0时encn（f，k）=PAf（k）encl（f，k，l）=FAf（k，l）q（l）Particleq（k）q∈Q这种编码在LTL公式的大小中产生线性数量的变量。由此产生的命题公式是线性的产品的数量的转变和k，再次除了FAf这是二次的k。3.3基于SNF的有界模型检测由于SNF是LTL的一种特殊化，我们可以使用标准的BMC方法对其进行编码，但 通 过 考 虑 规 则 的 结 构 ， 我 们 可 以 产 生 更 好 的 结 果 。 给 定 一 组 表 示LTLformulaf、muf的规则，我们分别识别每种类型的规则初始规则（start→f）指定初始条件：If（k）=<$f）（start→f）∈f全局不变规则pf是对各个状态的配置的约束Pf（i）=<$p→f）（p→f）∈f0我94D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83我T（k）=布拉KJKJ布拉布拉布拉布拉KKLK全局步骤规则（p→Xf）将状态与它们的后继者联系起来，类似于转移关系。上面，我们包括了encc中的转换关系以及encl中其状态的循环条件。然而，我们可以通过将时间1800秒502836838769.83142404387617.69表1使用三个有效规范的DME示例的zCha计时。指定为“名称（时态运算符的数量，最大嵌套深度）”;“大小”表示子句的数量。可伸缩性规范中出现的时态运算符的数量和嵌套深度在表中以数字对的形式报告我们使用了NuSMV的修改版本[2]，改进了CNF转换[16];在SAT求解器zCha中进行计时[15]。表1显示了验证三个正确质量标准的结果我们不报告每个自动机转换产生的状态数，而是报告CNF结果的大小。这意味着自动机方法可以直接与SNF和直接编码进行比较。我们观察到，随着规范变得越来越复杂，SNF编码的简单性具有越来越大的优势。交替自动机方法包含了由TMP产生的布赫自动机：一个特别有趣的结果，因为后者包括基于高级模拟的简化技术，而前者使用简单的转换和状态简化。我们通过比较两个不正确的规范与不同的最小反例来说明不同编码对反例大小的影响（表2）。她看到，由于产生了较长的反例，所以Bu¨ chi自动机的概率较其他程序都是可比的D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）8399桨编码器K时间K时间优先1 （4，2）优先2 （4，2）AA140.03530.30AA-140.03530.89SNF130.02520.49修复130.02520.83TMP533.26>200人Orig130.02521.15表2DME示例中使用两个无效规范的zCha中的计时。指定为尽管VWAA方法在较大的例子上稍微快5结论和今后的工作基于自动机的有界模型检测的主要优点是转换过程的高度发展，但转换过程的许多缺点却使其平衡。我们已经描述了如何使用交替自动机克服了许多这些问题，并证明了他们的BMC使用。一个简单的交替自动机编码已经被证明是几乎是一个安全的，一个高度发达的布希自动机方法，虽然在许多例子中落后于SNF编码（没有任何简化）。这项工作为进一步发展指明了几个有希望的方向。交替自动机[10]的基于模拟的简化可以提高该方法的性能，并且与SNF的密切关系可能意味着SNF编码也可以通过这种简化技术来改进。这种关系也可以产生更好的编码的co-Bu？chi条件，进一步提高了性能。一种可行的编码Co-Bu？chi条件的方法是采用Latvala等人提出的新的线性空间编码[13 ]第10段。6确认如果没有CHARME 2003的评审员的有用评论，我是不会开始研究这些编码方法的。我还感谢保罗·杰克逊博士对本文主题的广泛讨论和投入。100D. Sheridan/Electronic Notes in Theoretical Computer Science 119（2005）83引用[1] Biere，A.，A. Cimatti，E.Clarke和Y.Zhu，Symbolic model checking without BDD，in：W. Cleaveland，编辑，系统构造和分析的工具和算法。第五届国际会议，TACAS'99，计算机科学讲义1579（1999），页。193-207.[2] Cimatti，A.，E.克拉克角，澳-地Giunchiglia和M. Roveri，NU SMV：a new Symbolic ModelVerifier，in：N. Halbwachs和D. Peled，编辑，第十一届计算机辅助验证会议论文集（CAV495-499.[3] Cimatti，A.，M. Pistore，M. Roveri和R. LTL模型检验在SAT中的编码改进，A. Cortesi，编辑，第三届国际验证研讨会，模型检查和抽象解释，计算机科学讲义2294（2002），pp。196-207.[4] Cimatti，A.，M. Roveri和D. Sheridan，Bounded Verification of Past LTL，载于：A. J.Hu和A.K. Martin ， editors ， Formal Methods in Computer-Aided Design; 5th InternationalConference，FMCAD 2004，Lecture Notes in Computer Science（2004）.[5] Clarke，E. M.，D. Kroening，J. Ouaknine和O. Strichman，有界模型检验的完备性和复杂性，在 ： B 。 Ste Escheren 和 G. Levi ， editors ， Verification ， Model Checking ， and AbstractInterpretation ， 5th International Conference ， VMCAI 2004 ， Venice ， January 11-13 ，2004，Proceedings，Lecture Notes in Computer Science2937（2004），pp.85比96[6] 德韦拉湖，H. Ruewald和M. Sorea，Lazy theorem proventing for bounded model checking overin finite domains ， in ： A. Voronkov ， editor ， Automated Deduction - CADE-18; 18thInternational Conference on Automated Deduction ， Lecture Notes in Computer Science2392（2002），pp. 438-455.[7] 我是萨米，K。 和G.J.Holzman nn，O ptimi zingBu？chiautomata，in：C. 2000年8月22日至25日，美国宾夕法尼亚州大学帕克，第11届国际会议，计算机科学讲义，第1877（2000）页。153-167.[8] Fisher，M.，时间逻辑的一种解析方法，在：第十二届国际人工智能联合会议（IJCAI）（1991年）的会议记录。99-104.[9] Frisch，A.，D. Sheridan和T. Walsh，A fixpoint based en