{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T05:13:12Z","timestamp":1771045992329,"version":"3.50.1"},"reference-count":45,"publisher":"Emerald","issue":"4","license":[{"start":{"date-parts":[[2009,11,20]],"date-time":"2009-11-20T00:00:00Z","timestamp":1258675200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.emerald.com\/insight\/site-policies"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,11,20]]},"abstract":"<jats:sec><jats:title content-type=\"abstract-heading\">Purpose<\/jats:title><jats:p>The purpose of this paper is to consider the logical specification, and automated verification, of high\u2010level robotic behaviours.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Design\/methodology\/approach<\/jats:title><jats:p>The paper uses temporal logic as a formal language for providing abstractions of foraging robot behaviour, and successively extends this to multiple robots, items of food for the robots to collect, and constraints on the real\u2010time behaviour of robots. For each of these scenarios, proofs of relevant properties are carried out in a fully automated way. In addition to automated deductive proofs in propositional temporal logic, the possibility of having arbitrary numbers of robots involved is considered, thus allowing representations of robot swarms. This leads towards the use of first\u2010order temporal logics (FOTLs).<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Findings<\/jats:title><jats:p>The proofs of many properties are achieved using automatic deductive temporal provers for the propositional and FOTLs.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Research limitations\/implications<\/jats:title><jats:p>Many details of the problem, such as location of the robots, avoidance, etc. are abstracted away.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Practical implications<\/jats:title><jats:p>Large robot swarms are beyond the current capability of propositional temporal provers. Whilst representing and proving properties of arbitrarily large swarms using FOTLs is feasible, the representation of infinite numbers of pieces of food is outside of the decidable fragment of FOTL targeted, and practically, the provers struggle with even small numbers of pieces of food.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Originality\/value<\/jats:title><jats:p>The work described in this paper is novel in that it applies automatic temporal theorem provers to proving properties of robotic behaviour.<\/jats:p><\/jats:sec>","DOI":"10.1108\/17563780911005818","type":"journal-article","created":{"date-parts":[[2009,11,14]],"date-time":"2009-11-14T07:05:35Z","timestamp":1258182335000},"page":"604-643","source":"Crossref","is-referenced-by-count":17,"title":["Deductive verification of simple foraging robotic behaviours"],"prefix":"10.1108","volume":"2","author":[{"given":"Abdelkader","family":"Behdenna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","reference":[{"key":"key2022031519441852800_b1","doi-asserted-by":"crossref","unstructured":"Abate, P. and Gor\u00e9, R. (2003), \u201cThe tableaux work bench\u201d, Proceedings of International Workshop on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux), Aix\u2010en\u2010Proxence, Lecture Notes in Artificial Intelligence, Vol. 2796, pp. 230\u20106.","DOI":"10.1007\/978-3-540-45206-5_18"},{"key":"key2022031519441852800_b2","doi-asserted-by":"crossref","unstructured":"Balsiger, P., Heuerding, A. and Schwendimann, S. (1998), \u201cLogics workbench 1.0\u201d, Proceedings of International Workshop on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux), Lecture Notes in Computer Science, Springer, Oisterwijk, Vol. 1397, p. 35.","DOI":"10.1007\/3-540-69778-0_8"},{"key":"key2022031519441852800_b3","doi-asserted-by":"crossref","unstructured":"Beni, G. (2005), \u201cFrom swarm intelligence to swarm robotics\u201d, Proceedings of International Workshop on Swarm Robotics (SAB), Revised Selected Papers, Lecture Notes in Computer Science, Vol. 3342, Springer, Berlin, pp. 1\u20109.","DOI":"10.1007\/978-3-540-30552-1_1"},{"key":"key2022031519441852800_b4","doi-asserted-by":"crossref","unstructured":"Bonabeau, E., Dorigo, M. and Theraulaz, G. (1999), Swarm Intelligence: From Natural to Artificial Systems, Oxford University Press, New York, NY.","DOI":"10.1093\/oso\/9780195131581.001.0001"},{"key":"key2022031519441852800_b5","unstructured":"Chen, D. (2005), \u201cA simulation environment for swarm robotic system based on temporal logic specifications\u201d, Master's thesis, University of the West of England, Bristol."},{"key":"key2022031519441852800_b6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R. and Tacchella, A. (2002), \u201cNuSMV 2: an opensource tool for symbolic model checking\u201d, Proceedings of 14th International Conference on Computer\u2010aided Verification (CAV), Lecture Notes in Computer Science, Vol. 2404, Springer, Berlin, pp. 359\u201064.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"key2022031519441852800_b7","unstructured":"Clarke, E., Grumberg, O. and Peled, D.A. (2000), Model Checking, MIT Press, Cambridge, MA."},{"key":"key2022031519441852800_b8","doi-asserted-by":"crossref","unstructured":"Dixon, C., Fisher, M. and Konev, B. (2007a), \u201cTemporal logic with capacity constraints\u201d, Proceedings of 6th International Symposium on Frontiers of Combining Systems (FroCos), Lecture Notes in Computer Science, Vol. 4720, Springer, Berlin, pp. 163\u201077.","DOI":"10.1007\/978-3-540-74621-8_11"},{"key":"key2022031519441852800_b9","unstructured":"Dixon, C., Fisher, M. and Konev, B. (2007b), \u201cTractable temporal reasoning\u201d, Proceedings of 20th International Joint Conference on Artificial Intelligence (IJCAI), AAAI Press, Portland, OR, pp. 318\u201023."},{"key":"key2022031519441852800_b10","doi-asserted-by":"crossref","unstructured":"Dixon, C., Fisher, M., Konev, B. and Lisitsa, A. (2008), \u201cPractical first\u2010order temporal reasoning\u201d, Proceedings of 15th International Symposium on Temporal Representation and Reasoning (TIME), IEEE Press, Los Alamitos, CA.","DOI":"10.1109\/TIME.2008.15"},{"key":"key2022031519441852800_b11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A. (1990), \u201cTemporal and modal logic\u201d, in van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science, Elsevier, Amsterdam, pp. 996\u20101072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"key2022031519441852800_b12","doi-asserted-by":"crossref","unstructured":"Fainekos, G., Kress\u2010Gazit, H. and Pappas, G. (2005), \u201cTemporal logic motion planning for mobile robots\u201d, Proceedings of the IEEE International Conference on Robotics and Automation (ICRA), IEEE, Barcelona, Spain, pp. 2020\u20105.","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"key2022031519441852800_b13","unstructured":"Fisher, M. (2007), \u201cTemporal representation and reasoning\u201d, in van Harmelen, F., Porter, B. and Lifschitz, V. (Eds), Handbook of Knowledge Representation, Foundations of Artificial Intelligence, Vol. 2, Elsevier, Amsterdam."},{"key":"key2022031519441852800_b14","doi-asserted-by":"crossref","unstructured":"Fisher, M., Dixon, C. and Peim, M. (2001), \u201cClausal temporal resolution\u201d, ACM Transactions on Computational Logic, Vol. 2 No. 1, pp. 12\u201056.","DOI":"10.1145\/371282.371311"},{"key":"key2022031519441852800_b15","unstructured":"Fisher, M., Konev, B. and Lisitsa, A. (2006), \u201cPractical infinite\u2010state verification with temporal reasoning\u201d, Verification of Infinite State Systems and Security, NATO Security through Science Series: Information and Communication, Vol. 1, IOS Press, Amsterdam."},{"key":"key2022031519441852800_b16","doi-asserted-by":"crossref","unstructured":"Fisher, M., Konev, B. and Lisitsa, A. (2009), \u201cTemporal verification of fault\u2010tolerant protocols\u201d, Methods, Models and Tools for Fault Tolerance, Lecture Notes in Computer Science, Vol. 5454, Springer, Berlin, pp. 44\u201056.","DOI":"10.1007\/978-3-642-00867-2_3"},{"key":"key2022031519441852800_b17","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S. and Stavi, J. (1980), \u201cThe temporal analysis of fairness\u201d, Proceedings of 7th ACM Symposium on the Principles of Programming Languages, Las Vegas, NV, ACM, New York, NY, pp. 163\u201073.","DOI":"10.1145\/567446.567462"},{"key":"key2022031519441852800_b18","doi-asserted-by":"crossref","unstructured":"Gordon\u2010Spears, D. and Kiriakidis, K. (2004), \u201cReconfigurable robot teams: modeling and supervisory control\u201d, IEEE Transactions on Control Systems Technology, Vol. 12 No. 5, pp. 763\u20109.","DOI":"10.1109\/TCST.2004.825048"},{"key":"key2022031519441852800_b19","doi-asserted-by":"crossref","unstructured":"Harper, C. and Winfield, A. (2006), \u201cA methodology for provably stable behaviour\u2010based intelligent control\u201d, Robotics and Autonomous Systems, Vol. 54 No. 1, pp. 52\u201073.","DOI":"10.1016\/j.robot.2005.09.014"},{"key":"key2022031519441852800_b21","doi-asserted-by":"crossref","unstructured":"Hodkinson, I., Wolter, F. and Zakharyashev, M. (2000), \u201cDecidable fragments of first\u2010order temporal logics\u201d, Annals of Pure and Applied Logic, Vol. 106 Nos 1\u20103, pp. 85\u2010134.","DOI":"10.1016\/S0168-0072(00)00018-X"},{"key":"key2022031519441852800_b20","unstructured":"Hodkinson, I., Kontchakov, R., Kurucz, A., Wolter, F. and Zakharyaschev, M. (2003), \u201cOn the computational complexity of decidable fragments of first\u2010order linear temporal logics\u201d, Proceedings of TIME\u2010ICTL 2003, IEEE Press, Los Alamitos, CA."},{"key":"key2022031519441852800_b22","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J. (1997), \u201cThe model checker spin\u201d, IEEE Transactions on Software Engineering, Vol. 23 No. 5, pp. 279\u201095, (special issue on Formal Methods in Software Practice).","DOI":"10.1109\/32.588521"},{"key":"key2022031519441852800_b23","doi-asserted-by":"crossref","unstructured":"Hustadt, U. and Konev, B. (2003), \u201cTRP++2.0: a temporal resolution prover\u201d, Proceedings of 19th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, Vol. 2741, Springer, Berlin, pp. 274\u20108.","DOI":"10.1007\/978-3-540-45085-6_21"},{"key":"key2022031519441852800_b24","doi-asserted-by":"crossref","unstructured":"Hustadt, U., Konev, B., Riazanov, A. and Voronkov, A. (2004), \u201cTeMP: a temporal monodic prover\u201d, in Basin, D.A. and Rusinowitch, M. (Eds), Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), Lecture Notes in Artificial Intelligence, Vol. 3097, Springer, Berlin, pp. 326\u201030.","DOI":"10.1007\/978-3-540-25984-8_23"},{"key":"key2022031519441852800_b25","unstructured":"Janssen, G. (1999), \u201cLogics for digital circuit verification: theory, algorithms, and applications\u201d, PhD thesis, Eindhoven University of Technology, Eindhoven."},{"key":"key2022031519441852800_b26","doi-asserted-by":"crossref","unstructured":"Kloetzer, M. and Belta, C. (2007), \u201cTemporal logic planning and control of robotic swarms by hierarchical abstractions\u201d, IEEE Transactions on Robotics, Vol. 23, pp. 320\u201030.","DOI":"10.1109\/TRO.2006.889492"},{"key":"key2022031519441852800_b27","doi-asserted-by":"crossref","unstructured":"Konev, B., Degtyarev, A., Dixon, C., Fisher, M. and Hustadt, U. (2005), \u201cMechanising first\u2010order temporal resolution\u201d, Information and Computation, Vol. 199 Nos 1\u20102, pp. 55\u201086.","DOI":"10.1016\/j.ic.2004.10.005"},{"key":"key2022031519441852800_b28","doi-asserted-by":"crossref","unstructured":"Kontchakov, R., Lutz, C., Wolter, F. and Zakharyaschev, M. (2004), \u201cTemporalizing tableaux\u201d, Studia Logica, Vol. 76, pp. 91\u2010134.","DOI":"10.1023\/B:STUD.0000027468.28935.6d"},{"key":"key2022031519441852800_b29","doi-asserted-by":"crossref","unstructured":"Lerman, K., Martinoli, A. and Galstyan, A. (2005), \u201cA review of probabilistic macroscopic models for swarm robotic systems\u201d, Swarm Robotics, Lecture Notes in Computer Science, Vol. 3342, Springer, Berlin, pp. 143\u201052.","DOI":"10.1007\/978-3-540-30552-1_12"},{"key":"key2022031519441852800_b30","doi-asserted-by":"crossref","unstructured":"Liu, W., Winfield, A.F.T., Sa, J., Chen, J. and Dou, L. (2007), \u201cStrategies for energy optimisation in a swarm of foraging robots\u201d, Proceedings of 2nd International Workshop on Swarm Robotics (SAB), Lecture Notes in Computer Science, Vol. 4433, Springer, Berlin, pp. 14\u201026.","DOI":"10.1007\/978-3-540-71541-2_2"},{"key":"key2022031519441852800_b31","doi-asserted-by":"crossref","unstructured":"Ludwig, M. and Hustadt, U. (2009\/2010), \u201cImplementing a fair monodic temporal prover\u201d, AI Communications (in press)..","DOI":"10.3233\/AIC-2010-0457"},{"key":"key2022031519441852800_b32","doi-asserted-by":"crossref","unstructured":"Martinoli, A., Easton, K. and Agassounon, W. (2004), \u201cModeling swarm robotic systems: a case study in collaborative distributed manipulation\u201d, International Journal of Robotics Research, Vol. 23 No. 4, pp. 415\u201036.","DOI":"10.1177\/0278364904042197"},{"key":"key2022031519441852800_b33","unstructured":"Nembrini, J., Winfield, A.F.T. and Melhuish, C. (2002), \u201cMinimalist coherent swarming of wireless connected autonomous mobile robots\u201d, Proceedings of 7th International Conference on Simulation of Adaptive Behavior (ICSAB), MIT Press, Cambridge, MA, pp. 373\u201082."},{"key":"key2022031519441852800_b34","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (1981), \u201cThe temporal semantics of concurrent programs\u201d, Theoretical Computer Science, Vol. 13, pp. 45\u201060.","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"key2022031519441852800_b35","doi-asserted-by":"crossref","unstructured":"Rouff, C.A., Hinchey, M.G., Pena, J. and Ruiz\u2010Cortes, A. (2007), \u201cUsing formal methods and agent\u2010oriented software engineering for modeling NASA swarm\u2010based systems\u201d, Proceedings of International Swarm Intelligence Symposium (SIS), IEEE Press, Los Alamitos, CA, pp. 348\u201055.","DOI":"10.1109\/SIS.2007.367958"},{"key":"key2022031519441852800_b36","doi-asserted-by":"crossref","unstructured":"Sahin, E. and Winfield, A.F.T. (2008), \u201cSpecial issue on swarm robotics\u201d, Swarm Intelligence, Vol. 2 Nos 2\u20104, pp. 69\u201072.","DOI":"10.1007\/s11721-008-0020-6"},{"key":"key2022031519441852800_b37","doi-asserted-by":"crossref","unstructured":"Schwendimann, S. (1998), \u201cA new one\u2010pass tableau calculus for PLTL\u201d, Proceedings of International Workshop on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Lecture Notes in Artificial Intelligence, Vol. 1397, Springer, Berlin, pp. 277\u201091.","DOI":"10.1007\/3-540-69778-0_28"},{"key":"key2022031519441852800_b38","doi-asserted-by":"crossref","unstructured":"Sistla, A.P. and Clarke, E.M. (1985), \u201cComplexity of propositional linear temporal logics\u201d, Journal of the ACM, Vol. 32 No. 3, pp. 733\u201049.","DOI":"10.1145\/3828.3837"},{"key":"key2022031519441852800_b39","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Vardi, M. and Wolper, P. (1987), \u201cThe complementation problem for B\u00fcchi automata with applications to temporal logic\u201d, Theoretical Computer Science, Vol. 49, pp. 217\u201037.","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"key2022031519441852800_b40","doi-asserted-by":"crossref","unstructured":"Spears, W.M., Spears, D.F., Hamann, J.C. and Heil, R. (2004), \u201cDistributed, physics\u2010based control of swarms of vehicles\u201d, Autonomous Robots, Vol. 17 Nos 2\u20103, pp. 137\u201062.","DOI":"10.1023\/B:AURO.0000033970.96785.f2"},{"key":"key2022031519441852800_b41","unstructured":"TRP++ (2002), \u201cTemporal resolution prover\u201d, available at: www.csc.liv.ac.uk\/\u223ckonev\/software\/trp++."},{"key":"key2022031519441852800_b42","doi-asserted-by":"crossref","unstructured":"Winfield, A. and Nembrini, J. (2006), \u201cSafety in numbers: fault tolerance in robot swarms\u201d, International Journal of Modelling Identification and Control, Vol. 1 No. 1, pp. 30\u20107.","DOI":"10.1504\/IJMIC.2006.008645"},{"key":"key2022031519441852800_b43","doi-asserted-by":"crossref","unstructured":"Winfield, A., Sa, J., Fern\u00e1ndez Gago, M.\u2010C., Dixon, C. and Fisher, M. (2005), \u201cOn formal specification of emergent behaviours in swarm robotic systems\u201d, International Journal of Advanced Robotic Systems, Vol. 2 No. 4, pp. 363\u201070.","DOI":"10.5772\/5769"},{"key":"key2022031519441852800_b44","unstructured":"Wolper, P. (1985), \u201cThe tableau method for temporal logic: an overview\u201d, Logique et Analyse, Vol. 110\u2010111, pp. 119\u201036."},{"key":"key2022031519441852800_b45","doi-asserted-by":"crossref","unstructured":"Wolter, F. and Zakharyaschev, M. (2002), \u201cAxiomatizing the monodic fragment of first\u2010order temporal logic\u201d, Annals of Pure and Applied Logic, Vol. 118 Nos 1\u20102, pp. 133\u201045.","DOI":"10.1016\/S0168-0072(01)00124-5"}],"container-title":["International Journal of Intelligent Computing and Cybernetics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.emeraldinsight.com\/doi\/full-xml\/10.1108\/17563780911005818","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/17563780911005818\/full\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/17563780911005818\/full\/html","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T23:44:17Z","timestamp":1753400657000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.emerald.com\/ijicc\/article\/2\/4\/604-643\/137270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11,20]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,11,20]]}},"alternative-id":["10.1108\/17563780911005818"],"URL":"https:\/\/doi.org\/10.1108\/17563780911005818","relation":{},"ISSN":["1756-378X"],"issn-type":[{"value":"1756-378X","type":"print"}],"subject":[],"published":{"date-parts":[[2009,11,20]]}}}