A logic-based agent that plans for extended reachability goals |
| |
Authors: | Silvio Lago Pereira Leliane Nunes de Barros |
| |
Affiliation: | 1. Institute of Mathematics and Statistics, University of S?o Paulo, Sao Paulo, Brazil
|
| |
Abstract: | Planning to reach a goal is an essential capability for rational agents. In general, a goal specifies a condition to be achieved
at the end of the plan execution. In this article, we introduce nondeterministic planning for extended reachability goals (i.e., goals that also specify a condition to be preserved during the plan execution). We show that, when this kind of goal is
considered, the temporal logic ctl turns out to be inadequate to formalize plan synthesis and plan validation algorithms. This is mainly due to the fact that
the ctl’s semantics cannot discern among the various actions that produce state transitions. To overcome this limitation, we propose
a new temporal logic called α-ctl. Then, based on this new logic, we implement a planner capable of synthesizing reliable plans for extended reachability goals,
as a side effect of model checking. |
| |
Keywords: | Automated planning Model checking Temporal logic |
本文献已被 SpringerLink 等数据库收录! |
|