This video shows the results of our paper titled "DoS-Resilient Multi-Robot Temporal Logic Motion Planning". This paper addresses the problem of how to design trajectories for a team of robots when operating in adversarial environments with denial-of-service (communication jammers) exist. The robots must maintain a multi-hop communication with the base stations at all time. We use a Satisfiability Modulo Convex (SMC) Programming solver to generate those trajectories.

These videos show the results of our paper titled "Scalable lazy SMT-based motion planning" and "Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming". Given a mission captured by Linear Temporal Logic (LTL) along with the robots' dynamics, states, and inputs constraints, our tool synthesizes trajectories that are guaranteed to satisfy the mission.

In the first video, we demonstrate the single robot case. The mission is "ALWAYS avoid the obstacles AND infinitely often visit the top right corner AND infinitely often visit the top left corner". The video shows the actual trajectory of the Quadrotor along with a simulation projecting the trajectory onto the workspace obstacles.

In the second video, we demonstrate the multi robot case with simple reach-avoid missions. Each robot needs to go from point A to point B without colliding with the obstacles while leaving some distance (safety distance) to other robots.

In the third video, we demonstrate the multi robot case with the following mission: (1) INFINITELY OFTEN: each robot should visit its charging station (right top corner and bottom left corner), (2) EVENTUALLY ALWAYS: one robot must be patrolling the middle corridor, and (3) ALWAYS: avoid the obstacles and leave safety distance of 1 meter from each other

This video shows the results of our papers titled "Secure state estimation under sensor attacks: A Satisfiability Modulo Theory approach" and "Secure State Reconstruction in Differentially Flat Systems under Sensor Attacks Using Satisfiability Modulo Theory Solving,". These papers focus on scenarios where measurements from various sensors are sent to a central unit to be fused together in order to detect and isolate malicious sensors. Once the malicious sensors are detected and isolated, one can estimate the state of the underlying physical system by using the data collected from the attack-free sensors. This technique is referred to as "secure state estimation".

In the first video: we simulate an active cruise control scenario in which the velocity measurements is under attack. Both red and blue cars are following the yellow car while maintaining a safe distance. The blue car is running our secure state estimator to filter out the attack signal and correctly estimate the car velocity. The red car estimates the velocity directly from the sensor measurements. As a consequence, when the attack strength increases, the error in state estimation increases forcing the red car to crash into the yellow one.

In the second video, we show an experiment where the information collected by some of the sensors are corrupted before it is fed to the controller. In the first part of the video, we show the case when our secure state estimation algorithm is not activated while the attack signal strength is increasing until the Quadrotor crashes. In the second part of the video, we show the same attack scenario when our secure state estimation algorithm is running and filtering out the attack signal.

This video shows the results of our paper titled "Non-invasive spoofing attacks for anti-lock braking systems". In this paper, we expose a largely unexplored vector of physical-layer attacks with demonstrated consequences in automobiles. By modifying the physical environment around analog sensors, an attacker can exploit weaknesses in automotive speed sensors in order to corrupt speed measurements and cause life-threatening situations.