R
[Rab69] Michael O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society 141:1-35. American Mathematical Society, juillet 1969.
@article{TAMS141-Rab,
  author =              {Rabin, Michael O.},
  title =               {Decidability of Second-Order Theories and Automata
                         on Infinite Trees},
  publisher =           {American Mathematical Society},
  journal =             {Transactions of the American Mathematical Society},
  volume =              {141},
  pages =               {1-35},
  year =                {1969},
  month =               jul,
}
[Rab70] Michael O. Rabin. Weakly definable relations and special automata. In SMLFST'70, pages 1-23. North-Holland, 1970.
@inproceedings{smlfst1970-Rab,
  author =              {Rabin, Michael O.},
  title =               {Weakly definable relations and special automata},
  editor =              {Bar{-}Hillel, Yehoshua},
  booktitle =           {{P}roceedings of the {S}ymposium on {M}athematical
                         {L}ogic and {F}oundations of {S}et {T}heory
                         ({SMLFST}'70)},
  acronym =             {{SMLFST}'70},
  publisher =           {North-Holland},
  pages =               {1-23},
  year =                {1970},
}
[Rab72] Michael O. Rabin. Automata on infinite objects and Church's thesis. Regional Conference Series in Mathematics 13. American Mathematical Society, 1972.
@book{AIOCT1972-Rab,
  author =              {Rabin, Michael O.},
  title =               {Automata on infinite objects and {C}hurch's thesis},
  publisher =           {American Mathematical Society},
  series =              {Regional Conference Series in Mathematics},
  number =              {13},
  year =                {1972},
}
[Rab00] Alexander Rabinovich. Star Free Expressions over the Reals. Theoretical Computer Science 233(1-2):233-245. Elsevier, février 2000.
@article{tcs233(1-2)-Rab,
  author =              {Rabinovich, Alexander},
  title =               {Star Free Expressions over the Reals},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {233},
  number =              {1-2},
  pages =               {233-245},
  year =                {2000},
  month =               feb,
}
[Rab02] Alexander Rabinovich. Expressive Power of Temporal Logic. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 57-75. Springer-Verlag, août 2002.
@inproceedings{concur2002-Rab,
  author =              {Rabinovich, Alexander},
  title =               {Expressive Power of Temporal Logic},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {57-75},
  year =                {2002},
  month =               aug,
}
[Rab03] Alexander Rabinovich. Quantitative analysis of probabilistic lossy channel systems. In ICALP'03, Lecture Notes in Computer Science 2719, pages 1008-1021. Springer-Verlag, juin 2003.
@inproceedings{icalp2003-Rab,
  author =              {Rabinovich, Alexander},
  title =               {Quantitative analysis of probabilistic lossy channel
                         systems},
  editor =              {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow,
                         Joachim and Woeginger, Gerhard J.},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'03)},
  acronym =             {{ICALP}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2719},
  pages =               {1008-1021},
  year =                {2003},
  month =               jun,
}
[Rab03] Alexander Rabinovich. Automata over Continuous Time. Theoretical Computer Science 300(1-3):331-363. Elsevier, mai 2003.
@article{tcs300(1-3)-Rab,
  author =              {Rabinovich, Alexander},
  title =               {Automata over Continuous Time},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {300},
  number =              {1-3},
  pages =               {331-363},
  year =                {2003},
  month =               may,
}
[Rab08] Roman Rabinovich. Complexity Measures for Directed Graphs. Diplomarbeit, RWTH Aachen, Germany, Août 2008.
@mastersthesis{diplom08-Rab,
  author =              {Rabinovich, Roman},
  title =               {Complexity Measures for Directed Graphs},
  year =                {2008},
  month =               aug,
  school =              {RWTH Aachen, Germany},
  type =                {Diplomarbeit},
}
[Rac78] Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. Theoretical Computer Science 6:223-231. Elsevier, 1978.
@article{tcs6()-Rac,
  author =              {Rackoff, Charles},
  title =               {The Covering and Boundedness Problems for Vector
                         Addition Systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {6},
  pages =               {223-231},
  year =                {1978},
  doi =                 {10.1016/0304-3975(78)90036-1},
}
[Rah09] George Rahonis. Fuzzy Languages. In Manfred Droste, Werner Kuich et Walter Vogler (eds.), Handbook of Weighted Automata. Springer-Verlag, 2009.
@incollection{hwa-ch12-Rah,
  author =              {Rahonis, George},
  title =               {Fuzzy Languages},
  editor =              {Droste, Manfred and Kuich, Werner and Vogler,
                         Walter},
  booktitle =           {Handbook of Weighted Automata},
  publisher =           {Springer-Verlag},
  pages =               {481-517},
  chapter =             {12},
  year =                {2009},
  doi =                 {10.1007/978-3-642-01492-5 12},
}
[Ram98] Jorge Luis Ramírez Alfonsín. On Variations of the Subset Sum Problem. Discrete Applied Mathematics 81(1-3):1-7. Elsevier, janvier 1998.
@article{dam81(1-3)-Ram,
  author =              {Ram{\'\i}rez{ }Alfons{\'\i}n, Jorge Luis},
  title =               {On Variations of the Subset Sum Problem},
  publisher =           {Elsevier},
  journal =             {Discrete Applied Mathematics},
  volume =              {81},
  number =              {1-3},
  pages =               {1-7},
  year =                {1998},
  month =               jan,
}
[Ram98] Solofo Ramangalahi. Strategies for comformance testing. Research Report 98-010, Max-Planck Institut für Informatik, Germany, Mai 1998.
@techreport{mpi-i-98-010-Ram,
  author =              {Ramangalahi, Solofo},
  title =               {Strategies for comformance testing},
  number =              {98-010},
  year =                {1998},
  month =               may,
  institution =         {Max-Planck Institut f{\"u}r Informatik, Germany},
  type =                {Research Report},
}
[Ras99] Jean-François Raskin. Logics, Automata and Classical theories for Deciding Real Time. Thèse de doctorat, FUNDP, Namur, Belgium, Juin 1999.
@phdthesis{phd-raskin,
  author =              {Raskin, Jean-Fran{\c c}ois},
  title =               {Logics, Automata and Classical theories for Deciding
                         Real Time},
  year =                {1999},
  month =               jun,
  school =              {FUNDP, Namur, Belgium},
  type =                {Th\`ese de doctorat},
}
[RB98] Theo C. Ruys et Ed Brinksma. Experience with Literate Programming in the Modelling and Validation of Systems. In TACAS'98, Lecture Notes in Computer Science 1384, pages 393-407. Springer-Verlag, mars 1998.
@inproceedings{tacas1998-RB,
  author =              {Ruys, Theo C. and Brinksma, Ed},
  title =               {Experience with Literate Programming in the
                         Modelling and Validation of Systems},
  editor =              {Steffen, Bernhard},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'98)},
  acronym =             {{TACAS}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1384},
  pages =               {393-407},
  year =                {1998},
  month =               mar,
}
[RBL07] Jacob Illum Rasmussen, Gerd Behrmann et Kim Guldstrand Larsen. Complexity in Simplicity: Flexible Agent-Based State Space Exploration. In TACAS'07, Lecture Notes in Computer Science 4424, pages 231-245. Springer-Verlag, mars 2007.
@inproceedings{tacas2007-RBL,
  author =              {Rasmussen, Jacob Illum and Behrmann, Gerd and
                         Larsen, Kim Guldstrand},
  title =               {Complexity in Simplicity: Flexible Agent-Based State
                         Space Exploration},
  editor =              {Grumberg, Orna and Huth, Michael},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'07)},
  acronym =             {{TACAS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4424},
  pages =               {231-245},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71209-1_19},
}
[Rei84] John H. Reif. The Complexity of Two-Player Games of Incomplete Information. Journal of Computer and System Sciences 29(2):274-301. Academic Press, octobre 1984.
@article{jsl66(3)-Reif,
  author =              {Reif, John H.},
  title =               {The Complexity of Two-Player Games of Incomplete
                         Information},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {29},
  number =              {2},
  pages =               {274-301},
  year =                {1984},
  month =               oct,
}
[Rei13] Julien Reichert. On The Complexity of Counter Reachability Games. In RP'13, Lecture Notes in Computer Science 8169, pages 196-208. Springer-Verlag, septembre 2013.
@inproceedings{rp2013-Rei,
  author =              {Reichert, Julien},
  title =               {On The Complexity of Counter Reachability Games},
  editor =              {Abdulla, Parosh Aziz and Potapov, Igor},
  booktitle =           {{P}roceedings of the 7th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'13)},
  acronym =             {{RP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8169},
  pages =               {196-208},
  year =                {2013},
  month =               sep,
  doi =                 {10.1007/978-3-642-41036-9_18},
}
[Rei16] Julien Reichert. On The Complexity of Counter Reachability Games. Fundamenta Informaticae 143(3-4):415-436. IOS Press, 2016.
@article{fundi143(3-4)-Rei,
  author =              {Reichert, Julien},
  title =               {On The Complexity of Counter Reachability Games},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {143},
  number =              {3-4},
  pages =               {415-436},
  year =                {2016},
  doi =                 {10.3233/FI-2016-1320},
}
[Rey99] Mark Reynolds. The Complexity of Temporal Logic over the Reals. Research Report cs.LO/9910012, arXiv, Octobre 1999.
@techreport{arxiv-cs.LO/9910012,
  author =              {Reynolds, Mark},
  title =               {The Complexity of Temporal Logic over the Reals},
  number =              {cs.LO/9910012},
  year =                {1999},
  month =               oct,
  institution =         {arXiv},
  type =                {Research Report},
}
[Rey01] Mark Reynolds. An Axiomatization of Full Computation Tree Logic. Journal of Symbolic Logic 66(3):1011-1057. Association for Symbolic Logic, septembre 2001.
@article{jsl66(3)-Rey,
  author =              {Reynolds, Mark},
  title =               {An Axiomatization of Full Computation Tree Logic},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {66},
  number =              {3},
  pages =               {1011-1057},
  year =                {2001},
  month =               sep,
}
[Rey04] Mark Reynolds. The Complexity of the Temporal Logic with "Until" Over General Linear Time. Journal of Computer and System Sciences 66(2):393-426. Academic Press, mars 2004.
@article{jcss66(2)-Rey,
  author =              {Reynolds, Mark},
  title =               {The Complexity of the Temporal Logic with
                         {"}Until{"} Over General Linear Time},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {66},
  number =              {2},
  pages =               {393-426},
  year =                {2004},
  month =               mar,
}
[Rey05] Mark Reynolds. An Axiomatization of PCTL*. Information and Computation 201(1):72-119. Academic Press, août 2005.
@article{icomp201(1)-Rey,
  author =              {Reynolds, Mark},
  title =               {An Axiomatization of {PCTL}{\(^*\)}},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {201},
  number =              {1},
  pages =               {72-119},
  year =                {2005},
  month =               aug,
}
[Rey07] Pierre-Alain Reynier. Vérification de systèmes temporisés et distribués : modèles, algorithmes et implémentabilité. PhD thesis, Lab. Spécification & Vérification, ENS Cachan, France, Juin 2007.
@phdthesis{phd-reynier,
  author =              {Reynier, Pierre-Alain},
  title =               {V{\'e}rification de syst{\`e}mes temporis{\'e}s et
                         distribu{\'e}s~: mod{\`e}les, algorithmes et
                         impl{\'e}mentabilit{\'e}},
  year =                {2007},
  month =               jun,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
}
[Rey10] Mark Reynolds. The Complexity of Temporal Logic over the Reals. Annals of Pure and Applied Logic 161(8):1063-1096. Elsevier, mai 2010.
@article{apal161(8)-Rey,
  author =              {Reynolds, Mark},
  title =               {The Complexity of Temporal Logic over the Reals},
  publisher =           {Elsevier},
  journal =             {Annals of Pure and Applied Logic},
  volume =              {161},
  number =              {8},
  pages =               {1063-1096},
  year =                {2010},
  month =               may,
}
[RG01] Muriel Roger et Jean Goubault-Larrecq. Log Auditing through Model-Checking. In CSFW'01, pages 220-236. IEEE Comp. Soc. Press, juin 2001.
@inproceedings{csfw2001-RG,
  author =              {Roger, Muriel and Goubault{-}Larrecq, Jean},
  title =               {Log Auditing through Model-Checking},
  booktitle =           {{P}roceedings of the 14th {IEEE} {C}omputer
                         {S}cience {F}oundations {W}orkshop ({CSFW}'01)},
  acronym =             {{CSFW}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {220-236},
  year =                {2001},
  month =               jun,
}
[RJL+10] Christopher Thomas Ryan, Albert Xin Jiang et Kevin Leyton-Brown. Symmetric Games with Piecewise Linear Utilities. In BQGT'10. ACM Press, mai 2010.
@inproceedings{bqgt10-RJL,
  author =              {Ryan, Christopher Thomas and Jiang, Albert Xin and
                         Leyton-Brown, Kevin},
  title =               {Symmetric Games with Piecewise Linear Utilities},
  editor =              {Dror, Moshe and So{\v{s}}i{\'c}, Greys},
  booktitle =           {{P}roceedings of the {B}ehavioral and {Q}uantitative
                         {G}ame {T}heory: {C}onference on {F}uture
                         {D}irections ({BQGT}'10)},
  acronym =             {{BQGT}'10},
  publisher =           {ACM Press},
  year =                {2010},
  month =               may,
  doi =                 {10.1145/1807406.1807447},
}
[RK97] Jürgen Ruf et Thomas Kropf. A New Algorithm for Discrete Timed Symbolic Model Checking. In HART'97, Lecture Notes in Computer Science 1201, pages 18-32. Springer-Verlag, mars 1997.
@inproceedings{hart1997-RK,
  author =              {Ruf, J{\"u}rgen and Kropf, {\relax Th}omas},
  title =               {A New Algorithm for Discrete Timed Symbolic Model
                         Checking},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {18-32},
  year =                {1997},
  month =               mar,
}
[RK00] Jürgen Ruf et Thomas Kropf. Analyzing Real-Time Systems. In DATE'00, pages 243-248. IEEE Comp. Soc. Press, mars 2000.
@inproceedings{date2000-RK,
  author =              {Ruf, J{\"u}rgen and Kropf, {\relax Th}omas},
  title =               {Analyzing Real-Time Systems},
  booktitle =           {{P}roceedings of the 2000 {D}esign, {A}utomation and
                         {T}est in {E}urope ({DATE}'00)},
  acronym =             {{DATE}'00},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {243-248},
  year =                {2000},
  month =               mar,
}
[RLS06] Jacob Illum Rasmussen, Kim Guldstrand Larsen et K. Subramani. On using priced timed automata to achieve optimal scheduling. Formal Methods in System Design 29(1):97-114. Springer-Verlag, juillet 2006.
@article{fmsd29(1)-RLS,
  author =              {Rasmussen, Jacob Illum and Larsen, Kim Guldstrand
                         and Subramani, K.},
  title =               {On using priced timed automata to achieve optimal
                         scheduling},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {29},
  number =              {1},
  pages =               {97-114},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/s10703-006-0014-1},
}
[RM00] Alexander Rabinovich et Shahar Maoz. Why so many Temporal Logics Climb un the Trees?. In MFCS'00, Lecture Notes in Computer Science 1893, pages 629-639. Springer-Verlag, août 2000.
@inproceedings{mfcs2000-RM,
  author =              {Rabinovich, Alexander and Maoz, Shahar},
  title =               {Why so many Temporal Logics Climb un the Trees?},
  editor =              {Nielsen, Mogens and Rovan, Branislav},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'00)},
  acronym =             {{MFCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1893},
  pages =               {629-639},
  year =                {2000},
  month =               aug,
}
[RM01] Alexander Rabinovich et Shahar Maoz. An Infinite Hierarchy of Temporal Logics over Branching Time. Information and Computation 171(2):306-332. Academic Press, décembre 2001.
@article{icomp171(2)-RM,
  author =              {Rabinovich, Alexander and Maoz, Shahar},
  title =               {An Infinite Hierarchy of Temporal Logics over
                         Branching Time},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {171},
  number =              {2},
  pages =               {306-332},
  year =                {2001},
  month =               dec,
}
[RMD+92] Y. Srinivas Ramakrishna, Louise E. Moser, Laura K. Dillon, P. Michael Melliar-Smith et George Kutty. An Automata Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until. Fundamenta Informaticae 17(3):272-282. IOS Press, novembre 1992.
@article{fundi17(3)-RMDMK,
  author =              {Ramakrishna, Y. Srinivas and Moser, Louise E. and
                         Dillon, Laura K. and Melliar{-}Smith, P. Michael and
                         Kutty, George},
  title =               {An Automata Theoretic Decision Procedure for
                         Propositional Temporal Logic with Since and Until},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {17},
  number =              {3},
  pages =               {272-282},
  year =                {1992},
  month =               nov,
}
[RN95] Stuart J. Russell et Peter Norvig. Artificial Intelligence – A modern approach. Prentice Hall, 1995.
@book{RN95-AIMA,
  author =              {Russell, Stuart J. and Norvig, Peter},
  title =               {Artificial Intelligence~-- A~modern approach},
  publisher =           {Prentice Hall},
  year =                {1995},
}
[Rog03] Muriel Roger. Raffinements de la résolution et vérification de protocoles cryptographiques. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, Octobre 2003.
@phdthesis{phd-roger,
  author =              {Roger, Muriel},
  title =               {Raffinements de la r{\'e}solution et
                         v{\'e}rification de protocoles cryptographiques},
  year =                {2003},
  month =               oct,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[Roh97] Scott Rohde. Alternating automata and the temporal logic of ordinals. PhD thesis, University of Illinois, 1997.
@phdthesis{phd-rohde,
  author =              {Rohde, Scott},
  title =               {Alternating automata and the temporal logic of
                         ordinals},
  year =                {1997},
  school =              {University of Illinois},
}
[Ros67] Pierre Rosenstiehl. Theory of Graphs. Gordon and Breach Science Publishers, 1967.
@book{ToG-Ros67,
  title =               {Theory of Graphs},
  editor =              {Rosenstiehl, Pierre},
  booktitle =           {Theory of Graphs},
  publisher =           {Gordon and Breach Science Publishers},
  year =                {1967},
}
[Ros73] Robert W. Rosenthal. A class of games possessing pure-strategy Nash equilibria. International Journal of Game Theory 2(1):65-67. Springer-Verlag, décembre 1973.
@article{ijgt2(1)-Ros,
  author =              {Rosenthal, Robert W.},
  title =               {A~class of games possessing pure-strategy {N}ash
                         equilibria},
  publisher =           {Springer-Verlag},
  journal =             {International Journal of Game Theory},
  volume =              {2},
  number =              {1},
  pages =               {65-67},
  year =                {1973},
  month =               dec,
  doi =                 {10.1007/BF01737559},
}
[Ros73] Robert W. Rosenthal. The network equilibrium problem in integers. Networks 3(1):53-59. John Wiley & Sons, janvier 1973.
@article{netw3(1)-Ros,
  author =              {Rosenthal, Robert W.},
  title =               {The network equilibrium problem in integers},
  publisher =           {John Wiley \& Sons},
  journal =             {Networks},
  volume =              {3},
  number =              {1},
  pages =               {53-59},
  year =                {1973},
  month =               jan,
  doi =                 {10.1002/net.3230030104},
}
[Ros03] Laurent Rosaz. The word problem for 1LC congruences is NP-hard. Theoretical Computer Science 306(1-3):245-268. Elsevier, septembre 2003.
@article{tcs306(1-3)-Ros,
  author =              {Rosaz, Laurent},
  title =               {The word problem for {\(1\mathcal{LC}\)} congruences
                         is {NP}-hard},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {306},
  number =              {1-3},
  pages =               {245-268},
  year =                {2003},
  month =               sep,
}
[Rot02] Günter Rote. Crossing the Bridge at Night. EATCS Bulletin 78:241-246. EATCS, octobre 2002.
@article{eatcs-bull78()-Rot,
  author =              {Rote, G{\"u}nter},
  title =               {Crossing the Bridge at Night},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {78},
  pages =               {241-246},
  year =                {2002},
  month =               oct,
}
[Rou07] Tim Roughgarden. Routing games. In Noam Nisan, Tim Roughgarden, Éva Tardos et Vijay V. Vazirani (eds.), Algorithmic Game Theory. Cambridge University Press, 2007.
@incollection{agt2007-ch18-Rou,
  author =              {Roughgarden, Tim},
  title =               {Routing games},
  editor =              {Nisan, Noam and Roughgarden, Tim and Tardos, {\'E}va
                         and Vazirani, Vijay V.},
  booktitle =           {Algorithmic Game Theory},
  publisher =           {Cambridge University Press},
  pages =               {461-486},
  chapter =             {18},
  year =                {2007},
}
[Rou20] Victor Roussanaly. Efficient verification of real-time systems. Thèse de doctorat, Université Rennes 1, France, Novembre 2020.
@phdthesis{phd-roussanaly,
  author =              {Roussanaly, Victor},
  title =               {Efficient verification of real-time systems},
  year =                {2020},
  month =               nov,
  school =              {Universit{\'e} Rennes~1, France},
  type =                {Th\`ese de doctorat},
}
[RP86] Roni Rosner et Amir Pnueli. A Choppy Logic. In LICS'86, pages 306-313. IEEE Comp. Soc. Press, juin 1986.
@inproceedings{lics1986-RP,
  author =              {Rosner, Roni and Pnueli, Amir},
  title =               {A Choppy Logic},
  booktitle =           {{P}roceedings of the 1st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'86)},
  acronym =             {{LICS}'86},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {306-313},
  year =                {1986},
  month =               jun,
}
[RP03] Stéphane Riedweg et Sophie Pinchinat. Quantified μ-Calculus for Control Synthesis. In MFCS'03, Lecture Notes in Computer Science 2747, pages 642-651. Springer-Verlag, août 2003.
@inproceedings{mfcs2003-RP,
  author =              {Riedweg, St{\'e}phane and Pinchinat, Sophie},
  title =               {Quantified {{\(\mu\)}}-Calculus for Control
                         Synthesis},
  editor =              {Rovan, Branislav and Vojt{\'a}s, Peter},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'03)},
  acronym =             {{MFCS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2747},
  pages =               {642-651},
  year =                {2003},
  month =               aug,
  doi =                 {10.1007/978-3-540-45138-9_58},
}
[RP03] Stéphane Riedweg et Sophie Pinchinat. Quantified Loop-mu-calculus for Control under Partial Observation. Research Report 4949, IRISA, Septembre 2003.
@techreport{inria4949-RP,
  author =              {Riedweg, St{\'e}phane and Pinchinat, Sophie},
  title =               {Quantified Loop-mu-calculus for Control under
                         Partial Observation},
  number =              {4949},
  year =                {2003},
  month =               sep,
  institution =         {IRISA},
  type =                {Research Report},
}
[RP03] Stéphane Riedweg et Sophie Pinchinat. Quantified Mu-calculus for Control Synthesis. Research Report 4793, IRISA, Avril 2003.
@techreport{inria4793-RP,
  author =              {Riedweg, St{\'e}phane and Pinchinat, Sophie},
  title =               {Quantified Mu-calculus for Control Synthesis},
  number =              {4793},
  year =                {2003},
  month =               apr,
  institution =         {IRISA},
  type =                {Research Report},
}
[RPV17] Nima Roohi, Pavithra Prabhakar et Mahesh Viswanathan. Robust model checking of timed automata under clock drifts. In HSCC'17, pages 153-162. ACM Press, avril 2017.
@inproceedings{hscc2017-RPV,
  author =              {Roohi, Nima and Prabhakar, Pavithra and Viswanathan,
                         Mahesh},
  title =               {Robust model checking of timed automata under clock
                         drifts},
  editor =              {Frehse, Goran and Mitra, Sayan},
  booktitle =           {{P}roceedings of the 20th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'14)},
  acronym =             {{HSCC}'17},
  publisher =           {ACM Press},
  pages =               {153-162},
  year =                {2017},
  month =               apr,
  doi =                 {10.1145/3049797.3049821},
}
[RR95] Olivier F. Roux et Vlad Rusu. Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata. In HSCC'94, Lecture Notes in Computer Science 999, pages 405-416. Springer-Verlag, 1995.
@inproceedings{hscc1994-RR,
  author =              {Roux, Olivier F. and Rusu, Vlad},
  title =               {Deciding time-bounded properties for {ELECTRE}
                         reactive programs with stopwatch automata},
  editor =              {Antsaklis, Panos and Kohn, Wolf and Nerode, Anil and
                         Sastry, Shankar},
  booktitle =           {{H}ybrid {S}ystems~{II} ({HSCC}'94)},
  acronym =             {{HSCC}'94},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {999},
  pages =               {405-416},
  year =                {1995},
}
[RRD+07] Talal Rahwan, Sarvapali D. Ramchurn, Viet Dung Dang, Andrea Giovannucci et Nicholas R. Jennings. Anytime Optimal Coalition Structure Generation. In AAAI-IAAI'07, pages 1184-1190. AAAI Press, juillet 2007.
@inproceedings{aaai2007-RRDGJ,
  author =              {Rahwan, Talal and Ramchurn, Sarvapali D. and Dung
                         Dang, Viet and Giovannucci, Andrea and Jennings,
                         Nicholas R.},
  title =               {Anytime Optimal Coalition Structure Generation},
  booktitle =           {{P}roceedings of the 22nd {N}ational {C}onference on
                         {A}rtificial {I}ntelligence ({AAAI}'07) and 19th
                         {I}nnovative {A}pplications of {A}rtificial
                         {I}ntelligence {C}onference ({IAAI}'07)},
  acronym =             {{AAAI-IAAI}'07},
  publisher =           {AAAI Press},
  pages =               {1184-1190},
  year =                {2007},
  month =               jul,
}
[RS59] Michael O. Rabin et Dana S. Scott. Finite automata and their decision problems. IBM Journal of Research and Development 3(2):114-125. Avril 1959.
@article{IBMJRD3(2)-RS,
  author =              {Rabin, Michael O. and Scott, Dana S.},
  title =               {Finite automata and their decision problems},
  journal =             {IBM Journal of Research and Development},
  volume =              {3},
  number =              {2},
  pages =               {114-125},
  year =                {1959},
  month =               apr,
  doi =                 {10.1147/rd.32.0114},
}
[RS84] Neil Robertson et Paul D. Seymour. Graph minors III: Planar tree-width. Journal of Combinatorial Theory, series B 86(1):49-64. Elsevier, février 1984.
@article{jctB36(1)-RS,
  author =              {Robertson, Neil and Seymour, Paul D.},
  title =               {Graph minors~{III}: Planar tree-width},
  publisher =           {Elsevier},
  journal =             {Journal of Combinatorial Theory, series~{B}},
  volume =              {86},
  number =              {1},
  pages =               {49-64},
  year =                {1984},
  month =               feb,
  doi =                 {10.1016/0095-8956(84)90013-3},
}
[RS86] Neil Robertson et Paul D. Seymour. Graph minors II: Algorithmic aspects of tree-width. Journal of Algorithms 7(3):309-322. Elsevier, septembre 1986.
@article{ja7(3)-RS,
  author =              {Robertson, Neil and Seymour, Paul D.},
  title =               {Graph minors~{II}: Algorithmic aspects of
                         tree-width},
  publisher =           {Elsevier},
  journal =             {Journal of Algorithms},
  volume =              {7},
  number =              {3},
  pages =               {309-322},
  year =                {1986},
  month =               sep,
  doi =                 {10.1016/0196-6774(86)90023-4},
}
[RS97] Jean-François Raskin et Pierre-Yves Schobbens. State Clock Logic: A Decidable Real-Time Logic. In HART'97, Lecture Notes in Computer Science 1201, pages 33-47. Springer-Verlag, mars 1997.
@inproceedings{hart1997-RS,
  author =              {Raskin, Jean-Fran{\c c}ois and Schobbens,
                         Pierre-Yves},
  title =               {State Clock Logic: A~Decidable Real-Time Logic},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {33-47},
  year =                {1997},
  month =               mar,
}
[RS99] Jean-François Raskin et Pierre-Yves Schobbens. The Logic of Event-Clocks: Decidability, Complexity and Expressiveness. Journal of Automata, Languages and Combinatorics 4(3):247-286. 1999.
@article{jalc4(3)-RS,
  author =              {Raskin, Jean-Fran{\c c}ois and Schobbens,
                         Pierre-Yves},
  title =               {The Logic of Event-Clocks: Decidability, Complexity
                         and Expressiveness},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {4},
  number =              {3},
  pages =               {247-286},
  year =                {1999},
}
[RS06] Alexander Rabinovich et Philippe Schnoebelen. BTL2 and Expressive Completeness for ECTL+. Information and Computation 204(7):1023-1044. Elsevier, juillet 2006.
@article{icomp204(7)-RS,
  author =              {Rabinovich, Alexander and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {{BTL}{\(_2\)} and Expressive Completeness for
                         {ECTL}{\(^+\)}},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {204},
  number =              {7},
  pages =               {1023-1044},
  year =                {2006},
  month =               jul,
}
[RS08] R. Ramanujam et Sunil Simon. Dynamic Logic on Games with Structured Strategies. In KR'08, pages 49-58. AAAI Press, septembre 2008.
@inproceedings{kr2008-RS,
  author =              {Ramanujam, R. and Simon, Sunil},
  title =               {Dynamic Logic on Games with Structured Strategies},
  editor =              {Brewka, Gerhard and Lang, J{\'e}r{\^o}me},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {P}rinciples of {K}nowledge
                         {R}epresentation and {R}easoning ({KR}'08)},
  acronym =             {{KR}'08},
  publisher =           {AAAI Press},
  pages =               {49-58},
  year =                {2008},
  month =               sep,
}
[RSM19] Victor Roussanaly, Ocan Sankur et Nicolas Markey. Abstraction Refinement Algorithms for Timed Automata. In CAV'19, Lecture Notes in Computer Science 11561, pages 22-40. Springer-Verlag, juillet 2019.
Résumé

We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.

@inproceedings{cav2019-RSM,
  author =              {Roussanaly, Victor and Sankur, Ocan and Markey,
                         Nicolas},
  title =               {Abstraction Refinement Algorithms for Timed
                         Automata},
  editor =              {Dillig, I{\c s}il and Ta{\c s}iran, Serdar},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'19)},
  acronym =             {{CAV}'19},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {11561},
  pages =               {22-40},
  year =                {2019},
  month =               jul,
  doi =                 {10.1007/978-3-030-25540-4_2},
  abstract =            {We~present abstraction-refinement algorithms for
                         model checking safety properties of timed automata.
                         The~abstraction domain we consider abstracts away
                         zones by restricting the set of clock constraints
                         that can be used to define them, while the
                         refinement procedure computes the set of constraints
                         that must be taken into consideration in the
                         abstraction so as to exclude a given spurious
                         counterexample. We~implement this idea in two~ways:
                         an~enumerative algorithm where a lazy abstraction
                         approach is adopted, meaning that possibly different
                         abstract domains are assigned to each exploration
                         node; and a symbolic algorithm where the abstract
                         transition system is encoded with Boolean formulas.},
}
[RT98] Jérôme Renault et Tristan Tomala. Repeated proximity games. International Journal of Game Theory 27(4):539-559. Springer-Verlag, décembre 1998.
@article{ijgt27(4)-RT,
  author =              {Renault, J{\'e}r{\^o}me and Tomala, Tristan},
  title =               {Repeated proximity games},
  publisher =           {Springer-Verlag},
  journal =             {International Journal of Game Theory},
  volume =              {27},
  number =              {4},
  pages =               {539-559},
  year =                {1998},
  month =               dec,
}
[RT01] Michaël Rusinowitch et Mathieu Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. Research Report 4134, LORIA, Nancy, France, Mars 2001.
@techreport{inria4134-RT,
  author =              {Rusinowitch, Micha{\"e}l and Turuani, Mathieu},
  title =               {Protocol Insecurity with Finite Number of Sessions
                         is {NP}-complete},
  number =              {4134},
  year =                {2001},
  month =               mar,
  institution =         {LORIA, Nancy, France},
  type =                {Research Report},
}
[RT02] Tim Roughgarden et Éva Tardos. How bad is selfish routing?. Journal of the ACM 49(2):236-259. ACM Press, mars 2002.
@article{jacm49(2)-RT,
  author =              {Roughgarden, Tim and Tardos, {\'E}va},
  title =               {How bad is selfish routing?},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {49},
  number =              {2},
  pages =               {236-259},
  year =                {2002},
  month =               mar,
  doi =                 {10.1145/506147.506153},
}
[RT04] Tim Roughgarden et Éva Tardos. Bounding the inefficiency of equilibria in non-atomic congestion games. Games and Economic Behavior 47(2):389-403. Mai 2004.
@article{geb47(2)-RT,
  author =              {Roughgarden, Tim and Tardos, {\'E}va},
  title =               {Bounding the inefficiency of equilibria in
                         non-atomic congestion games},
  journal =             {Games and Economic Behavior},
  volume =              {47},
  number =              {2},
  pages =               {389-403},
  year =                {2004},
  month =               may,
  doi =                 {10.1016/j.geb.2003.06.004},
}
[RT08] Frank G. Radmacher et Wolfgang Thomas. A Game Theoretic Approach to the Analysis of Dynamic Networks. In VerAS'07, Electronic Notes in Theoretical Computer Science 200(2), pages 21-37. Elsevier, février 2008.
@inproceedings{veras2007-RT,
  author =              {Radmacher, Frank G. and Thomas, Wolfgang},
  title =               {A~Game Theoretic Approach to the Analysis of Dynamic
                         Networks},
  editor =              {Ballis, Demis and Escobar, Santiago and Marchiori,
                         Massimo},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on
                         {V}erification of {A}daptive {S}ystems ({VerAS}'07)},
  acronym =             {{VerAS}'07},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {200(2)},
  pages =               {21-37},
  year =                {2008},
  month =               feb,
  confyear =            {2007},
}
[Ruf01] Jürgen Ruf. RAVEN: Real-Time Analyzing and Verification Environment. Journal of Universal Computer Science 7(1):89-104. Know-Center, Technische Universität Graz, Austria, janvier 2001.
@article{jucs7(1)-Ruf,
  author =              {Ruf, J{\"u}rgen},
  title =               {{RAVEN}: {R}eal-Time Analyzing and Verification
                         Environment},
  publisher =           {Know-Center, Technische Universit{\"a}t Graz,
                         Austria},
  journal =             {Journal of Universal Computer Science},
  volume =              {7},
  number =              {1},
  pages =               {89-104},
  year =                {2001},
  month =               jan,
}
[Rut01] Éric Rutten. A Framework for Using Discrete Control Synthesis in Safe Robotic Programming and Teleoperation. In ICRA'01, pages 4104-4109. IEEE Comp. Soc. Press, mai 2001.
@inproceedings{icra2001-Rut,
  author =              {Rutten, {\'E}ric},
  title =               {A Framework for Using Discrete Control Synthesis in
                         Safe Robotic Programming and Teleoperation},
  booktitle =           {{P}roceedings of the 2001 {IEEE} {I}nternational
                         {C}onference on {R}obotics and {A}utomation
                         ({ICRA}'01)},
  acronym =             {{ICRA}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {4104-4109},
  year =                {2001},
  month =               may,
}
[Rut11] Michał Rutkowski. Two-Player Reachability-Price Games on Single-Clock Timed Automata. In QAPL'11, Electronic Proceedings in Theoretical Computer Science 57, pages 31-46. Massink, Mieke and Norman, Gethin, avril 2011.
@inproceedings{qapl2011-Rut,
  author =              {Rutkowski, Micha{\l}},
  title =               {Two-Player Reachability-Price Games on Single-Clock
                         Timed Automata},
  booktitle =           {{P}roceedings of the 9th {W}orkshop on
                         {Q}uantitative {A}spects of {P}rogramming
                         {L}anguages ({QAPL}'11)},
  acronym =             {{QAPL}'11},
  publisher =           {Massink, Mieke and Norman, Gethin},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {57},
  pages =               {31-46},
  year =                {2011},
  month =               apr,
}
[Ruz81] Walter L. Ruzzo. On uniform circuit complexity. Journal of Computer and System Sciences 22(3):365-383. Academic Press, juin 1981.
@article{jcss22(3)-Ruz,
  author =              {Ruzzo, Walter L.},
  title =               {On uniform circuit complexity},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {22},
  number =              {3},
  pages =               {365-383},
  year =                {1981},
  month =               jun,
  doi =                 {10.1016/0022-0000(81)90038-6},
}
[RV76] Ronald L. Rivest et Jean Vuillemin. On Recognizing Graph Properties from Adjacency Matrices. Theoretical Computer Science 3(3):371-384. Elsevier, 1976.
@article{tcs3(3)-RV,
  author =              {Rivest, Ronald L. and Vuillemin, Jean},
  title =               {On Recognizing Graph Properties from Adjacency
                         Matrices},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {3},
  number =              {3},
  pages =               {371-384},
  year =                {1976},
}
[RV98] Steffen Reith et Heribert Vollmer. The Complexity of Computing Optimal Assignments of Generalized Propositional Formulae. Research Report cs.CC/9809116, arXiv, Septembre 1998.
@techreport{arxiv-cs.CC/9809116,
  author =              {Reith, Steffen and Vollmer, Heribert},
  title =               {The Complexity of Computing Optimal Assignments of
                         Generalized Propositional Formulae},
  number =              {cs.CC/9809116},
  year =                {1998},
  month =               sep,
  institution =         {arXiv},
  type =                {Research Report},
}
[RW87] Peter J. Ramadge et W. Murray Wonham. Supervisory Control of a Class of Discrete Event Processes. SIAM Journal on Control and Optimization 25(1):206-230. Society for Industrial and Applied Math., janvier 1987.
@article{siamjco25(1)-RW,
  author =              {Ramadge, Peter J. and Wonham, W. Murray},
  title =               {Supervisory Control of a Class of Discrete Event
                         Processes},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Control and Optimization},
  volume =              {25},
  number =              {1},
  pages =               {206-230},
  year =                {1987},
  month =               jan,
  doi =                 {10.1137/0325013},
}
[RW89] Peter J. Ramadge et W. Murray Wonham. The Control of Discrete Event Systems. Proceedings of the IEEE 77(1):81-98. IEEE Comp. Soc. Press, janvier 1989.
@article{ieee77(1)-RW,
  author =              {Ramadge, Peter J. and Wonham, W. Murray},
  title =               {The Control of Discrete Event Systems},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {Proceedings of the IEEE},
  volume =              {77},
  number =              {1},
  pages =               {81-98},
  year =                {1989},
  month =               jan,
}
[RY86] Louis E. Rosier et Hsu-Chun Yen. A Multiparameter Analysis of the Boundedness Problem for Vector Addition Systems. Journal of Computer and System Sciences 32(1):105-135. Academic Press, février 1986.
@article{jcss32(1)-RY,
  author =              {Rosier, Louis E. and Yen, Hsu-Chun},
  title =               {A~Multiparameter Analysis of the Boundedness Problem
                         for Vector Addition Systems},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {32},
  number =              {1},
  pages =               {105-135},
  year =                {1986},
  month =               feb,
  doi =                 {10.1016/0022-0000(86)90006-1},
}
[Rys83] Igor K. Rystsov. Polynomial-complete problems in automata theory. Information Processing Letters 16(1):147-151. Elsevier, avril 1983.
@article{ipl16(3)-Rys,
  author =              {Rystsov, Igor K.},
  title =               {Polynomial-complete problems in automata theory},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {16},
  number =              {1},
  pages =               {147-151},
  year =                {1983},
  month =               apr,
  doi =                 {10.1016/0020-0190(83)90067-4},
}
[Ryt99] Wojciech Rytter. Algorithms on Compressed Strings and Arrays. In SOFSEM'99, Lecture Notes in Computer Science 1725, pages 48-65. Springer-Verlag, novembre 1999.
@inproceedings{sofsem1999-Ryt,
  author =              {Rytter, Wojciech},
  title =               {Algorithms on Compressed Strings and Arrays},
  editor =              {Pavelka, Jan and Tel, Gerard and Bartosek, Miroslav},
  booktitle =           {{P}roceedings of the 26th {C}onference on {C}urrent
                         {T}rends in {T}heory and {P}ractice of {I}nformatics
                         ({SOFSEM}'99)},
  acronym =             {{SOFSEM}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1725},
  pages =               {48-65},
  year =                {1999},
  month =               nov,
}
[Ryt00] Wojciech Rytter. Compressed and Fully Compressed Pattern-Matching in One and Two Dimensions. Proceedings of the IEEE 88(11):1769 - 1778. IEEE Comp. Soc. Press, novembre 2000.
@article{ieee88(11)-Ryt,
  author =              {Rytter, Wojciech},
  title =               {Compressed and Fully Compressed Pattern-Matching in
                         One and Two Dimensions},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {Proceedings of the IEEE},
  volume =              {88},
  number =              {11},
  pages =               {1769 - 1778},
  year =                {2000},
  month =               nov,
  doi =                 {10.1109/5.892712},
}
[Ryt03] Wojciech Rytter. Application of Lempel-Ziv Factorization to the Approximation of Grammar-Based Compression. Theoretical Computer Science 302(1-3):211-222. Elsevier, juin 2003.
@article{tcs302(1-3)-Ryt,
  author =              {Rytter, Wojciech},
  title =               {Application of {L}empel-{Z}iv Factorization to the
                         Approximation of Grammar-Based Compression},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {302},
  number =              {1-3},
  pages =               {211-222},
  year =                {2003},
  month =               jun,
}
Liste des auteurs