Advertisement

Proof-Carrying Plans

  • Christopher Schwaab
  • Ekaterina Komendantskaya
  • Alasdair HillEmail author
  • František Farka
  • Ronald P. A. Petrick
  • Joe Wells
  • Kevin Hammond
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11372)

Abstract

It is becoming increasingly important to verify safety and security of AI applications. While declarative languages (of the kind found in automated planners and model checkers) are traditionally used for verifying AI systems, a big challenge is to design methods that generate verified executable programs. A good example of such a “verification to implementation” cycle is given by automated planning languages like PDDL, where plans are found via a model search in a declarative language, but then interpreted or compiled into executable code in an imperative language. In this paper, we show that this method can itself be verified. We present a formal framework and a prototype Agda implementation that represent PDDL plans as executable functions that inhabit types that are given by formulae describing planning problems. By exploiting the well-known Curry-Howard correspondence, type-checking then automatically ensures that the generated program corresponds precisely to the specification of the planning problem.

Keywords

AI planning Curry-Howard correspondence Constructive logic Verification Dependent types 

Notes

Acknowledgements

This research has been generously supported by EPSRC Platform Grant EP/N014758/1 “The Integration and Interaction of Multiple Mathematical Reasoning Processes”, EPSRC Doctoral Training Partnership, EPSRC grant EP/PP020631 “Discovery: Pattern Discovery and Program Shaping for Manycore Systems”, and by EU Horizon 2020 grant ICT-779882 “TeamPlay: Time, Energy and security Analysis for Multi/Many-core heterogenous PLAtforms”.

References

  1. 1.
    Claßen, J., Eyerich, P., Lakemeyer, G., Nebel, B.: Towards an integration of Golog and planning. In: Veloso, M.M. (ed.) IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, 6–12 January 2007, pp. 1846–1851 (2007)Google Scholar
  2. 2.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  3. 3.
    Dutertre, B., De Moura, L.: The Yices SMT solver. Technical report, August 2006. Tool paper at http://yices.csl.sri.com/tool-paper.pdf
  4. 4.
    Fikes, R., Nilsson, N.J.: STRIPS: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3/4), 189–208 (1971)CrossRefGoogle Scholar
  5. 5.
    Fourati, F., Bhiri, M.T., Robbana, R.: Verification and validation of PDDL descriptions using Event-B formal method. In: 2016 5th International Conference on Multimedia Computing and Systems (ICMCS), pp. 770–776, September 2016Google Scholar
  6. 6.
    Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in horn clause logic. Formal Asp. Comput. 29(3), 453–474 (2017)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A.: Proof relevant corecursive resolution. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 126–143. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-29604-3_9CrossRefGoogle Scholar
  8. 8.
    Howey, R., Long, D., Fox, M.: VAL: automatic plan validation, continuous effects and mixed initiative planning using PDDL. In: 16th IEEE International Conference on Tools with Artificial Intelligence, pp. 294–301 (2004)Google Scholar
  9. 9.
    Khatib, L., Muscettola, N., Havelund, K.: Verification of plan models using UPPAAL. In: Rash, J.L., Truszkowski, W., Hinchey, M.G., Rouff, C.A., Gordon, D. (eds.) FAABS 2000. LNCS, vol. 1871, pp. 114–122. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45484-5_9CrossRefGoogle Scholar
  10. 10.
    Levesque, H.J., Reiter, R., Lespérance, Y., Lin, F., Scherl, R.B.: GOLOG: a logic programming language for dynamic domains. J. Logic Program. 31(1), 59–83 (1997)MathSciNetCrossRefGoogle Scholar
  11. 11.
    McDermott, D., et al.: PDDL - The Planning Domain Definition Language (Version 1. 2). Technical Report CVC TR-98-003/DCS TR-1165, Yale Center for Computational Vision and Control (1998)Google Scholar
  12. 12.
    Necula, G.C.: Proof-carrying code. In: POPL, pp. 106–119 (1997)Google Scholar
  13. 13.
    Ong, L.: Higher-order model checking: an overview. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6–10 July 2015, pp. 1–15 (2015)Google Scholar
  14. 14.
    Raimondi, F., Pecheur, C., Brat, G.: PDVer, a tool to verify PDDL planning domains. In: ICAPS 2009 Workshop on Verification and Validation of Planning and Scheduling Systems, Thessaloniki, Greece, 20 September 2009Google Scholar
  15. 15.
    Reiter, R.: On closed world data bases. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 55–76. Plenum Press, New York (1978)CrossRefGoogle Scholar
  16. 16.
    Schubert, A., Urzyczyn, P.: Answer set programming in intuitionistic logic. Indagationes Mathematicae 29(1), 276–292 (2018). l.E.J. Brouwer, fifty years laterMathSciNetCrossRefGoogle Scholar
  17. 17.
    Scwaab, C., Hill, A., Farka, F., Komendantskaya, E.: Proof-Carrying Plans: Agda Implementation and Examples (2018). https://github.com/PDTypes
  18. 18.
    Scwaab, C., et al.: Proof-Carrying Plans: Extended Version of This Paper with Appendices (2018). https://github.com/PDTypes/PADL19/blob/master/padl-pddl-verification.pdf
  19. 19.
    Sorensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism, Studies in Logic, vol. 149. Elsevier, New York (2006)zbMATHGoogle Scholar
  20. 20.
    Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)CrossRefGoogle Scholar
  21. 21.
    Waldinger, R.J.: Achieving several goals simultaneously. Machine Intelligence 8 (1977)Google Scholar
  22. 22.
    Zarrieß, B., Claßen, J.: Decidable verification of GOLOG programs over non-local effect actions. In: Schuurmans, D., Wellman, M.P. (eds.) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, Arizona, USA, 12–17 February 2016, pp. 1109–1115. AAAI Press (2016)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Christopher Schwaab
    • 1
  • Ekaterina Komendantskaya
    • 2
  • Alasdair Hill
    • 2
    Email author
  • František Farka
    • 1
    • 2
  • Ronald P. A. Petrick
    • 2
  • Joe Wells
    • 2
  • Kevin Hammond
    • 1
  1. 1.School of Computer ScienceUniversity of St AndrewsSt AndrewsUK
  2. 2.Department of Computer ScienceHeriot-Watt UniversityEdinburghUK

Personalised recommendations