20 Years of Planning via Model Checking: From Theory to Practice

Planning via Model Checking is nowadays a well-known technique. Techniques based on model checking have been successfully applied for dealing with different kinds of planning problems. In classical planning domains, LTL based model checking has been used to guide the search towards the goal. Classical planners based on BDDs have participated to the international planning competition since its early editions. Techniques based on both explicit state and symbolic model checking have been used to address the problem of planning under uncertainty, including planning with full observability in non-deterministic domains (FOND), planning with partial observability (POND), conformant planning, and planning in non-deterministic domains with temporally extended LTL and CTL goals. Techniques for interleaving planning via model checking and partial plan execution have been explored. Model checking techniques have also been used for planning with preferences, and planning in asynchronous domains. Recently, planning via model checking has been successfully applied to hybrid systems. In my talk, I will review some of the different approaches in planning via model checking. I will then discuss some applications in different domains, e.g., applications for safety critical systems, web services and business processes, the dynamic management of harbor facilities, and planning for services in the field of smart cities and communities. I will discuss some lessons learned and some future challenges for the practical application of planning via model checking.