Abstract
The temporal logic ctl has been the preferred specification language in the model checking framework. However, when this framework is used for nondeterministic planning, it is not adequate to deal with many useful planning problems with temporally extended goals. This is because the validity of ctl formulas expressing such goals is not evaluated on the planning domain, but on the execution structure of the policy synthesized by the planning algorithm. In previous work we have presented a new variant of ctl, named α -ctl, which semantics can be defined directly on the planning domain. An advantage of this new logic is that plan synthesis can be obtained as a collateral effect of verifying the validity of a formula in the planning domain. In this paper we show how to use α -ctl to express some complex planning goals.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bacchus, F., Kabanza, F.: Planning for temporally extended goals. In: AAAI 1996, pp. 1215–1222. AAAI Press, Menlo Park (1996)
Baral, C., Zhao, J.: Goal specification in presence of non-deterministic actions. In: Mántaras, R.L., Saitta, L. (eds.) ECAI, pp. 273–277 (2004)
Baral, C., Zhao, J.: Goal specification, non-determinism and quantifying over policies. In: AAAI (2006)
Bylander, T.: The computational complexity of propositional STRIPS planning. Artificial Intelligence 69(1-2), 165–204 (1994)
Cimatti, A., Giunchiglia, F., Giunchiglia, E., Traverso, P.: Planning via model checking: A decision procedure for AR. In: Steel, S. (ed.) ECP 1997. LNCS, vol. 1348, pp. 130–142. Springer, Heidelberg (1997)
Cimatti, A., Roveri, M., Traverso, P.: Strong planning in non-deterministic domains via model checking. In: AIPS, pp. 36–43 (1998)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52–71. Springer, London (1982)
Daniele, M., Traverso, P., Vardi, M.Y.: Strong cyclic planning revisited. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 35–48. Springer, Heidelberg (2000)
Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. Morgan Kaufmann Publishers, San Francisco (2004)
Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 1–20. Springer, Heidelberg (2000)
Kabanza, F., Barbeau, M., St.-Denis, R.: Planning control rules for reactive agents. Artificial Intelligence 95(1), 11–67 (1997)
Dal Lago, U., Pistore, M., Traverso, P.: Planning with a language for extended goals. In: Eighteenth national conference on Artificial intelligence, pp. 447–454. AAAI, Menlo Park (2002)
De Nicola, R., Vaandrager, F.: 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, pp. 407–419. Springer, New York (1990)
Pecheur, C., Raimondi, F.: Symbolic Model Checking of Logics with Actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 113–128. Springer, Heidelberg (2007)
Pereira, S.L., Barros, L.N.: A logic-based agent that plans for extended reachability goals. Autonomous Agents and Multi-Agent Systems 9034, 327–344 (2008)
Pistore, M., Bettin, R., Traverso, P.: Symbolic techniques for planning with extended goals in non-deterministic domains (2001)
Pistore, M., Traverso, P.: Planning as model checking for extended goals in non-deterministic domains. In: IJCAI, pp. 479–486 (2001)
Thiébaux, S., Gretton, C., Slaney, J., Price, D., Kabanza, F.: Decision-theoretic planning with non-markovian rewards. JAIR 25(2), 75–118 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
do Lago Pereira, S., de Barros, L.N. (2008). Using α -ctl to Specify Complex Planning Goals. In: Hodges, W., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2008. Lecture Notes in Computer Science(), vol 5110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69937-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-69937-8_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69936-1
Online ISBN: 978-3-540-69937-8
eBook Packages: Computer ScienceComputer Science (R0)