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.