{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:33:36Z","timestamp":1750307616726,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,10,6]],"date-time":"2008-10-06T00:00:00Z","timestamp":1223251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,10,6]]},"DOI":"10.1145\/1456659.1456673","type":"proceedings-article","created":{"date-parts":[[2008,11,6]],"date-time":"2008-11-06T13:49:50Z","timestamp":1225979390000},"page":"114-123","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Planning as model checking"],"prefix":"10.1145","author":[{"given":"Tertia","family":"H\u00f6rne","sequence":"first","affiliation":[{"name":"University of South Africa"}]},{"given":"John A.","family":"van der Poll","sequence":"additional","affiliation":[{"name":"University of South Africa"}]}],"member":"320","published-online":{"date-parts":[[2008,10,6]]},"reference":[{"volume-title":"The B-Book: Assigning programs to meanings","author":"Abrial J.-R.","key":"e_1_3_2_1_1_1","unstructured":"Abrial , J.-R. 1996. The B-Book: Assigning programs to meanings . Cambridge University Press . Abrial, J.-R. 1996. The B-Book: Assigning programs to meanings. Cambridge University Press."},{"volume-title":"Mathematical logic for Computer Science, 2 ed","author":"Ben-Ari M.","key":"e_1_3_2_1_2_1","unstructured":"Ben-Ari , M. 2001. Mathematical logic for Computer Science, 2 ed . Springer . Ben-Ari, M. 2001. Mathematical logic for Computer Science, 2 ed. Springer."},{"volume-title":"Prolog Programming for Artificial Intelligence, 3 ed","author":"Bratko I.","key":"e_1_3_2_1_3_1","unstructured":"Bratko , I. 2001. Prolog Programming for Artificial Intelligence, 3 ed . Addison-Wesley . Bratko, I. 2001. Prolog Programming for Artificial Intelligence, 3 ed. Addison-Wesley."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_3_2_1_5_1","volume-title":"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","volume":"3582","author":"Butler M.","unstructured":"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. 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."},{"key":"e_1_3_2_1_6_1","unstructured":"Cavada R. 2008. Private email communication.  Cavada R. 2008. Private email communication."},{"key":"e_1_3_2_1_7_1","unstructured":"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.  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."},{"key":"e_1_3_2_1_8_1","volume-title":"Technical Report 0006--04.","author":"Cimatti A.","year":"2000","unstructured":"Cimatti , A. and Roveri , M . 2000 . Conformant Planning vis Symbolic Model Cheking. Tech. rep., ITC-irst, Trento, Italy . Technical Report 0006--04. Cimatti, A. and Roveri, M. 2000. Conformant Planning vis Symbolic Model Cheking. Tech. rep., ITC-irst, Trento, Italy. Technical Report 0006--04."},{"key":"e_1_3_2_1_9_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.   Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Daniele M. Traverso P. and Vardi M. 2000. Strong cyclic planning revisited. In Recent Advances in AI Planning. Springer Heidelberg 35--48.   Daniele M. Traverso P. and Vardi M. 2000. Strong cyclic planning revisited. In Recent Advances in AI Planning. Springer Heidelberg 35--48.","DOI":"10.1007\/10720246_3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"volume-title":"Elements of Set Theory","author":"Enderton H.","key":"e_1_3_2_1_12_1","unstructured":"Enderton , H. 1977. Elements of Set Theory . Academic Press, Inc. Enderton, H. 1977. Elements of Set Theory. Academic Press, Inc."},{"volume-title":"First-Order Logic and Automated Theorem Proving, 2 ed","author":"Fitting M.","key":"e_1_3_2_1_13_1","unstructured":"Fitting , M. 1996. First-Order Logic and Automated Theorem Proving, 2 ed . Springer . Fitting, M. 1996. First-Order Logic and Automated Theorem Proving, 2 ed. Springer."},{"key":"e_1_3_2_1_14_1","unstructured":"Formal Systems Europe Ltd. Failures-Divergence Refinement - FDR User Manual.  Formal Systems Europe Ltd. Failures-Divergence Refinement - FDR User Manual."},{"key":"e_1_3_2_1_15_1","volume-title":"Lecture Notes in Artificial Intelligence","volume":"1809","author":"Giunchiglia F.","unstructured":"Giunchiglia , F. and Traverso , P . 1999. Planning as Model Checking. In Recent advances in AI Planning . Lecture Notes in Artificial Intelligence , vol. 1809 . Springer. Giunchiglia, F. and Traverso, P. 1999. Planning as Model Checking. In Recent advances in AI Planning. Lecture Notes in Artificial Intelligence, vol. 1809. Springer."},{"volume-title":"Proceedings of the 5th European Conference on Planning. Recent Advances in AI Planning. Springer.","author":"Giunchiglia F.","key":"e_1_3_2_1_16_1","unstructured":"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. 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."},{"volume-title":"Communicating Sequential Processes","author":"Hoare C.","key":"e_1_3_2_1_17_1","unstructured":"Hoare , C. 1985. Communicating Sequential Processes . Prentice-Hall , Englewood Cliffs, NJ . Hoare, C. 1985. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_19_1","volume-title":"FME 2003: Formal Methods. Lecture Notes in Computer Science","volume":"2805","author":"Leuschel M.","unstructured":"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. 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."},{"key":"e_1_3_2_1_20_1","unstructured":"Leuschel M. Butler M. and Presti S. L. 2005. ProB User Manual. University of Southampton UK.  Leuschel M. Butler M. and Presti S. L. 2005. ProB User Manual. University of Southampton UK."},{"key":"e_1_3_2_1_21_1","volume-title":"International Symposium of Formal Methods Europe. Lecture Notes in Computer Science","volume":"2021","author":"Leuschel M.","unstructured":"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. 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."},{"key":"e_1_3_2_1_22_1","volume-title":"Deterministic Domains: Preliminary Report. In Proceedings of the AIMSA '98 Conference. Number 1480 in Lecture Notes in Artificial Intelligence","author":"Manzo M. D.","year":"1999","unstructured":"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. 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."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Marinagi C. Panayiotopoulos T. and Spyropoulos C. 2005. AI Planning and Intelligent Agents. Idea Group Inc. 225--257.  Marinagi C. Panayiotopoulos T. and Spyropoulos C. 2005. AI Planning and Intelligent Agents. Idea Group Inc. 225--257.","DOI":"10.4018\/978-1-59140-450-7.ch007"},{"volume-title":"Symbolic Model Checking","author":"McMillan K.","key":"e_1_3_2_1_25_1","unstructured":"McMillan , K. 1993. Symbolic Model Checking . Kluwer Academic Press , Massachusetts . McMillan, K. 1993. Symbolic Model Checking. Kluwer Academic Press, Massachusetts."},{"key":"e_1_3_2_1_26_1","volume-title":"Technical Report 0101-03.","author":"Pistore M.","year":"2000","unstructured":"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. 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."},{"key":"e_1_3_2_1_27_1","unstructured":"Tatibouet B. 2001. The JBTools Package. Available at http:\/\/lifc.univfcomte.fr\/PEOPLE\/tatibouet\/JBTOOLS\/BParseren.html.  Tatibouet B. 2001. The JBTools Package. Available at http:\/\/lifc.univfcomte.fr\/PEOPLE\/tatibouet\/JBTOOLS\/BParseren.html."},{"volume-title":"Constraint Programming","author":"Wallace M.","key":"e_1_3_2_1_28_1","unstructured":"Wallace , M. 1998. Constraint Programming . CRC Press LLC , 17.1--17.17. Wallace, M. 1998. Constraint Programming. CRC Press LLC, 17.1--17.17."},{"volume-title":"Software Engineering with B","author":"Wordsworth J.","key":"e_1_3_2_1_29_1","unstructured":"Wordsworth , J. 1996. Software Engineering with B . Addison-Wesley . Wordsworth, J. 1996. Software Engineering with B. Addison-Wesley."}],"event":{"name":"SAICSIT '08: 2008 Annual Conference of the South African Institute of Computer Scientists and Information Technologists","sponsor":["Microsoft Microsoft"],"location":"Wilderness South Africa","acronym":"SAICSIT '08"},"container-title":["Proceedings of the 2008 annual research conference of the South African Institute of Computer Scientists and Information Technologists on IT research in developing countries: riding the wave of technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1456659.1456673","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1456659.1456673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:45:45Z","timestamp":1750250745000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1456659.1456673"}},"subtitle":["the performance of ProB vs NuSMV"],"short-title":[],"issued":{"date-parts":[[2008,10,6]]},"references-count":28,"alternative-id":["10.1145\/1456659.1456673","10.1145\/1456659"],"URL":"https:\/\/doi.org\/10.1145\/1456659.1456673","relation":{},"subject":[],"published":{"date-parts":[[2008,10,6]]},"assertion":[{"value":"2008-10-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}