Paulin Fournier

Postdoctoral fellow

Paulin Fournier

Publications

Conferences

  • L. Dartois, P. Fournier, I. Jecker and N. Lhote
    On reversible Transducers
    Accepted in ICALP17

    Abstract

  • N. Bertrand, P. Fournier and A. Sangnier.
    Distributed local strategies in broadcast networks
    In Proceedings of the 26th International Conference on Concurrency Theory (Concur'15), Madrid, Spain, September 2015. LIPIcs 42, pages 44-57. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.

    PdfAbstract

  • N. Bertrand, P. Fournier and A. Sangnier.
    Playing with probabilities in reconfigurable broadcast networks
    In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), Grenoble, France, April 2014. LNCS 8412, pages 134-148. Springer.

    PdfAbstract

  • N. Bertrand and P. Fournier.
    Parameterized verification of many identical probabilistic timed processes
    In proceedings of the 33rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'13), Guwahati, India, December 2013. LIPIcs 24, pages 501-513. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.

    PdfAbstract

Ph.D. thesis

Parameterized verification of networks of many identical processes

Pdf

This thesis deals with formal verification of distributed systems. Model checking is a technique for verifying that the model of a system under study fulfills a given property. This PhD investigates the parameterized verification of networks composed of many identical processes for which the number of processes is the parameter.

  • Considering networks of probabilistic timed protocols, we show that the parameterized reachability and synchronization problems are undecidable when the communication topology is a clique. However, assuming probabilistic creation and deletion of processes, the problems become decidable.
  • Regarding selective networks, where the messages only reach a subset of the components, we show decidability of the parameterized reachability problem thanks to reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem.
  • Finally, we consider local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete.