{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T15:23:43Z","timestamp":1771082623385,"version":"3.50.1"},"publisher-location":"New York, New York, USA","reference-count":18,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1145\/3287921.3287947","type":"proceedings-article","created":{"date-parts":[[2018,12,13]],"date-time":"2018-12-13T15:45:16Z","timestamp":1544715916000},"page":"351-358","source":"Crossref","is-referenced-by-count":3,"title":["Formal Verification of ALICA Multi-agent Plans Using Model Checking"],"prefix":"10.1145","author":[{"given":"Thao Nguyen","family":"Van","sequence":"first","affiliation":[{"name":"Distributed Systems Group, University of Kassel, Kassel, Germany"}]},{"given":"Nugroho","family":"Fredivianus","sequence":"additional","affiliation":[{"name":"Distributed Systems Group, University of Kassel, Kassel, Germany"}]},{"given":"Huu Tam","family":"Tran","sequence":"additional","affiliation":[{"name":"Distributed Systems Group, University of Kassel, Kassel, Germany"}]},{"given":"Kurt","family":"Geihs","sequence":"additional","affiliation":[{"name":"Distributed Systems Group, University of Kassel, Kassel, Germany"}]},{"given":"Thi Thanh Binh","family":"Huynh","sequence":"additional","affiliation":[{"name":"Hanoi University of Science and Technology, Hanoi, Vietnam"}]}],"member":"320","reference":[{"key":"key-10.1145\/3287921.3287947-1","doi-asserted-by":"crossref","unstructured":"Flora Amato, Nicola Mazzocca, Francesco Moscato, and Fatos Xhafa. 2018. Multi-agent Collaborative Planning in Smart Environments. In Advances in Intelligent Networking and Collaborative Systems, Leonard Barolli, Isaac Woungang, and Omar Khadeer Hussain (Eds.). Springer International Publishing, Cham, 250--261.","DOI":"10.1007\/978-3-319-65636-6_22"},{"key":"key-10.1145\/3287921.3287947-2","doi-asserted-by":"crossref","unstructured":"Mathilde Arnaud, Veronique Cortier, and Stephanie Delaune. 2014. Modeling and verifying ad hoc routing protocols. Information and Computation 238 (2014), 30--67. https:\/\/doi.org\/10.1016\/j.ic.2014.07.004 Special Issue on Security and Rewriting Techniques.","DOI":"10.1016\/j.ic.2014.07.004"},{"key":"key-10.1145\/3287921.3287947-3","doi-asserted-by":"crossref","unstructured":"Howard Barringer, Klaus Havelund, and Robert A Morris. 2011. Checking Flight Rules with TraceContract Application of a Scala DSL for Trace Analysis. (2011).","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"key-10.1145\/3287921.3287947-4","unstructured":"Gerd Behrmann, Alexandre David, and Kim G Larsen. 2004. A tutorial on uppaal. In Formal methods for the design of real-time systems. Springer, 200--236."},{"key":"key-10.1145\/3287921.3287947-5","unstructured":"Edmund M Clarke, Orna Grumberg, and Doron Peled. 1999. Model checking.MIT press."},{"key":"key-10.1145\/3287921.3287947-6","unstructured":"Hyggo Oliveira de Almeida, Leandro Dias da Silva, Angelo Perkusich, and Evandro de Barros Costa. 2004. A formal approach for the modelling and verification of multiagent plans based on model checking and Petri nets. In International Workshop on Software Engineering for Large-Scale Multi-agent Systems. Springer, 162--179."},{"key":"key-10.1145\/3287921.3287947-7","unstructured":"Gilles Dowek, César Munoz, and Corina Pasareanu. 2007. A formal analysis framework for PLEXIL. In Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems. Citeseer, 45--51."},{"key":"key-10.1145\/3287921.3287947-8","doi-asserted-by":"crossref","unstructured":"Xiang Gan, Jori Dubrovin, and Keijo Heljanko. 2014. A symbolic model checking approach to verifying satellite onboard software. Science of Computer Programming 82 (2014), 44--55. https:\/\/doi.org\/10.1016\/j.scico.2013.03.005 Special Issue on Automated Verification of Critical Systems (AVoCS11).","DOI":"10.1016\/j.scico.2013.03.005"},{"key":"key-10.1145\/3287921.3287947-9","unstructured":"Lina Khatib, Nicola Muscettola, and Klaus Havelund. 2000. Verification of plan models using UPPAAL. In International Workshop on Formal Approaches to Agent-Based Systems. Springer, 114--122."},{"key":"key-10.1145\/3287921.3287947-10","doi-asserted-by":"crossref","unstructured":"H. Bel Mokadem, B. Berard, V. Gourcuff, O. De Smet, and J. M. Roussel. 2010. Verification of a Timed Multitask System With Uppaal. IEEE Transactions on Automation Science and Engineering 7, 4 (Oct 2010), 921--932. https:\/\/doi.org\/10.1109\/TASE.2010.2050199","DOI":"10.1109\/TASE.2010.2050199"},{"key":"key-10.1145\/3287921.3287947-11","doi-asserted-by":"crossref","unstructured":"Stephan Opfer, Stefan Niemczyk, and Kurt Geihs. 2016. MultiAgent Plan Verification with Answer Set Programming. In Proceedings of the 3rd Workshop on Model-Driven Robot Software Engineering. ACM, 32--39.","DOI":"10.1145\/3022099.3022104"},{"key":"key-10.1145\/3287921.3287947-12","doi-asserted-by":"crossref","unstructured":"Hendrik Skubch. 2012. Modelling and controlling of behaviour for autonomous mobile robots. Springer Science & Business Media.","DOI":"10.1007\/978-3-658-00811-6"},{"key":"key-10.1145\/3287921.3287947-13","doi-asserted-by":"crossref","unstructured":"Hendrik Skubch, Michael Wagner, Roland Reichle, and Kurt Geihs. 2011. A modelling language for cooperative plans in highly dynamic domains. Mechatronics 21, 2 (2011), 423--433.","DOI":"10.1016\/j.mechatronics.2010.10.006"},{"key":"key-10.1145\/3287921.3287947-14","unstructured":"Hendrik Skubch, Michael Wagner, Roland Reichle, Stefan Triller, and Kurt Geihs. 2010. Towards a Comprehensive Teamwork Model for Highly Dynamic Domains.. In ICAART (2). 121--127."},{"key":"key-10.1145\/3287921.3287947-15","unstructured":"Margaret H Smith, Gerard J Holzmann, Gordon C Cucullu, and BD Smith. 2005. Model Checking Autonomous Planners: Even the Best Laid Plans Must be Verified. In Aerospace Conference, 2005 IEEE. IEEE, 1--11."},{"key":"key-10.1145\/3287921.3287947-16","unstructured":"Vandi Verma, Tara Estlin, Ari Jónsson, Corina Pasareanu, Reid Simmons, and Kam Tso. 2005. Plan execution interchange language (PLEXIL) for executable plans and command sequences. In International symposium on artificial intelligence, robotics and automation in space (iSAIRAS)."},{"key":"key-10.1145\/3287921.3287947-17","doi-asserted-by":"crossref","unstructured":"A. Witsch, S. Opfer, and K. Geihs. 2014. A formal multi-agent language for cooperative autonomous driving scenarios. In 2014 International Conference on Connected Vehicles and Expo (ICCVE). 546--551. https:\/\/doi.org\/10.1109\/ICCVE.2014.7297608","DOI":"10.1109\/ICCVE.2014.7297608"},{"key":"key-10.1145\/3287921.3287947-18","doi-asserted-by":"crossref","unstructured":"Dianxiang Xu, Richard Volz, Thomas Ioerger, and John Yen. 2002. Modeling and verifying multi-agent behaviors using predicate\/transition nets. In Proceedings of the 14th international conference on software engineering and knowledge engineering. ACM, 193--200.","DOI":"10.1145\/568760.568794"}],"event":{"name":"the Ninth International Symposium","location":"Danang City, Viet Nam","acronym":"SoICT 2018","number":"9","sponsor":["SOICT, School of Information and Communication Technology - HUST","NAFOSTED, The National Foundation for Science and Technology Development"],"start":{"date-parts":[[2018,12,6]]},"end":{"date-parts":[[2018,12,7]]}},"container-title":["Proceedings of the Ninth International Symposium on Information and Communication Technology - SoICT 2018"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3287921.3287947","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=3287947&ftid=2025989&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:54Z","timestamp":1750208274000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=3287921.3287947"}},"subtitle":[],"proceedings-subject":"Information and Communication Technology","short-title":[],"issued":{"date-parts":[[2018]]},"references-count":18,"URL":"https:\/\/doi.org\/10.1145\/3287921.3287947","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}