|
|
|
Reasoning about actions with loops via Hoare logic |
Jiankun HE,Xishun ZHAO( ) |
| Institute of Logic and Cognition, Sun Yat-sen University, Guangzhou 512075, China |
|
|
|
|
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 AKL, 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
|
|
Corresponding Author(s):
Xishun ZHAO
|
|
Just Accepted Date: 10 December 2015
Online First Date: 12 June 2016
Issue Date: 07 September 2016
|
|
| 1 |
Gelfond M, Lifschitz V. Representing action and change by logic programs. Journal of Logic Programming, 1993, 17(2–4): 301–322
https://doi.org/10.1016/0743-1066(93)90035-F
|
| 2 |
Son T C, Baral C. Formalizing sensing actions—a transition function based approach. Artificial Intelligence, 2001, 125(1–2): 19–91
https://doi.org/10.1016/S0004-3702(00)00080-1
|
| 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
https://doi.org/10.1017/S1471068406002948
|
| 4 |
Giunchiglia E, Kartha G N, Lifschitz V. Representing action: indeterminacy and ramifications. Artificial Intelligence, 1997, 95(2): 409–438
https://doi.org/10.1016/S0004-3702(97)00037-4
|
| 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
https://doi.org/10.1016/j.artint.2012.07.005
|
| 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
https://doi.org/10.1016/j.artint.2014.07.007
|
| 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
https://doi.org/10.1023/A:1026761331498
|
| 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
https://doi.org/10.1023/B:AMAI.0000031197.13122.aa
|
| 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
https://doi.org/10.1007/978-3-642-30743-0_35
|
| 14 |
Dimopoulos Y, Hashmi M A, Moraitis P. μ-satplan: multi-agent planning as satisfiability. Knowledge-Based Systems, 2010, 29, 54–62
https://doi.org/10.1016/j.knosys.2011.07.019
|
| 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
https://doi.org/10.1145/201019.201021
|
| 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
https://doi.org/10.1109/ICRA.2013.6630692
|
| 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
https://doi.org/10.1145/363235.363259
|
| 23 |
Apt K R, de Boer F S, Olderog E. Verification of Sequential and Concurrent Programs. London: Springer-Verlag, 2009
https://doi.org/10.1007/978-1-84882-745-5
|
| 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
https://doi.org/10.1145/226643.226644
|
| 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
https://doi.org/10.1007/s11023-012-9288-9
|
| 29 |
Shen Y P, Zhao X S. Proof systems for planning under 0-approximation semantics. Science China Information Sciences, 2014, 57, 1–12
https://doi.org/10.1007/s11432-012-4668-6
|
| 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
https://doi.org/10.1017/CBO9780511801174
|
| 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
https://doi.org/10.1016/S0004-3702(02)00374-0
|
| 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
https://doi.org/10.1145/357146.357150
|
| 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
https://doi.org/10.1007/BF01530762
|
| 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
https://doi.org/10.1016/j.artint.2010.10.006
|
| 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
https://doi.org/10.1016/B978-0-934613-30-9.50004-4
|
| 45 |
Fikes R E, Nilsson N J. STRIPS, a retrospective. Artificial Intelligence, 1993, 59(1–2): 227–232
https://doi.org/10.1016/0004-3702(93)90190-M
|
| 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
https://doi.org/10.1007/3-540-47745-4_3
|
| 47 |
Nipkow T. Hoare logics in Isabelle/HOL. In: Schwichtenberg H, Steinbrüggen R, <Eds/>. Proof and System-Reliability. Kluwer Academic Publisher, 2002
https://doi.org/10.1007/978-94-010-0413-8_11
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
