{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:15Z","timestamp":1762458975571},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_24","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:49:46Z","timestamp":1340786986000},"page":"343-357","source":"Crossref","is-referenced-by-count":6,"title":["A Formal Interactive Verification Environment for the Plan Execution Interchange Language"],"prefix":"10.1007","author":[{"given":"Camilo","family":"Rocha","sequence":"first","affiliation":[]},{"given":"H\u00e9ctor","family":"Cadavid","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"additional","affiliation":[]},{"given":"Radu","family":"Siminiceanu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Balasubramanian, D., P\u0103s\u0103reanu, C., Whalen, M.W., Karsai, G., Lowry, M.R.: Polyglot: modeling and analysis for multiple Statechart formalisms. In: Dwyer, M.B., Tip, F. (eds.) ISSTA, pp. 45\u201355. ACM (2011)","DOI":"10.1145\/2001420.2001427"},{"issue":"5","key":"24_CR2","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/TSMCA.2011.2109709","volume":"41","author":"M.L. Bolton","year":"2011","unstructured":"Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: A systematic approach to model checking human-automation interaction using task analytic models. IEEE Transactions on Systems, Man, and Cybernetics\u2013Part A: Systems and Humans\u00a041(5), 961\u2013976 (2011)","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics\u2013Part A: Systems and Humans"},{"issue":"1-3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R. Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science\u00a0360(1-3), 386\u2013414 (2006)","journal-title":"Theoretical Computer Science"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"24_CR5","unstructured":"Dowek, G., Mu\u00f1oz, C., P\u0103s\u0103reanu, C.: A small-step semantics of PLEXIL. Technical Report 2008-11, National Institute of Aerospace, Hampton, VA (2008)"},{"key":"24_CR6","unstructured":"Dowek, G., Mu\u00f1oz, C., P\u0103s\u0103reanu, C.: A formal analysis framework for PLEXIL. In: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems (September 2007)"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Dowek, G., Mu\u00f1oz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. In: Klin, B., Sobocinski, P. (eds.) SOS. EPTCS, vol.\u00a018, pp. 77\u201391 (2009)","DOI":"10.4204\/EPTCS.18.6"},{"key":"24_CR8","unstructured":"Estlin, T., J\u00f3nsson, A., P\u0103s\u0103reanu, C., Simmons, R., Tso, K., Verma, V.: Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006-213483, NASA (2006)"},{"issue":"3","key":"24_CR9","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.entcs.2009.05.022","volume":"238","author":"N. Mart\u00ed-Oliet","year":"2009","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for maude strategies. Electronic Notes in Theoretical Computer Science\u00a0238(3), 227\u2013247 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"24_CR10","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1109\/SMC-IT.2009.31","volume-title":"IEEE International Conference on Space Mission Challenges for Information Technology","author":"C. Rocha","year":"2009","unstructured":"Rocha, C., Mu\u00f1oz, C., Cadavid, H.: A graphical environment for the semantic validation of a plan execution language. In: IEEE International Conference on Space Mission Challenges for Information Technology, pp. 201\u2013207. IEEE Computer Society, Los Alamitos (2009)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-25032-3_5","volume-title":"Formal Methods, Foundations and Applications","author":"C. Rocha","year":"2011","unstructured":"Rocha, C., Mu\u00f1oz, C.: Simulation and Verification of Synchronous Set Relations in Rewriting Logic. In: da Silva Sim\u00e3o, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol.\u00a07021, pp. 60\u201375. Springer, Heidelberg (2011)"},{"issue":"37","key":"24_CR13","doi-asserted-by":"publisher","first-page":"4853","DOI":"10.1016\/j.tcs.2011.01.027","volume":"412","author":"C. Rocha","year":"2011","unstructured":"Rocha, C., Mu\u00f1oz, C., Dowek, G.: A formal library of set relations and its application to synchronous languages. Theoretical Computer Science\u00a0412(37), 4853\u20134866 (2011)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"24_CR14","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G. Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming\u00a079(6), 397\u2013434 (2010)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"1","key":"24_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.12.002","volume":"258","author":"S. Santiago","year":"2009","unstructured":"Santiago, S., Talcott, C.L., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Electronic Notes in Theoretical Computer Science\u00a0258(1), 3\u201320 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"24_CR16","unstructured":"Strauss, P.J.: Executable semantics for PLEXIL: simulating a task-scheduling language in Haskell. Master\u2019s thesis, Oregon State University (2009)"},{"issue":"1-2","key":"24_CR17","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s10703-005-2254-x","volume":"27","author":"A. Verdejo","year":"2005","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods in System Design\u00a027(1-2), 113\u2013172 (2005)","journal-title":"Formal Methods in System Design"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Verma, V., J\u00f3nsson, A., P\u0103s\u0103reanu, C., Iatauro, M.: Universal Executive and PLEXIL: Engine and language for robust spacecraft control and operations. In: Proceedings of the American Institute of Aeronautics and Astronautics Space Conference (2006)","DOI":"10.2514\/6.2006-7449"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30729-4_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:28:57Z","timestamp":1620127737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}