Projects

During the course of both my studies and professional career, I have been fortunate to work on very diverse topics. This page contains a summary of some projects that I have been recently working on.

Safety-critical control via robust controlled invariant sets

A safety enforcing controller should indefinitely keep the state of the system within a set of safe states. One way to achieve this is by initializing the state of the system inside a (Robust) Controlled Invariant Sets (RCIS) within the set of safe states as starting any trajectory in an RCIS allows one to force it to remain there.

A novel algorithm is proposed to compute an implicit representation of an RCIS in the space of states and control inputs in closed-form. This representation can be readily used for solving safety-critical control problems, such as the supervisory control problem, where a nominal input is corrected if it is considered unsafe. The closed-form expression allows the computation of different implicit RCISs online, e.g., for dynamic settings where the safe set changes. Alternatively, if the safe set is known a-priori and not changing, the implicit representation can be projected (offline) onto the state space to obtain an RCIS.

In practice the use of the implicit representation is only limited by the size of an optimization problem one affords to solve.
I also developed a MATLAB and C++ library found this repo, which was tested on the obstacle-avoidance problem for drones.

Relevant publications:

• T. Anevlavis, Z. Liu, N. Ozay, and P. Tabuada, Controlled invariant sets: implicit closed-form representations and applications, IEEE Transactions on Automatic Control.
• Z. Liu, T. Anevlavis, N. Ozay, and P. Tabuada, Automaton-based implicit controlled invariant set computation for discrete-time linear systems,” In 2021 IEEE 60th Conference on Decision and Control (CDC).
• L. Pannocchi, T. Anevlavis, and P. Tabuada, Trust your supervisor: quadrotor obstacle avoidance using controlled invariant sets,” In 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS).
• T. Anevlavis, Z. Liu, N. Ozay, and P. Tabuada, An enhanced hierarchy for (robust) controlled invariance,” In 2021 American Control Conference (ACC).
• T. Anevlavis and P. Tabuada, A simple hierarchy for computing controlled invariant sets,” In Proceedings of the 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC ’20).
• T. Anevlavis and P. Tabuada, Computing controlled invariant sets in two moves,” In 2019 IEEE 58th Conference on Decision and Control (CDC).

Relevant publications:

• T. Anevlavis, M. Philippe, D. Neider, and P. Tabuada, Being correct is not enough: efficient verification using robust linear temporal logic,” ACM Transactions on Computational Logic, 2022.
• T. Anevlavis, D. Neider, M. Philippe, and P. Tabuada, Evrostos: The rLTL Verifier,” In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC ’19).
• T. Anevlavis, M. Philippe, D. Neider, and P. Tabuada, Verifying rLTL formulas: now faster than ever before!,” In 2018 IEEE Conference on Decision and Control (CDC).

rLTL: Formally reasoning about correctness and robustness in verification

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. The logic rLTL provides a means to formally reason about both correctness and robustness in system design. As a multi-valued logic it augments the classic LTL in terms of expressiveness, the ability to describe robustness, and the fine-grained information it brings to the process of system verification.

My work was focused on making verification using rLTL accessible, so that the advantages of this logic can be practical. First, I identified a large fragment of rLTL for which the complexity of verifying an rLTL formula φ is at most O(3^|φ|), where |φ| is the length of φ. This result improves the previously known bound of O(5^|φ^|) is closer to the LTL bound of O(2^|φ|). Secondly, I developed the first rLTL model-checking software, Evrostos, which can be found in this repo.

Case studies with Evrostos show that the advantages of rLTL come at a low computational overhead when compared to LTL verification.

Computer vision for autonomous vehicles perception

Github Repos: AV Lane Detection, PackNet Monocular Depth Estimation

Trying to understand how one can enable an autonomous vehicle to "see", I played around with classic computer vision algorithms for:

1. Camera calibration;
2. Ego-lane detection;
3. Camera view to bird's eye view transformation.

Modules for self driving cars

Github Repos: EKF, Path-Planning, MPC
(Udacity's Self-Driving Car Engineer Nanodegree program).

While on the topic of autonomous vehicles, I have experience applying control theoretic approaches towards creating controllers for self-driving cars. More specifically I implemented:

1. An Extended Kalman Filter module to estimate the state of moving cars based on noisy LiDAR and RADAR data.
2. A path planning module for the car to safely navigate in a highway with other traffic. The planner takes into account a target velocity, road speed limits, and state/actuation constraints. Sensor fusion measurements are used to predict the evolution of the surrounding environment. The planner outputs waypoints for the car to follow.
3. A non-linear model predictive controller for path following. The cost function was designed to represent a trade-off between accuracy in path following, fuel efficiency, and driving comfort. The above modules were all implemented in C++ and validated in a realistic highway simulator from Unity.