Rules on desirable State Sequences: TLPlan approach

TLPlan [Bacchus & Kabanza, 95/98] controls a

forward state-space planner

Rules are written on state sequences

using the linear temporal logic (LTL)

LTL is an extension of prop logic with temporal modalities U until [] always

O next <> eventually

Example:

If you achieve on(B,A), then preserve it until On(C,B) is achieved:

[] ( on(B,A) => on(B,A) U on(C,B) )