{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T07:10:07Z","timestamp":1741936207861,"version":"3.38.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,9,1]],"date-time":"2011-09-01T00:00:00Z","timestamp":1314835200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2011,9]]},"DOI":"10.1007\/s10472-011-9270-x","type":"journal-article","created":{"date-parts":[[2011,11,18]],"date-time":"2011-11-18T11:59:23Z","timestamp":1321617563000},"page":"31-52","source":"Crossref","is-referenced-by-count":10,"title":["Kripke modelling and verification of temporal specifications of a multiple UAV system"],"prefix":"10.1007","volume":"63","author":[{"given":"Gopinadh","family":"Sirigineedi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonios","family":"Tsourdos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian A.","family":"White","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafa\u0142","family":"\u017bbikowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,11,19]]},"reference":[{"key":"9270_CR1","doi-asserted-by":"crossref","unstructured":"Beard, R.W., McLain, T.W., Nelson, D.B.: Decentralized cooperative aerial surveillance using fixed-wing miniature UAVs. In: Proceedings of the IEEE, vol.\u00a094, pp. 1306\u20131324 (2007)","DOI":"10.1109\/JPROC.2006.876930"},{"key":"9270_CR2","doi-asserted-by":"crossref","unstructured":"Gaudiano, P., Bonabeau, E., Shargel, B.: Evolving behaviors for a swarm of unmanned air vehicles. In: Proceedings of the 2005 IEEE Swarm Intelligence Symposium, pp. 317\u2013324 (2005)","DOI":"10.1109\/SIS.2005.1501638"},{"key":"9270_CR3","unstructured":"Jin, Y., Minai, A.A., Polycarpou, M.M.: Cooperative real-time search and task allocation in UAV teams. In: Proceedings of IEEE Conference on Decision and Control, pp. 7\u201312 (2003)"},{"key":"9270_CR4","doi-asserted-by":"crossref","first-page":"716","DOI":"10.1115\/1.2764515","volume":"129","author":"Y Yang","year":"2007","unstructured":"Yang, Y., Polycarpou, M., Minai, A.A.: Multi-UAV cooperative search using an opportunistic learning method. J. Dyn. Syst. Meas. Control 129, 716\u2013728 (2007)","journal-title":"J. Dyn. Syst. Meas. Control"},{"key":"9270_CR5","doi-asserted-by":"crossref","unstructured":"Su Park, C., Jea Tahk, M., Bang, H.: Multiple aerial vehicles formation using swarm intelligence. In: AIAA Guidance, Navigation, and Control Conference and Exhibit (2003)","DOI":"10.2514\/6.2003-5729"},{"key":"9270_CR6","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)"},{"key":"9270_CR7","unstructured":"Hinchey, M.G., Rash, J.L., Rouff, C.A.: Verification and validation of autonomous systems. In: Proceedings of 26th Annual NASA Goddard Software Engineering Workshop (2002)"},{"key":"9270_CR8","doi-asserted-by":"crossref","unstructured":"Gat, E.: Autonomy software verification and validation might not be as hard as it seems. In: Proceedings of IEEE Aerospace Conference, pp. 3123\u20133128 (2004)","DOI":"10.1109\/AERO.2004.1368117"},{"key":"9270_CR9","doi-asserted-by":"crossref","unstructured":"Rouff, C., Hinchey, M., Truszkowski, W., Rash, J.: Verifying large number of cooperating adaptive agents. In: Proceedings of the 11th International Conference on Parallel and Distributed Systems (ICPADS 2005), vol.\u00a01, pp. 391\u2013397 (2005)","DOI":"10.1109\/ICPADS.2005.294"},{"key":"9270_CR10","doi-asserted-by":"crossref","unstructured":"Brat, G., Jonsson, A.: Challenges in verification and validation of autonomous systems for space exploration. In: Proceedings of IEEE International Joint Conference on Neural Networks, vol.\u00a05, pp. 2909\u20132914 (2005)","DOI":"10.1109\/IJCNN.2005.1556387"},{"key":"9270_CR11","unstructured":"Pecheur, C.: Verification and Validation of Autonomy Software at NASA. NASA\/TM 2000-209602 (2000)"},{"issue":"2","key":"9270_CR12","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"9270_CR13","first-page":"14","volume":"59","author":"D Kotmanov\u00e1","year":"2008","unstructured":"Kotmanov\u00e1, D.: Temporal logic in verification of digital circuits. J. Electr. Eng. 59(1), 14\u201321 (2008)","journal-title":"J. Electr. Eng."},{"key":"9270_CR14","doi-asserted-by":"crossref","unstructured":"Lu, Y., Jorda, M.: Verifying a gigabit ethernet switch using SMV. In: Proceedings of the 41st Annual Conference on Design Automation, pp. 230\u2013233 (2004)","DOI":"10.1145\/996566.996631"},{"key":"9270_CR15","unstructured":"Schuppan, V., Biere, A.: Verifying the IEEE 1394 firewire tree identify protocol with SMV. Form. Asp. Comput 14, 267\u2013280 (2003)"},{"key":"9270_CR16","doi-asserted-by":"crossref","unstructured":"Miao, H., Zeng, H.: Model checking-based verification of web applications. In: Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems, pp. 47\u201355 (2007)","DOI":"10.1109\/ICECCS.2007.30"},{"key":"9270_CR17","unstructured":"Di Sciascio, E., Donini, F.M., Mongiello, M., Piscitelli, G.: Web applications design and maintenance using symbolic model checking. In: Proceedings of the Seventh European Conference On Software Maintenance And Reengineering (2003)"},{"issue":"3","key":"9270_CR18","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1016\/j.infsof.2008.08.003","volume":"51","author":"P Moreno-Ger","year":"2009","unstructured":"Moreno-Ger, P., Fuentes-Fern\u00e1ndez, R., Sierra, J.L., Fern\u00e1ndez-Manj\u00f3n, B.: Model-checking for adventure videogames. Trans. Info. Softw. Tech. 51(3), 564\u2013580 (2009)","journal-title":"Trans. Info. Softw. Tech"},{"key":"9270_CR19","unstructured":"Scherer, S., Lerda, F., Clarke, E.M.: Model checking robotic control systems. In: Proceedings of the 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (2005)"},{"key":"9270_CR20","doi-asserted-by":"crossref","unstructured":"Shukla, S.K., Gupta, R.K.: A model checking approach to evaluating system level dynamic power management polocies for embedded systems. In: Proceedings of Sixth IEEE International High-Level Design Validation and Test Workshop, pp. 53\u201357 (2001)","DOI":"10.1109\/HLDVT.2001.972807"},{"issue":"7","key":"9270_CR21","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W Chan","year":"1998","unstructured":"Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498\u2013520 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"9270_CR22","doi-asserted-by":"crossref","first-page":"926","DOI":"10.1109\/70.736776","volume":"14","author":"T Balch","year":"1998","unstructured":"Balch, T., Arkin, R.C.: Behavior based formation control for multirobot teams. IEEE Trans. Robot. Autom. 14(6), 926\u2013939 (1998)","journal-title":"IEEE Trans. Robot. Autom."},{"key":"9270_CR23","doi-asserted-by":"crossref","unstructured":"Hebert, M., Stentz, A., Thorpe, C.: Mobility planning for autonomous navigation multiple robots in unstructured environments. In: Proceedings of the IEEE-ISIC-CIRA-ISAS Joint Conference, pp. 652\u2013657 (1998)","DOI":"10.1109\/ISIC.1998.713788"},{"issue":"6","key":"9270_CR24","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1080\/00207720500438472","volume":"37","author":"S Jeyaraman","year":"2006","unstructured":"Jeyaraman, S., Tsourdos, A., \u017bbikowski, R., White, B.: Kripke modelling approaches of a multiple robots system with minimalist communication: a formal approach of choice. Int. J. Syst. Sci. 37(6), 339\u2013349 (2006)","journal-title":"Int. J. Syst. Sci."},{"key":"9270_CR25","doi-asserted-by":"crossref","unstructured":"Melholt Quottrup, M., Bak, T., Izadi-Zamanabadi, R.: Multi-robot planning: a timed automata approach. In: Proceedings of the 2004 IEEE International Conference on Robotics and Automation (2004)","DOI":"10.1109\/ROBOT.2004.1302413"},{"issue":"3","key":"9270_CR26","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1109\/TSMCA.2006.886378","volume":"37","author":"JM Esposito","year":"2007","unstructured":"Esposito, J.M., Kim, M.: Using formal modeling with an automated analysis tool to design and parametrically analyze a multirobot coordination protocol: a case study. IEEE Trans. Syst. Man Cybern., Part A, Syst. Humans 37(3), 285\u2013297 (2007)","journal-title":"IEEE Trans. Syst. Man Cybern., Part A, Syst. Humans"},{"key":"9270_CR27","doi-asserted-by":"crossref","unstructured":"Sirigineedi, G., Tsourdos, A., White, B.A., \u017bbikowski, R.: Towards verifiable approach to mission planning for multiple UAVs. In: AIAA Infotech@Aerospace Conference and AIAA Unmanned. Unlimited Conference (2009)","DOI":"10.2514\/6.2009-1853"},{"key":"9270_CR28","unstructured":"Sirigineedi, G., Tsourdos, A., Z\u02d9 bikowski, R., White, B.A.: Modelling and verfication of multiple UAV mission using SMV. In: Workshop on Formal Methods for Aerospace, FM2009, 16th International Symposium on Formal Methods (2009)"},{"key":"9270_CR29","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science, 2nd edn. Cambridge University Press, Cambridge, England (2004)","edition":"2"},{"issue":"1","key":"9270_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"SA Kripke","year":"1959","unstructured":"Kripke, S.A.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1\u201314 (1959)","journal-title":"J. Symb. Log."},{"key":"9270_CR31","first-page":"83","volume":"16","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical considerations on modal logic. Acta Philos. Fenn 16, 83\u201394 (1963)","journal-title":"Acta Philos. Fenn"},{"key":"9270_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer Publications (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9270_CR33","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"9270_CR34","unstructured":"Holzmann, G.J.: The Model Checker Spin. Addison-Wesley (2004)"},{"key":"9270_CR35","doi-asserted-by":"crossref","unstructured":"Coifman, B., McCord, M., Mishalani, R.G., Iswalt, M., Ji, Y.: Roadway traffic monitoring from an unmanned aerial vehicle. In: Proceedings of IEE Intelligent Transport Systems, vol. 153, pp. 11\u201320 (2006)","DOI":"10.1049\/ip-its:20055014"},{"key":"9270_CR36","doi-asserted-by":"crossref","unstructured":"Boskovic, J.D., Prakash, R., Mehra, R.K.: A multi-layer control architecture for unmanned aerial vehicles. In: Proceedings of the 2002 American Control Conference, pp.\u00a01825\u20131830 (2002)","DOI":"10.1109\/ACC.2002.1023832"},{"issue":"6","key":"9270_CR37","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1109\/TRA.2002.805653","volume":"18","author":"RW Beard","year":"2002","unstructured":"Beard, R.W., McLain, T.W., Goorich, M.A., Anderson, E.P.: Coordinated target assignment and intercept for unmanned air vehicles. IEEE Trans. Robot. Autom. 18(6), 911\u2013922 (2002)","journal-title":"IEEE Trans. Robot. Autom."},{"key":"9270_CR38","doi-asserted-by":"crossref","first-page":"3403","DOI":"10.1016\/j.cor.2005.02.011","volume":"33","author":"D Ahr","year":"2006","unstructured":"Ahr, D., Reinelt, G.: A tabu search algorithm for the min-max k-chinese postman problem. Comput. Oper. Res. 33, 3403\u20133422 (2006)","journal-title":"Comput. Oper. Res."},{"key":"9270_CR39","unstructured":"Osterhues, A., Mariak, F.: On Variants of the k-Chinese Postman Problem. Operations Research and Wirtschaftsinformatik, University Dortmund, No. 30 (2005)"},{"key":"9270_CR40","unstructured":"Burgard, W., Moors, M., Stachniss, C., Schneider, F.E.: Coordinated multi-robot exploration. IEEE Trans. Robotics 21(3), 376\u2013386 (2005)"},{"issue":"3","key":"9270_CR41","doi-asserted-by":"crossref","first-page":"497","DOI":"10.2307\/2372560","volume":"79","author":"LE Dubins","year":"1957","unstructured":"Dubins, L.E.: On curves of minimal length with a constraint on average curvature, and with prescribed initial and terminal positions and tangents. Am. J. Math. 79(3), 497\u2013516 (1957)","journal-title":"Am. J. Math."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9270-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-011-9270-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9270-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T06:21:27Z","timestamp":1741933287000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-011-9270-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["9270"],"URL":"https:\/\/doi.org\/10.1007\/s10472-011-9270-x","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2011,9]]}}}