关于CTL与EAGLE两种规划扩展目标表示语言的语义比较

A Comparison of Semantics of Extended Goals Expressed in CTL and E_AG_(LE)

在不确定的智能规划领域中,CTL和EAGLE是两种重要的扩展目标表示语言.虽然与CTL相比EAGLE具有可以表示规划意图和失败处理机制的特点,但是有关严格比较这两种目标表示语言语义的研究工作还不多.文章在规划的执行结构这一语义层次上对这两种语言做了严格的比较,证明了对于许多包括原来曾被认为无法用CTL表示的EAGLE规划目标而言,都存在着一个与之语义等价的CTL规划目标,并且进一步分析了这两种语言在表示规划目标和指导规划求解这两个层次上的优缺点.

In automated planning under uncertainty, extended goals are often expressed as tem poral logic formulas, particularly as CTL（computation tree logic） formulas and EAGLE formulas. Though it is said that the capability of representing the ＂intentional＂ aspects of goals and the possibility of dealing with failure are the main new features of EAGLE with respect to CTL, there is not enough work devoted to formal comparison of semantics of these two languages. According to the formal semantics of EAGEE and CTL goals on Kripke structures （i. e. , execution structures induced by plans from initial states）, it is proven that many EAGLE goals including some having been deemed to be unexpressive in CTL（e. g. , some EAGLE goals in which TryReach operator and Fail operator appear） can be expressed in CTL in fact, and an analysis of the characters of these two languages in expressing extended goals and guiding the search for plans that satisfy them is given.