Extended Goals [Top]
 

Planning for Temporally Extended Goals

MBP can synthesize plans that solve temporally extended goals. These goals express conditions on the execution paths associated to the solution plan, i.e., on the sequences of states resulting from execution, rather than just conditions on the final states.

MBP provides two languages for expressing temporally extended goals, namely CTL and EaGLe. 

CTL is a temporal logics that is widely used in the model checking community for expressing properties of dynamic systems. CTL can express temporal conditions that take into account the fact that an action may non-deterministically result in different outcomes. Hence, extended goals allow us to distinguish between temporal requirements on "all the possible executions" and on "some executions" of a plan.

EaGLe ("Extended Goal Language") is a new language for specifying temporally extended goals. It extends CTL with the possibility of expressing classes of goals that are typical of real world applications, but that cannot be expressed in CTL and other existing temporal logics. Examples of EaGLe goals are "try achieve a goal whenever possible" or "if you fail to achieve a goal, recover by trying a different goal".

Further information on planning for extended goals can be found here.
 

An example

Consider the domain depicted in the picture below (left part). Three engines may provide power. At every step, it is possible to increase or decrease (by one unit) the power provided by one of the engines.

Consider the problem of turning on the engines in order to reach a desired total power starting from 0, and to keep it. A possible requirement would be to always have the engines "balanced": at any step of the plan execution, the maximum difference between the power of any engine with that of any other must be at most 1 (see picture, right part). This can be expressed as an extended goal.

(define (domain saturation_balancing)
  (:types engine_no power_range total_power_range)
  (:functions
       (engine_power ?e - engine_no) - power_range
       (desired_power)               - total_power_range)

  (:action increase_power
   :parameters (?e - engine_no)
   :precondition (not (= (engine_power ?e) (sup power_range)))
   :effect        (assign (engine_power ?e) (+ (engine_power ?e) 1)))

  (:action decrease_power
   :parameters (?e - engine_no)
   :precondition (not (= (engine_power ?e) (inf power_range)))
   :effect        (assign (engine_power ?e) (- (engine_power ?e) 1)))

  (:action nop)
)

The following problem describes the CTL goal of reaching and keeping full power from 0 keeping balancing of the powers provided by the engines (see picture, right part). Intuitively, the CTL goal expresses (a) that maximum power must be reached (the "AF" clause), and (b) that for every pair of engines, the maximum allowed power difference is always 1 (the "forall... AG" clause).
Notice that :

(define (problem satbal_pb)
        (:domain saturation_balancing)
        (:typedef
            engine_no         - (range 1 3)
            total_power_range - (range 0 6)
            power_range       - (range 0 2))
        (:init
           (forall (?e - engine_no)
              (= (engine_power ?e) (inf power_range))))
        (:ctlgoal
           (and
             (af (= 6
                  (sum (?e - engine_no) (engine_power ?e))))
             (forall (?e1 - engine_no)
               (forall (?e2 - engine_no)
                  (ag (not (> (engine_power ?e1) (+ (engine_power ?e2) 1)))))))))  

The same problem can be expressed using EaGLe. In this case, keyword doreach is used to express the requirement that the maximum power must be reached, and keyword domaintain is used for the requirement that the maximum allowed power difference cannot exceed 1.

(define (problem satbal_pb)
       [....]
       (:eglgoal
           (and
             (doreach (= 6
                  (sum (?e - engine_no) (engine_power ?e))))
             (forall (?e1 - engine_no)
               (forall (?e2 - engine_no)
                  (domaintain (not (> (engine_power ?e1) (+ (engine_power ?e2) 1)))))))))

To solve the problem, run

MBP-solve -plan_output - <domain> <problem>

where <domain> and <problem> are the domain and problem above.