Model checking for real-time systems is a fundamental problem in formal verification. The goal here is to check whether a system (modelled using automata) satisfies a specification (provided by a logical formula). In the untimed setting, the approach to the model-checking problem involves reducing it to the reachability problem on the product of the automaton that models the system and the automaton corresponding to the negation of the logical formula. In the timed setting, a central challenge for model-checking is the  mismatch in formalisms used for modelling systems and specifications. While the behaviours of real-time systems are typically captured either using Timed automata or Automata with timers, the predominant formalism for capturing timed specifications is either Event clock automata (ECA) or logics such as Metric Interval Temporal Logic (MITL). Further, the translations between these different formalisms are usually quite expensive. Consequently, a framework that can simultaneously capture the features of various timed models (clocks, timers, event-clocks), and an efficient translation from timed logics to this framework would provide a single-shot solution to real-time verification, be it reachability analysis or model-checking of timed systems.

We propose a new model, called Generalized Timed Automata (GTA), that unifies the features of various models such as timed automata, event-clock automata, and automata with timers. The model comes with several powerful additional features, and yet, the best known zone-based reachability and liveness algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. Further, we propose a logic-to-automata translation from MITL to GTA. Our translation, which is modular, benefits from the powerful features of GTA that allow us to obtain automata with fewer states, transitions and clocks. Since most of the formalisms used for modelling real-time systems are also captured by GTAs, thanks to this translation, the model checking problem reduces to checking reachability for GTAs.

Based on the following works:

1. A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation. S. Akshay, Paul Gastin, R. Govind, Aniruddha R. Joshi and B. Srivathsan. International Conference on Computer Aided Verification (CAV) 2023.

2. MITL Model Checking via Generalized Timed Automata and a new Liveness Algorithm. S. Akshay, Paul Gastin, R. Govind and B. Srivathsan. International Conference on Concurrency Theory (CONCUR) 2024.

Short Bio: Govind is a postdoctoral researcher in the Algorithmic Verification group at the Department of Information Technology at Uppsala University. Before this, he was a postdoctoral research fellow at IIT Bombay. Prior to that, he did his Ph.D jointly at LaBRI, Université de Bordeaux and Chennai Mathematical Institute (CMI). His research is in formal methods, where, in particular, he is interested in in automata theory, logic, and automated synthesis, and its applications in formal verification.