Pierre-Alain Reynier

Professor, Aix-Marseille University, Computer Science department

Researcher at LIS

Head of the modelisation and verification (MoVe) group at LIS

Head of the Master Curriculum "Parcours Informatique et Mathématiques Discrètes" (Computer Science and Discrete Maths)

Co-head (with Nathalie Bertrand) of the working group on Verification of the GDR IM of the CNRS


Contact:

Laboratoire d’Informatique et Systèmes
Parc Scientifique de Luminy
163 avenue de Luminy - Case 901
F-13288 Marseille Cedex 9, France


Office : A208 (academic library, 2nd floor)
Phone : +33 (0)4 86 09 06 73
Fax : +33 (0)4 86 09 ?? ??

E-mail : firstname.lastname@lis-lab.fr (New!)



Books/Book chapters

  1. Reachability Problems - 12th International Conference, RP 2018, Marseille, France, September 24-26, 2018, Proceedings. Igor Potapov and Pierre-Alain Reynier.
    Springer. 2018.
    ISBN: 978-3-030-00249-7

  2. MSR 2017 - 11th National Colloquium on Modelization of Reactive Systems. Isabel Demongodin and Pierre-Alain Reynier.
    November 15-17, 2017. Marseille, France


  3. MOVEP 2012 - 10th International Winter School on Modelization and Verification of Parallel Processes. Pierre-Alain Reynier.
    December 3-7, 2012. Marseille, France


  4. An Introduction to Automatic Synthesis of Discrete and Timed Controllers. Franck Cassez, Kim Larsen, Jean-François Raskin and Pierre-Alain Reynier.
    In Quantitative Model-Based Analysis of Real-Time Embedded Systems. Springer. 2012.
    ISBN: 978-94-007-1368-0

  5. Timed Controller Synthesis: An Industrial Case Study. Franck Cassez, Kim Larsen, Jean-François Raskin and Pierre-Alain Reynier.
    In Quantitative Model-Based Analysis of Real-Time Embedded Systems. Springer. 2012.
    ISBN: 978-94-007-1368-0

  6. Verification of Timed Systems. Pierre-Alain Reynier.
    In Models and Analysis in Distributed Systems, pages 271–306. Wiley. 2011.
    ISBN: 978-18-482-1314-2

Journals

  1. Copyful Streaming String Transducers. Emmanuel Filiot and Pierre-Alain Reynier.
    In Fundamenta Informaticae. IOS Press. 2019. To appear


  2. Streamability of nested word transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais.
    In Logical Methods in Computer Science, volume 15 (2), . 2019.
    DOI: 10.23638/LMCS-15(2:1)2019

  3. Aperiodic String Transducers. Luc Dartois, Isma\"el Jecker and Pierre-Alain Reynier.
    In International Journal of Foundations of Computer Science, volume 29 (5), pages 801–824. World Scientific. 2018.
    DOI: 10.1142/S0129054118420054

  4. Decision Problems of Tree Transducers with Origin. Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Information and Computation, volume 261, pages 311–335. Elsevier. 2018.
    DOI: 10.1016/j.ic.2018.02.011

  5. Visibly Pushdown Transducers. Emmanuel Filiot, Jean-Francois Raskin, Pierre-Alain Reynier, Frédéric Servais and Jean-Marc Talbot.
    In Journal of Computer and System Sciences. Elsevier. 2018.
    DOI: 10.1016/j.jcss.2018.05.002

  6. Transducers, logic and algebra for functions of finite words. Emmanuel Filiot and Pierre-Alain Reynier.
    In SIGLOG News, volume 3 (3), pages 4–19. 2016.
    DOI: 10.1145/2984450.2984453

  7. Visibly Pushdown Transducers with Well-nested Outputs. Pierre-Alain Reynier and Jean-Marc Talbot.
    In International Journal of Foundations of Computer Science, volume 27 (2), pages 235–258. World Scientific. 2016.
    DOI: 10.1142/S0129054116400086

  8. Robustness of Time Petri Nets under Guard Enlargement. S. Akshay, Loic Hélouet, Claude Jard and Pierre-Alain Reynier.
    In Fundamenta Informaticae, volume 143 (3-4), pages 207–234. IOS Press. 2016.
    DOI: 10.3233/FI-2016-1312

  9. Trimming Visibly Pushdown Automata. Mathieu Caralp, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Theoretical Computer Science, volume 578, pages 13–29. Elsevier. 2015.
    DOI: 10.1016/j.tcs.2015.01.018

  10. Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. Pierre-Alain Reynier and Frédéric Servais.
    In Fundamenta Informaticae, volume 122 (1-2), pages 1–30. IOS Press. 2013.
    DOI: 10.3233/FI-2013-781

  11. On Characteristic Formulae for Event-Recording Automata. Omer-Landry Nguena-Timo and Pierre-Alain Reynier.
    In RAIRO - Theoretical Informatics and Applications, volume 47 (1), pages 69–96. EDP Sciences. 2013.
    DOI: 10.1051/ita/2012029

  12. Undecidability Results for Timed Automata with Silent Transitions. Patricia Bouyer, Serge Haddad and Pierre-Alain Reynier.
    In Fundamenta Informaticae, volume 92 (1-2), pages 1–25. IOS Press. 2009.
    DOI: 10.3233/FI-2009-0063

  13. Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. Patricia Bouyer, Serge Haddad and Pierre-Alain Reynier.
    In Information and Computation, volume 206 (1), pages 73–107. Elsevier. 2008.
    DOI: 10.1016/j.ic.2007.10.004

International conferences

  1. Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach. Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier and Ocan Sankur.
    In Proc. 31st International Conference on Computer Aided Verification (CAV 2019), pages 572–590, volume 11561 of Lecture Notes in Computer Science. Springer. 2019.
    DOI: 10.1007/978-3-030-25540-4\_33

  2. Synthesis of Data Word Transducers. Léo Exibard, Emmanuel Filiot and Pierre-Alain Reynier.
    In Proc. 30th International Conference on Concurrency Theory (CONCUR 2019), pages 24:1–24:15, volume 140 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2019.
    DOI: 10.4230/LIPIcs.CONCUR.2019.24

  3. Sequentiality of String-to-Context Transducers. Pierre-Alain Reynier and Didier Villevalois.
    In Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), pages 128:1–128:14, volume 132 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2019.
    DOI: 10.4230/LIPIcs.ICALP.2019.128

  4. On the Computation of the Minimal Coverability Set of Petri Nets. Pierre-Alain Reynier and Frédéric Servais.
    In Proc. 13th International Conference on Reachability Problems (RP 2019), pages 164–177, volume 11674 of Lecture Notes in Computer Science. Springer. 2019.
    DOI: 10.1007/978-3-030-30806-3\_13

  5. Symbolic approximation of weighted timed games. Damien Busatto-Gaston, Benjamin Monmege and Pierre-Alain Reynier.
    In Proc. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), pages 28:1–28:16 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2018.
    DOI: 10.4230/LIPIcs.FSTTCS.2018.28

  6. From Two-Way Transducers to Regular Function Expressions. Nicolas Baudru and Pierre-Alain Reynier.
    In Proc. 22nd International Conference on Developments in Language Theory (DLT 2018), pages 96–108, volume 11088 of Lecture Notes in Computer Science. Springer. 2018.
    DOI: 10.1007/978-3-319-98654-8\_8

  7. Optimal and Robust Controller Synthesis - Using Energy Timed Automata with Uncertainty. Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey and Pierre-Alain Reynier.
    In Proc. 22nd International Symposium on Formal Methods, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, pages 203–221, volume 10951 of Lecture Notes in Computer Science. Springer. 2018.
    DOI: 10.1007/978-3-319-95582-7\_12

  8. Copyful Streaming String Transducers. Emmanuel Filiot and Pierre-Alain Reynier.
    In Proc. of 11th International Workshop on Reachability Problems (RP 2017), pages 75–86, volume 10506 of Lecture Notes in Computer Science. Springer. 2017.
    DOI: 10.1007/978-3-319-67089-8_6

  9. Degree of sequentiality of weighted automata. Laure Daviaud, Ismael Jecker, Pierre-Alain Reynier and Didier Villevalois.
    In Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), pages 215–230, volume 10203 of Lecture Notes in Computer Science. Springer. 2017.
    DOI: 10.1007/978-3-662-54458-7_13

  10. Optimal Reachability in Divergent Weighted Timed Games. Damien Busatto-Gaston, Benjamin Monmege and Pierre-Alain Reynier.
    In Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), pages 162–178, volume 10203 of Lecture Notes in Computer Science. Springer. 2017.
    DOI: https://doi.org/10.1007/978-3-662-54458-7_10

  11. Aperiodic String Transducers. Luc Dartois, Ismael Jecker and Pierre-Alain Reynier.
    In Proc. 20th International Conference on Developments in Language Theory (DLT 2016), pages 125–137, volume 9840 of Lecture Notes in Computer Science. Springer. 2016.
    DOI: 10.1007/978-3-662-53132-7_11

  12. Two-Way Visibly Pushdown Automata and Transducers. Luc Dartois, Emmanuel Filiot, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Proc. 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'16), pages 217–226. ACM. 2016.
    DOI: 10.1145/2933575.2935315

  13. A Generalized Twinning Property for Minimisation of Cost Register Automata. Laure Daviaud, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Proc. 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'16), pages 857–866. ACM. 2016.
    DOI: 10.1145/2933575.2934549

  14. Decision Problems of Tree Transducers with Origin. Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Proc. 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015), pages 209–221, volume 9135 of Lecture Notes in Computer Science. Springer. 2015.
    DOI: 10.1007/978-3-662-47666-6_17

  15. Probabilistic Robust Timed Games. Youssouf Oualhadj, Pierre-Alain Reynier and Ocan Sankur.
    In Proc. 25th International Conference on Concurrency Theory (CONCUR'14), pages 203–217, volume 8704 of Lecture Notes in Computer Science. Springer. 2014.
    DOI: 10.1007/978-3-662-44584-6_15

  16. Visibly Pushdown Transducers with Well-nested Outputs. Pierre-Alain Reynier and Jean-Marc Talbot.
    In Proc. 18th International Conference on Developments in Language Theory (DLT'14), pages 129–141, volume 8633 of Lecture Notes in Computer Science. Springer. 2014.
    DOI: 10.1007/978-3-319-09698-8_12

  17. Expressiveness of Visibly Pushdown Transducers. Mathieu Caralp, Emmanuel Filiot, Pierre-Alain Reynier, Frédéric Servais and Jean-Marc Talbot.
    In Proc. 2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT'13), pages 17–26, volume 134. EPTCS. 2013.
    DOI: 10.4204/EPTCS.134.3

  18. Robust Controller Synthesis in Timed Automata. Ocan Sankur, Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier.
    In Proc. 24th International Conference on Concurrency Theory (CONCUR'13), pages 546–560, volume 8052 of Lecture Notes in Computer Science. Springer. 2013.
    DOI: 10.1007/978-3-642-40184-8_38

  19. Trimming Visibly Pushdown Automata. Mathieu Caralp, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Proc. 18th International Conference on Implementation and Application of Automata (CIAA'13), pages 84–96, volume 7982 of Lecture Notes in Computer Science. Springer. 2013.
    DOI: 10.1007/978-3-642-39274-0_9

  20. From Two-Way to One-Way Finite State Transducers. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais.
    In Proc. 28th Annual IEEE Symposium on Logic in Computer Science (LICS'13), pages 468–477. IEEE Computer Society. 2013.
    DOI: 10.1109/LICS.2013.53

  21. Robustness of Time Petri Nets under Guard Enlargement. S. Akshay, Loic Hélouet, Claude Jard and Pierre-Alain Reynier.
    In Proc. 6th International Workshop on Reachability Problems (RP'12), pages 92–106, volume 7550 of Lecture Notes in Computer Science. Springer. 2012.
    DOI: 10.1007/978-3-642-33512-9_9

  22. Controllers with Minimal Observation Power (Application to Timed Systems). Peter Bulychev, Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Jean-Francois Raskin and Pierre-Alain Reynier.
    In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), pages 223–237, volume 7561 of Lecture Notes in Computer Science. Springer. 2012.
    DOI: 10.1007/978-3-642-33386-6_19

  23. Visibly Pushdown Automata with multiplicities: Finiteness and K-Boundedness. Mathieu Caralp, Pierre-Alain Reynier and Jean-Marc Talbot.
    In Proc. 16th International Conference on Developments in Language Theory (DLT'12), pages 226–238, volume 7410 of Lecture Notes in Computer Science. Springer. 2012.
    DOI: 10.1007/978-3-642-31653-1_21

  24. Streamability of Nested Word Transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais.
    In Proc. 31st Annual International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), pages 312–324, volume 13 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2011.
    DOI: 10.4230/LIPIcs.FSTTCS.2011.312

  25. A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems. Janusz Malinowski, Peter Niebert and Pierre-Alain Reynier.
    In Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), pages 198–212, volume 6996 of Lecture Notes in Computer Science. Springer. 2011.
    DOI: 10.1007/978-3-642-24372-1_15

  26. Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. Pierre-Alain Reynier and Frédéric Servais.
    In Proc. 32nd International Conference on Application and Theory of Petri Nets and Concurrency (ICATPN'11), pages 69–88, volume 6709 of Lecture Notes in Computer Science. Springer. 2011.
    DOI: 10.1007/978-3-642-21834-7_5

  27. Quantitative Robustness Analysis of Flat Timed Automata. Rémi Jaubert and Pierre-Alain Reynier.
    In Proc. 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11), pages 229–244, volume 6604 of Lecture Notes in Computer Science. Springer. 2011.
    DOI: 10.1007/978-3-642-19805-2_16

  28. Properties of Visibly Pushdown Transducers. Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier Reynier, Frédéric Servais and Jean-Marc Talbot.
    In Proc. 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10), pages 355–367, volume 6281 of Lecture Notes in Computer Science. Springer. 2010.
    DOI: 10.1007/978-3-642-15155-2_32

  29. Weak Time Petri Nets strike back!. Pierre-Alain Reynier and Arnaud Sangnier.
    In Proc. 20th International Conference on Concurrency Theory (CONCUR'09), pages 557–571, volume 5710 of Lecture Notes in Computer Science. Springer. 2009.
    DOI: 10.1007/978-3-642-04081-8_37

  30. Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study. Franck Cassez, Jan J. Jessen, Kim G. Larsen, Jean-François Raskin and Pierre-Alain Reynier.
    In Proc. 12th International Conference on Hybrid Systems: Computation and Control (HSCC'09), pages 90–104, volume 5469 of Lecture Notes in Computer Science. Springer. 2009.
    DOI: 10.1007/978-3-642-00602-9_7

  31. Robust Analysis of Timed Automata via Channel Machines. Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier.
    In Proc. 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 157–171, volume 4962 of Lecture Notes in Computer Science. Springer. 2008.
    DOI: 10.1007/978-3-540-78499-9_12

  32. Timed Unfoldings for Networks of Timed Automata. Patricia Bouyer, Serge Haddad and Pierre-Alain Reynier.
    In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), pages 292–306, volume 4218 of Lecture Notes in Computer Science. Springer. 2006.
    DOI: 10.1007/11901914_23

  33. Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences. Patricia Bouyer, Serge Haddad and Pierre-Alain Reynier.
    In Proc. 33rd International Colloquium on Automata, Languages and Programming (ICALP'06), pages 420–431, volume 4052 of Lecture Notes in Computer Science. Springer. 2006.
    DOI: 10.1007/11787006_36

  34. Extended Timed Automata and Time Petri Nets. Patricia Bouyer, Serge Haddad and Pierre-Alain Reynier.
    In Proc. 6th International Conference on Application of Concurrency to System Design (ACSD'06), pages 91–100. IEEE Computer Society Press. 2006.
    DOI: 10.1109/ACSD.2006.6

  35. Robust Model-Checking of Linear-Time Properties in Timed Automata. Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier.
    In Proc. 7th Latin American Symposium on Theoretical Informatics (LATIN'06), pages 238–249, volume 3887 of Lecture Notes in Computer Science. Springer. 2006.
    DOI: 10.1007/11682462_25

  36. Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. Patricia Bouyer, François Laroussinie and Pierre-Alain Reynier.
    In Proc. 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'05), pages 112–126, volume 3829 of Lecture Notes in Computer Science. Springer. 2005.
    DOI: 10.1007/11603009_10

Invited contributions

  1. Robustness of Timed Systems. Pierre-Alain Reynier.
    In Actes de la 11ème Ecole d'été sur la Modélisation et la Vérification des Systèmes Parallèles (MOVEP'14), pages 64–68. 2014. Invited paper


  2. Implémentabilité des automates temporisés. Karine Altisen, Nicolas Markey, Pierre-Alain Reynier and Stavros Tripakis.
    In Actes du 5ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'05), pages 395–406. Hermès. 2005. Invited paper

International conferences without proceedings

  1. On Characteristic Formulae for Event-Recording Automata. Omer-Landry Nguena-Timo and Pierre-Alain Reynier.
    In Proc. Workshop on Fixpoints In Computer Science (FICS'09), pages 70–78. 2009.


  2. Forward Analysis of Timed Automata. Pierre-Alain Reynier.
    In Proc. 5th Winter School on Modelling and Verifying Parallel Processes (MOVEP'04), pages 52–57. 2004.

Thesis

  1. Contributions to timed systems and transducers. Pierre-Alain Reynier.
    Habilitation à diriger des recherches. Laboratoire d'informatique fondamentale de Marseille, Aix-Marseille Université, France. 2015.


  2. Vérification de systèmes temporisés et distribués : modèles, algorithmes et implémentabilité. Pierre-Alain Reynier.
    Thèse de doctorat. Laboratoire Spécification et Vérification, ENS Cachan, France. 2007.


  3. Analyse en avant des automates temporisés. Pierre-Alain Reynier.
    Master Thesis. DEA Algorithmique, Paris. 2004.

Other publications

  1. Diagonal constraints handled efficiently in UppAal. Pierre-Alain Reynier.
    Research Report. Number LSV-07-02. Laboratoire Spécification et Vérification, ENS Cachan, France. 2007.