PUBLIC VIVA-VOCE NOTIFICATION
Date and Time : Wednesday, 30 March 2022, 3:30 pm
Venue : CMI Seminar Hall (in hybrid mode)
Subject : Computer Science
Reachability in Timed Automata with Diagonal Constraints and Updates
Sayan Mukherjee
Chennai Mathematical Institute.
30-03-22

---

Abstract

Timed Automata (TA) are a popular model for real-time systems. TA extend finite-state automata with non-negative real valued variables, called clocks. Several extensions and restrictions of TA have been studied over the years and several decision problems have also been considered over these models. This thesis deals with the classic reachability problem in TA and in an extended class of TA called Updatable Timed Automata (UTA). UTA extend TA by allowing transitions to set values of clocks to richer expressions than resetting to only 0, as is the case in TA.

Reachability is undecidable in UTA. However, there are several (interesting) subclasses of UTA that retain decidability. There exists an efficient ‘zone’ based algorithm for checking reachability in TA without diagonal constraints (expressions comparing difference of two clocks with an integer). This thesis extends this zone based algorithm to handle diagonal constraints and (some of the) updates. In order to extend the zone based algorithm, this thesis proposes a new simulation relation between zones and provides a procedure to employ this relation inside the zone based algorithm. A prototype implementation has been done in the tool TChecker. Preliminary experiments show promising gains.