Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, Nathalie Sznajder
Temporal graphs are graphs where the presence or properties of their vertices and edges change over time. When time is discrete, a temporal graph can be defined as a sequence of static graphs over a discrete time span, called lifetime, or as a single graph where each edge is associated with a specific set of time instants where the edge is alive. For static graphs, Courcelle's Theorem asserts that any graph problem expressible in monadic second-order logic can be solved in linear time on graphs of bounded tree-width. We propose the first adaptation of Courcelle's Theorem for monadic second-order logic on temporal graphs that does not explicitly rely on a parameter proportional to the lifetime, or defined as the maximum number of time-edges incident with any vertex which in the worst case is higher than the lifetime. We then introduce the notion of derivative over a sliding time window of a chosen size, and define the tree-width and twin-width of the temporal graph's derivative. We exemplify its usefulness with meta-theorems with respect to a temporal variant of first-order logic. The resulting logic expresses a wide range of temporal graph problems including a version of temporal cliques, an important notion when querying time series databases for community structures.
Reach-avoid (RA) games have significant applications in security and defense, particularly for unmanned aerial vehicles (UAVs). These problems are inherently challenging due to the need to consider obstacles, consider the adversarial nature of opponents, ensure optimality, and account for nonlinear dynamics. Hamilton-Jacobi (HJ) reachability analysis has emerged as a powerful tool for tackling these challenges; however, while it has been applied to games involving two spatial dimensions, directly extending this approach to three spatial dimensions is impossible due to high dimensionality. On the other hand, alternative approaches for solving RA games lack the generality to consider games with three spatial dimensions involving agents with non-trivial system dynamics. In this work, we propose a novel framework for dimensionality reduction by decomposing the problem into a horizontal RA sub-game and a vertical RA sub-game. We then solve each sub-game using HJ reachability analysis and consider second-order dynamics that account for the defender's acceleration. To reconstruct the solution to the original RA game from the sub-games, we introduce a HJ-based tracking control algorithm in each sub-game that not only guarantees capture of the attacker but also tracking of the attacker thereafter. We prove the conditions under which the capture guarantees are maintained. The effectiveness of our approach is demonstrated via numerical simulations, showing that the decomposition maintains optimality and guarantees in the original problem. Our methods are also validated in a Gazebo physics simulator, achieving successful capture of quadrotors in three spatial dimensions space for the first time to the best of our knowledge.