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, July 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, February 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, August 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, June 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, May 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, August 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, and 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, January 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, May 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, June 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 and 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, March 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, and 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, March 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, October 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, September 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, October 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, September 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, March 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, August 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, June 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, May 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 and Jean Goubault-Larrecq. Log Auditing through Model-Checking. In CSFW'01, pages 220-236. IEEE Comp. Soc. Press, June 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, and Kevin Leyton-Brown. Symmetric Games with Piecewise Linear Utilities. In BQGT'10. ACM Press, May 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 and 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, March 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 and Thomas Kropf. Analyzing Real-Time Systems. In DATE'00, pages 243-248. IEEE Comp. Soc. Press, March 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, and K. Subramani. On using priced timed automata to achieve optimal scheduling. Formal Methods in System Design 29(1):97-114. Springer-Verlag, July 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 and 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, August 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 and Shahar Maoz. An Infinite Hierarchy of Temporal Logics over Branching Time. Information and Computation 171(2):306-332. Academic Press, December 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, and George Kutty. An Automata Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until. Fundamenta Informaticae 17(3):272-282. IOS Press, November 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 and 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, October 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, December 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, January 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, September 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, October 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, and 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, November 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 and Amir Pnueli. A Choppy Logic. In LICS'86, pages 306-313. IEEE Comp. Soc. Press, June 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 and Sophie Pinchinat. Quantified μ-Calculus for Control Synthesis. In MFCS'03, Lecture Notes in Computer Science 2747, pages 642-651. Springer-Verlag, August 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 and Sophie Pinchinat. Quantified Loop-mu-calculus for Control under Partial Observation. Research Report 4949, IRISA, September 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 and Sophie Pinchinat. Quantified Mu-calculus for Control Synthesis. Research Report 4793, IRISA, April 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, and Mahesh Viswanathan. Robust model checking of timed automata under clock drifts. In HSCC'17, pages 153-162. ACM Press, April 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 and 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, and Nicholas R. Jennings. Anytime Optimal Coalition Structure Generation. In AAAI-IAAI'07, pages 1184-1190. AAAI Press, July 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 and Dana S. Scott. Finite automata and their decision problems. IBM Journal of Research and Development 3(2):114-125. April 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 and Paul D. Seymour. Graph minors III: Planar tree-width. Journal of Combinatorial Theory, series B 86(1):49-64. Elsevier, February 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 and Paul D. Seymour. Graph minors II: Algorithmic aspects of tree-width. Journal of Algorithms 7(3):309-322. Elsevier, September 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 and 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, March 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 and 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 and Philippe Schnoebelen. BTL2 and Expressive Completeness for ECTL+. Information and Computation 204(7):1023-1044. Elsevier, July 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 and Sunil Simon. Dynamic Logic on Games with Structured Strategies. In KR'08, pages 49-58. AAAI Press, September 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, and Nicolas Markey. Abstraction Refinement Algorithms for Timed Automata. In CAV'19, Lecture Notes in Computer Science 11561, pages 22-40. Springer-Verlag, July 2019.
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.

@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 and Tristan Tomala. Repeated proximity games. International Journal of Game Theory 27(4):539-559. Springer-Verlag, December 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 and Mathieu Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. Research Report 4134, LORIA, Nancy, France, March 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 and Éva Tardos. How bad is selfish routing?. Journal of the ACM 49(2):236-259. ACM Press, March 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 and Éva Tardos. Bounding the inefficiency of equilibria in non-atomic congestion games. Games and Economic Behavior 47(2):389-403. May 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 and 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, February 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, January 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, May 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, April 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, June 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 and 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 and Heribert Vollmer. The Complexity of Computing Optimal Assignments of Generalized Propositional Formulae. Research Report cs.CC/9809116, arXiv, September 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 and 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., January 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 and W. Murray Wonham. The Control of Discrete Event Systems. Proceedings of the IEEE 77(1):81-98. IEEE Comp. Soc. Press, January 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 and 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, February 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, April 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, November 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, November 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, June 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,
}
List of authors