|
11 AM, Seminar Hall Reachability in timed automata with diagonal constraints Sayan Mukherjee Chennai Mathematical Institute. 24-08-18 Abstract We study the reachability problem for timed automata having diagonal constraints (like x - y <= 5, w - x > 2, etc) as guards in transitions. Timed automata restricted to constraints of the form x <= 5, y >= 2 (that is, not having comparison of difference between clocks with a constant) are called diagonal-free automata. It is known that diagonal constraints do not add expressive power, but they could yield exponentially more succinct automata. This motivates the use of diagonal constraints in the modelling of real-time systems, as they could potentially give smaller models. However, existing algorithms for timed automata analysis are tuned for diagonal free constraints, and their naive extensions to the case of diagonal constraints have been shown incorrect. In this talk, we present a (correct) extension of the core algorithm for diagonal-free automata to the case of diagonal constraints. Joint work with Paul Gastin (ENS Paris-Saclay) and B Srivathsan (CMI)
|
