In this paper we propose a new approach to planning based on a "high level action language", called AR, and "model checking". AR is an expressive formalism which is able to handle, among other things, ramifications and non-deterministic effects. We define a decision procedure for planning in AR which is based on "symbolic model checking", a technique which has been successfully applied in hardware and software verification. The decision procedure always terminates with an optimal solution or with failure if no solution exists. We have constructed a planner, called mbp, which implements the decision procedure.
CITATION STYLE
Cimatti, A., Giunchiglia, E., Giunchiglia, F., & Traverso, P. (1997). Planning via model checking: A decision procedure for AR. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1348 LNAI, pp. 130–142). Springer Verlag. https://doi.org/10.1007/3-540-63912-8_81
Mendeley helps you to discover research relevant for your work.