B. Srivathsan (CMI) will visit LaBRI from September 27 to October 11, 2019. He will be working with Frédéric Herbreteau, Govind R. and Igor Walukiewicz on partial-order techniques for the verification of timed systems, and the EDT specification formalism.
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 and on recent FIFO models.
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.
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 (now PhD student in LaBRI) 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.
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.
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 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.