Tertia Hörne
ABSTRACT
In this paper we investigate the feasibility of using two different model-checking techniques for solving a number of classical AI planning problems. The ProB model checker, based on mathematical set theory and first-order logic, is specifically designed to validate specifications of concurrent programs written in the B specification language. ProB uses a constraint logic programming environment to perform model checking. NuSMV is the other model checker used in this work. It is an extension of SMV and makes use of symbolic model checking techniques to deal with the state explosion problem common to model checking in general. The problem is represented using Binary Decision Diagrams and model checking is performed using tableaux theorem proving techniques. The scope of the problems chosen is currently limited but it is envisaged that the methodology proposed could usefully be extended to larger planning problems.
- Abrial, J.-R. 1996. The B-Book: Assigning programs to meanings. Cambridge University Press. Google Scholar
Digital Library
- Ben-Ari, M. 2001. Mathematical logic for Computer Science, 2 ed. Springer. Google ScholarDigital Library
- Bratko, I. 2001. Prolog Programming for Artificial Intelligence, 3 ed. Addison-Wesley. Google ScholarDigital Library
- Bryant, R. 1992. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24, 3, 142--170. Google ScholarDigital Library
- Butler, M. and Leuschel, M. 2005. Combining CSP and B for Specification and Property Verification. In International Symposium of Formal Methods Europe, J. Fitzgerald, I. Hayes, and A. Tarlecki, Eds. Lecture Notes in Computer Science, vol. 3582. Springer, Heidelberg, 221--236.Google Scholar
- Cavada, R. 2008. Private email communication.Google Scholar
- Cavada, R., Cimatti, A., Jochim, C., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., and Tchaltsev, A. 2005. NuSMV 2.4 User Manual. CMU and ITC-irst.Google Scholar
- Cimatti, A. and Roveri, M. 2000. Conformant Planning vis Symbolic Model Cheking. Tech. rep., ITC-irst, Trento, Italy. Technical Report 0006--04.Google Scholar
- Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press. Google ScholarDigital Library
- Daniele, M., Traverso, P., and Vardi, M. 2000. Strong cyclic planning revisited. In Recent Advances in AI Planning. Springer, Heidelberg, 35--48. Google ScholarDigital Library
- Davis, M. and Putnam, H. 1960. A Computing Procedure for Quantification Theory. Journal of the ACM 7, 1, 201--215. Google ScholarDigital Library
- Enderton, H. 1977. Elements of Set Theory. Academic Press, Inc.Google Scholar
- Fitting, M. 1996. First-Order Logic and Automated Theorem Proving, 2 ed. Springer. Google ScholarDigital Library
- Formal Systems Europe Ltd. Failures-Divergence Refinement - FDR User Manual.Google Scholar
- Giunchiglia, F. and Traverso, P. 1999. Planning as Model Checking. In Recent advances in AI Planning. Lecture Notes in Artificial Intelligence, vol. 1809. Springer. Google ScholarDigital Library
- Giunchiglia, F. and Traverso, P. 2000. A partial order approach to branching time temporal logic model checking. In Proceedings of the 5th European Conference on Planning. Recent Advances in AI Planning. Springer.Google Scholar
- Hoare, C. 1985. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Holzmann, G. 1997. The model checker SPIN. IEEE Transactions on Software Engineering 23, 5, 279--295. Google ScholarDigital Library
- Leuschel, M. and Butler, M. 2003. ProB: A model checker for B. In FME 2003: Formal Methods. Lecture Notes in Computer Science, vol. 2805. Springer, Heidelberg, 855--874.Google Scholar
- Leuschel, M., Butler, M., and Presti, S. L. 2005. ProB User Manual. University of Southampton, UK.Google Scholar
- Leuschel, M., Massart, T., and Currie, A. 2001. How to Make FDR Spin: LTL Model Checking of CSP by Refinement. In International Symposium of Formal Methods Europe. Lecture Notes in Computer Science, vol. 2021. Springer, 99--118. Google ScholarDigital Library
- Manzo, M. D., Giunchiglia, E., and Ruffino, S. 1999. Planning via Model Checking in Deterministic Domains: Preliminary Report. In Proceedings of the AIMSA '98 Conference. Number 1480 in Lecture Notes in Artificial Intelligence. Springer, Heidelberg, 221--229.Google Scholar
- Marinagi, C., Panayiotopoulos, T., and Spyropoulos, C. 2005. AI Planning and Intelligent Agents. Idea Group Inc., 225--257.Google Scholar
- McMillan, K. 1992. Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. thesis, Carnegie Mellon University. Google ScholarDigital Library
- McMillan, K. 1993. Symbolic Model Checking. Kluwer Academic Press, Massachusetts. Google ScholarDigital Library
- Pistore, M. and Traverso, P. 2000. Planning as Model Checking for Extended Goals in Non-deterministic Domains. Tech. rep., ICT-irst, Trento, Italy. Technical Report 0101-03.Google Scholar
- Tatibouet, B. 2001. The JBTools Package. Available at http://lifc.univfcomte.fr/PEOPLE/tatibouet/JBTOOLS/BParseren.html.Google Scholar
- Wallace, M. 1998. Constraint Programming. CRC Press LLC, 17.1--17.17.Google Scholar
- Wordsworth, J. 1996. Software Engineering with B. Addison-Wesley. Google ScholarDigital Library
Index Terms
- Planning as model checking: the performance of ProB vs NuSMV
Recommendations
Model checking: recent improvements and applications
Model checking (Baier and Katoen in Principles of model checking, MIT Press, Cambridge, 2008; Clarke et al. in Model checking, MIT Press, Cambridge, 2001) is an automatic technique to formally verify that a given specification of a concurrent system ...
Combining Theorem Proving with Model Checking through Predicate Abstraction
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software EngineeringSoftware model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
Comments