{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:30:25Z","timestamp":1743071425081,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642004308"},{"type":"electronic","value":"9783642004315"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00431-5_9","type":"book-chapter","created":{"date-parts":[[2009,2,24]],"date-time":"2009-02-24T06:14:35Z","timestamp":1235456075000},"page":"132-146","source":"Crossref","is-referenced-by-count":2,"title":["Experimental Evaluation of a Planning Language Suitable for Formal Verification"],"prefix":"10.1007","author":[{"given":"Radu I.","family":"Siminiceanu","sequence":"first","affiliation":[]},{"given":"Rick W.","family":"Butler","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Allen, J.F., Ferguson, G.: Actions and Events in Interval Temporal Logic. Technical Report TR521, University of Rochester (1994)","DOI":"10.1093\/logcom\/4.5.531"},{"key":"9_CR2","unstructured":"Bedrax-Weiss, T., McGann, C., Bachmann, A., Edington, W., Iatauro, M.: EUROPA2: User and Contributor Guide. Technical report, NASA Ames Research Center, Moffett Field, CA (February 2005)"},{"key":"9_CR3","unstructured":"Butler, R.W., Mu\u00f1oz, C.A.: An Abstract Plan Preparation Language. Report 214518, NASA Langley, Hampton VA 23681-2199, USA (2006)"},{"key":"9_CR4","unstructured":"Butler, R.W., Siminiceanu, R.I., Mu\u00f1o, C.A.: The ANMLite language and logic for specifying planning problems. Report 215088, NASA Langley, Hampton VA 23681-2199, USA (November 2007)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-63912-8_81","volume-title":"Recent Advances in AI Planning","author":"A. Cimatti","year":"1997","unstructured":"Cimatti, A., Giunchiglia, F., Giunchiglia, E., Traverso, P.: Planning via model checking: a decision procedure for AR. In: Steel, S. (ed.) ECP 1997. LNCS (LNAI), vol.\u00a01348, pp. 130\u2013142. Springer, Heidelberg (1997)"},{"key":"9_CR6","unstructured":"de Moura, L., Dutertre, B.: Yices 1.0: An Efficient SMT Solver. Technical report, SRI International, SMCOMP (2006), http:\/\/yices.csl.sri.com"},{"key":"9_CR7","unstructured":"de Moura, L., Owre, S., Shankar, N.: The SAL Language Manual. Technical Report SRI-CSL-01-02, CSL Technical Report (2003)"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Drusinsky, D., Watney, G.: Applying Run-Time Monitoring to the Deep-Impact Fault Protection Engine. In: 28th IEEE\/NASA Software Engineering Workshop, p. 127 (2003)","DOI":"10.1109\/SEW.2003.1270735"},{"key":"9_CR9","unstructured":"Edelkamp, S.: Heuristic search planning with BDDs. In: PuK (2000)"},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1023\/A:1008711707946","volume":"8","author":"M.S. Feather","year":"2001","unstructured":"Feather, M.S., Smith, B.: Automatic Generation of Test Oracles \u2013 From Pilot Studies to Application. Automated Software Eng.\u00a08(1), 31\u201361 (2001)","journal-title":"Automated Software Eng."},{"key":"9_CR11","unstructured":"Ferraris, P., Giunchiglia, E.: Planning as satisfiability in nondeterministic domains. In: AAAI, pp. 748\u2013753 (2000)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1023\/A:1025842019552","volume":"8","author":"J. Frank","year":"2003","unstructured":"Frank, J., Jonsson, A.: Constraint-based Attribute and Interval Planning. Journal of Constraints\u00a08, 339\u2013364 (2003)","journal-title":"Journal of Constraints"},{"key":"9_CR13","unstructured":"Hoey, J., St-Aubin, R., Hu, A., Boutilier, C.: SPUDD: Stochastic planning using decision diagrams. In: Uncertainty in Artificial Intelligence (UAI 1999), pp. 279\u2013288 (1999)"},{"key":"9_CR14","unstructured":"Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic Verification of Knowledge and Time with NuSMV. In: IJCAI, pp. 1384\u20131389 (2007)"},{"key":"9_CR15","unstructured":"Drew McDermott and AIPS 1998\u00a0IPC Committee. PDDL \u2013 the Planning Domain Definition Language. Technical report, Yale University (1998)"},{"key":"9_CR16","unstructured":"Owre, S., Shankar, N.: Formal Analysis Methods for Spacecraft Autonomy, Final Report. Technical Report SRI-17625, SRI International (2007)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-74128-2_8","volume-title":"Model Checking and Artificial Intelligence","author":"C. Pecheur","year":"2007","unstructured":"Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS, vol.\u00a04428, pp. 113\u2013128. Springer, Heidelberg (2007)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/11564751_45","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"H.M. Sheini","year":"2005","unstructured":"Sheini, H.M., Peintner, B., Sakallah, K.A., Pollack, M.E.: On solving soft temporal constraints using SAT techniques. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 607\u2013621. Springer, Heidelberg (2005)"},{"issue":"1","key":"9_CR19","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1017\/S0269888900001089","volume":"15","author":"D.E. Smith","year":"2000","unstructured":"Smith, D.E., Frank, J., Jonsson, A.K.: Bridging the Gap between Planning and Scheduling. The Knowledge Engineering Rev.\u00a015(1), 113\u2013128 (2000)","journal-title":"The Knowledge Engineering Rev."},{"key":"9_CR20","unstructured":"Smith, D.E., Frank, J., McGann, C.: The ANML Language. Technical report, NASA Ames, unpublished report (2006)"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00431-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T21:32:42Z","timestamp":1738963962000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00431-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642004308","9783642004315"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00431-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}