A Flexible and Efficient Temporal Logic Tool for Python: PyTeLo

Temporal logic is an important tool for specifying complex behaviors of systems. It can be used to define properties for verification and monitoring, as well as goals for synthesis tools, allowing users to specify rich missions and tasks. Some of the most popular temporal logics include Metric Temporal Logic (MTL), Signal Temporal Logic (STL), and weighted STL (wSTL), which also allow the definition of timing constraints. In this work, we introduce PyTeLo, a modular and versatile Python-based software that facilitates working with temporal logic languages, specifically MTL, STL, and wSTL. Applying PyTeLo requires only a string representation of the temporal logic specification and, optionally, the dynamics of the system of interest. Next, PyTeLo reads the specification using an ANTLR-generated parser and generates an Abstract Syntax Tree (AST) that captures the structure of the formula. For synthesis, the AST serves to recursively encode the specification into a Mixed Integer Linear Program (MILP) that is solved using a commercial solver such as Gurobi. We describe the architecture and capabilities of PyTeLo and provide example applications highlighting its adaptability and extensibility for various research problems.

Event-Triggered Control for Weight-Unbalanced Directed Networks

We develop an event-triggered control strategy for a weighted-unbalanced directed homogeneous robot network to reach a dynamic consensus in this work. We present some guarantees for synchronizing a robot network when all robots have access to the reference and when a limited number of robots have access. The proposed event-triggered control can reduce and avoid the periodic updating of the signals. Unlike some current control methods, we prove stability by making use of a logarithmic norm, which extends the possibilities of the control law to be applied to a wide range of directed graphs, in contrast to other works where the event-triggered control can be only implemented over strongly connected and weight-balanced digraphs. We test the performance of our algorithm by carrying out experiments both in simulation and in a real team of robots.

Non-Prehensile Manipulation of Cuboid Objects Using a Catenary Robot

Transporting objects using quadrotors with cables has been widely studied in the literature. However, most of those approaches assume that the cables are previously attached to the load by human intervention. In tasks where multiple objects need to be moved, the efficiency of the robotic system is constrained by the requirement of manual labor. Our approach uses a non-stretchable cable connected to two quadrotors, which we call the catenary robot, that fully automates the transportation task. Using the cable, we can roll and drag the cuboid object (box) on planar surfaces. Depending on the surface type, we choose the proper action, dragging for low friction, and rolling for high friction. Therefore, the transportation process does not require any human intervention as we use the cable to interact with the box without requiring fastening. We validate our control design in simulation and with actual robots, where we show them rolling and dragging boxes to track desired trajectories.

The Catenary Robot: Design and Control of a Cable Propelled by Two Quadrotors

Transporting objects using aerial robots has been widely studied in the literature. Still, those approaches always assume that the connection between the quadrotor and the load is made in a previous stage. However, that previous stage usually requires human intervention, and autonomous procedures to locate and attach the object are not considered. Additionally, most of the approaches assume cables as rigid links, but manipulating cables requires considering the state when the cables are hanging. In this work, we design and control a catenary robot. Our robot is able to transport hook-shaped objects in the environment. The robotic system is composed of two quadrotors attached to the two ends of a cable. By defining the catenary curve with five degrees of freedom, position in 3-D, orientation in the z-axis, and span, we can drive the two quadrotors to track a given trajectory. We validate our approach with simulations and real robots. We present four different scenarios of experiments. Our numerical solution is computationally fast and can be executed in real-time.