Short-term visitors

2024

Sreejith A.V. (IIT Goa) will visit LaBRI from April to July 2024 to work with Vincent Penelle. His visit is supported by the Visiting Scholars program of the University of Bordeaux. They will work on formal verification of adaptive control algorithms.

Patrick Polo (IMJ-PRG) will visit CMI January 7-27, 2024. He will teach a 10-session course on schemes in reductive groups, and will continue his collaboration with V. Balaji (CMI), Yashonidhi Pandey (IISER Mohali) and Rajarshi Ghosh (CMI) on n-schemes in Bruhat-Tits groups.

2023

Paul Gastin, November 2 to December 16, IIT Bombay

Xavier Caruso

Madhavan Mukund at ACTS

Prakash Saivasan at ACTS

K. Narayan Kumar at ACTS

Aiswarya C.

Howard Straubing

Balthazar Charles (Ph.D. student, LISN, Univ. Paris-Saclay)

Patrick Polo (IMJ-PRG) visited CMI from August 6 to September 6, 2023. He taught a 10-session course on schemes in reductive groups, which will be published in CMI’s lecture notes. He also started collaborating with V. Balaji (CMI), Yashonidhi Pandey (IISER Mohali) and Rajarshi Ghosh (CMI) on n-schemes in Bruhat-Tits groups. Patrick will return to CMI January 7-27, 2024, to further this collaboration and for a second 10-session course.

Arnab Sur (Ph.D. student, CMI) was in France from June 5 to July 13. He mainly worked with Benjamin Monmege (LIS) on the synthesis of asynchronous timed and untimed automata. During his visit to Marseille, he traveled to LaBRI from June 26 to June 30, where he worked on the implementation of parametric timed automata verification in the tool TChecker with Frédéric Herbreteau (LaBRI).

Biswajyoti Saha (IIT Delhi) visited IMJ-PRG June 19 to xxx. There, he continued his work with Patrice Philippon on the Schanuel conjecture, which predicts the algebraic independence of particular values of arithmetic functions arising in geometry.

Malay Mandal (Ph.D. student, CMI) visited IMJ-PRG, February 15 to April 15, 2023. He worked with Pierre Fima on the KK-theory of a certain non-commutative unitary algebra. During his stay in Paris, Malay attended two working seminars and gave a talk.

Jacques Sakarovitch (CNRS, IRIF and Telecom Paris)) visited CMI from January 1st to March 3rd, 2023. He taught a 2-month course on the theory of transducers and weighted automata.

2022

Patricia Bouyer-Decitre (LMF) visited Chennai in December 2022 to work with researchers from CMI, especially B Srivathsan. She was a plenary lecturer at FSTTCS, which took place at IIT Madras.

Paul Gastin (LMF) visited IIT Mumbai, November 14 to December 18, 2022. He worked with:
– S Akshay (IIT Bombay), R. Govind (post-doc at IIT Mumbai), Aniruddha R Joshi (Master student at IIT Mumbai) and B Srivathsan (CMI) on a unified model for real-time systems. This general model includes both history clocks as in classical timed automata and future clocks extending both timers and event predicting clocks. We developed a new simulation-based zone algorithm for checking reachability in this unified model. This is the first algorithm that can handle simultaneously all of the timed features above. We also worked on a prototype implementation for our model and show experimental results on several benchmarks. Our general model can be used for model-checking event-clock specifications over systems described by timed automata.
– S. Krishna (IIT Bombay), R. Govind and Luc Dartois (LaCL, Univ. Paris Est Créteil) on the generalisation to sweeping transducers of a result by Straubing stating that if a language is both regular and definable in FO[Num] (first-order with arbitrary numerical predicates) then it is also definable in FO[<,mod] where, in addition to the order <, the numerical predicates are restricted to modulo (regular) predicates.
– Bharat Adsul (IIT Mumbai), Kulkarni Shantanu (PhD student at IIT Mumbai) and Pascal Weil (ReLaX) on the decomposition of asynchronous automata for Mazurkiewicz traces. In a previous work, we proved that every regular trace language can be accepted by a cascade product of the gossip asynchronous automaton, a well-known device introduced by Mukund-Sohoni in 1997, followed by a sequence of local asynchronous automata (a local automaton only reads the sequence of events executed by one of the sequential process in the system). This work resulted in a paper which appeared in CONCUR’22. This left open the case of the gossip asynchronous automaton itself. Is it possible to obtain such an automaton as a composition of local and simple asynchronous automata. The problem is related to the expressivity of a basic propositional dynamic logic (PDL) for traces without constants allowing to compare the relative order of last events of processes, which is the very purpose of the gossip automaton. We started working on this question during this visit. The work was continued during the visit of Paul Gastin to CMI in 2024.

R. Govind (IIT Mumbai) visited LMF from September 7 to October 31, 2022, and INRIA Rennes from September 30 to October 7, 2022. He worked

• • with Paul Gastin (LMF), S. Krishna (IIT Bombay) and Luc Dartois (LaCL, Univ. Paris Est Créteil) on regular transducers, especially on the efficient transformation of regular transducer expressions (RTEs) to machine models such as two-way transducers. This is a follow-up of recent work, where they proposed an efficient construction of a two-way reversible transducer (2RFT) equivalent to a given RTE, the first known elementary procedure that translates an RTE to a transducer. The plan, this time, is to work on adapting the construction for the full fragment of RTE, which also allows function composition as an operator of the RTE syntax. While this does not increase expressiveness, it would be quite useful in practice. They also plan to investigate if their construction can be adapted to work for infinite words.
  • with S Akshay (IIT Bombay) and B Srivathsan (Chennai Mathematical Institute) on efficient verification procedures for Event Clock Automata. In a recent work, they proposed a first step towards an implementation of a reachability procedure for ECAs, by proposing a zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. They were able to adapt the state-of-the-art technology such as zone graph computation and the G-simulation to the setting of ECAs. During this visit, the plan is to work on extending that approach to more general models such as event clock automata with diagonal constraints, and to work on the implementation of the zone based technique in the open source model checking tool TChecker. The performance benefits observed for the G-simulation-based reachability procedures for timed automata supports the belief that an implementation of their algorithm would also yield good results.
  • with Loïc Hélouët at INRIA Rennes, on extending the work on resilience of timed systems to the more general setting of timed hyperproperties.

B Srivathsan (CMI) visited LaBRI September 5 to 10, 2022 and LMF September 19 to 21, 2022. At LaBRI, he worked with Frédéric Herbreteau and Igor Walukiewicz on Partial-order reduction (POR) techniques. POR have been successfully applied to mitigate the state-space explosion problem that arises in verification of parallel programs. Applying these techniques to real-time software is however still a challenge. In two recent publications, we have introduced a framework that enables partial-order reduction based verification of timed automata. The next step, and objective of this visit, is to design POR techniques that lift timed verification algorithms to parallel real-time models which are out of reach of current state-of-the-art techniques. At LMF, he worked with Paul Gastin (together with R. Govind from IIT Mumbai) on the continuation of their recent work on simulations for event-clock automata. Srivathsan also worked with Patricia Bouyer-Decitre on simulations for weighted timed automata, which is the subject of the Masters’ project of Hrishikesh Balakrishnan (M.Sc student at CMI).

Adnane Khattabi (LaBRI) visited CMI August 15-30. He interacted especially with S.P. Suresh and Madhavan Mukund, on topics related to his ongoing PhD work in distributed algorithms. He is particularly interested in fault tolerance and relaxation of various shared objects in the quest for efficient implementations.

Julian Rüth visited IMSc and CMI from July 24 to August 27. With others he organized the Sage Days #114 at IMSc (July 25-27). He then organized, with Samuel Lelièvre — who visited IMSc and CMI August 15-30 —, a Sage Club at CMI and IMSc during the following 4 weeks. Both particularly interacted with Amritanshu Prasad (IMSc) and with PhD students and postdocs working with him.

Shibashis Guha (TIFR, Mumbai) visited LMF from June 20th to June 27th to initiate a collaboration with Dietmar Berwanger and Laurent Doyen on stochastic games with quantitative objectives.

Krishna Menon (PhD student, CMI) visited LaBRI and LORIA, June 5 to July 2nd. At LaBRI, he worked with Jean-Christophe Aval (LaBRI) on the question whether the chromatic quasisymmetric function distinguishes directed paths. He also attended the Journées de combinatoire de Bordeaux. At LORIA, he worked with Xavier Goaoc on independent sets in graphs, order types, and the principle of inclusion-exclusion. In between LaBRI and LORIA, Krishna attended Polytopes in Paris and more: Geometry, Combinatorics and Optimization.

S. Krishna (IIT Mumbai) visited LMF in May to continue her work with Paul Gastin and others on the problem of efficiently constructing a reversible transducer given by an RTE (regular transducer expression). One important question left open was how to handle composition as an operation on RTEs. Existing solutions did not preserve the complexity bound. While composition is an extremely useful operation to have, it is quite challenging to  construct a reversible transducer for the full fragment of RTE which also allows composition.

Bharat Adsul (IIT Mumbai) visited LMF and LaBRI.

Jacques Sakarovitch (IRIF) visited CMI March 15 to 29. He interacted with Pascal Weil and C. Aiswarya on topics in automata theory, in the context of the preparation of a course he will teach at CMI in 2023.

Enric Ventura (Univ. Polit. Catalunya) visited CMI February 27 to March 8 2022. He worked with Pascal Weil and Mallika Roy on algorithmic problems in free groups, and with Mallika Roy and Oorna Mitra on the twisted conjugacy problem in Baumslag-Solitar groups.

2021

Pascal Weil (LaBRI) visited IIT Mumbai December 6 to 9, 2021. He worked with Bharat Adsul (IIT Mumbai), Paul Gastin (LMF) and  Saptarshi Sarkar (IIT Mumbai) on the decomposition of asynchronous automata for Mazurkiewicz traces.

Paul Gastin (LMF) visited IIT Mumbai November 4 to December 10, 2021.  He worked with:

• S. Krishna (IIT Mumbai), R. Govind (post-doc at IIT Mumbai) and Luc Dartois (LaCL, Univ. Paris Est Créteil) on efficient constructions of reversible transducers from regular transducer expressions (RTE). This work started with S. Krishna’s visit to LMF from Oct. 22nd to Nov. 6th. It is very common and convenient to use RTEs as a specification language and we need to transform them into machines (transducers) for algorithmic applications. It  was already known that RTEs have the same expressive power as 2-way deterministic transducers (2DFT) but the existing constructions were inductive and incurred an exponential blow-up at each step, making them unsuitable in practice for applications. We were able to design an efficient construction from RTEs to two-way reversible finite-state transducers (RFT). In the most general case, the size of the constructed RFT is doubly exponential in the size of the given RTE. When the RTE does not use Hadamard products or chained-stars, the size is single exponential. This work resulted in a paper which appeared in LICS’22.
• S. Akshay (IIT Mumbai), R. Govind (post-doc at IIT Mumbai) and B. Srivathsan (CMI) on an efficient reachability algorithm for event-clock automata (ECA). ECA is a well-known class of timed systems enjoying admirable theoretical properties (e.g., determinisability) and very convenient to capture timed specifications. Unlike timed automata there exist no efficient algorithm which could be implemented in a tool for analysing reachability problems for ECAs. This is due to the difficulty in adapting zone based algorithms, critical in the timed automata setting, to ECAs. We proposed a new definition of zones for ECAs and developed an algorithm for the reachability problem in ECAs. Termination of the algorithm, which is one of the main difficulty, is based on a new simulation relation on ECA-zones. This work resulted in a paper which appeared in CONCUR’22.
• Bharat Adsul (IIT Mumbai), Saptarshi Sarkar (PhD student at IIT Mumbai) and Pascal Weil (LaBRI, Univ. Bordeaux and IRL ReLaX) on the decomposition of asynchronous automata for Mazurkiewicz traces. To address this problem, we first developed a propositional dynamic logic (PDL) for traces and proved that it is expressively complete for regular trace languages. This logic is past-oriented, but indeed there is a symmetric future-oriented version which is also expressively complete. Such logics are extremely convenient for specifications, much easier to use than other expressively complete logics such as the monadic second order logic (MSO) on traces. The definition of the logic and the expressive completeness result is therefore of independent interest: it allows for a powerful and easy to use specification language. Our second main result is the fact that every regular trace language can be accepted by a cascade product of the gossip asynchronous automaton, a well-known device introduced by Mukund-Sohoni in 1997, followed by a sequence of local asynchronous automata (a local automaton only reads the sequence of events executed by one of the sequential process in the system). This is a new proof and a strengthening of the famous and deep theorem by Zielonka (1987) showing that regular trace languages can be accepted by deterministic asynchronous automata. This work resulted in a paper which appeared in CONCUR’22.

S. Krishna (IIT Mumbai) visits LMF  from October 22 to November 6, 2021, to work with Paul Gastin on the problem of efficiently constructing a reversible transducer given by an RTE (regular transducer expression). The objective was to construct of a suitable parser (1NFT / 2RFT) which parses a word w given an RTE. Depending on the expressiveness of the starting RTE, the parser can be 1 NFT/2RFT.  This was one of the crucial steps in obtaining an overall efficient construction. 

2020

Pascal Weil (LaBRI) visited CMI March 10 to 16, 2020. He worked with Madhavan Mukund on the governance of UMI ReLaX. This visit was perturbed, and eventually cut short, by the CoViD-19 crisis.

Varun Ramanathan (LaBRI) visited CMI February 3 to 21, 2020. He worked with M. Praveen on expanding queries on graph databases with data value constraints. He also worked with B. Srivathsan on an MSO logic for characterizing certain sub-classes of rational relations. Finally, he gave a talk on the alternation hierarchy of synchronous relations.

Sinnou David (IMJ-PRG)  visited IMSc January 27 to March 19, 2020, to work with Sanoli Gun on supersingular primes of elliptic curves. The visit, initially scheduled till June 2020 was cut short after the closure of institutes in view of the then upcoming pandemic. Co-guidance plans of a student (N. Khandil) were discontinued and two students from CMI wishing to go for internship also discontinued their project. However an undergraduate student (Akash Roy) and a postgraduate fellow (Abhishek T. Bharadwaj) continue their projects through regular video-conferencing meetings. Roy works on the recent advances on the Schinzel-Zassenhauss conjecture and Bharadwaj works on the Villegas conjecture.

Paul Gastin (LSV) visited IIT Bombay January 24 to February 8, 2020. He worked with

– Luc Dartois and S. Krishna on star-free regular expressions for first-order definable regular functions, or equivalently functions definable by aperiodic transducers. Instead of the classical unrestricted Kleene star, the idea is to restrict iteration to functions whose domains is a prefix code with bounded synchronization delay. This is inspired by Schützenberger’s characterization of aperiodic languages by regular expressions with this restricted iteration.

– Bharat Adsul, Saptarshi Sarkar (PhD student), and Pascal Weil on wreath/cascade products and related decomposition results for the concurrent setting of Mazurkiewicz traces.

Paul Gastin (LSV) visited CMI January 7 to 23, 2019. He worked with

– C. Aiswarya on the complexity of the evaluation problem for weighted tiling systems for graphs. The evaluation problem is, given a weighted tiling system and a graph, to compute the weight of the graph. We study the complexity of the evaluation problem and give tight upper and lower bounds for several commutative semirings.  Further  we provide an efficient evaluation algorithm if the input graph is of bounded tree-width.

– Sayan Mukherjee and B. Srivathsan on the reachability problem for updatable timed automata (UTA). we get (1) an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modeling schedulability problems, (2) an algorithm for clock-bounded reachability using zones and simulations for the entire class of UTA, and (3) an improvement over the static analysis procedure for classical (reset) timed automata that is implemented in state-of-the-art tools. We have implemented our procedure in the tool TChecker.

– K. Narayan Kumar on first-order logic and temporal logic for message sequence charts (MSC). We proved that FO is separable over universally bounded MSCs. We also defined a natural temporal logic over MSCs and proved that it has the same expressive power has first-order logic over existentially bounded MSCs.

2019

Béatrice Bérard (LIP6, Sorbonne Université) visited CMI from December 15 to December 21, 2019. She worked with B. Srivathsan, C. Aiswarya, and Benjamin Monmege (LIS), on the local vs global semantics  for networks of timed automata, and the associated languages. She also gave a seminar on the  verification of hybrid systems and discussed the techniques related to o-minimality with two students.

Benjamin Monmège (LIS, Aix-Marseille Université) attended FSTTCS 2019 in Bombay, and then visited CMI from December 15 to December 21, 2019. He worked with B. Srivathsan, C. Aiswarya, and Béatrice Bérard (LIP6), on the languages recognised by networks of timed automata. He also discussed with C. Aiswarya a possible link between evolutionary game theory and the synthesis of distributed algorithms.

Anca Muscholl (LaBRI) traveled to Mumbai December 11-15, 2019, to attend FSTTCS 2019 and GALA 2019, where she delivered a talk  about transducers. She worked with S. Krishna (IITB) and Sougata Bose (PhD student at LaBRI) on resynchronizations  of transducers.

Vincent Penelle (LaBRI) visited IIT Goa December 10 to 20, 2019 to work with Sreejith A.V. They mainly worked with Prince Matthew, PhD student at IIT Goa, on a project initiated last year about a procedure to effectively compute downward closure of a language if a certain pumping lemma is satisfied (and its application to one-counter automata), and on a new project whose goal is to study the equivalence problem for probabilistic one-counter automata. Vincent and Sreejith discussed with Meenakshi D’Souza (IIIT Bangalore) on a potential future project with an industrial partner, to develop a verification tool for the plugin stateflow of Mathlab. Finally, they discussed the work initiated last year with Gabriele Puppis (University of Udine) on transducers on words over linear countable ordering.

Alain Finkel (LSV) visited IIT Bombay December 9-21, 2019, to work with S. Akshay and they worked on FIFO models. Ekanshdeep Gupta, a student of CMI, presented a common work on well structured Presburger counter machines (done during his second year internship at LSV in May-July, 2019) at FSTTCS 2019. He also participated to GALA 2019.

Paul Gastin (LSV) visited IIT Bombay from December 8 to 16, 2019, to co-chair  the international conference FSTTCS’19 which took place at IITB.

Marc Zeitoun (LaBRI) traveled to Kochi December 7 to 13, 2019 to attend ICSAA 2019, where he gave a lecture on the star-free closure operation.

Pascal Weil (LaBRI) visited CMI December 3 to 22, 2019. He worked with Madhavan Mukund on the governance of UMI ReLaX, and with Partha Mukhopadhyay on weighted automata. During his stay, he traveled to Kerala to attend ICSAA 2019 and ICART 2019, and to give a talk at the latter meeting.

Gabriele Puppis (formerly LaBRI, now University of Udine, Italy) traveled to Mumbai November 30 to December 11, 2019, to work with S. Krishna (IITB) and Sougata Bose (PhD student at LaBRI), as well as to attend FSTTCS 2019.

Paul Gastin (LSV) visited CMI from November 23 to December 7, 2019. He worked with:
– C. Aiswarya on weighted tiling systems for graphs. These systems represent functions from graphs to a commutative semiring such as the Natural semiring or the Tropical semiring. The system labels the nodes of a graph by its states, checks whether the neighbourhood of every node belongs to a the set of  permissible tiles, and assigns a weight accordingly. The weight of a labeling is the semiring-product of the weights assigned to the nodes, and the weight of the graph is the semiring-sum of the weights of labelings. We show that we can model interesting algorithmic questions using this formalism — like computing the clique number of a graph  or computing the permanent of a matrix.

– Sayan Mukherjee and B. Srivathsan on the reachability problem for
updatable timed automata (UTA), which are extensions of classical timed automata that allow special updates to clock variables on transitions, like x:= x – 1, x := y + 2, etc.  Reachability for UTA is undecidable in general.  Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed; second, reachable sets of configurations, called zones, are enumerated. They improve the algorithm for the static analysis: their method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective.

Paul Gastin (LSV) visited IIT Bombay from November 10 to 23, 2019. He worked with S. Akshay, S. Krishna and Sparsa Roy Choudhury (PhD student at IITB) on Boolean programs with multiple recursive threads which can be captured as pushdown automata with multiple stacks. They propose a new class of bounded underapproximations for multipushdown systems, which subsumes most existing classes.  They develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations.  They implement it in their tool TRIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway, TRIM solves the binary reachability problem in pushdown automata.  To show the versatility of this approach, they then extend their algorithm to the timed setting and provide the first implementation that can handle timed multi-pushdown automata with closed guards.

Sougata Bose (LaBRI, PhD student with  Anca Muscholl and Gabriele Puppis)  visited IIT Bombay from November 5 to December 15, 2019. During this period, he worked with S. Krishna (IITB) and his advisors Gabriele Puppis (Udine University) and Anca Muscholl (LaBRI), who were also visiting IITB, on one-way resynchronizability of transducers. He also visited CMI January 6 to 8, 2020 where he gave a talk on Resynchronization for Word Transducers with Origin Information.

B. Srivathsan (CMI) and Sayan Mukherjee visited LSV September 23 – 27, 2019 to work with Paul Gastin on extending their recent work on algorithms for updateable timed automata. He then moved on to LaBRI, from September 27 to October 11, 2019. There he worked with Frédéric Herbreteau, R. Govind and Igor Walukiewicz on partial-order techniques for the verification of timed systems, and the EDT specification formalism.

Anantha Padmanabha (PhD student at IMSc) visited LaBRI September 5-14, 2019. He gave a talk at the Formal Methods seminar and had scientific discussions with Diego Figueira, Igor Walukiewicz and Pascal Weil about modal logic and its applications to database theory.

Ramanathan S. Thinniyam (formerly a postdoc at CMI, now a postdoc at MPI SWS, Kaiserslautern) visited Philippe Schnoebelen (LSV) July 22nd to 26th, 2019. They worked on Simon’s congruence and the characterization of piecewise-testable atoms.

Sreejith A.V. (IIT Goa) visited LaBRI from June 24 to July 4, 2019. He worked with Vincent Penelle and Gabriele Puppis on transducers over countable linear orderings. The goal is to check for equivalence of Monadic second order (MSO) transductions over countable linear orderings. We were able to show equivalence for the subset of one-way transducers.

K. Narayan Kumar (CMI) visited LSV from May 27 to June 14, 2019. He worked with Paul Gastin on the separation problem for first-order logic on message sequence charts (MSCs) and on temporal logics for MSCs. They proved that when channels are existentially bounded, there is a (one-dimensional) temporal logic which is expressively complete for first-order logic over MSCs. It should be noted that the usual reduction from existentially or universally bounded MSCs to Mazurkiewicz traces cannot be applied since it involves some modulo counting which is not expressible in first-order logic. Instead, our technique is based on a canonical linearization (due to Thiagarajan and Walukiewicz) which is first-order definable.

Madhavan Mukund (CMI) visited LaBRI during May 20-31, 2019.  This visit was part of the CEFIPRA project IoTTTA.  During this visit, he had discussions with Anca Muscholl and Igor Walukiewicz on automata learning in the context of the negotiation model.  It was proposed that Adwitee Roy, a PhD student at CMI jointly supervised by Madhavan and Anca, will work on this in the coming months.  Madhavan also had discussions with Akka Zemmari and Mohamed Mosbah on potential collaboration in the area of distributed machine learning. Following this, Madhavan Mukund visited IRIF during June 3-5, 2019 to work with Ahmed Bouajjani and Constantin Enea on verification techniques for formal models of web services.

Sunil Simon (IIT Kanpur) visited LORIA, Nancy from May 13 to June 30, 2019. He worked with Hans van Ditmarsch on the topic of boolean games, in relation with prior work by van Ditmarsch on Knowledge Games and Public Announcement Games. More…

S. Krishna (IITB) visited LSV from May 10 to 24, 2019. She worked with Paul Gastin (LSV) and Luc Dartois (Univ. Créteil) on star-free regular expressions for aperiodic transducers. The full class of regular functions can be defined with various transducers (two-way deterministic, one-way with copyless registers, …) and also with regular transducer expressions. The goal is find restricted expressions to describe first-order transductions.

Vineeta Jain (PhD student at MNIT Jaipur) visited LaBRI from March 30th to April 20th,  2019. She worked with Mohamed Mosbah (LaBRI) and Dominique Méry (LORIA) on formally proving a secure authentication protocol that we designed in an earlier work.  After a comparison between many tools,  we decided to choose Scyther  as it is suitable for the verification of security protocols. She spent three days at LORIA (Nancy) and presented her work to the verification group.

Manoj Singh Gaur (IIT Jammu) visited LaBRI from April 1st to 4rd, 2019. He worked with Mohamed Mosbah (LaBRI) on the PhD progress of Vineeta Jain as she was also in LaBRI. As co-supervisers of this PhD, they discussed its content and validated the plan she presented for writing her manuscript.  Manoj discussed also with Akka Zemmari  and Jenny Benois-Pineau  (LaBRI) about an MoU between University of Bordeaux and IIT Jammu for student academic exchanges.

Vaishnavi Sundararajan (PhD CMI 2018, post-doc at IRISA) visited LaBRI March 19th to 22nd, 2019. She gave a talk at the Méthodes Formelles seminar on the certification of security protocols (more specifically: on a theory of assertions for Dolev-Yao models), and she participated in a meeting of  the ANR project BRAVAS on vector addition systems.

Jayakrishnan M. (PhD student, IMSc, Chennai) visited LIRMM from March 16th to May 31st, 2019. He worked with Christophe Paul and Stéphane Bessy on parametrized algorithms for directed graphs modification problems. More precisely we worked on two distinct problems which we didn’t solve yet but on which this collaboration will continue. The first  problem is the computation of the inversion index of a tournament. Known results establish the existence of XP algorithms for this problem. But is it still open to know whether the problem is NP-complete (which is expected) or whether it could be solved in FPT time. The second problem is the bipolar digraph vertex deletion (BDVP) problem which is a special case of the feedback vertex set problem (FVS). It is known that FVS can be solved in FPT time but the existence of a polynomial size kernel is one of the major open problem in the FPT community. We started the work on the existence of a polynomial kernel for BDVP.

C. Aiswarya (CMI) visited LSV from February 27 to March 16 and from June 17 to 30, 2019. She worked with Paul Gastin on the gossip problem for message sequence charts. This is a fundamental problem which has been extensively studied already and solved for universally bounded MSCs. The goal is to improve existing algorithm, using less resources while being applicable to a wider class of MSCs. She also worked with K.S. Thejaswini, Paul Gastin and Stefan Schwoon on the control problem for asynchronous automata (see K.S. Thejaswini’s internship).

Alain Finkel (LSV) visited IIT Bombay February 13 to March 11, 2019, to work again with S. Akshay and S. Krishna. They continued their discussion on VASS extended with three unbounded counters and on recent FIFO models.

Sinnou David (IMJ-PRG) visited CMI and IMSc January 28 to June 6, 2019. He gave an elective course on Elliptic curves at CMI and ran a seminar on diophantine geometry at IMSc. During that period, doctoral student Abhishek T. Bharadwaj (advisor: Purusottam Rath) worked with him to learn Mahler method in transcendence number theory. Former CMI student A. Mukhapadhyay took an internship with him (January-April) on the Manin-Mumford conjecture.

Philippe Schnoebelen (LSV) visited CMI from January 17th to January 31st, 2019. He worked with Ramanathan S. Thinniyam (a postdoctoral researcher at CMI) on algorithmic questions for piecewise testable languages, focusing on the equivalence classes of Simon’s subword congruence. This is part of a general research agenda (see [Karandikar, Schnoebelen. The height of piecewise-testable languages and the complexity of the logic of subwords, Logical Methods in Computer Science, 2019]) aiming at understanding the piecewise complexity of various languages and constructions.

Pascal Weil visited CMI from January 15th to January 26th, 2019. He worked with Madhavan Mukund on the functioning of UMI ReLaX.

Alain Finkel (LSV) visited CMI from January 11th to February 12th, 2019. He worked with M. Praveen on FIFO systems.

Sougata Bose (LaBRI, PhD student with  Anca Muscholl and Gabriele Puppis) visited IIT Bombay from January 6 to January 20, 2019. There he started a collaboration with S. Krishna on the synthesis of resynchronizers for transducers, which led to a publication at MFCS 2019.

Paul Gastin (LSV) visited CMI from November 17 to December 1st, 2018 and from January 4 to 25, 2019. He worked with
– B. Srivathsan and their joint PhD student Sayan Mukherjee (CMI) on algorithms for the verification of timed automata. They proposed a new simulation relation between zones ensuring termination of the zone based forward analysis method for timed automata with diagonal constraints.  Experiments with an implementation of this simulation show significant gains over existing methods. This work resulted in a paper accepted at CAV’19: Fast Algorithms for Handling Diagonal Constraints in Timed Automata.
– K. Narayan Kumar on temporal logics for message sequence charts (MSCs) which are behaviours of finite state distributed systems communicating via unbounded FIFO channels.  They defined a temporal logic based on natural unary modalities and proved that this temporal logic is expressively complete for FO^2, the fragment of first-order logic restricted to two variable names. Indeed, these two variables can be quantified and reused several times in a formula. This expressive completeness result holds without any channel bounds.
– C. Aiswarya and K.S. Thejaswini on the control problem for asynchronous automata (see K.S. Thejaswini’s internship).
– Also, following their work started in 2017 at CMI, Amaldev Manuel (now IIT Goa), R. Govind and Paul Gastin wrote a paper accepted at DLT’19: Logics for Reversible Regular Languages and Semigroups with Involution. They present MSO and FO logics with between and neighbour predicates that characterise various fragments of the class of regular languages closed under the reverse operation.  The standard connections that exist between MSO and FO logics and varieties of finite semigroups extend to this setting with semigroups extended with an involution.  The case is different for FO with neighbour relation where we show that one needs additional equations to characterise the class.

2018

Paul Gastin (LSV) visited IIT Bombay from October 30 to November 17 and from December 1 to 24, 2018. He worked with
– S. Akshay, S. Krishna and Vincent Jugé (LIGM, Univ. Paris Est, Marne la Vallée) on the verification of timed systems with data structures. They proposed a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. The idea is to reduce the reachability problem to the satisfiability problem of some formula in a variant of propositional dynamic logic. One main difficulty is to show the definability of the realizability property for graphs with timing constraints. This work resulted in a paper accepted at LICS’19:
Timed Systems through the Lens of Logic.
– S. Akshay, S. Krishna and Sparsa Roy Choudhury (PhD student at IITB). We propose a new class of bounded under-approximations for timed multi-pushdown systems, which subsumes most existing classes, even in the untimed setting. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fixpoint computations. We implement this algorithm and build, to the best of our knowledge, the first tool (TRiM) that can analyze timed multi-pushdown systems. We illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway, TRiM solves the binary reachability problem in timed automata and timed (one stack) pushdown automata.
– S. Krishna on first-order logic for aperiodic transducers with origin. The problem is to find a natural specification language to describe the semantics with origin of aperiodic transducers (streaming string transducers or two-way transducers).

Vincent Penelle (LaBRI) visited IIT Goa from December 17th to 21st 2018, to work with Sreejith A.V. They continued the work initiated with Gabriele Puppis on transducers on words over linear countable ordering. They also worked on the links between certain pumping lemmas for a language class and effective computation of downward and upward closure of languages from that class. From that, they hope to obtain complexity result for the computation of downward closure of languages of one-counter automata and image languages of sweeping transducers. Both projects are ongoing. The second one will involve Prince, a Junior Research Fellow at IIT Goa, soon to be a PhD student of Sreejith.

Alain Finkel (LSV) visited IIT Bombay December 3 to 9, 2018, to work with S. Akshay and S. Krishna. They discussed extended VASS with three unbounded counters and tried to solve some open problems.

Pascal Weil (LaBRI) visited CMI October 22nd to November 3rd, 2018. He worked with B. Srivathsan and Madhavan Mukund on the preparation of the workshop CAALM (January 2019) and he hosted, with Madhavan Mukund, the AURA meeting.

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.

Sreejith A.V. (IIT Goa) visited LaBRI from September 26th to October 4th 2018, to work with Vincent Penelle. They held exploratory discussions on probabilistic algorithm for counting problems. They also started to define transducers over words on linear countable ordering, and study the equivalence and origin-equivalence problem on this model together with Gabriele Puppis, this last work being currently in progress. Sreejith also gave a seminar on Languages over countable linear orderings and had discussions with Mohamed Mosbah about potential student exchanges between IIT Goa and Bordeaux INP.

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 R. Govind (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.

2017

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.

Amaldev Manuel (CMI) visited LSV and IRIF May 19th to June 30th 2017. He worked with Paul Gastin, Stefan Göller and Thomas Colcombet on problems related to logic, games and regular languages. More…

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.

Antoine Meyer (LIGM) visited IMSc April 1st to April 11, 2017. He worked with Kamal Lodaya on augmentations of temporal logic, such as counting and graded temporal logic. More…

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 R. 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.

Alain Finkel (LSV) visited CMI January 17 to February 6, 2017. He worked on counter systems with M. Praveen and gave two seminar on Well Structured Transition Systems.