LTL模型检测技术在验证、计划合成与控制器综合中的应用

理论计算机科学电子笔记149（2006）91-104www.elsevier.com/locate/entcs分析LTL模型检测技术的计划综合和控制器综合（工作进展中）Sylvain Kerjean，Froduald Kabanza，Richard St-Denis西尔万·克尔让，弗罗杜阿尔德·卡班扎，理查德·圣丹尼斯1，2DepartemendSherbrooke（Qu′ebec），CanadaJ1K2R1SylvieThi'ebaux3澳大利亚国立大学国家信息通信技术和计算机科学堪培拉ACT 0200澳大利亚摘要在本文中，我们提出了处理可达性测试中的不变性的替代方法，无论是通过多过程还是通过比较，还是通过Bu？hiatomat a。这些结果与模型检测的三种不同应用有关：验证、计划合成以及人工智能规划的启发式指导和控制器合成。我们包括从使用LTL2Bu？hi转换器和公式级数的一个家族的改进的Lechekkking获得的从预处理实验室获得的实验主要工作：LTL2Buéchitra n stors，用于多过程、改进、验证和系统分析。1本研究得到加拿大自然科学和工程研究委员会的资助2我说：{西尔万·凯尔杰安，弗罗杜·乌尔德。圣-德尼斯}@美国她的博客。CA3 电子邮件：Sylvie. anu.edu.au1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.02892S. Kerjean等人/理论计算机科学电子笔记149（2006）911介绍用线性时序逻辑（LTL）进行模型检验已经证明了在程序验证、计划综合和控制器综合问题中的潜在价值。在这些问题中，我们将系统建模为状态图，表示其可能的执行序列。为了验证系统关于某些行为的正确性，我们可以将行为表示为LTL公式，然后使用LTL模型检查来执行验证[24，10，12]。为了沿着目标函数的期望路径控制系统，我们可以将目标表示为LTL公式，并使用LTL模型检查来合成一个行动计划，该计划指示在每个点执行的行动，以便系统表现出满足目标的行为，可能是最优的[2，13，22]。同样的技术也可以用来实现规划系统的搜索控制策略，也就是说，在特定的应用领域中如何有效地计算规划的经验法则[3]。为了防止系统陷入不期望的行为，我们可以将期望的行为表示为LTL公式，并使用LTL模型检查来合成禁止不期望事件的控制器[4，5]。这些程序验证、计划综合和控制器综合框架的模型检查器一种方法是使用LTL2Bu？chi翻译器[17，8，11，12，9]将LTL翻译为等价的Bu？chi自动机，然后使用它来执行验证过程，计划综合过程或控制器综合过程。另一种替代方案，到目前为止，在计划综合[2，13，22]和控制器综合[4，5]中使用的是沿着搜索引擎生成的状态序列推进LTL公式，该搜索引擎是验证、计划综合或控制器综合程序的基础。虽然从根本上植根于LTL公式的自动机理论表征，公式级数是非常简单的描述，抽象自动机理论的概念。这种简单性大概解释了，至少部分解释了它在人工智能规划中的吸引力，例如，它对非模态时间逻辑的适应，即TALplanner中的时间动作语言。在这种情况下，验证与计划或控制器综合之间的区别等同于公式编译与公式级数之间的区别。我 们 要 解 决 的 主 要 问 题 是 确 定 这 两 种 方 法 中 的 哪 一 种（moddelcheckingviaexplicitLTL2Buéchitransitionvsfor mulaprogression）在每种情况下最适合。 尽管翻译水平有了很大的提高，但LTL2Bu？chi翻译器仍然面临着一个潜在的瓶颈。对于程序验证来说，这可能不是很戏剧性，因为我们通常关注的是O-线验证过程，其中以分钟为单位的运行时间是可以接受的。在计划合成中，对于机器人应用程序，例如[6]，运行S. Kerjean等人/理论计算机科学电子笔记149（2006）9193时间以毫秒为单位。我们可能会认为LTL2Buéchitranslators只适用于简单的公式，但这是否适用于更复杂的目标（例如，[9]中的公平性，但具有量化）或规划问题的复杂搜索控制策略[2]必须得到验证。在规划综合中，搜索控制策略被一次性指定，作为规划应用领域指定的一部分。对于给定初始状态/目标问题的规划器的后续调用，它们保持不变[2，14]。在这种情况下，能够将LTL公式预编译为某种类型的Buechi自动程序将通过重新计算一些子公式级数来提供一些计算，这是公式级数算法经常发生的事情在某种程度上，这就是Kvarn-strom和Magnuson在TALplanner[16]中试图做的，但使用的是一些特殊的方法，尽管如此，这些方法还是带来了显著的改进。更具体地说，在每一步都从搜索控制规则和当前状态导出上下文，并在推理过程中使用这个过程通过使用所有经典重言式和一阶谓词逻辑的技术，减少了分配给命题变量或域量化变量的可能值这种部分编译还允许减少布尔公式中的析取和合取的数量（以及在量化变量的情况下要探索的有限域的大小），因为指定在规划区域中通常是多余因此，公式的大小在其发展过程中急剧缩小。一个系统性的L2翻译似乎是一个更有原则的方法。不幸的是，TLVs搜索控制策略是使用有界量化来指定的。一方面，即使这相当于有无限多个实例化的，但压倒性的大LTL公式，我们担心运行一个LTL2Buéchi翻译器对suchf或mulasmayca使用一个不切实际的爆炸。另一方面，到目前为止，我们还不知道任何有效的LTL2Bu？chi翻译器用于编译器的有约束的LTL。 如果没有这样的翻译器存在，我们的目标之一将是尝试开发一个。如果它存在，那么我们将不得不实施它，并将其与公式进展进行比较。由于我们仍处于研究的早期阶段，因此仅提供初步结果然而，给出了关于这种解释背后的背景的更多细节，即LTL语法和语义、公式进展算法、LTL2Bu？chi翻译器，以及对程序验证、计划综合和控制器综合框架的理解。94S. Kerjean等人/理论计算机科学电子笔记149（2006）912线性时序逻辑我们使用有界量化的LTL语言的定义是从一阶语言开始，包含常量，函数和谓词符号的集合和，以及常用的连接词<$和。这些都是增加了一元目标模态、一元时间模态“下一个”和二元时间模态“直到”。在所有这些运算符下的复合是不受限制的(in允许在时间上下文中进行特定量化），不同之处在于，在GOAL的范围内可能不会出现UAL、UAL和GOAL。 添加GOAL模态的动机是区分LTL目标和搜索控制策略（关于如何实现目标），也在LTL中表达[2，3，14]。在下文中，我们假设所有变量都有界。LTLi是一个可解的有限序列s，满足mr=r0r1· ··，其中每个ri是由当前世界状态si和一组当前目标状态Gi组成的一对（si，Gi）。这个想法是，在序列的阶段Γi我们处于世界状态si，并且正试图到达Gi中的一个状态。 时间模态允许表达这样的序列的一般属性。直觉上，非时态公式f意味着f现在成立（即在序列的第一阶段Γ0）;非时态公式f意味着f下一阶段成立（即，f本身可能包含其他时态算子，但对子集Γ（1）为真）;f1Uf2意味着f2在未来的某个阶段为真，并且f1在此之前为真（即f2对某些子集Γ（i）为真，并且f1必须对从Γi开始的所有子集为真）;GOAL（f）意味着f在当前阶段的所有目标状态Gi中为真，而GOAL范围之外的非时态公式指的是当前阶段的世界状态si序列的目标部分在正常的程序验证问题中是不相关的，可以被丢弃。在最初的TLRIGHT实现[3]中，目标组件是不变的（它是一个人试图达到的最终目标状态），因此它也可以被丢弃，并被全局变量取代在这种情况下，我们考虑的无限状态序列由一个有限序列和一个空闲的最终状态组成最近的TLTL扩展更一般，允许动态改变目标状态和循环计划，需要状态序列，如刚才介绍的解释LTL公式[14]。形式上，设一个有限集合D是话语的域，我们假设它在所有世界和目标状态中是恒定的，并设Γ是一个序列，定义为：其中，ri =（si，Gi）。我们说，公式f对于Γ（记为Γ）是真的|= f）i（r，0）|= f，其中真值递归定义如下：• 如果f是一个原子式，（Γ，i）|= f i si|= f根据一阶谓词逻辑的标准解释规则;S. Kerjean等人/理论计算机科学电子笔记149（2006）9195• （r，i）|= GOAL（f）i ∈Gi，Gi|= f根据一阶谓词逻辑的标准解释规则;• （r，i）|=x f i（Γ，i）|= f [x/d]，其中f [x/d]表示用d的名字替换f中的x;• （r，i）|=<$f i <$（Γ，i）|= f;• （r，i）|= f1<$f2i <$（Γ，i）|= f1和（r，i）|= f2;• （r，i）|= f i（Γ，i +1）|= f;并且• （r，i）|= f1Uf2i≠存在j≥i使得（Γ，j）|= f2，对于所有k，i ≤ k

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