# zbMATH — the first resource for mathematics

Cyclic-routing of unmanned aerial vehicles. (English) Zbl 1423.68445
Summary: Various missions carried out by Unmanned Aerial Vehicles (UAVs) are concerned with permanent monitoring of a predefined set of ground targets under relative deadline constraints, i.e., the targets have to be revisited ’indefinitely’ and there is an upper bound on the time between two consecutive successful scans of each target. A solution to the problem is a set of routes – one for each UAV – that jointly satisfy these constraints. Our goal is to find a solution with the least number of UAVs. We show that the decision version of the problem (given $$k$$, is there a solution with $$k$$ UAVs?) is PSPACE-complete. On the practical side, we propose a portfolio approach that combines the strengths of constraint solving and model checking. We present an empirical evaluation of the different solution methods on several hundred randomly generated instances.
##### MSC:
 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) 68Q60 Specification and verification (program logics, model checking, etc.)
##### Keywords:
motion planning; computational complexity; model checking
##### Software:
ABC; AIGER; NuSMV; z3
Full Text:
##### References:
 [1] The \scCR-UAV problem home-page [2] Unmanned air vehicle systems association [3] Alighanbari, M.; Kuwata, Y.; How, J. P., Coordination and control of multiple UAVs with timing constraints and loitering, (Proceedings of ACC 2003, vol. 6, (2003), IEEE Press), 5311-5316 [4] Sundar, K.; Rathinam, S., Route planning algorithms for unmanned aerial vehicles with refueling constraints, (Proceedings of ACC 2012, (2012), IEEE Press), 3266-3271 [5] Yang, G.; Kapila, V., Optimal path planning for unmanned air vehicles with kinematic and tactical constraints, (Proceedings of CDC 2002, vol. 2, (2002), IEEE Press), 1301-1306 [6] Richards, A.; How, J. P., Aircraft trajectory planning with collision avoidance using mixed integer linear programming, (Proceedings of ACC 2002, vol. 3, (2002), IEEE Press), 1936-1941 [7] Drucker, N.; Penn, M.; Strichman, O., Cyclic Routing of Unmanned Air Vehicles, (2014), available from [1] [8] Basilico, N.; Gatti, N.; Amigoni, F., Developing a deterministic patrolling strategy for security agents, (Proceedings of WI-IAT 2009, (2009), IEEE Computer Society Press), 565-572 [9] Orlin, J. B., The complexity of dynamic languages and dynamic optimization problems, (Proceedings of STOC 1981, (1981), ACM Press), 218-227 [10] Pnueli, A., The temporal logic of programs, (Proceedings of FOCS 1977, (1977), IEEE Computer Society Press), 46-57 [11] de Moura, L.; Bjørner, N., Z3: an efficient SMT solver, (Proceedings of TACAS 2008. Proceedings of TACAS 2008, Lect. Notes Comput. Sci., vol. 4963, (2008), Springer-Verlag), 337-340 [12] Ho, H.-M.; Ouaknine, J., The CR-UAV problem is PSPACE-complete, (Proceedings of FoSSaCS 2015. Proceedings of FoSSaCS 2015, Lect. Notes Comput. Sci., vol. 9034, (2015), Springer), 328-342 · Zbl 1459.68077 [13] Drucker, N.; Penn, M.; Strichman, O., Cyclic routing of unmanned aerial vehicles, (Proceedings of CPAIOR 2016. Proceedings of CPAIOR 2016, Lect. Notes Comput. Sci., vol. 9676, (2016), Springer), 125-141 · Zbl 06598661 [14] Bar-Noy, A.; Ladner, R. E.; Tamir, T.; VanDeGrift, T., Windows scheduling of arbitrary-length jobs on multiple machines, J. Sched., 15, 2, 141-155, (2012) · Zbl 1280.90030 [15] Liu, C. L.; Layland, J. W., Scheduling algorithms for multiprogramming in a hard-real-time environment, J. ACM, 20, 1, 46-61, (1973) · Zbl 0265.68013 [16] Henzinger, T. A.; Manna, Z.; Pnueli, A., What good are digital clocks?, (Proceedings of ICALP 1992. Proceedings of ICALP 1992, Lect. Notes Comput. Sci., vol. 623, (1992), Springer), 545-558 [17] McMillan, K. L., Symbolic Model Checking, (1993), Kluwer · Zbl 0784.68004 [18] Sipser, M., Introduction to the Theory of Computation, (2012), Cengage Learning [19] Papadimitriou, C. H., The Euclidean traveling salesman problem is NP-complete, Theor. Comput. Sci., 4, 3, 237-244, (1977) · Zbl 0386.90057 [20] Christofides, N., Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, (1976), CMU, Tech. Rep. 388 [21] Baier, C.; Katoen, J.-P., Principles of Model Checking, (2008), MIT Press [22] Biere, A.; Cimatti, A.; Clarke, E. M.; Strichman, O.; Zhu, Y., Bounded model checking, Adv. Comput., 58, 117-148, (2003) [23] Doyen, L.; Raskin, J.-F., Antichains algorithms for finite automata, (Proceedings of TACAS 2010. Proceedings of TACAS 2010, Lect. Notes Comput. Sci., vol. 6015, (2010), Springer), 2-22 · Zbl 1284.68348 [24] Bohy, A., Antichain Based Algorithms for the Synthesis of Reactive Systems, (2014), University of Mons, Ph.D. thesis [25] Sinnott, R. W., Virtues of the haversine, Sky Telesc., 68, 158, (1984) [26] Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NuSMV2: an opensource tool for symbolic model checking, (Proceedings of CAV 2002. Proceedings of CAV 2002, Lect. Notes Comput. Sci., vol. 2404, (2002), Springer), 359-364 · Zbl 1010.68766 [27] Brayton, R. K.; Mishchenko ABC, A., An academic industrial-strength verification tool, (Proceedings of CAV 2010. Proceedings of CAV 2010, Lect. Notes Comput. Sci., vol. 6174, (2010), Springer), 24-40 [28] B. Sterin, Personal communication, 2014. [29] Biere, A., The AIGER and-inverter graph (AIG) format, available at [30] Biere, A., (2014), available at [31] Hassan, Z.; Bradley, A. R.; Somenzi, F., Incremental, inductive CTL model checking, (Proceedings of CAV 2012. Proceedings of CAV 2012, Lect. Notes Comput. Sci., vol. 7358, (2012), Springer), 532-547 [32] Emerson, E. A.; Sistla, A. P., Symmetry and model checking, Form. Methods Syst. Des., 9, 105-131, (1996) [33] Las Fargeas, J.; Hyun, B.; Kabamba, P.; Girard, A., Persistent visitation under revisit constraints, (Proceedings of ICUAS 2013, (2013), IEEE Press), 952-957 [34] Böckenhauer, H.-J.; Hromkovic, J.; Kneis, J.; Kupke, J., The parameterized approximability of TSP with deadlines, Theory Comput. Syst., 41, 3, 431-444, (2007) · Zbl 1148.68052 [35] Savelsbergh, M. W., Local search in routing problems with time windows, Ann. Oper. Res., 4, 1, 285-305, (1985) [36] Feinberg, E. A.; Curry, M. T., Generalized pinwheel problem, Math. Methods Oper. Res., 62, 1, 99-122, (2005) · Zbl 1093.90015 [37] Zhao, W.; Ammar, M. H.; Zegura, E. W., A message ferrying approach for data delivery in sparse mobile ad hoc networks, (Proceedings of MobiHoc 2004, (2004), ACM Press), 187-198 [38] Marathe, M. V.; Hunt, H. B.; Stearns, R. E.; Radhakrishnan, V., Approximation algorithms for PSPACE-hard hierarchically and periodically specified problems, SIAM J. Comput., 27, 5, 1237-1261, (1998) · Zbl 0911.68153
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.