Ramanathan S. Thinniyam (PhD student, IMSc, Chennai) visited LSV from August 19th to 26th, 2018. He worked with Philippe Schnoebelen on combinatorial aspects of embedding relations. In particular, there is a rich theory for embeddings between words or strings that could be leveraged when considering embeddings between trees or graphs.
S. Akshay (IIT Bombay) visited LSV from July 3rd to 13th. He worked with Paul Gastin on timed extensions of multithreaded recursive programs. Together with Sparsa Roy Choudhurry (PhD student at IITB) and S. Krishna (IITB), he is developing a tool to check non-emptiness of such systems under scope bounded restriction. Their approach via tree-width actually covers a much larger under-approximation than scope-bounded. They have obtained a mature theory for this timed extension and are actively developing a prototype tool.
K. Narayan Kumar (CMI) visited LaBRI June 17 to 24 to hold discussions with Pascal Weil. He also gave a seminar titled Verification of Asynchronous Programs with Locks. He then visited LSV June 25 to July 1st, to work with Benedikt Bollig, Marie Fortin and Paul Gastin on temporal logics for message sequence charts (MSCs). As a consequence of results obtained by Bollig, Fortin and Gastin which will appear in CONCUR’18, they obtained a two-dimensional temporal logic which is expressively complete for the first-order logic over MSCs. Their goal is to find a one-dimensional temporal logic which is also FO-complete. They proved that this is possible when restricting to bounded MSCs. They are currently investigating the unbounded case.
S. Krishna (IIT Bombay) visited LSV from June 3rd to 16th. She worked with Paul Gastin on an unambiguous version of the famous factorization forest theorem due to Imre Simon. They proved that, given a morphism to a finite semigroup, one can construct an unambiguous automaton with some nice properties. Then, applying a refined version of state elimination, one obtains an unambiguous regular expression such that each sub-expression E is mapped to a single semigroup element, which is moreover an idempotent if E^+ or E^ω is also a sub-expression. The construction works for both finite and infinite words. An article is in preparation.
The work on regular transducer expressions which appeared in LICS’18 is based on this unambiguous factorization forest.
B. Srivathsan (CMI) visited LaBRI June 1st to 29. He worked with Frédéric Herbreteau and Igor Walukiewicz on partial-order techniques for timed automata. Together with Govind Rajanbabu (co-tutelle Ph.D. student LaBRI/CMI), they develop new abstraction techniques for timed automata that take concurrency into account to improve verification algorithms. An article based on this work is in preparation. They are also working on improving their abstraction techniques by using partial order techniques.
Madhavan Mukund (CMI) visited LaBRI during May 14-25, 2018. He and Anca Muscholl (LaBRI) are jointly supervising the PhD thesis of Adwitee Roy, who was also visiting LaBRI during the summer of 2018. During this visit, some work was initiated in the area of synthesizing distributed negotiations from sequential specifications.
Madhavan Mukund then visited IRIF from May 28 to June 8 to work with Ahmed Bouajjani and Constantin Enea. This visit was part of the CEFIPRA project AVeCSo. Research discussions were on two ongoing topics: formalizing replicated data types that support multiple levels of consistency (joint work with Gautham Shenoy R. and S. P. Suresh, CMI) and verification techniques for formal models of web services (joint work with Nisarg Patel, M.Sc. student at CMI who was an intern at IRIF in May 2017).
M. Praveen visited LSV May 11 to 24. He continued the work with Alain Finkel on flat FIFO systems, initiated when Alain Finkel visited CMI in February 2018. Archit, the MSc student at CMI involved in this work, finished his MSc thesis based on a part of this work. M. Praveen also worked with Philippe Schnoebelen at LSV on characterizing functions which are weakly computable by grammar controlled vector addition systems, preparing a future submission.
B. Srivathsan visited LSV between May 2 – 18, and PhD student Sayan Mukherjee visited LSV between May 2 – 31, to work with Paul Gastin on simulation relations for timed automata with diagonal constraints. During this visit, they worked on a better formulation of their previous work on such a simulation relation, and extended it to a larger class of automata. Better algorithms for simulation tests between zones were discussed. An extended journal version of their preliminary results is in preparation.
Alain Finkel visited CMI January 30 to February 18, to work with M. Praveen and a M.Sc. student, Archit, on flat FIFO systems. He also participated in the Future Tour (February 1-2). He then traveled to IISc Bangalore, CSA Department February 19 to 23, to work with Deepak D’Sousa, K.V. Raghavan and Sriram Rajamani (the latter, Director of Microsoft India). They discussed the verification of concurrent programs and he gave two seminars at Bangalore on WSTS. Alain Finkel then proceeded to the CSE Department, IIT Bombay February 23 to March 12, to work with S. Akshay. He gave two lectures on WBTS and the famous Erdös-Tarski Theorem and a seminar on WSTS for the faculty members. He also was invited on February 28 by the research group on the verification of programs in Pune, and at the TCS Department, TIFR by Paritosh K. Pandya. He visited also the Homi Bhabha Centre for Science Education, Tata Institute of Fundamental Research, to share his research on the pedagogics of mathematics. Finally, he participated in the ENS Paris-Saclay delegation which visited the IITB on March 7.
Pascal Weil (LaBRI) visited CMI January 27 to February 2, 2018. He worked with Paul Gastin (LSV), Madhavan Mukund and K. Narayan Kumar on the organization of the future ReLaX events. He also participated in the Bonjour India event sponsored by Institut Français India. The previous week, he taught a class at the Mathematics Department of the University of Kerala at Kariavattom, under the Government of Kerala’s Erudite Program.
Xavier Goaoc (Université Paris Est) visited CMI from January 20 to 27, 2018. He worked with Priyavrat Deshpande on the organization of student exchanges between CMI and Université Paris Est, and gave three lectures, one of which was within a Computational Geometry Day at CMI, organized by Priyavrat Deshpande. He also initiated discussions with Samir Datta on algorithmic questions on geometric graphs, with M. Praveen on the geometric questions underlying some questions in verification, and with Priyavrat Deshpande on notions of topological complexity.
Shweta Bhandari (PhD student at MNIT Jaipur) visited LaBRI January 15 to 31, 2018. She worked with Akka Zemmari (LaBRI) on the use of typical paths and machine learning techniques to detect malware apps. They also worked (with Frédéric Herbreteau, LaBRI) on the use of model checking to detect data leakage in colluding apps.
Vineeta Jain (PhD student at MNIT Jaipur) visited LaBRI January 15 to 31, 2018. She worked with Mohamed Mosbah (LaBRI) on device-to-device attacks in Android, mainly focussed on attacks launched through evil twins in the network.
Paul Gastin (LSV) visited CMI January 10 to February 14. He worked with K. Narayan Kumar on the separation problem for first-order logic over message sequence charts (MSCs) which are behaviors of finite state distributed systems communicating via unbounded FIFO channels. They proved that in general first-order logic is not separable over MSCs. This negative result holds even for existentially bounded MSCs. In contrast, for universally bounded MSCs, they gave an inductive construction showing that FO is separable. During this visit, Paul Gastin also worked on timed systems with B. Srivathsan and Sayan Mukherjee (a jointly advised PhD student, more details here). They developed a symbolic reachability analysis for timed systems featuring diagonal constraints. The main difficulty is to extend the zone based approach to cope with diagonal constraints and in particular to check zone inclusion up to a simulation relation. This work resulted in a paper accepted at CONCUR’18.
Pascal Weil (LaBRI) visited CMI November 11 to 18, 2017, on the occasion of the formal signing of UMI ReLaX. He worked with Madhavan Mukund on the planification of the UMI’s activities.
Paul Gastin (LSV) visited IIT Bombay October 30 to December 23, 2017. He worked on combinator expressions with S. Krishna and Vrunda Dave (PhD student at IITB), and on timed systems with S. Akshay, S. Krishna and Sparsa Roy Choudhury (PhD student at IITB). More…
K. Narayan Kumar (CMI) visited LSV and IRIF June 25 to July 9 and again, July 16 to 22, 2017. He worked with Paul Gastin, revisiting the classical problems of expressive completeness and separation theorems for logics over words and Mazurkiewicz traces, with a view to extending these results to other partially ordered structures. He worked also with Ahmed Bouajjani and with M.F Atig (Uppsala Univ.) and P. Saivasan (Univ. Braunschweig) on the analysis of asynchronous programs with lock based synchronization.
S. Krishna (IIT Bombay) visited LSV June 29 to July 13, 2017. She worked with Paul Gastin on the analysis of timed systems, and with Patricia Bouyer-Decitre on stochastic timed games. Her visit was partially supported by Project AVeRTS. More…
S. Akshay (IIT Bombay) visited LSV June 26 to July 17, 2017. He worked with Paul Gastin, S. Krishna and others on the analysis of timed systems. His visit was partially supported by Project AVeRTS. More…
M. Praveen (CMI) visited LSV June 18 to July 1, 2017. He worked with Philippe Schnoebelen on characterizing functions weakly computable by grammar controlled vector addition systems, concentrating on proving that hyper-Ackermannian functions can be weakly computed. He also worked with Stéphane Demri on satisfiability of constraint LTL over ordered domains, concentrating on identifying problems that they can collaborate on in the coming months. He also worked with Alain Finkel, identifying potential topics for MSc thesis. The topics discussed consist of flattable FIFO systems and approaches for implementation of verification algorithms for counter systems.
C. Aiswarya (CMI) visited LSV June 1st to 25, 2017. She worked with Paul Gastin and Benedikt Bollig, on propositional dynamic logic on data words over an ordered domain, concentrating on questions of expressiveness and on the complexity of satisfiability.
Madhavan Mukund (CMI) visited LSV and IRIF May 13 to 26 2017. He participated in the 20th anniversary celebration of LSV and worked with Ahmed Bouajjani and Constantin Enea on formal models for session systems and new consistency notions for replicated data.
Didier Caucal (LIGM) visited IMSc April 1st to 22, 2017. He worked with Kamal Lodaya on monadic second-order decidability on the event structures of one safe Petri nets. They considered a property more general than that of the existence of a grid which had been considered by Thiagarajan. The restriction to the existence of a grid for the undecidability of the monadic theory remains to be established.
Philippe Schnoebelen (LSV) visited CMI January 4 to February 7 and February 18 to March 5, 2017. He gave a series of lectures on Algorithmic Aspects of WQO Theory and worked with M. Praveen (CMI) on grammar controlled vector addition systems, and with K. Narayan Kumar (CMI) on ideal-based data structures and algorithms for WQOs.
Paul Gastin (LSV) visited CMI January 1st to March 10, 2017. He worked with C. Aiswarya (CMI) on distributed control for asynchronous systems with Rendez-vous communication and on formal methods for the verification of distributed algorithms; with B. Srivathsan (CMI) on parity games; with Amaldev Manuel (CMI) and Govind (CMI Master student) on automata and logical characterizations of regular languages of undirected words. The specifications in logics (FO, MSO, …) use non-oriented predicates (e.g., neighbor instead of successor). The corresponding languages are closed under reverse. The goal is to find algebraic characterizations for such reversible regular languages.
Ahmed Bouajjani (IRIF) visited CMI January to February, 2017.