Reasoning about actions and planning in LTL action theories
Diego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi · 2002
In this paper, we study reasoning about actions and planning with incomplete information in a setting where the dynamic system is specified by adopting Linear Temporal Logic (ltl). Specifically we study: (i) reasoning about action effects (i.e., projection, historical queries, etc.), in such a setting; (ii) when actions can be legally executed, assuming a non-prescriptive approach, where executing an action is possible in a given situation unless forbidden by the system specification; (iii) the problem of finding conformant plans for temporally extended goals that consist of arbitrary LTL formulas, thus allowing for expressing sophisticated dynamic requirements. For each of these problems we establish techniques and characterize the computational complexity. For the last two problems we make use of a second-order variant of LTL.