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.
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
References
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)
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_24
Dutertre, B., De Moura, L.: The Yices SMT solver. Technical report, August 2006. Tool paper at http://yices.csl.sri.com/tool-paper.pdf
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)
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 2016
Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in horn clause logic. Formal Asp. Comput. 29(3), 453–474 (2017)
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_9
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)
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_9
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)
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)
Necula, G.C.: Proof-carrying code. In: POPL, pp. 106–119 (1997)
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)
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 2009
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)
Schubert, A., Urzyczyn, P.: Answer set programming in intuitionistic logic. Indagationes Mathematicae 29(1), 276–292 (2018). l.E.J. Brouwer, fifty years later
Scwaab, C., Hill, A., Farka, F., Komendantskaya, E.: Proof-Carrying Plans: Agda Implementation and Examples (2018). https://github.com/PDTypes
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
Sorensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism, Studies in Logic, vol. 149. Elsevier, New York (2006)
Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)
Waldinger, R.J.: Achieving several goals simultaneously. Machine Intelligence 8 (1977)
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)
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”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Schwaab, C. et al. (2019). Proof-Carrying Plans. In: Alferes, J., Johansson, M. (eds) Practical Aspects of Declarative Languages. PADL 2019. Lecture Notes in Computer Science(), vol 11372. Springer, Cham. https://doi.org/10.1007/978-3-030-05998-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-05998-9_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-05997-2
Online ISBN: 978-3-030-05998-9
eBook Packages: Computer ScienceComputer Science (R0)