{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:12Z","timestamp":1740109092624,"version":"3.37.3"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP110101211"],"award-info":[{"award-number":["DP110101211"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>An autonomous agent is one that is not only directed by its environment, but is also driven by internal motivation to achieve certain goals based on beliefs about the environmental behaviour. Design paradigms for autonomous agents such as belief-desire-intention take into account the agent\u2019s \u201cmental\u201d features when presenting its patterns of behaviour. In this paper we present an approach to modelling autonomous agents by introducing mental features to conventional transition system specifications. Mental features such as belief and desire are represented by declarative linear temporal logic formulas. Refinement is then proposed to define the correctness of the agent design and development. It turns out, however, that the introduction of these mental features is not monotonic with respect to refinement. We therefore introduce additional refinement proof obligations to enable the use of simulation rules when checking refinement.<\/jats:p>","DOI":"10.1007\/s00165-016-0391-1","type":"journal-article","created":{"date-parts":[[2016,8,9]],"date-time":"2016-08-09T14:35:27Z","timestamp":1470753327000},"page":"227-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Refining autonomous agents with declarative beliefs and desires"],"prefix":"10.1145","volume":"29","author":[{"given":"Qin","family":"Li","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.04.009"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1855020"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"A\u015ftef\u0103noaei L de Boer FS (2010) The refinement of multi-agent systems. In: Dastani M Hindriks KV Meyer J-JC (eds) Specification and verification of multi-agent systems chapter 2. Springer-Verlag Berlin pp 35\u201365","DOI":"10.1007\/978-1-4419-6984-2_2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA Kupferman O Vardi MY (1998) Alternating refinement relations. In: International conference on concurrency theory (CONCUR \u201998) LNCS vol 1466. Springer-Verlag Berlin pp 163\u2013178","DOI":"10.1007\/BFb0055622"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Back R-JR (1990) Refinement calculus part II: parallel and reactive programs. In: Stepwise refinement of distributed systems models formalisms correctness. Springer Berlin pp 67\u201393","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-006-5955-7"},{"key":"e_1_2_1_2_8_2","unstructured":"Broda K Hogger CJ (2004) Designing and simulating individual teleo-reactive agents. In: Annual German conference on artificial intelligence (KI 2004) Lecture notes in artificial intelligence vol 3238. Springer-Verlag Berlin pp 1\u201315"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Chen Q Li Q Su K Luo X (2014) Quantified coalition logic for BDI-Agents: completeness and complexity. In: Pham D-N Park S-B (eds) Pacific Rim International Conference on Artificial Intelligence (PRICAI 2014) Lecture Notes in Computer Science vol 8862. Springer International Publishing Switzerland pp 871\u2013876","DOI":"10.1007\/978-3-319-13560-1_72"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Derrick J Boiten E (2014) Refinement in Z and Object-Z foundations and advanced applications 2nd edn. Springer-Verlag London","DOI":"10.1007\/978-1-4471-5355-9"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"d\u2019Inverno M Luck M (1997) Development and application of a formal agent framework. In: International conference on formal engineering methods (ICFEM \u201997). IEEE Computer Society Washington DC USA pp 222\u2013231","DOI":"10.1109\/ICFEM.1997.630429"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science vol B. Elsevier Amsterdam p 996\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"e_1_2_1_2_13_2","unstructured":"Fagundes MS Billhardt H Ossowski S (2010) Reasoning about norm compliance with rational agents. In: European conference on artificial intelligence (ECAI 2010) vol 215 pp 1027\u20131028"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.09.004"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0957-4174(02)00070-2"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hindriks KV de Boer FS Hoek W Meyer JC (2001) Agent programming with declarative goals. In: International workshop on intelligent agents VII: agent theories architectures and languages (ATAL \u201900). Springer-Verlag Berlin pp 228\u2013243","DOI":"10.1007\/3-540-44631-1_16"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hindriks KV (2009) Programming rational agents in GOAL. In: Bordini RH Dastani M Dix J El Fallah Seghrouchni A (eds) Multi-agent programming: languages platforms and applications vol 2 chapter 4. Springer-Verlag USA pp 119\u2013157","DOI":"10.1007\/978-0-387-89299-3_4"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-013-9238-9"},{"key":"e_1_2_1_2_19_2","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hindriks KV Riemsdijk MB (2009) Using temporal logic to integrate goals and qualitative preferences into agent programming. In: Baldoni M Son T Riemsdijk MB Winikoff M (eds) Declarative agent languages and technologies VI (DALT 2008) Lecture notes in computer science vol 5397. Springer-Verlag Berlin pp 215\u2013232","DOI":"10.1007\/978-3-540-93920-7_14"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Li Q Smith G (2013) A refinement framework for autonomous agents. In: Iyoda J de Moura L (eds) Brazilian Symposium on Formal Methods (SBMF 2013) Lecture Notes in Computer Science vol 8195. Springer-Verlag Berlin pp 163\u2013178","DOI":"10.1007\/978-3-642-41071-0_12"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Laibinis L Troubitsyna E Graja Z Migeon F Hadj Kacem A (2014) Formal modelling and verification of cooperative ant behaviour in Event-B. In: Giannakopoulou D Sala\u00fcn G (eds) Software engineering and formal methods (SEFM 2014) Lecture notes in computer science vol 8702. Springer International Publishing Switzerland pp 363\u2013377","DOI":"10.1007\/978-3-319-10431-7_29"},{"key":"e_1_2_1_2_23_2","unstructured":"Moreira \u00c1F Bordini RH (2002) An operational semantics for a bdi agent-oriented programming language. In: Proceedings of the workshop on logics for agent-based systems (LABS-02) held in conjunction with the Eighth International Conference on Principles of Knowledge Representation and Reasoning (KR2002) April pp 45\u201359"},{"key":"e_1_2_1_2_24_2","unstructured":"Meyer J-JCh Broersen J Herzig A (2015) BDI logics. In: van Ditmarsch H Halpern JY van der Hoek W Kooi B (eds) Handbook of logics for knowledge and belief. College publications pp 453\u2013498"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Meyer J-JCh (2014) Logics for intelligent agents and multi-agent systems. In: Siekmann JH (ed) Handbook of the history of logic vol 9. North-Holland pp 629\u2013658","DOI":"10.1016\/B978-0-444-51624-4.50014-9"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1618595.1618602"},{"key":"e_1_2_1_2_27_2","unstructured":"Rao AS Georgeff MP (1995) BDI agents: from theory to practice. In: 1st International conference of multi-agent systems (ICMAS-95). MIT Press Cambridge pp 312\u2013319"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.12.010"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Smith G Li Q (2014) MAZE: An extension of Object-Z for multi-agent systems. In: Ait Ameur Y Schewe K-D (eds) International conference on abstract state machines Alloy B TLA VDM and Z (ABZ 2014) Lecture Notes in Computer Science vol 8477. Springer-Verlag Berlin pp 72\u201385","DOI":"10.1007\/978-3-662-43652-3_6"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"e_1_2_1_2_31_2","unstructured":"Su K Sattar A Wang K Luo X Governatori G Padmanabhan V (2005) Observation-based model for BDI-Agents. In: Veloso MM Kambhampati S (eds) National conference on artificial intelligence (AAAI 2005). AAAI Press Pittsburgh Pennsylvania pp 190\u2013195"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Smith G Winter K (2012) Incremental development of multi-agent systems in Object-Z. In: IEEE software engineering workshop (SEW 2012). IEEE Press New York pp 120\u2013129","DOI":"10.1109\/SEW.2012.19"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Su K Yue W Sattar A Orgun MA Luo X (2006) Observation-based logic of knowledge belief desire and intention. In: Lang J Lin F Wang J (eds) Knowledge science engineering and management (KSEM 2006) Lecture notes in computer science vol 4092. Springer-Verlag Berlin pp 366\u2013378","DOI":"10.1007\/11811220_31"},{"key":"e_1_2_1_2_34_2","unstructured":"Winikoff M Dastani M van Riemsdijk MB (2010) A unified interaction-aware goal framework. In: European conference on artificial intelligence (ECAI 2010). IOS Press Amsterdam The Netherlands pp 1033\u20131034"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900008122"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-014-9263-3"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/1695886"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Zhu H (2001) Formal specification of agent behaviour through environment scenarios. In: Rash JL Truszkowski W Hinchey MG Rouff CA Gordon D (eds) Formal approaches to agent-based systems (FAABS 2000) Lecture notes in computer science vol 1871. Springer-Verlag Berlin pp 263\u2013277","DOI":"10.1007\/3-540-45484-5_21"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0391-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0391-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0391-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0391-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:56:17Z","timestamp":1641538577000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0391-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["10.1007\/s00165-016-0391-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0391-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,3]]},"assertion":[{"value":"16 February 2015","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 August 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}