《GP——基于规划图的遗传规划算法》由会员分享，可在线阅读，更多相关《GP——基于规划图的遗传规划算法（15页珍藏版）》请在金锄头文库上搜索。
1、1关于关于 CTL 与与 EAGLE两种规划扩展目标表示语言的语义比较两种规划扩展目标表示语言的语义比较 黄巍黄巍1 姜云飞姜云飞2 文中华文中华3 彭宏彭宏1（华南理工大学计算机科学与工程学院（华南理工大学计算机科学与工程学院 广州广州 510641）1（中山大学软件研究所（中山大学软件研究所 广州广州 510275）2（湘潭大学信息工程学院（湘潭大学信息工程学院 湘潭湘潭 411105）3摘要摘要 在不确定的智能规划领域中，CTL 和 EAGLE是两种重要的扩展目标表示语言。虽然 与 CTL 相比 EAGLE具有可以表示规划意图和失败处理机制的特点，但是有关严格比较这两 种目标表示语言语义
2、的研究工作还不多。本文在规划的执行结构这一语义层次上对这两种 语言做了严格的比较，证明了对于许多包括原来曾被认为无法用 CTL 表示的 EAGLE规划目 标而言，都存在着一个与之语义等价 CTL 规划目标，并且进一步分析了这两种语言在表示 规划目标和指导规划求解这两个层次上的优缺点。关键词关键词 不确定的智能规划; 扩展的规划目标; 执行结构; CTL; EAGLE 中图法分类号中图法分类号 TP18引言与经典规划中的可达性目标不同，扩展的规划目标往往包含了对规划执行过程的时态要求，所以它们往往被表示成时态逻辑公式1-2。而在不确定的规划领域中，具有分支计算结构的CTL3和EAGLE4是目前两
3、种重要的扩展目标表示语言。CTL由于已被广泛应用于模型检测的领域，所以它也在基于模型检测的规划方法5-7中被用于表示扩展的规划目标；而EAGLE是一种专门描述扩展的规划目标的语言，它长于表示规划者的规划意图（如其语法中的TryReachTryReach和DoReachDoReach算子分别表示“尽量试着到达”和“必须保证到达” ，而TryMaintTryMaint和DoMaintDoMaint算子则分别表示“尽量保持”和“必须保持” ）以及失败处理机制（如其语法中的FailFail算子表示“若失败则” ）4, 7, 8。如何选择合适的规划目标表示语言并将目标公式转化为用于指导搜索规划解的控制自
4、动机是一个很重要的问题。因为目标语言的表达能力决定了对规划解的搜索是否可能，而由目标公式产生的控制自动机的状态数目部分决定了整个搜索空间的大小4-5。虽然在文献4和7中，一些用EAGLE公式（例如一些含有TryReachTryReach算子和FailFail算子的EAGLE公式）表示的扩展目标被认为无法用CTL表示，但是至今有关CTL和EAGLE在语义层次上比较的研究还很少。本文在规划的执行结构这一语义层次上对这两种语言做了严格的比较，证明了对于许多EAGLE目标公式（包括了文献4和7所列举的所有不可被CTL表示的EAGLE目标本课题得到国家自然科学基金（60773201）、广东省自然科学基金
5、（07006474）和广东省科技攻关项目基金（2007B01020044）资助. 黄巍黄巍, 男, 1979 年生, 博士, 博士后, 主要研究方向为智能规划、自动推理 和基于模型诊断. Email: . 姜云飞姜云飞, 男, 1945 年生, 硕士, 教授, 博士生导师, 主要 研究领域为智能规划、自动推理和基于模型诊断等. 文中华文中华, 男, 1966 年生, 博士, 副教授, 主要研究方向 为智能规划和图论. 彭宏彭宏, 男, 1956 年生, 博士, 教授, 博士生导师, 主要研究领域为数据挖掘和智能网络 技术.2公式）而言，都存在着一个与之语义等价CTL目标公式。并进一步分析指出了
6、EAGLE与CTL相比在表示规划目标时更简洁、相应的控制自动机构造过程更简单，但是它无法表示一些基本的CTL语义特征。下文内容安排如下：第2部介绍了有关不确定规划的基本概念，第3部分则是CTL和EAGLE目标公式严格的语法和语义定义，第4部分即本文的核心是CTL和EAGLE之间的语义比较，最后的第5部分则给出了结论以及下一步研究展望。2 不确定的规划领域与带有上下文信息的规划所谓规划领域是指现实动态系统的抽象模型。在本文中，规划领域是指一个不确定的状态转换系统，它由系统的状态集合、动作集合以及状态转换函数构成。其中，各系统状态可以用命题公式描述，状态转换函数则描述了如何通过执行某个动作而使系统
7、从一个状态不确定地转换到若干个不同的可能状态。定义定义1(规划领域规划领域)：一个规划领域D是一个四元组P, S, A, R，其中：P 是一个有限非空的原子命题集合，S 2P是系统的状态集合，A 是一个有限的动作集合，而R : SA2S是一个状态转换函数。在后面的内容里，F(P)表示建立在原子命题集P上的命题公式集合。对扩展目标作规划时，规划的目的已不再仅仅限于令系统能够从初始状态到达目标状态（即可达性目标） ，当中还可能包括了对系统的状态转换历史的具有时态性质和强度差别的要求。例如，要求一个可移动的机器人尽量试着到达某一指定位置并要求它永远避开那些危险的区域；又或者，要求机器人不断地在位置A
8、与位置B（如果可能的话）之间来回移动。像上述这些扩展目标往往被表示成时态逻辑公式，特别是CTL公式或EAGLE公式。为了满足扩展的规划目标，规划中须包含上下文信息（即应考虑系统的状态转换历史）。定义定义2(规划规划)：对于一个规划领域D = P, S, A, R而言，它的一个规划是一个四元组C, c0, act, ctxt，其中：C 是一个上下文集合，c0C 是 D 的初始上下文，act: SCA 为动作选择函数，而ctxt: SCSC为上下文更新函数。在定义定义2中，act和ctxt的含义是：若D处于状态s下并且当前上下文为c，那么act(s,c)将返回此时规划所指定的待执行动作，而ctxt
9、(s,c,s)将为某一可能的下一状态s指定其相应的上下文。act和ctxt都是部分函数，因为某些状态上下文的组合在规划的执行过程中也许不可能出现。如果当act (s,c)=a且ctxt (s,c,s)=c时都有sR (s,a)，那么称是可执行的；如果当act (s,c)=a且sR (s,a)时都有(cC)(ctxt (s,c,s)=c)，那么称是完备的。在后面内容里，我们所讨论的规划都是可执行的且完备的。其实，一个带有上下文信息的规划的执行过程就是一个当前状态上下文序对不断3转换的过程。我们可以用下面定义的执行结构来表示的所有可能的执行情况。定义定义3(执行结构执行结构)：设C, c0, ac
10、t, ctxt是规划领域D = P, S, A, R的一个规划， I S为D初始的可能状态的集合。从I所导出的的执行结构为K=Q, T, L，其中QSC 和T QQ 是满足以下条件的最小集合：若 sI，那么s, c0 Q；若s, cQ，act(s,c)=a，sR(s, a)且ctxt (s, c, s)=c，则s, cQ且(s, c, s, c)T。另外，函数L: SCS的定义为：L(s, c)=s。qQ是K的一个终止状态上下文序对当且仅当不存在qQ使得(q, q)T。直观地讲，执行结构K 就是一个有向图，其中的节点集 Q 是系统在以 I 为初始状态集执行规划时所可能到达的所有状态上下文序对的
11、集合，而 T 则表示了相应的所有可能的状态上下文序对的转换。K 的各个终止状态上下文序对则代表了规划执行的终止。其实，定义定义 3 里的执行结构就是一个 Kripke 结构3。一个执行结构描述了执行一个给定的规划所可能出现的各种情况。而执行结构中的一条执行路径则表示了相应规划的一种可能的执行历史情况，它是执行结构中的一个状态上下文序对序列。定义定义4(执行路径执行路径)：设K=Q, T, L是规划领域D的规划C, c0, act, ctxt从初始状态集I 所导出的执行结构。K里的一条从q0Q出发的执行路径是一个状态上下文序对序列q0, q1, ，其中各 qi 都属于Q而且：若 qi是该序列的最
12、后一个状态上下文序对，那么 qi是 K 里的一个终止状态上下文序对；否则(qi, qi+1)T。从上面的定义里可以发现执行路径既可以是有限的也可以是无限的。若一个状态上下文序对序列是某个执行路径的有限子序列，那么我们称之为相应执行结构中的一条路径路径。若有一条从 q 到 q的路径，那么就称 q是 q 可达的。为了便于后面的叙述，这里规定了一些有关执行路径和路径的标记方法。表示空路径。设 K 是一个执行结构，那么 HISTORIESOF(K)和 PATHSOF(K)分别表示 K 的执行路径集合与路径集合。若, PATHSOF(K)且，则：（或）表示是的一个前缀；（或j0)(K, qj h)且(K
13、, qi h)且(Sg1(q0)(K, LAST () g)（定义定义 7）(=q0, q1, HISTORIESOF(K)(i0)(ij0) (K, qj h)且(K, qi h)且(K, qi g)（定义定义 6）K, q0 A A(h U U (hg)（4）若 g1 = TryReachTryReach h，那么(4.1)（定理定理 3）K, q0 A A(EFEF h) WW h)且(Sg1(q0)(K, LAST () g)（定义定义 6）(=q0, q1, HISTORIESOF(K)(i 0)(K, qi h)或者(k0) (K, qk EFEF h)，且(Sg1(q0)(K,
14、LAST () g)(=q0, q1, HISTORIESOF(K)(i 0)(K, qi h)或者(k0)(K, qk EFEF h)且(K, qk h)，且(Sg1(q0)(K, LAST () g)(=q0, q1, HISTORIESOF(K)(i 0)(ij0)(K, qj h)且(K, qi h)或(k0)(K, qk EFEF h)且(K, qk h)，且(Sg1(q0)(K, LAST() g)（定义定义 7）(=q0, q1, HISTORIESOF(K)(i 0)(ij0)(K, qj h)且(K, qi h)且(K, qi g)或(k0)(K, qk EFEF h)且(K
15、, qk h)（定义定义 6）K, q0 A A(hEFEF h) WW (hg)由以上（1） 、 （2） 、 （3）和（4） ，定理定理 4 得证。9虽然文献10提出分别用 AFAF (hg)和 A A(EFEF(hg) WW (hg)来表示(DoReachDoReach h) ThenThen g 和(TryReachTryReach h) ThenThen g（其中 gC, E g） ，但是当中没有考虑到相应的 EAGLE公式语义对极小路径集的要求，所以有关的 CTL 公式所表示的规划目标较弱。ThenThen 算子的直观含义是“顺序实现” 。 “g1 ThenThen g2”形式的 EAGLE目标公式所表示的规划意图是“先实现子目标 g1 然后再实现子目标 g2” 。其实根据定义定义 7，ThenThen 算子是满足结合律的。辅助定
