Les journées auront si possible lieu au LaBRI, à l’Université de Bordeaux en ligne, les matins du 16, 17 et 18 juin 2021.
Plus d’informations techniques (notamment un lien de connexion) seront disponibles ultérieurement.
Organisateur: Vincent Penelle. Vous pouvez le contacter (vincent DOT penelle AT labri DOT fr) pour toute question concernant les journées.
L’inscription est gratuite, mais obligatoire. Lien vers la page d’inscription. Vous pourrez y proposer un exposé ou non (ainsi qu’éventuellement un titre et/ou un résumé si vous le connaissez déjà). Dans ce cas, l’organisateur vous contactera pour régler les détails. Cela dit, le programme est maintenant complet.
Mercredi  
8:459:00  Ouverture de la salle et mot de bienvenue (vers la fin). 
9:0010:00 
In this talk, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS), a method known to be scalable to large state spaces. We will present their theoretical guarantees. Formal analysis of MCTS is notably challenging, and we will discuss recent results in that area. Moreover, we augment the MCTS algorithm with a notion of symbolic advice, and show that its theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We illustrate our techniques using a scheduling problem and the popular game PacMan.

10:0010:15  Break 
10:1510:45 
We propose a new machine model recognizing starfree languages, with a geometric flavor. Our starting point is the characterization of regular languages using twoway automata (2DFA). The idea is to take seriously the visual representations found throughout the literature of the behavior of a 2DFA on a word ; by putting a total order on the set of states, one can formally define what it means for such a behavior to be planar, in a sense analogous to the planarity of combinatorial maps. Starfree languages are then exactly the languages recognized by "planar 2DFA". We also show that the corresponding planar transducer model characterizes the class of firstorder transductions (a.k.a. aperiodic regular functions). If time allows, the talk will briefly discuss the connections of this work with the noncommutative lambdacalculus (cf. our recent paper Aperiodicity in a noncommutative logic, ICALP'20). This is joint work with Pierre Pradic (University of Oxford).

10:5011:20 
Most processors can now use instructions that work on blocks of bits, called SIMD. These instructions make it necessary to develop new algorithms to use them at best. There are already many articles about the use of SIMD instructions in order to vectorize particular automata, however it would be better if we were able to vectorize any automaton. In this talk I will focus on languages which syntactic monoid belongs to the variety of languages DA.

11:2511:55 
We study the synthesis problem for systems with a parameterized number of processes. As in the classical case due to Church, the system selects actions depending on the program run so far, with the aim of fulfilling a given specification. The difficulty is that, at the same time, the environment executes actions that the system cannot control. In contrast to the case of fixed, finite alphabets, here we consider the case of parameterized alphabets. An alphabet reflects the number of processes, which is static but unknown. The synthesis problem then asks whether there is a finite number of processes for which the system can satisfy the specification. This variant is already undecidable for very limited logics. Therefore, we consider a firstorder logic without the order on word positions. We show that even in this restricted case synthesis is undecidable if both the system and the environment have access to all processes. On the other hand, we prove that the problem is decidable if the environment only has access to a bounded number of processes. In that case, there is even a cutoff meaning that it is enough to examine a bounded number of process architectures to solve the synthesis problem. This talk is based on an article published at FoSSaCS 2020, and is a joint work with Béatrice Bérard, Benedikt Bollig, and Tali Sznajder.

Jeudi  
8:459:00  Ouverture de la salle. 
9:0010:00 
We propose a syntax of regular expressions which captures exactly counting MSO definable languages of graphs of treewidth 2. A similar syntax is given for CMSO definable languages of series parallel graphs and connected treewidth 2 graphs.

10:0010:15  Break 
10:1510:45 
Automata and games over infinite words are widely used in verification and synthesis of reactive systems. Several different kinds of acceptance conditions can be used in these systems, which may differ in their complexity and expressive power. For their simplicity and usefulness, parity conditions are of special relevance. However, in many applications such as LTLsynthesis, the automata that are obtained in the first place use more complex conditions (Muller conditions) and we have to transform them in parity ones. In this talk, I will present a construction that takes as input a Muller automaton and transforms it into a parity automaton in an optimal way. More precisely, the resulting parity automaton has minimal size and uses a minimal number of priorities among those automata that admit a locally bijective morphism to the original Muller automaton. This transformation and the optimality result can also be applied to games and other types of transition systems. We show two applications: an improvement on the determinisation of Büchi automata into deterministic parity automata and characterisations of automata that admit parity, Rabin or Streett conditions in top of them. This is joint work with Thomas Colcombet and Nathanaël Fijalkow. It will appear at ICALP 2021.

10:5011:20 
We study deterministic and stochastic zerosum games on graphs, which are prevalent tools to model decisionmaking in presence of an antagonistic opponent. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., with respect to randomization or memory requirements)? Our contributions further the understanding of arenaindependent finitememory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in twoplayer games to the easier study of oneplayer games. Second, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This extends a work about memoryless determinacy by Gimbert and Zielonka from 2005. This talk is based on an article published at CONCUR 2020 and a recent online preprint. This is joint work with Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, and Mickael Randour.

11:2511:55 
FIFO systems are systems of automata communicating through FIFO queues. This simple and rather idealised model can be used to analyse some aspects of messagepassing systems, reactive systems with event queues, weak memory models with buffered reads and writes, etc. From a purely computational perspective, this is a Turing complete model even for just one automaton and one FIFO queue. In this talk, I will present a personal selection of existing works on the problem of the automatic (pushbutton) verification of such systems. I will consider in particular the works that try to address the verification of FIFO systems that are "nearly" systems with rendezvous synchronisation. Nearly synchronous FIFO systems can be found for instance in the work of Lipton on reduction [1], Elrad&Francez on communication closed layers [2], Bultan et al on synchronisability [3], Mushcoll et al on existential boundedness [4], or more recently Bouajjani et al on ksynchronous systems [5]. This idea is also implicitly present in several works on multiparty session types [6], although the connection there is only well understood in the bipartite setting, where it matches the notion of halfduplex communications [7,8]. The aim of the talk will also be to present recent personal contributions and ongoing works on ksynchronous systems, existentiallybounded systems, and halfduplex systems [9,10,11,12]. [1] Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975). https://doi.org/10.1145/361227.361234 [2] Elrad, T., Francez, N.: Decomposition of distributed programs into communicationclosed layers. Sci. Comput. Program. 2(3), 155–173 (1982). https://doi.org/10.1016/01676423(83)900138 [3] Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. https://doi.org/10.1016/j.tcs.2016.09.023 [4] Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(13), 147–167 (2007), http://content.iospress.com/articles/fundamentainformaticae/fi801309 [5] Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. CAV'18, https://doi.org/10.1007/9783319961422 23, and https://arxiv.org/abs/1804.06612 [6] Honda, K., Yoshida, N., Carbone, M., Multiparty asynchronous session types https://dl.acm.org/doi/10.1145/1328897.1328472 [7] Cécé, G., Finkel, A. Verification of programs with halfduplex communication. Inf. Comput. 202(2): 166190 (2005) https://www.sciencedirect.com/science/article/pii/S0890540105001082?via%3Dihub [8] Lozes, E., Villard, J. Reliable Contracts for Unreliable HalfDuplex Communications. WSFM 2011: 216 https://link.springer.com/chapter/10.1007%2F9783642298349_2 [9] Di Giusto, C., Laversa, L., Lozes, E. On the ksynchronizability of Systems. FoSSaCS 2020: 157176 https://link.springer.com/chapter/10.1007%2F9783030452315_9 [10] Di Giusto, C., Laversa, L., Lozes, E. Guessing the buffer bound for ksynchronizability. CIAA 2021. To appear. https://arxiv.org/abs/2104.14408 [11] Bollig, B., Di Giusto, C., Finkel, A., Laversa, L., Lozes, E., Suresh, A. A Unifying Framework for Deciding Synchronizability submitted. [12] Di Giusto, C., GermerieGuizouarn, L., Lozes, E., Towards Generalised HalfDuplex Systems. submitted.

Vendredi  
8:459:00  Ouverture de la salle. 
9:009:30 
We study the dynamic membership problem for regular languages: fix a language L, read a word w, build in time O(w) a data structure indicating if w is in L, and maintain this structure efficiently under substitution edits on w. We consider this problem on the unit cost RAM model with logarithmic world length, where the problem always has a solution in O(log w / log log w). We show that the problem is in O(log log w) for languages in an algebraicallydefined class QSG, and that it is in O(1) for another class QLZG. We show that languages not in QSG admit a reduction from the prefix problem for a cyclic group, so that they require \Omega(log n/ log log n) operations in the worst case; and that QSG languages not in QLZG admit a reduction from the prefix problem for the monoid U_1, which we conjecture cannot be maintained in O(1). This yields a conditional trichotomy. We also investigate intermediate cases between O(1) and O(log log n). Our results are shown via the dynamic word problem for monoids and semigroups, for which we also give a classification. We thus solve open problems of the paper of Skovbjerg Frandsen, Miltersen, and Skyum on the dynamic word problem, and additionally cover regular languages.

9:3510:05 
I will discuss an approach for program synthesis using learned probabilistic context free grammars, and show the recent progress we made in making it scalable across parallel architectures. No knowledge of any terms in this title and abstract is required for the talk!

10:0510:20  Break 
10:2010:50 
Normalisation strategies provide a categorical description of the notion of contracting homotopies via rewriting. On the other hand, globular 2Kleene algebras provide a formal setting for reasoning about coherence proofs via abstract rewriting systems. We present a formalisation of the notion of normalisation strategy in this setting, and show how these are related to convergence (confluence and termination) of abstract rewriting systems. This allows us to formulate and prove a formal coherence theorem via convergence.

10:5511:25 
In finite semigroup theory, the join operation between two varieties of finite semigroups or monoids has been studied a lot. The join of two varieties V and W corresponds to the smallest variety containing both V and W and one of the motivations to study it is that it corresponds, via the Eilenberg correspondence, to the class of regular languages obtained when considering parallel computations of automata for the languages in the classes corresponding to, respectively, V and W. The focus of the aforementioned studies has often been on finding a set of profinite identities defining the join of V and W, often proving decidability of this join along the way. A great majority of works along this line rely on deep developments in profinite topology. I shall present a new method to determine a set of profinite identities defining the join of any variety of finite monoids verifying some condition with the variety of finite locally trivial semigroups LI. The advantage of this method is that it only uses algebraic and languagetheoretic techniques and is rather straightforward to apply once the stage is set. Basically, to obtain a set of identities for the join of V and LI for V some variety of finite monoids for which some defining set of identities is known, one just has to prove that the class of languages corresponding to V verifies some criterion. This allows me to give some new and straightforward proofs of a characterisation via identities of the join of LI with, respectively, the classical varieties of finite monoids R, L, J and any variety of finite groups. My work is actually a sort of rediscovery of the work of J. C. Costa around 20 years ago hinging on algebra and language theory rather than on profinite topology.

11:3012:00 
We initiate a study of the expressive power of tree algebras, and more generally infinitely sorted algebras, based on their asymptotic complexity. Tree algebras in many of their forms, such as clones, hyperclones, operads, etc, as well as other kind of algebras, are infinitely sorted: the carrier is a multi sorted set indexed by a parameter that can be interpreted as the number of variables or hole types. Finite such algebras  meaning when all sorts are finite  can be classified depending on the asymptotic size of the carrier sets as function of the parameter, that we call the complexity of the algebra. This naturally defines the notions of algebras of bounded, linear, polynomial, exponential or doubly exponential complexity... Our main result precisely characterizes the tree algebras of bounded complexity based on the languages that they recognize as Boolean closures of simple languages. Along the way, we prove that such algebras that are syntactic are exactly those in which, as soon as there are sufficiently many variables, the elements are invariant under permutation of the variables. This is joint work with Thomas Colcombet. It will appear at ICALP 2021.
