Reasoning about actions with loops via Hoare logic

Abstract

Plans with loops are more general and compact than classical sequential plans, and gaining increasing attentions in artificial intelligence (AI). While many existing approaches mainly focus on algorithmic issues, few work has been devoted to the semantic foundations on planning with loops. In this paper, we first develop a tailored action language {\mathfrak{A}}_K^L, together with two semantics for handling domains with non-deterministic actions and loops. Then we propose a sound and (relative) complete Hoare-style proof system for efficient plan generation and verification under 0- approximation semantics, which uses the so-called idea offline planning and on-line querying strategy in knowledge compilation, i.e., the agent could generate and store short proofs as many as possible in the spare time, and then perform quick query by constructing a long proof from the stored shorter proofs using compositional rule. We argue that both our semantics and proof system could serve as logical foundations for reasoning about actions with loops.

Keywords

action language / plan generation / plan verification / loop-plan / Hoare logic

References

[1] Gelfond M, Lifschitz V. Representing action and change by logic programs. Journal of Logic Programming, 1993, 17(2–4): 301–322

[2] Son T C, Baral C. Formalizing sensing actions—a transition function based approach. Artificial Intelligence, 2001, 125(1–2): 19–91

[3] Tu P H, Son T C, Baral C. Reasoning and planning with sensing actions, incomplete information, and static laws using answering set programming. Theory and Practice of Logic Programming, 2007, 7(4): 377–450

[4] Giunchiglia E, Kartha G N, Lifschitz V. Representing action: indeterminacy and ramifications. Artificial Intelligence, 1997, 95(2): 409–438

[5] Boutilier C, Friedman N. Nondeterministic actions and the frame problem. AAAI Spring Symposium on Extending Theories of Actions, 1995, 39–44

[6] De Giacomo G, Patrizi F, Sardina S. Generalized planning with loops under strong fairness constraints. In: Proceedings of KR’10. 2010, 351–361

[7] Srivastava S, Immerman N, Zilberstein S. Applicability conditions forplans with loops: computability results and algorithms. Artificial Intelligence, 2012, 191: 1–19

[8] Alford R, Kuter U, Nau D, Goldman R P. Plan aggregation for strong cyclic planning in nondeterministic domains. Artificial Intelligence, 2014, 216: 206–232

[9] Lespérance Y, Levesque H J, Lin F Z, Scher R Bl. Ability and knowing how in the situation calculus. Studia Logica, 2000, 66(1): 165–186

[10] Sardina S, De Giacomo G, Lespèrance Y, Levesque H J. On the semantics of deliberation in IndiGolog—from theory to implementation. Annals of Mathematics and Artificial Intelligence, 2004, 41(2–4): 259–299

[11] Amir E. Planning with nondeterministic actions and sensing. In: Proceedings of AAAI-02 Workshop on Cognitive Robotics. 2002

[12] Ghallab M, Nau D, Traverso P. Automated Planning: Theory and Practice. San Francisco: Morgan Kaufmann Publisher, 2004

[13] Pontelli E, Son T C, Baral C, Gelfond G. Answer set programming and planning with knowledge and world-altering actions in multiple agent domains. Correct Reasoning, 2012, 7265, 509–526

[14] Dimopoulos Y, Hashmi M A, Moraitis P. μ-satplan: multi-agent planning as satisfiability. Knowledge-Based Systems, 2010, 29, 54–62

[15] Otwell C, Remshagen A, Truemper K. An effective QBF solver for planning problems. MSV/AMCS, 2004, 311–316

[16] Turban E, Aronson J E, Liang T P. Decision Support Systems and Intelligent Systems. 7th Edtion. New Jersey: Prentice-Hall, 2004

[17] Lin F Z, Shoham Y. Provably correct theories of action. Journal of the ACM, 1995, 42(2): 293–320

[18] Reiter R. Knowledge in Action: Logical Foundation for Specifying and Implementing Dynamical Systems. Cambrige, Massachuesstts and London, England: The MIT Press, 2001

[19] Yoo C, Fitch R, Sukkarieh S. Provably-correct stochastic motion planning with safety constraints. In: Proceedings of 2013 IEEE International Conference on Robotics and Automation. 2013, 981–986

[20] Quottrup M M, Bak T, Zamanabadi R I. Multi-robot motion planning: atimed automata approach. In: Proceedings of IEEE International Conference on Robotics and Automation. 2004, 4417–4422

[21] Baral C, Kreinovich V, Trejo R. Computational complexity of planning and approximate planning in the presence of incompleteness. Artificial Intelligence, 200, 122(1–2): 241–267

[22] Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576–580

[23] Apt K R, de Boer F S, Olderog E. Verification of Sequential and Concurrent Programs. London: Springer-Verlag, 2009

[24] Sipser M. Introduction to the Theory of Computation. 3rd Edition. Boston, MA: Cengage Learning, 2012

[25] Selman B, Kautz H. Knowledge compilation and theory approximation. Journal of the ACM, 1996, 43(2): 193–224

[26] Cadoli M, Donini F M. A survey on knowledge compilation. AI Communication, 1997, 10(3–4): 137–150

[27] Darwiche A, Marquis P. A knowledge compilation map. Journal of Artificial Intelligence Research, 2002, 17(1): 229–264

[28] Shen Y P, Zhao X S. Proof systems for planning under cautious semantics. Minds and Machines, 2013, 23(1): 5–45

[29] Shen Y P, Zhao X S. Proof systems for planning under 0-approximation semantics. Science China Information Sciences, 2014, 57, 1–12

[30] Malinowski G. Many-valued logic. In Goble L ed. The Blackwell Guide to Philosophical Logic, New York: Wiley-Blackwell, 2001, 309–335

[31] Priest G. An Introduction to Non-Classical Logic. 2nd Edition. Cambridge: Cambridge University Press, 2008

[32] Cimatti A, Pistore M, Roveri M, Traverso P. Weak, strong, and strong cyclic planning via symbolic model checking. Artificial Intelligence, 2003, 147(1): 35–84

[33] Fu J C, Ng V, Bastani F B, Yen I L. Simple and fast strong cyclic planning for fully-observable nondeterministic planning problems. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence.2011

[34] van Harmelen F, Lifschitz V, Porter B. Handbook of Knowledge Representation. Amsterdam: Elsevier Science, 2008

[35] Apt K R. Ten years of Hoare’s logic: a survey—part I. ACM Transaction on Programming Languages and Systems, 1981, 3(4): 431–483

[36] Cook S A. Soundness and completeness of an axiom system for program verification. AIAM Journal of Computing, 1987, 7(1): 70–90

[37] Lobo J, Mendez G, Taylor S R. Knowledge and the action description language A. Theory and Practice of Logic Programming, 2001, 1(2): 129–184

[38] Gelfond M. Logic programming and reasoning with incomplete information. Annals of Mathematics and Artificial Intelligence, 1994, 12, 98–116

[39] Zhang Y. Computational properties of epistemic logic programs. In: Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning. 2006, 308–317

[40] Levesque H J. Planning with loops. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI-05). 2005, 509–515

[41] Srivastava S, Immerman N, Zilberstein S. A new representation and associated algorithms for generalized planning. Artificial Intelligence, 2011, 175(2): 615–647

[42] Winner E Z, Veloso M. Loopdistill: learning domain-specific planners from example plans. In: Proceedings of ICAPS-07 Workshopon AI Planning and Learning. 2007

[43] Slonneger K, Kurtz B L. Formal Syntax and Semantics of Programming Languages. New York: Addison Wesley Longman, 1995

[44] Lifschitz V. On the semantics of STRIPS. In George M P, Lansky A, <Eds/>. Reasoning about Actions and Plans. Los Altos, CA: MorganKaufmann, 1987

[45] Fikes R E, Nilsson N J. STRIPS, a retrospective. Artificial Intelligence, 1993, 59(1–2): 227–232

[46] van der Hoek W. Logical foundation of agent-based computing. In: Luck M. <Eds/>. Multi-Agent Systems and Applications. New York: Springer Berlin Heidelberg, 2001

[47] Nipkow T. Hoare logics in Isabelle/HOL. In: Schwichtenberg H, Steinbrüggen R, <Eds/>. Proof and System-Reliability. Kluwer Academic Publisher, 2002

RIGHTS & PERMISSIONS

2016 Higher Education Press and Springer-Verlag Berlin Heidelberg