{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T10:55:09Z","timestamp":1785322509079,"version":"3.55.0"},"reference-count":31,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2017,1,17]],"date-time":"2017-01-17T00:00:00Z","timestamp":1484611200000},"content-version":"vor","delay-in-days":701,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/J011770\/1"],"award-info":[{"award-number":["EP\/J011770\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K006193\/1"],"award-info":[{"award-number":["EP\/K006193\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004186","name":"Northwest Regional Development Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004186","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,4,20]]},"DOI":"10.1093\/logcom\/exv002","type":"journal-article","created":{"date-parts":[[2015,2,17]],"date-time":"2015-02-17T04:10:55Z","timestamp":1424146255000},"page":"499-523","source":"Crossref","is-referenced-by-count":10,"title":["Two-stage agent program verification"],"prefix":"10.1093","volume":"28","author":[{"given":"Louise A","family":"Dennis","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, Merseyside, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, Merseyside, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matt","family":"Webster","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, Merseyside, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2015,2,16]]},"reference":[{"key":"key\n\t\t\t\t20180419114414_B1"},{"key":"key\n\t\t\t\t20180419114414_B2"},{"key":"key\n\t\t\t\t20180419114414_B3","doi-asserted-by":"crossref","first-page":"1385","DOI":"10.1093\/logcom\/exp029","article-title":"Property-based slicing for agent verification","volume":"19","author":"Bordini","year":"2009","journal-title":"Journal of Logic and Computation"},{"key":"key\n\t\t\t\t20180419114414_B4","first-page":"275","article-title":"Memory-efficient algorithms for the verification of temporal properties","volume-title":"Formal Methods in System Design","author":"Courcoubetis","year":"1992"},{"key":"key\n\t\t\t\t20180419114414_B5"},{"key":"key\n\t\t\t\t20180419114414_B6"},{"key":"key\n\t\t\t\t20180419114414_B7","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","article-title":"Model checking agent programming languages","volume":"19","author":"Dennis","year":"2012","journal-title":"Automated Software Engineering"},{"key":"key\n\t\t\t\t20180419114414_B8","first-page":"996","article-title":"Temporal and modal logic","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson","year":"1990"},{"key":"key\n\t\t\t\t20180419114414_B9","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/2500468.2494558","article-title":"Verifying autonomous systems","volume":"56","author":"Fisher","year":"2013","journal-title":"ACM Communications"},{"key":"key\n\t\t\t\t20180419114414_B10"},{"key":"key\n\t\t\t\t20180419114414_B11","first-page":"4622","article-title":"Joint action understanding improves robot-to-human object handover","volume-title":"Proceedings of the IROS","author":"Grigore","year":"2013"},{"key":"key\n\t\t\t\t20180419114414_B12","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Hansson","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"key\n\t\t\t\t20180419114414_B13"},{"key":"key\n\t\t\t\t20180419114414_B14"},{"key":"key\n\t\t\t\t20180419114414_B15","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann","year":"2004"},{"key":"key\n\t\t\t\t20180419114414_B16"},{"key":"key\n\t\t\t\t20180419114414_B17"},{"key":"key\n\t\t\t\t20180419114414_B18"},{"key":"key\n\t\t\t\t20180419114414_B19"},{"key":"key\n\t\t\t\t20180419114414_B20"},{"key":"key\n\t\t\t\t20180419114414_B21","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","article-title":"Automatic verification of real-time systems with discrete probability distributions","volume":"282","author":"Kwiatkowska","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"key\n\t\t\t\t20180419114414_B22","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/MCI.2013.2279559","article-title":"Autonomous asteroid exploration \u2014 agent based control for autonomous spacecraft in complex environments","volume":"8","author":"Lincoln","year":"2013","journal-title":"IEEE Computational Intelligence"},{"key":"key\n\t\t\t\t20180419114414_B23"},{"key":"key\n\t\t\t\t20180419114414_B24","first-page":"1","article-title":"Model checking for probabilistic timed automata","author":"Norman","year":"2012","journal-title":"Formal Methods in System Design"},{"key":"key\n\t\t\t\t20180419114414_B25"},{"key":"key\n\t\t\t\t20180419114414_B26"},{"key":"key\n\t\t\t\t20180419114414_B27","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/MIS.2002.1039830","article-title":"Modeling and simulating work practice: a method for work systems design","volume":"17","author":"Sierhuis","year":"2002","journal-title":"IEEE Intelligent Systems"},{"key":"key\n\t\t\t\t20180419114414_B28"},{"key":"key\n\t\t\t\t20180419114414_B29","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","article-title":"Model checking programs","volume":"10","author":"Visser","year":"2003","journal-title":"Automated Software Engineering"},{"key":"key\n\t\t\t\t20180419114414_B30","doi-asserted-by":"crossref","first-page":"258","DOI":"10.2514\/1.I010096","article-title":"Generating certification evidence for autonomous unmanned aircraft using model checking and simulation","volume":"11","author":"Webster","year":"2014","journal-title":"Journal of Aerospace Information Systems"},{"key":"key\n\t\t\t\t20180419114414_B31","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about Rational Agents","author":"Wooldridge","year":"2000"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/28\/3\/499\/24671772\/exv002.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T07:33:19Z","timestamp":1747639999000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/28\/3\/499\/2917787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,16]]},"references-count":31,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2015,2,16]]},"published-print":{"date-parts":[[2018,4,20]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exv002","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2018,4]]},"published":{"date-parts":[[2015,2,16]]}}}