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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Backstrom C. (1995). Expressive equivalence of planning formalisms. Artificial Intelligence 76(1-2): 17–34
Baral, C., & Zhao, J. (2006). Goal specification, non-determinism and quantifying over policies. In: AAAI-2006, pp. 231–237.
Bryant R.E. (1992). Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3): 293–318
Bylander T. (1994). The computational complexity of propositional STRIPS planning. Artificial Intelligence 69(1-2): 165–204
Cimatti, A., Giunchiglia, F., Giunchiglia, E., & Traverso, P. (1997). Planning via model checking: A decision procedure for \({\mathcal{AR}}\) . In 4th European conference on planning (ECP’99), vol. 1348, pp. 130–142.
Cimatti, A., Roveri, M., & Traverso, P. (1998). Strong planning in non-deterministic domains via model checking. In AIPS, pp. 36–43.
Clarke, E. M., & Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, workshop (pp. 52–71). London, UK: Springer-Verlag.
Clarke, E. M., & Wing, J. (1996). Formal methods: state of the art and future directions. In ACM Computing Systems Surveys, vol. 28.
Daniele, M., Traverso, P., & Vardi, M. Y. (1999). Strong cyclic planning revisited. In 5th European conference on planning (ECP’99), vol. 1809, pp. 35–48.
Fikes R.E. and Nilsson N.J. (1990). STRIPS: A new approach to the application of theorem proving to problem solving. In: Allen, J., Hendler, J. and Tate, A. (eds) Readings in planning, pp 88–97. Kaufmann, San Mateo CA
Franklin, S., & Graesser, A. (1996). Is it an Agent, or just a Program?: A Taxonomy for Autonomous Agents. In Intelligent agents III. agent theories, architectures and languages (ATAL’96), vol 1193, Berlin, Germany, Springer-Verlag.
Ghallab M., Nau D. and Traverso P. (2004). Automated planning: Theory and practice. Morgan Kaufmann Publishers Inc., USA
Giunchiglia, F., & Traverso, P. (1999). Planning as model checking. In 5th European conference on planning (ECP’99), vol. 1809, pp. 1–20.
Kabanza F., Barbeau M. and St.-Denis R. (1997). Planning control rules for reactive agents. Artificial Intelligence 95(1): 67–11
Dal Lago, U., Pistore, M., & Traverso, P. (2002). Planning with a language for extended goals. In Eighteenth National Conference on Artificial Intelligence (pp. 447–454). CA, USA: Menlo Park.
Müller-Olm, M., Schimidt, D., & Steffen, B. (1999). Model checking: A tutorial introduction. In SAS’99, LNCS 1694, pp. 330–354.
De Nicola, R., & Vaandrager, F. (1990). Action versus state based logics for transition systems. In Proceedings of the LITP spring school on theoretical computer science on Semantics of systems of concurrent processes. New York, NY: Springer-Verlag, pp. 407–419.
Pecheur, C., & Raimondi, F. (2006). Symbolic model checking of logics with actions. In MoChArt 2006 (pp. 1215–1222). Springer Verlag.
Pereira, S. L. (2007). Planning under uncertainty for extended reachability goals. PhD thesis, IME-USP.
Pereira, S. L., & Barros, L. N. (2007). Nondeterministic planning based on α-ctl: implementation and formal properties. Technical Report RT-MAC-2007-11, IME-USP, São Paulo, Brasil.
Ramadge P.J.G. and Wonham W.M. (1989). The control of discrete event systems. Proceedings of the IEEE 77(1): 81–98
Russell S. and Norvig P. (2002). Artificial Intelligence: a modern approach (2nd ed). Prentice-Hall, New Jersey USA
Saiedian H. (1996). An invitation to formal methods. IEEE Computer 29(4): 16–30
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Pereira, S.L., de Barros, L.N. A logic-based agent that plans for extended reachability goals. Auton Agent Multi-Agent Syst 16, 327–344 (2008). https://doi.org/10.1007/s10458-008-9034-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10458-008-9034-0