{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T15:23:01Z","timestamp":1726068181595},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030414177"},{"type":"electronic","value":"9783030414184"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-41418-4_11","type":"book-chapter","created":{"date-parts":[[2020,2,19]],"date-time":"2020-02-19T06:14:01Z","timestamp":1582092841000},"page":"141-154","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Forward Chaining Heuristic Search with Spatio-Temporal Control Knowledge"],"prefix":"10.1007","author":[{"given":"Xu","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin","family":"Cui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yansong","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wensheng","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Runzhe","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yifeng","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qing","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,2,20]]},"reference":[{"issue":"1\u20132","key":"11_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0004-3702(99)00071-5","volume":"116","author":"F Bacchus","year":"2000","unstructured":"Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1\u20132), 123\u2013191 (2000). \nhttps:\/\/doi.org\/10.1016\/S0004-3702(99)00071-5","journal-title":"Artif. Intell."},{"key":"11_CR2","unstructured":"Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals using heuristic search. In: Proceedings of the Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16\u201320, 2006, Boston, Massachusetts, USA, pp. 788\u2013795 (2006). \nhttp:\/\/www.aaai.org\/Library\/AAAI\/2006\/aaai06-125.php"},{"issue":"2","key":"11_CR3","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1109\/TR.2018.2806349","volume":"67","author":"J Cui","year":"2018","unstructured":"Cui, J., Duan, Z., Tian, C., Du, H.: A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans. Reliab. 67(2), 481\u2013493 (2018). \nhttps:\/\/doi.org\/10.1109\/TR.2018.2806349","journal-title":"IEEE Trans. Reliab."},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z Duan","year":"2014","unstructured":"Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169\u2013190 (2014). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2014.02.011","journal-title":"Theor. Comput. Sci."},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1016\/j.tcs.2015.08.039","volume":"609","author":"Z Duan","year":"2016","unstructured":"Duan, Z., Tian, C., Zhang, N.: A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor. Comput. Sci. 609, 544\u2013560 (2016). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2015.08.039","journal-title":"Theor. Comput. Sci."},{"key":"11_CR6","unstructured":"Erol, K., Hendler, J.A., Nau, D.S.: HTN planning: complexity and expressivity. In: Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31\u2013August 4, 1994, vol. 2, pp. 1123\u20131128 (1994). \nhttp:\/\/www.aaai.org\/Library\/AAAI\/1994\/aaai94-173.php"},{"issue":"2","key":"11_CR7","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"PE Hart","year":"1968","unstructured":"Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for the heuristic determination of minimum cost paths. IEEE Trans. Syst. Sci. Cybern. 4(2), 100\u2013107 (1968). \nhttps:\/\/doi.org\/10.1109\/TSSC.1968.300136","journal-title":"IEEE Trans. Syst. Sci. Cybern."},{"issue":"2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/S0004-3702(02)00364-8","volume":"143","author":"M Helmert","year":"2003","unstructured":"Helmert, M.: Complexity results for standard benchmark domains in planning. Artif. Intell. 143(2), 219\u2013262 (2003). \nhttps:\/\/doi.org\/10.1016\/S0004-3702(02)00364-8","journal-title":"Artif. Intell."},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1613\/jair.1705","volume":"26","author":"M Helmert","year":"2006","unstructured":"Helmert, M.: The fast downward planning system. J. Artif. Intell. Res. 26, 191\u2013246 (2006). \nhttps:\/\/doi.org\/10.1613\/jair.1705","journal-title":"J. Artif. Intell. Res."},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1613\/jair.855","volume":"14","author":"J Hoffmann","year":"2001","unstructured":"Hoffmann, J., Nebel, B.: The FF planning system: fast plan generation through heuristic search. J. Artif. Intell. Res. 14, 253\u2013302 (2001). \nhttps:\/\/doi.org\/10.1613\/jair.855","journal-title":"J. Artif. Intell. Res."},{"key":"11_CR11","unstructured":"Kvarnstr\u00f6m, J., Magnusson, M.: Talplanner in IPC-2002: extensions and control rules. CoRR. \nhttp:\/\/arxiv.org\/abs\/1106.5266\n\n (2011)"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Lu, X., Tian, C., Duan, Z.: Temporalising separation logic for planning with search control knowledge. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19\u201325, 2017, pp. 1167\u20131173 (2017). \nhttps:\/\/doi.org\/10.24963\/ijcai.2017\/162","DOI":"10.24963\/ijcai.2017\/162"},{"issue":"10","key":"11_CR13","doi-asserted-by":"publisher","first-page":"1915","DOI":"10.1109\/TKDE.2018.2810144","volume":"30","author":"X Lu","year":"2018","unstructured":"Lu, X., Tian, C., Duan, Z., Du, H.: Planning with spatio-temporal search control knowledge. IEEE Trans. Knowl. Data Eng. 30(10), 1915\u20131928 (2018). \nhttps:\/\/doi.org\/10.1109\/TKDE.2018.2810144","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1613\/jair.1141","volume":"20","author":"DS Nau","year":"2003","unstructured":"Nau, D.S., et al.: SHOP2: an HTN planning system. J. Artif. Intell. Res. (JAIR) 20, 379\u2013404 (2003). \nhttps:\/\/doi.org\/10.1613\/jair.1141","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th IEEE Symposium on Logic in Computer Science (LICS 2002), July 22\u201325, 2002, Copenhagen, Denmark, pp. 55\u201374 (2002). \nhttps:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Tian, C., Duan, Z., Duan, Z., Ong, C.L.: More effective interpolations in software model checking. In: Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30\u2013November 03, 2017, pp. 183\u2013193 (2017). \nhttps:\/\/doi.org\/10.1109\/ASE.2017.8115631","DOI":"10.1109\/ASE.2017.8115631"},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1017\/S096012950800738X","volume":"19","author":"C Tian","year":"2009","unstructured":"Tian, C., Duan, Z.: Complexity of propositional projection temporal logic with star. Math. Struct. Comput. Sci. 19(1), 73\u2013100 (2009). \nhttps:\/\/doi.org\/10.1017\/S096012950800738X","journal-title":"Math. Struct. Comput. Sci."},{"issue":"18","key":"11_CR18","doi-asserted-by":"publisher","first-page":"1729","DOI":"10.1016\/j.tcs.2010.12.047","volume":"412","author":"C Tian","year":"2011","unstructured":"Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729\u20131744 (2011). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2010.12.047","journal-title":"Theor. Comput. Sci."},{"issue":"12","key":"11_CR19","doi-asserted-by":"publisher","first-page":"1206","DOI":"10.1109\/TSE.2014.2357442","volume":"40","author":"C Tian","year":"2014","unstructured":"Tian, C., Duan, Z., Duan, Z.: Making CEGAR more efficient in software model checking. IEEE Trans. Softw. Eng. 40(12), 1206\u20131223 (2014). \nhttps:\/\/doi.org\/10.1109\/TSE.2014.2357442","journal-title":"IEEE Trans. Softw. Eng."},{"key":"11_CR20","unstructured":"Wang, L., Baier, J., McIlraith, S.: Viewing landmarks as temporally extended goals. In: ICAPS 2009 Workshop on Heuristics for Domain-Independent Planning, pp. 49\u201356 (2009)"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2017.07.032","volume":"749","author":"K Yang","year":"2018","unstructured":"Yang, K., Duan, Z., Tian, C., Zhang, N.: A compiler for MSVL and its applications. Theor. Comput. Sci. 749, 2\u201316 (2018). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2017.07.032","journal-title":"Theor. Comput. Sci."},{"issue":"Part","key":"11_CR22","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jpdc.2017.09.003","volume":"118","author":"B Yu","year":"2018","unstructured":"Yu, B., Duan, Z., Tian, C., Zhang, N.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118(Part), 89\u201399 (2018). \nhttps:\/\/doi.org\/10.1016\/j.jpdc.2017.09.003","journal-title":"J. Parallel Distrib. Comput."},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1016\/j.tcs.2015.05.007","volume":"609","author":"N Zhang","year":"2016","unstructured":"Zhang, N., Duan, Z., Tian, C.: A complete axiom system for propositional projection temporal logic with cylinder computation model. Theor. Comput. Sci. 609, 639\u2013657 (2016). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2015.05.007","journal-title":"Theor. Comput. Sci."},{"issue":"11","key":"11_CR24","doi-asserted-by":"publisher","first-page":"118101","DOI":"10.1007\/s11432-015-0882-6","volume":"59","author":"N Zhang","year":"2016","unstructured":"Zhang, N., Duan, Z., Tian, C.: Model checking concurrent systems with MSVL. Sci. China Inf. Sci. 59(11), 118101 (2016). \nhttps:\/\/doi.org\/10.1007\/s11432-015-0882-6","journal-title":"Sci. China Inf. Sci."}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-41418-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,19]],"date-time":"2020-02-19T06:14:43Z","timestamp":1582092883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-41418-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030414177","9783030414184"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-41418-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"20 February 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SOFL+MSVL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Structured Object-Oriented Formal Language and Method","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shenzhen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sofl2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/csse.szu.edu.cn\/icfem2019\/soflmsvl.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}