BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1520
DTSTAMP:20250214T082427Z
SUMMARY:Model Checking for Real-time Systems using Generalized Timed Automa
 ta
DESCRIPTION:Speaker: Govind Rajanbabu (Uppsala University\, Sweden)\n\nAbst
 ract: \nModel checking for real-time systems is a fundamental problem in f
 ormal verification. The goal here is to check whether a system (modelled u
 sing automata) satisfies a specification (provided by a logical formula). 
 In the untimed setting\, the approach to the model-checking problem involv
 es 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 mode
 l-checking is the  mismatch in formalisms used for modelling systems and 
 specifications. While the behaviours of real-time systems are typically c
 aptured either using Timed automata or Automata with timers\, the predomin
 ant formalism for capturing timed specifications is either Event clock aut
 omata (ECA) or logics such as Metric Interval Temporal Logic (MITL). Furth
 er\, 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 a
 n efficient translation from timed logics to this framework would provide 
 a single-shot solution to real-time verification\, be it reachability anal
 ysis or model-checking of timed systems.We propose a new model\, called Ge
 neralized Timed Automata (GTA)\, that unifies the features of various mode
 ls such as timed automata\, event-clock automata\, and automata with timer
 s. The model comes with several powerful additional features\, and yet\, t
 he best known zone-based reachability and liveness algorithms for timed au
 tomata have been extended to the GTA model\, with the same complexity for 
 all the zone operations. Further\, we propose a logic-to-automata translat
 ion from MITL to GTA. Our translation\, which is modular\, benefits from t
 he powerful features of GTA that allow us to obtain automata with fewer st
 ates\, transitions and clocks. Since most of the formalisms used for model
 ling real-time systems are also captured by GTAs\, thanks to this translat
 ion\, the model checking problem reduces to checking reachability for GTAs
 .Based on the following works:\nA Unified Model for Real-Time Systems: Sym
 bolic Techniques and Implementation. S. Akshay\, Paul Gastin\, R. Govind\,
  Aniruddha R. Joshi and B. Srivathsan. International Conference on Compute
 r Aided Verification (CAV) 2023.\nMITL Model Checking via Generalized Time
 d Automata and a new Liveness Algorithm. S. Akshay\, Paul Gastin\, R. Govi
 nd and B. Srivathsan. International Conference on Concurrency Theory (CONC
 UR) 2024.\nShort Bio: Govind is a postdoctoral researcher in the Algorithm
 ic Verification group at the Department of Information Technology at Uppsa
 la 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 form
 al methods\, where\, in particular\, he is interested in in automata theor
 y\, logic\, and automated synthesis\, and its applications in formal verif
 ication.\n
URL:https://www.tcs.tifr.res.in/web/events/1520
DTSTART;TZID=Asia/Kolkata:20250218T160000
DTEND;TZID=Asia/Kolkata:20250218T170000
LOCATION:via Zoom in A201
END:VEVENT
END:VCALENDAR