2017, Umesh Kumar’s internship

A timed automaton is called robust if it accepts all timed words robustly, which in topological semantics means that for every accepted timed word, there is a neighbourhood around it which is also accepted. This interpretation leads to two notions of robustness: one in which we care about a particular path and an other in which we allow a close timed trajectory to take a different path. Umesh reduced path specific robustness checking to emptiness checking and also studied the decidability of language equivalence between an automaton and its interior, in which all the guards are replaced by their strict counterparts.

Updatable timed automata allow the possibility to update the clocks in a more elaborate way than simply resetting them to zero. Various subclasses were studied in the paper [BDFP04]. Umesh understood the expressiveness of updatable timed automata and proposed a construction of a classical timed automata with only resets, to establish the equivalence between classical timed automata and updatable timed automata with diagonal free constraints but allowing diagonal updates.