2017, Paul Gastin’s visit

During his visit, Paul Gastin worked with
S. Krishna (IITB) and Vrunda Dave (PhD student @ IITB) on combinator expressions. The goal is to have a formalism similar to weighted rational expressions ensuring functionality and expressively equivalent to MSO-transductions and two-way functional transducers. Interestingly, our proof uses an unambiguous version of Simon’s forest factorization theorem.
S. Akshay, S. Krishna and Sparsa Roy Choudhury (PhD student @ IITB) on a generic approach to lift existing decision procedures on untimed systems to similar systems enhanced with real-time clocks. The approach is based on tree-width and decision procedures are obtained via tree automata. Based on this, we are also developing a tool to check emptiness of timed systems such as timed automata, pushdown timed automata, multi-pushdown timed automata with suitable restrictions (bounded context, bounded scope, bounded phase, …).
S. Akshay, Vincent Jugé (LIGM) and S. Krishna on logical definability of realizability for graphs with timing constraints. The logical definability of realizability is a key ingredient when using the tree-width and tree automaton technique to check emptiness of timed systems. We show that realizability is MSO-definable for sequential systems, but not for distributed systems even when restricted to two sequential threads. We define a natural restriction (triangulation with timed-bounded cycles) and show that realizability is MSO-definable for distributed systems under this restriction. MSO-definability gives decidability but does not result in good complexity upper-bounds. We also prove the definability of realizability in the logic EQ-LCPDL (Existentially Quantified Propositional Dynamic Logic with Loop and Converse). This results in many cases in optimal complexity upper-bounds such as PSPACE or EXPTIME depending on the timed system under study.