Abstract
Several realistic non-deterministic planning domains require plans that encode iterative trial-and-error strategies, e.g., “pick up a block until succeed”. In such domains, a certain effect (e.g., action success) might never be guaranteed a priori of execution and, in principle, iterative plans might loop forever. Here, the planner should generate iterative plans whose executions always have a possibility of terminating and, when they do, they are guaranteed to achieve the goal. In this paper, we define the notion of strong cyclic plan, which formalizes in temporal logic the above informal requirements for iterative plans, define a planning algorithm based on model-checking techniques, and prove that the algorithm is guaranteed to return strong cyclic plans when they exist or to terminate with failure when they do not. We show how this approach can be extended to formalize plans that are guaranteed to achieve the goal and do not involve iterations (strong plans) and plans that have a possibility (but are not guaranteed) to achieve the goal (weak plans). The results presented in this paper constitute a formal account for “planning via model checking” in non-deterministic domains, which has never been provided before.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999. Springer, Heidelberg (1995)
Bacchus, F., Kabanza, F.: Using temporal logic to express search control knowledge for planning. Artificial Intelligence (1998) (Submitted for pubblication)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Cesta, A., Riccucci, P., Daniele, M., Traverso, P., Giunchiglia, E., Piaggio, M., Shaerf, M.: Jerry: a system for the automatic generation and execution of plans for robotic devices - the case study of the Spider arm. In: Proc. of ISAIRAS 1999 (1999)
Chen, X.J., de Giacomo, G.: Reasoning about nondeterministic and concurrent actions: A process algebra approach. Artificial Intelligence 107(1), 29–62 (1999)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSmv: a reimplementation of smv. Technical Report 9801-06, IRST, Trento, Italy (January 1998)
Cimatti, A., Giunchiglia, E., Giunchiglia, F., Traverso, P.: Planning via Model Checking: A Decision Procedure for AR. In: ECP 1997, pp. 130–142 (1997)
Cimatti, A., Roveri, M.: Conformant Planning via Model Checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809. Springer, Heidelberg (2000)
Cimatti, A., Roveri, M., Traverso, P.: Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains. In: Proc. of AAAI 1998 (1998)
Cimatti, A., Roveri, M., Traverso, P.: Strong Planning in Non-Deterministic Domains via Model Checking. In: Proc. of AIPS 1998 (1998)
Daniele, M., Traverso, P., Vardi, M.Y.: Strong Cyclic Planning Revisited. Technical Report 9908-03, IRST, Trento, Italy (August 1999)
de Giacomo, G., Vardi, M.Y.: Automata-theoretic approach to planning with temporally extended goals. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809. Springer, Heidelberg (2000)
Dean, T., Kaelbling, L., Kirman, J., Nicholson, A.: Planning Under Time Constraints in Stochastic Domains. Artificial Intelligence 76(1-2), 35–74 (1995)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Hand book of Theoretical Computer Science. Formal Models and Semantics, ch. 16, Vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
Ernst, M., Millstein, T., Weld, D.: Automatic SAT-compilation of planning problems. In: Proc. of IJCAI 1997 (1997)
Fikes, R.E., Nilsson, N.J.: STRIPS: A new approach to the application of Theorem Proving to Problem Solving. Artificial Intelligence 2(3-4), 189–208 (1971)
Giunchiglia, E., Kartha, G.N., Lifschitz, V.: Representing action: Indeterminacy and ramifications. Artificial Intelligence 95(2), 409–438 (1997)
Giunchiglia, F., Traverso, P.: Planning as Model Checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809. Springer, Heidelberg (2000)
Goldman, R., Musliner, D., Krebsbach, K., Boddy, M.: Dynamic Abstraction Planning. In: Proc. of AAAI 1997 (1998)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Proc. of 2nd International Conference on Temporal Logic, pp. 91–106 (1997)
Penberthy, J., Weld, D.: UCPOP: A sound, complete, partial order planner for ADL. In: Proc. of KR 1992 (1992)
Schoppers, M.J.: Universal plans for Reactive Robots in Unpredictable Environments. In: Proc. of IJCAI 1987, pp. 1039–1046 (1987)
Smith, D., Weld, D.: Conformant Graphplan. In: AAAI 1998, pp. 889–896 (1998)
Steel, S.: Action under Uncertainty. J. of Logic and Computation, Special Issue on Action and Processes 4(5), 777–795 (1994)
Stephan, W., Biundo, S.: A New Logical Framework for Deductive Planning. In: Proc. of IJCAI 1993, pp. 32–38 (1993)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Weld, D., Anderson, C., Smith, D.: Extending Graphplan to Handle Uncertaintyand Sensing Actions. In: Proc. of AAAI 1998, pp. 897–904 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Daniele, M., Traverso, P., Vardi, M.Y. (2000). Strong Cyclic Planning Revisited. In: Biundo, S., Fox, M. (eds) Recent Advances in AI Planning. ECP 1999. Lecture Notes in Computer Science(), vol 1809. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720246_3
Download citation
DOI: https://doi.org/10.1007/10720246_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67866-3
Online ISBN: 978-3-540-44657-6
eBook Packages: Springer Book Archive