Research Interests

My primary research interest lies in studying formal logics, infinite-state models, and their interconnections, which are critical in theoretical computer science and formal methods.

1. Specification and Verification of Timed Systems:
   To specify real-time constraints, Linear Temporal Logic (LTL) was extended to Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL). However, fundamental problems like satisfiability and model checking for these logics are undecidable. My doctoral research focused on pushing the boundaries of decidability for Metric Logics. I extended decidable subclasses of MTL using different natural modalities maintaining decidability while enhancing expressive capabilities. Currently, my focus is on exploring natural decidable subclasses of TPTL and Alternating Timed Automata (ATA), advancing towards a unifying theory of decidable timed logics.
2. Network-Controlled Cyber-Physical Systems (NCPS):
   In classical closed-loop control systems, continuous communication between the plant and controller is assumed. With the rise of the Internet of Things (IoT), many systems are transitioning to network-controlled cyber-physical systems (NCPS), where communication may not be continuous. At Delft University of Technology, my focus was on designing schedulers for event-triggered control systems using techniques from games on automata. Currently, I am interested in the theory of automated scheduler/controller synthesis robust against network delays.
3. Formal Logics and Models of Computation:
   At MPI-SWS, I expanded my research to include the formal analysis of Vector Addition Systems (equivalently Petri Nets) and Counter Machines, as well as fundamental problems related to First-Order Logic. Notably, we developed an efficient quantifier elimination procedure for Presburger Arithmetic that eliminates a block of existentially quantified variables in singly exponential time, contradicting a previously published lower bound result by Weispfenning (in 1997) claiming that any such algorithm requires doubly exponential time. Currently, I am interested in exploring connections between classical first-order logic and decidable timed logics.