2003
[Mar03] Nicolas Markey. Temporal Logic with Past is Exponentially More Succinct. EATCS Bulletin 79:122-128. EATCS, February 2003.
Abstract

We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.

@article{eatcs-bull79()-Mar,
  author =              {Markey, Nicolas},
  title =               {Temporal Logic with Past is Exponentially More
                         Succinct},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {79},
  pages =               {122-128},
  year =                {2003},
  month =               feb,
  abstract =            {We positively answer the old question whether
                         temporal logic with past is more succinct than
                         pure-future temporal logic. Surprisingly, the proof
                         is quite simple and elementary, although the
                         question has been open for twenty years.},
}
[MS03] Nicolas Markey and Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In CONCUR'03, Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, August 2003.
Abstract

We consider the problem of checking whether a finite (or ultimately periodic) run satisfies a temporal logic formula. This problem is at the heart of "runtime verification" but it also appears in many other situations. By considering several extended temporal logics, we show that the problem of model checking a path can usually be solved efficiently, and profit from specialized algorithms. We further show it is possible to efficiently check paths given in compressed form.

@inproceedings{concur2003-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking a Path (Preliminary Report)},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {251-265},
  year =                {2003},
  month =               aug,
  doi =                 {10.1007/978-3-540-45187-7_17},
  abstract =            {We consider the problem of checking whether a finite
                         (or ultimately periodic) run satisfies a temporal
                         logic formula. This problem is at the heart of
                         {"}runtime verification{"} but it also appears in
                         many other situations. By considering several
                         extended temporal logics, we show that the problem
                         of model checking a path can usually be solved
                         efficiently, and profit from specialized algorithms.
                         We further show it is possible to efficiently check
                         paths given in compressed form.},
}
[Mar03] Nicolas Markey. Logiques temporelles pour la vérification : expressivité, complexité, algorithmes. Thèse de doctorat, Lab. Informatique Fondamentale d'Orléans, France, April 2003. 
@phdthesis{phd2003-Mar,
  author =              {Markey, Nicolas},
  title =               {Logiques temporelles pour la v{\'e}rification~:
                         expressivit{\'e}, complexit{\'e}, algorithmes},
  year =                {2003},
  month =               apr,
  school =              {Lab.~Informatique Fondamentale d'Orl{\'e}ans,
                         France},
  type =                {Th\`ese de doctorat},
}
[dA03] Luca de Alfaro. Quantitative Verification and Control via the Mu-Calculus. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 102-126. Springer-Verlag, August 2003. 
@inproceedings{concur2003-Alf,
  author =              {de Alfaro, Luca},
  title =               {Quantitative Verification and Control via the
                         Mu-Calculus},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {102-126},
  year =                {2003},
  month =               aug,
}
[ABB+03] Luca Aceto, Patricia Bouyer, Augusto Burgueño, and Kim Guldstrand Larsen. The Power of Reachability Testing for Timed Automata. Theoretical Computer Science 300(1-3):411-475. Elsevier, May 2003. 
@article{tcs300(1-3)-ABBL,
  author =              {Aceto, Luca and Bouyer, Patricia and Burgue{\~n}o,
                         Augusto and Larsen, Kim Guldstrand},
  title =               {The~Power of Reachability Testing for Timed
                         Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {300},
  number =              {1-3},
  pages =               {411-475},
  year =                {2003},
  month =               may,
  doi =                 {10.1016/S0304-3975(02)00334-1},
}
[ABK+03] Roy Armoni, Doron Bustan, Orna Kupferman, and Moshe Y. Vardi. Resets vs. Aborts in Linear Temporal Logic. In TACAS'03, Lecture Notes in Computer Science 2619, pages 65-80. Springer-Verlag, April 2003. 
@inproceedings{tacas2003-ABKV,
  author =              {Armoni, Roy and Bustan, Doron and Kupferman, Orna
                         and Vardi, Moshe Y.},
  title =               {Resets {vs.} Aborts in Linear Temporal Logic},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {65-80},
  year =                {2003},
  month =               apr,
}
[AFF+03] Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, and Moshe Y. Vardi. Enhanced Vacuity Detection in Linear Temporal Logic. In CAV'03, Lecture Notes in Computer Science 2725, pages 368-380. Springer-Verlag, July 2003. 
@inproceedings{cav2003-AFFGPTV,
  author =              {Armoni, Roy and Fix, Limor and Flaisher, Alon and
                         Grumberg, Orna and Piterman, Nir and Tiemeyer,
                         Andreas and Vardi, Moshe Y.},
  title =               {Enhanced Vacuity Detection in Linear Temporal Logic},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {368-380},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_35},
}
[dAF+03] Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The Element of Surprise in Timed Games. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 142-156. Springer-Verlag, August 2003. 
@inproceedings{concur2003-AFHMS,
  author =              {de Alfaro, Luca and Faella, Marco and Henzinger,
                         Thomas A. and Majumdar, Rupak and Stoelinga,
                         Mari{\"e}lle},
  title =               {The Element of Surprise in Timed Games},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {142-156},
  year =                {2003},
  month =               aug,
}
[AI03] Micah Adler and Neil Immerman. An n! Lower Bound On Formula Size. ACM Transactions on Computational Logic 4(3):296-314. ACM Press, July 2003. 
@article{tocl4(3)-AI,
  author =              {Adler, Micah and Immerman, Neil},
  title =               {An {{\(n!\)}} Lower Bound On Formula Size},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {4},
  number =              {3},
  pages =               {296-314},
  year =                {2003},
  month =               jul,
}
[AJ03] Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science 290(1):241-264. Elsevier, January 2003. 
@article{tcs290(1)-AJ,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt},
  title =               {Model checking of systems with many identical timed
                         processes},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {290},
  number =              {1},
  pages =               {241-264},
  year =                {2003},
  month =               jan,
  doi =                 {10.1016/S0304-3975(01)00330-9},
}
[AKM03] Yasmina Abdeddaïm, Abdelkarim Kerbaa, and Oded Maler. Task Graph Scheduling Using Timed Automata. In IPDPS'03, pages 237. IEEE Comp. Soc. Press, April 2003. 
@inproceedings{ipdps2003-AKM,
  author =              {Abdedda{\"\i}m, Yasmina and Kerbaa, Abdelkarim and
                         Maler, Oded},
  title =               {Task Graph Scheduling Using Timed Automata},
  booktitle =           {{P}roceedings of the 17th International Parallel and
                         Distributed Processing Symposium ({IPDPS}'03)},
  acronym =             {{IPDPS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {237},
  year =                {2003},
  month =               apr,
}
[ALM03] Rajeev Alur, Salvatore La Torre, and Parthasarathy Madhusudan. Playing Games with Boxes and Diamonds. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 127-141. Springer-Verlag, August 2003. 
@inproceedings{concur2003-ALM,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and
                         Madhusudan, Parthasarathy},
  title =               {Playing Games with Boxes and Diamonds},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {127-141},
  year =                {2003},
  month =               aug,
}
[AVW03] André Arnold, Aymeric Vincent, and Igor Walukiewicz. Games for Synthesis of Controllers with Partial Observation. Theoretical Computer Science 303(1):7-34. Elsevier, June 2003. 
@article{tcs303(1)-AVW,
  author =              {Arnold, Andr{\'e} and Vincent, Aymeric and
                         Walukiewicz, Igor},
  title =               {Games for Synthesis of Controllers with Partial
                         Observation},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {303},
  number =              {1},
  pages =               {7-34},
  year =                {2003},
  month =               jun,
}
[BBF+03] Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, and Kim Guldstrand Larsen. Static Guard Analysis in Timed Automata Verification. In TACAS'03, Lecture Notes in Computer Science 2619, pages 254-270. Springer-Verlag, April 2003. 
@inproceedings{tacas2003-BBFL,
  author =              {Behrmann, Gerd and Bouyer, Patricia and Fleury,
                         Emmanuel and Larsen, Kim Guldstrand},
  title =               {Static Guard Analysis in Timed Automata
                         Verification},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {254-270},
  year =                {2003},
  month =               apr,
}
[BC03] Marco Benedetti and Alessandro Cimatti. Bounded Model Checking for Past LTL. In TACAS'03, Lecture Notes in Computer Science 2619, pages 18-33. Springer-Verlag, April 2003. 
@inproceedings{tacas2003-BC,
  author =              {Benedetti, Marco and Cimatti, Alessandro},
  title =               {Bounded Model Checking for Past {LTL}},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {18-33},
  year =                {2003},
  month =               apr,
}
[BCC+03] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded Model Checking. In Marvin Zelkowitz (eds.), Highly Dependable Software, Advances in Computers 58, pages 117-148. Academic Press, 2003. 
@incollection{AC58-BCCSZ,
  author =              {Biere, Armin and Cimatti, Alessandro and Clarke,
                         Edmund M. and Strichman, Ofer and Zhu, Yunshan},
  title =               {Bounded Model Checking},
  editor =              {Zelkowitz, Marvin},
  booktitle =           {Highly Dependable Software},
  publisher =           {Academic Press},
  series =              {Advances in Computers},
  volume =              {58},
  pages =               {117-148},
  chapter =             {3},
  year =                {2003},
}
[BCF03] Harry Buhrman, Richard Chang, and Lance Fortnow. One Bit of Advice. In STACS'03, Lecture Notes in Computer Science 2607, pages 547-558. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-BCF,
  author =              {Buhrman, Harry and Chang, Richard and Fortnow,
                         Lance},
  title =               {One Bit of Advice},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {547-558},
  year =                {2003},
  month =               feb,
}
[BDM+03] Patricia Bouyer, Deepak D'Souza, Parthasarathy Madhusudan, and Antoine Petit. Timed Control with Partial Observability. In CAV'03, Lecture Notes in Computer Science 2725, pages 180-192. Springer-Verlag, July 2003. 
@inproceedings{cav2003-BDMP,
  author =              {Bouyer, Patricia and D'Souza, Deepak and Madhusudan,
                         Parthasarathy and Petit, Antoine},
  title =               {Timed Control with Partial Observability},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {180-192},
  year =                {2003},
  month =               jul,
}
[BDR03] Véronique Bruyère, Emmanuel Dall'Olio, and Jean-François Raskin. Durations, Parametric Model Checking in Timed Automata with Presburger Arithmetic. In STACS'03, Lecture Notes in Computer Science 2607, pages 687-698. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-BDR,
  author =              {Bruy{\`e}re, V{\'e}ronique and Dall'Olio, Emmanuel
                         and Raskin, Jean-Fran{\c c}ois},
  title =               {Durations, Parametric Model Checking in Timed
                         Automata with {P}resburger Arithmetic},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {687-698},
  year =                {2003},
  month =               feb,
}
[Bea03] Danièle Beauquier. On probabilistic timed automata. Theoretical Computer Science 292(1):65-84. Elsevier, January 2003. 
@article{tcs292(1)-Bea,
  author =              {Beauquier, Dani{\`e}le},
  title =               {On~probabilistic timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {292},
  number =              {1},
  pages =               {65-84},
  year =                {2003},
  month =               jan,
  doi =                 {10.1016/S0304-3975(01)00215-8},
}
[BFH+03] Albert Benveniste, Éric Fabre, Stefan Haar, and Claude Jard. Diagnosis of asynchronous discrete event systems: A net-unfolding approach. IEEE Transactions on Automatic Control 48(5):714-727. IEEE Comp. Soc. Press, 2003. 
@article{tac48(5)-BFHJ,
  author =              {Benveniste, Albert and Fabre, {\'E}ric and Haar,
                         Stefan and Jard, Claude},
  title =               {Diagnosis of asynchronous discrete event systems:
                         A~net-unfolding approach},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Automatic Control},
  volume =              {48},
  number =              {5},
  pages =               {714-727},
  year =                {2003},
  doi =                 {10.1109/TAC.2003.811249},
}
[BG03] Régis Barbanchon and Étienne Grandjean. The Minimal Logically-Defined NP-Complete Problem. In STACS'04, Lecture Notes in Computer Science 2996, pages 338-349. Springer-Verlag, March 2003. 
@inproceedings{stacs2004-BG,
  author =              {Barbanchon, R{\'e}gis and Grandjean, {\'E}tienne},
  title =               {The Minimal Logically-Defined {NP}-Complete Problem},
  editor =              {Diekert, Volker and Habib, Michel},
  booktitle =           {{P}roceedings of the 21st {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'04)},
  acronym =             {{STACS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2996},
  pages =               {338-349},
  year =                {2003},
  month =               mar,
}
[BHJ03] Bernard Boigelot, Frédéric Herbreteau, and Sébastien Jodogne. Hybrid Acceleration using Real Vector Automata (extended abstract). In CAV'03, Lecture Notes in Computer Science 2725, pages 193-205. Springer-Verlag, July 2003. 
@inproceedings{cav2003-BHJ,
  author =              {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
                         and Jodogne, S{\'e}bastien},
  title =               {Hybrid Acceleration using Real Vector Automata
                         (extended abstract)},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {193-205},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_19},
}
[BHJ03] Bernard Boigelot, Frédéric Herbreteau, and Sébastien Jodogne. Hybrid Acceleration using Real Vector Automata. Technical Report 2003.18, Centre Fédéré en Vérification, Bruxelles, Belgium, 2003. 
@techreport{TR-cfv0318,
  author =              {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
                         and Jodogne, S{\'e}bastien},
  title =               {Hybrid Acceleration using Real Vector Automata},
  number =              {2003.18},
  year =                {2003},
  institution =         {Centre F\'ed\'er\'e en V\'erification, Bruxelles,
                         Belgium},
  type =                {Technical Report},
}
[BLN03] Dirk Beyer, Claus Lewerentz, and Andreas Noack. Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. In CAV'03, Lecture Notes in Computer Science 2725, pages 122-125. Springer-Verlag, July 2003. 
@inproceedings{cav2003-BLN,
  author =              {Beyer, Dirk and Lewerentz, Claus and Noack, Andreas},
  title =               {Rabbit: A~Tool for {BDD}-Based Verification of
                         Real-Time Systems},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {122-125},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_13},
}
[BLP03] Gerd Behrmann, Kim Guldstrand Larsen, and Radek Pelánek. To Store or not to Store. In CAV'03, Lecture Notes in Computer Science 2725, pages 433-445. Springer-Verlag, July 2003. 
@inproceedings{cav2003-BLP,
  author =              {Behrmann, Gerd and Larsen, Kim Guldstrand and
                         Pel{\'a}nek, Radek},
  title =               {To Store or not to Store},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {433-445},
  year =                {2003},
  month =               jul,
}
[Bou03] Patricia Bouyer. Untameable Timed Automata!. In STACS'03, Lecture Notes in Computer Science 2607, pages 620-631. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-Bou,
  author =              {Bouyer, Patricia},
  title =               {Untameable Timed Automata!},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {620-631},
  year =                {2003},
  month =               feb,
  doi =                 {10.1007/3-540-36494-3_54},
}
[BP03] Bruno Blanchet and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Temrination. In FoSSaCS'03, Lecture Notes in Computer Science 2620, pages 136-152. Springer-Verlag, April 2003. 
@inproceedings{fossacs2003-BP,
  author =              {Blanchet, Bruno and Podelski, Andreas},
  title =               {Verification of Cryptographic Protocols: Tagging
                         Enforces Temrination},
  editor =              {Gordon, Andrew D.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'03)},
  acronym =             {{FoSSaCS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2620},
  pages =               {136-152},
  year =                {2003},
  month =               apr,
}
[BR03] Véronique Bruyère and Jean-François Raskin. Real-Time Model-Checking: Parameters Everywhere. In FSTTCS'03, Lecture Notes in Computer Science 2914, pages 100-111. Springer-Verlag, December 2003. 
@inproceedings{fsttcs2003-BR,
  author =              {Bruy{\`e}re, V{\'e}ronique and Raskin, Jean-Fran{\c
                         c}ois},
  title =               {Real-Time Model-Checking: {P}arameters Everywhere},
  editor =              {Pandya, Paritosh K. and Radhakrishnan, Jaikumar},
  booktitle =           {{P}roceedings of the 23rd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'03)},
  acronym =             {{FSTTCS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2914},
  pages =               {100-111},
  year =                {2003},
  month =               dec,
}
[BY03] Johan Bengtsson and Wang Yi. On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata. In ICFEM'03. Springer-Verlag, November 2003. 
@incollection{icfem2003-BY,
  author =              {Bengtsson, Johan and Yi, Wang},
  title =               {On Clock Difference Constraints and Termination in
                         Reachability Analysis of Timed Automata},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}ormal {E}ngineering {M}ethods
                         ({ICFEM}'03)},
  acronym =             {{ICFEM}'03},
  publisher =           {Springer-Verlag},
  pages =               {491-503},
  year =                {2003},
  month =               nov,
}
[Cac03] Thierry Cachat. Games on Pushdown Graphs and Extensions. Thèse de doctorat, RWTH Aachen, Germany, December 2003. 
@phdthesis{phd-cachat,
  author =              {Cachat, Thierry},
  title =               {Games on Pushdown Graphs and Extensions},
  year =                {2003},
  month =               dec,
  school =              {RWTH Aachen, Germany},
  type =                {Th\`ese de doctorat},
}
[CdA+03] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource Interfaces. In EMSOFT'03, Lecture Notes in Computer Science 2855, pages 117-133. Springer-Verlag, October 2003. 
@inproceedings{emsoft2003-CdAHS,
  author =              {Chakrabarti, Arindam and de Alfaro, Luca and
                         Henzinger, Thomas A. and Stoelinga, Mari{\"e}lle},
  title =               {Resource Interfaces},
  editor =              {Alur, Rajeev and Lee, Insup},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'03)},
  acronym =             {{EMSOFT}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2855},
  pages =               {117-133},
  year =                {2003},
  month =               oct,
  doi =                 {10.1007/978-3-540-45212-6_9},
}
[Cai03] Benoît Caillaud. Project-Team S4. Activity Report, IRISA, Rennes, France, 2003. 
@techreport{AR-s4-2003,
  author =              {Caillaud, Beno{\^\i}t},
  title =               {Project-Team {S4}},
  year =                {2003},
  institution =         {IRISA, Rennes, France},
  type =                {Activity Report},
}
[CFH+03] Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, and Michael Theobald. Abstraction and Countrexample-Guided Refinement in Model Checking of Hybrid Systems. International Journal of Foundations of Computer Science 14(4):583-604. August 2003. 
@article{ijfcs14(4)-CFHKOST,
  author =              {Clarke, Edmund M. and Fehnker, Ansgar and Han, Zhi
                         and Krogh, Bruce H. and Ouaknine, Jo{\"e}l and
                         Stursberg, Olaf and Theobald, Michael},
  title =               {Abstraction and Countrexample-Guided Refinement in
                         Model Checking of Hybrid Systems},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {14},
  number =              {4},
  pages =               {583-604},
  year =                {2003},
  month =               aug,
  doi =                 {10.1142/S012905410300190X},
}
[CGJ+03] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM 50(5):752-794. ACM Press, September 2003. 
@article{jacm50(5)-CGJLV,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Jha, Somesh
                         and Lu, Yuan and Veith, Helmut},
  title =               {Counterexample-Guided Abstraction Refinement for
                         Symbolic Model Checking},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {50},
  number =              {5},
  pages =               {752-794},
  year =                {2003},
  month =               sep,
  doi =                 {10.1145/876638.876643},
}
[Cho03] Hana Chockler. Coverage Metrics for Model Checking. PhD thesis, Hebrew University, Jerusalem, Israel, September 2003. 
@phdthesis{phd-chockler,
  author =              {Chockler, Hana},
  title =               {Coverage Metrics for Model Checking},
  year =                {2003},
  month =               sep,
  school =              {Hebrew University, Jerusalem, Israel},
}
[CL03] Thomas Colcombet and Christof Löding. On the Expressiveness of Deterministic transducers over Infinite Trees. In STACS'04, Lecture Notes in Computer Science 2996, pages 428-439. Springer-Verlag, March 2003. 
@inproceedings{stacs2004-CL,
  author =              {Colcombet, {\relax Th}omas and L{\"o}ding, Christof},
  title =               {On the Expressiveness of Deterministic transducers
                         over Infinite Trees},
  editor =              {Diekert, Volker and Habib, Michel},
  booktitle =           {{P}roceedings of the 21st {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'04)},
  acronym =             {{STACS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2996},
  pages =               {428-439},
  year =                {2003},
  month =               mar,
}
[CL03] Maxime Crochemore and Thierry Lecrocq. Pattern Matching and Text Compression Algorithms. In Allen B. Tucker (eds.), Computer Science and Engineering Handbook. CRC Press, 2003. 
@incollection{CSEH2003-CL,
  author =              {Crochemore, Maxime and Lecrocq, {\relax Th}ierry},
  title =               {Pattern Matching and Text Compression Algorithms},
  editor =              {Tucker, Allen B.},
  booktitle =           {Computer Science and Engineering Handbook},
  publisher =           {CRC Press},
  pages =               {161-202},
  year =                {2003},
}
[CM03] Olivier Carton and Max Michel. Unambiguous Büchi Automata. Theoretical Computer Science 297(1-3):37-81. Elsevier, March 2003. 
@article{tcs297(1-3)-CM,
  author =              {Carton, Olivier and Michel, Max},
  title =               {Unambiguous B{\"u}chi Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {297},
  number =              {1-3},
  pages =               {37-81},
  year =                {2003},
  month =               mar,
}
[CS03] Maxime Crochemore and Valery T. Stefanov. Waiting time and complexity for matching patterns with automata. Information Processing Letters 87(3):119-125. Elsevier, August 2003. 
@article{ipl87(3)-CS,
  author =              {Crochemore, Maxime and Stefanov, Valery T.},
  title =               {Waiting time and complexity for matching patterns
                         with automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {87},
  number =              {3},
  pages =               {119-125},
  year =                {2003},
  month =               aug,
  doi =                 {10.1016/S0020-0190(03)00271-0},
}
[vD03] Govert van Drimmelen. Satisfiability in Alternating-time Temporal Logic. In LICS'03, pages 208-217. IEEE Comp. Soc. Press, June 2003. 
@inproceedings{lics2003-vD,
  author =              {van Drimmelen, Govert},
  title =               {Satisfiability in Alternating-time Temporal Logic},
  booktitle =           {{P}roceedings of the 18th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'03)},
  acronym =             {{LICS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {208-217},
  year =                {2003},
  month =               jun,
}
[Dan03] Zhe Dang. Pushdown Timed Automata: A Binary Reachability Characterization and Safety Verification. Theoretical Computer Science 302(1-3):93-121. Elsevier, June 2003. 
@article{tcs302(1-3)-Dang,
  author =              {Dang, Zhe},
  title =               {Pushdown Timed Automata: A~Binary Reachability
                         Characterization and Safety Verification},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {302},
  number =              {1-3},
  pages =               {93-121},
  year =                {2003},
  month =               jun,
}
[DD03] Stéphane Demri and Deepak D'Souza. An Automata-Theoretic Approach to Constraint LTL. Research Report LSV-03-11, Lab. Spécification & Vérification, ENS Cachan, France, August 2003. 
@techreport{LSV-03-11-DD,
  author =              {Demri, St{\'e}phane and D'Souza, Deepak},
  title =               {An Automata-Theoretic Approach to Constraint {LTL}},
  number =              {LSV-03-11},
  year =                {2003},
  month =               aug,
  institution =         {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Research Report},
}
[DJJ+03] Piotr Dembinski, Agata Janowska, Paweł Janowski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Bożna Woźna, and Andrzej Zbrzezny. Verics: A Tool for Verifying Timed Automata and Estelle Specifications. In TACAS'03, Lecture Notes in Computer Science 2619, pages 278-283. Springer-Verlag, April 2003. 
@inproceedings{tacas2003-DJJPPSWZ,
  author =              {Dembinski, Piotr and Janowska, Agata and Janowski,
                         Pawe{\l} and Penczek, Wojciech and P{\'o}lrola,
                         Agata and Szreter, Maciej and Wo{\'z}na, Bo{\.z}na
                         and Zbrzezny, Andrzej},
  title =               {Verics: A~Tool for Verifying Timed Automata and
                         Estelle Specifications},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {278-283},
  year =                {2003},
  month =               apr,
}
[Duf03] Marie Duflot. Algorithmes distribués sur des anneaux paramétrés : preuves de convergence probabiliste et déterministe. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, September 2003. 
@phdthesis{phd-duflot,
  author =              {Duflot, Marie},
  title =               {Algorithmes distribu{\'e}s sur des anneaux
                         param{\'e}tr{\'e}s : preuves de convergence
                         probabiliste et d{\'e}terministe},
  year =                {2003},
  month =               sep,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[EN03] E. Allen Emerson and Kedar Namjoshi. On Reasoning About Rings. International Journal of Foundations of Computer Science 14(4):527-550. August 2003. 
@article{ijfcs14(4)-EN,
  author =              {Emerson, E. Allen and Namjoshi, Kedar},
  title =               {On~Reasoning About Rings},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {14},
  number =              {4},
  pages =               {527-550},
  year =                {2003},
  month =               aug,
  doi =                 {10.1142/S0129054103001881},
}
[FH03] Lance Fortnow and Steve Homer. A Short History of Computational Complexity. EATCS Bulletin 80:95-133. EATCS, June 2003. 
@article{beatcs80-FH,
  author =              {Fortnow, Lance and Homer, Steve},
  title =               {A~Short History of Computational Complexity},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {80},
  pages =               {95-133},
  year =                {2003},
  month =               jun,
}
[FMP+03] Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. Schedulability Analysis Using Two Clocks. In TACAS'03, Lecture Notes in Computer Science 2619, pages 224-239. Springer-Verlag, April 2003. 
@inproceedings{tacas2003-FMPY,
  author =              {Fersman, Elena and Mokrushin, Leonid and Pettersson,
                         Paul and Yi, Wang},
  title =               {Schedulability Analysis Using Two Clocks},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {224-239},
  year =                {2003},
  month =               apr,
}
[FR03] Tim French and Mark Reynolds. A Sound and Complete Proof System for QPTL. In AIML'02, pages 127-148. King's College Publications, 2003. 
@inproceedings{aiml2002-FR,
  author =              {French, Tim and Reynolds, Mark},
  title =               {A~Sound and Complete Proof System for~{QPTL}},
  editor =              {Balbiani, {\relax Ph}ilippe and Suzuki, Nobu-Yuki
                         and Wolter, Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 4th {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'02)},
  acronym =             {{AIML}'02},
  publisher =           {King's College Publications},
  pages =               {127-148},
  year =                {2003},
  confyear =            {2002},
  confmonth =           {9-10},
}
[Fre03] Tim French. Quantified Propositional Temporal Logic with Repeating States. In TIME-ICTL'03, pages 155-165. IEEE Comp. Soc. Press, July 2003. 
@inproceedings{time2003-Fre,
  author =              {French, Tim},
  title =               {Quantified Propositional Temporal Logic with
                         Repeating States},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning and of the 4th {I}nternational
                         {C}onference on {T}emporal {L}ogic
                         ({TIME}-{ICTL}'03)},
  acronym =             {{TIME-ICTL}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {155-165},
  year =                {2003},
  month =               jul,
  doi =                 {10.1109/TIME.2003.1214891},
}
[Fri03] Carsten Fritz. Construction Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata. In CIAA'04, Lecture Notes in Computer Science 2759, pages 35-48. Springer-Verlag, July 2003. 
@inproceedings{ciaa2003-Fri,
  author =              {Fritz, Carsten},
  title =               {Construction {B}{\"u}chi Automata from Linear
                         Temporal Logic Using Simulation Relations for
                         Alternating {B}{\"u}chi Automata},
  editor =              {Ibarra, Oscar H. and Dang, Zhe},
  booktitle =           {{R}evised {S}elected {P}apers of the 9th
                         {I}nternational {C}onference on Implementation and
                         Application of Automata ({CIAA}'04)},
  acronym =             {{CIAA}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2759},
  pages =               {35-48},
  year =                {2003},
  month =               jul,
}
[FdR+03] Massimo Franceschet, Marteen de Rijke, and Bernd-Holger Schlingloff. Hybrid Logics on Linear Structures: Expressivity and Complexity. In TIME-ICTL'03, pages 166-173. IEEE Comp. Soc. Press, July 2003. 
@inproceedings{time2003-FRS,
  author =              {Franceschet, Massimo and de Rijke, Marteen and
                         Schlingloff, Bernd-Holger},
  title =               {Hybrid Logics on Linear Structures: Expressivity and
                         Complexity},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning and of the 4th {I}nternational
                         {C}onference on {T}emporal {L}ogic
                         ({TIME}-{ICTL}'03)},
  acronym =             {{TIME-ICTL}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {166-173},
  year =                {2003},
  month =               jul,
}
[GGS03] Georg Gottlob, Gianluigi Greco, and Francesco Scarcello. Pure Nash Equilibria: Hard and Easy Games. In TARK'03, pages 215-230. ACM Press, June 2003. 
@inproceedings{tark2003-GGS,
  author =              {Gottlob, Georg and Greco, Gianluigi and Scarcello,
                         Francesco},
  title =               {Pure {N}ash Equilibria: Hard and Easy Games},
  editor =              {Halpern, Joseph Y. and Tennenholtz, Moshe},
  booktitle =           {{P}roceedings of the 9th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'03)},
  acronym =             {{TARK}'03},
  publisher =           {ACM Press},
  pages =               {215-230},
  year =                {2003},
  month =               jun,
}
[GKS+03] Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, and Moshe Y. Vardi. On Complementing Nondeterministic Büchi Automata. In CHARME'03, Lecture Notes in Computer Science 2860. Springer-Verlag, October 2003. 
@inproceedings{charme2003-GKSV,
  author =              {Gurumurthy, Sankar and Kupferman, Orna and Somenzi,
                         Fabio and Vardi, Moshe Y.},
  title =               {On Complementing Nondeterministic B{\"u}chi
                         Automata},
  editor =              {Geist, Daniel and Tronci, Enrico},
  booktitle =           {{P}roceedings of the 12th {C}orrect {H}ardware
                         {D}esign and {V}erification {M}ethods ({CHARME}'03)},
  acronym =             {{CHARME}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2860},
  year =                {2003},
  month =               oct,
}
[GMP03] Villiam Geffert, Carlo Mereghetti, and Giovanni Pighizzini. Converting Two-way Nondeterministic Unary Automata into Simpler Automata. Theoretical Computer Science 295(1-3):189-203. Elsevier, February 2003. 
@article{tcs295(1-3)-GMP,
  author =              {Geffert, Villiam and Mereghetti, Carlo and
                         Pighizzini, Giovanni},
  title =               {Converting Two-way Nondeterministic Unary Automata
                         into Simpler Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {295},
  number =              {1-3},
  pages =               {189-203},
  year =                {2003},
  month =               feb,
}
[GO03] Paul Gastin and Denis Oddoux. LTL with Past and Two-way Very-weak Alternating Automata. In MFCS'03, Lecture Notes in Computer Science 2747, pages 439-448. Springer-Verlag, August 2003. 
@inproceedings{mfcs2003-GO,
  author =              {Gastin, Paul and Oddoux, Denis},
  title =               {{LTL} with Past and Two-way Very-weak Alternating
                         Automata},
  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 =               {439-448},
  year =                {2003},
  month =               aug,
}
[Hal03] Joseph Y. Halpern. A computer scientist looks at game theory. Games and Economic Behavior 45(1):114-131. October 2003. 
@article{geb45(1)-Hal,
  author =              {Halpern, Joseph Y.},
  title =               {A computer scientist looks at game theory},
  journal =             {Games and Economic Behavior},
  volume =              {45},
  number =              {1},
  pages =               {114-131},
  year =                {2003},
  month =               oct,
  doi =                 {10.1016/S0899-8256(02)00529-8},
}
[HBL+03] Martijn Hendriks, Gerd Behrmann, Kim Guldstrand Larsen, Peter Niebert, and Frits Vaandrager. Adding Symmetry Reduction to Uppaal. In FORMATS'03, Lecture Notes in Computer Science 2791. Springer-Verlag, September 2003. 
@inproceedings{formats2003-HBLNV,
  author =              {Hendriks, Martijn and Behrmann, Gerd and Larsen, Kim
                         Guldstrand and Niebert, Peter and Vaandrager, Frits},
  title =               {Adding Symmetry Reduction to {U}ppaal},
  editor =              {Larsen, Kim Guldstrand and Niebert, Peter},
  booktitle =           {{R}evised {P}apers of the 1st {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'03)},
  acronym =             {{FORMATS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2791},
  year =                {2003},
  month =               sep,
}
[Hes03] William Hesse. Dynamic Computational Complexity. PhD thesis, Department of Computer Science, University of Massachusetts at Amherst, USA, September 2003. 
@phdthesis{phd-hesse,
  author =              {Hesse, William},
  title =               {Dynamic Computational Complexity},
  year =                {2003},
  month =               sep,
  school =              {Department of Computer Science, University of
                         Massachusetts at Amherst, USA},
}
[HvdH+03] Paul Harrenstein, Wiebe van der Hoek, John-Jules Meyer, and Cees Witteveen. A Modal Characterization of Nash Equilibrium. Fundamenta Informaticae 57(2-4):281-321. IOS Press, 2003. 
@article{fundi57(2-4)-HHMW,
  author =              {Harrenstein, Paul and van der Hoek, Wiebe and Meyer,
                         John-Jules and Witteveen, Cees},
  title =               {A Modal Characterization of {N}ash Equilibrium},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {57},
  number =              {2-4},
  pages =               {281-321},
  year =                {2003},
}
[HJM03] Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample-Guided Control. In ICALP'03, Lecture Notes in Computer Science 2719, pages 886-902. Springer-Verlag, June 2003. 
@inproceedings{icalp2003-HJM,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak},
  title =               {Counterexample-Guided Control},
  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 =               {886-902},
  year =                {2003},
  month =               jun,
}
[HJM+03] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Software verification with BLAST. In SPIN'03, Lecture Notes in Computer Science 2648, pages 235-239. Springer-Verlag, April 2003. 
@inproceedings{spin2003-HJMS,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak and Sutre, Gr{\'e}goire},
  title =               {Software verification with {BLAST}},
  editor =              {Ball, Thomas and Rajamani, Sriram},
  booktitle =           {{P}roceedings of the 10th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'03)},
  acronym =             {{SPIN}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2648},
  pages =               {235-239},
  year =                {2003},
  month =               apr,
}
[HKM03] Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar. On the Universal and Existential Fragments of the μ-Calculus. In TACAS'03, Lecture Notes in Computer Science 2619, pages 49-64. Springer-Verlag, April 2003. 
@inproceedings{tacas2003-HKM,
  author =              {Henzinger, Thomas A. and Kupferman, Orna and
                         Majumdar, Rupak},
  title =               {On the Universal and Existential Fragments of the
                         {\(\mu\)}-Calculus},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {49-64},
  year =                {2003},
  month =               apr,
}
[HM03] Markus Holzer and Pierre McKenzie. Alternating and Empty Alternating Auxiliary Stack Automata. Theoretical Computer Science 299(1-3):307-326. Elsevier, April 2003. 
@article{tcs299(1-3)-HM,
  author =              {Holzer, Markus and McKenzie, Pierre},
  title =               {Alternating and Empty Alternating Auxiliary Stack
                         Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {299},
  number =              {1-3},
  pages =               {307-326},
  year =                {2003},
  month =               apr,
}
[HR03] Yoram Hirshfeld and Alexander Rabinovich. Future Temporal Logic Needs Infinitely Many Modalities. Information and Computation 187(2):196-208. Academic Press, December 2003. 
@article{icomp187(2)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Future Temporal Logic Needs Infinitely Many
                         Modalities},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {187},
  number =              {2},
  pages =               {196-208},
  year =                {2003},
  month =               dec,
}
[HRS03] Aidan Harding, Mark D. Ryan, and Pierre-Yves Schobbens. Towards Symbolic Strategy Synthesis for ⟨⟨A⟩⟩-LTL. In TIME-ICTL'03, pages 137-146. IEEE Comp. Soc. Press, July 2003. 
@inproceedings{time2003-HRS,
  author =              {Harding, Aidan and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {Towards Symbolic Strategy Synthesis for
  {\(\langle\)\,\llap{\(\langle\)}A\(\rangle\)\,\llap{\(\rangle\)}}-{LTL}},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning and of the 4th {I}nternational
                         {C}onference on {T}emporal {L}ogic
                         ({TIME}-{ICTL}'03)},
  acronym =             {{TIME-ICTL}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {137-146},
  year =                {2003},
  month =               jul,
}
[HSB03] John Hershberger, Subhash Suri, and Amir Bhosle. On the Difficulty of Some Shortest Path Problems. In STACS'03, Lecture Notes in Computer Science 2607, pages 343-354. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-HSB,
  author =              {Hershberger, John and Suri, Subhash and Bhosle,
                         Amir},
  title =               {On the Difficulty of Some Shortest Path Problems},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {343-354},
  year =                {2003},
  month =               feb,
}
[ISY03] Lucian Ilie, Baozhen Shan, and Sheng Yu. Expression Matching and Searching. In STACS'03, Lecture Notes in Computer Science 2607, pages 179-190. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-ISY,
  author =              {Ilie, Lucian and Shan, Baozhen and Yu, Sheng},
  title =               {Expression Matching and Searching},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {179-190},
  year =                {2003},
  month =               feb,
}
[Jer03] Thierry Jéron. Project-Team VerTeCs. Annual Reviews Inc., IRISA, Rennes, France, 2003. 
@techreport{AR-VerTeCs-2003,
  author =              {J{\'e}ron, Thierry},
  title =               {Project-Team {VerTeCs}},
  year =                {2003},
  institution =         {IRISA, Rennes, France},
  type =                {Annual Reviews Inc.},
}
[JL03] Jan Johannsen and Martin Lange. CTL+ is Complete for Double Exponential Time. In ICALP'03, Lecture Notes in Computer Science 2719, pages 767-775. Springer-Verlag, June 2003. 
@inproceedings{icalp2003-JL,
  author =              {Johannsen, Jan and Lange, Martin},
  title =               {{CTL{\(^+\)}} is Complete for Double Exponential
                         Time},
  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 =               {767-775},
  year =                {2003},
  month =               jun,
}
[JMR+03] Thierry Jéron, Hervé Marchand, Vlad Rusu, and Valéry Tschaen. Ensuring the Conformance of Reactive Discrete-Event Systems using Supervisory Control. In CDC'03, pages 2692- 2697. IEEE Comp. Soc. Press, December 2003. 
@inproceedings{cdc2003-JMRT,
  author =              {J{\'e}ron, Thierry and Marchand, Herv{\'e} and Rusu,
                         Vlad and Tschaen, Val{\'e}ry},
  title =               {Ensuring the Conformance of Reactive Discrete-Event
                         Systems using Supervisory Control},
  booktitle =           {{P}roceedings of the 42nd {IEEE} {C}onference on
                         {D}ecision and {C}ontrol ({CDC}'03)},
  acronym =             {{CDC}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {2692- 2697},
  year =                {2003},
  month =               dec,
}
[Joh03] Jan Johannsen. Satisfiability Problems Complete for Deterministic Logarithmic Space. In STACS'04, Lecture Notes in Computer Science 2996, pages 317-325. Springer-Verlag, March 2003. 
@inproceedings{stacs2004-Joh,
  author =              {Johannsen, Jan},
  title =               {Satisfiability Problems Complete for Deterministic
                         Logarithmic Space},
  editor =              {Diekert, Volker and Habib, Michel},
  booktitle =           {{P}roceedings of the 21st {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'04)},
  acronym =             {{STACS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2996},
  pages =               {317-325},
  year =                {2003},
  month =               mar,
}
[KLV03] George Karakostas, Richard J. Lipton, and Anastasios Viglas. On the Complexity of Intersecting Finite State Automata and NL versus NP. Theoretical Computer Science 302(1-3):257-274. Elsevier, June 2003. 
@article{tcs302(1-3)-KLV,
  author =              {Karakostas, George and Lipton, Richard J. and
                         Viglas, Anastasios},
  title =               {On the Complexity of Intersecting Finite State
                         Automata and {NL} versus~{NP}},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {302},
  number =              {1-3},
  pages =               {257-274},
  year =                {2003},
  month =               jun,
}
[KPA03] Kåre J. Kristoffersen, Christian Pedersen, and Henrik Reif Andersen. Runtime Verification of Timed LTL Using Disjunctive Normalized Equation Systems. In RV'03, Electronic Notes in Theoretical Computer Science 89(2). Elsevier, 2003. 
@inproceedings{rv2003-KPA,
  author =              {Kristoffersen, K{\aa}re J. and Pedersen, Christian
                         and Andersen, Henrik Reif},
  title =               {Runtime Verification of Timed {LTL} Using
                         Disjunctive Normalized Equation Systems},
  editor =              {Cook, Byron and Stoller, Scott and Viser, Willem},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'03)},
  acronym =             {{RV}'03},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {89},
  number =              {2},
  year =                {2003},
  confyear =            {2003},
  confmonth =           {7},
}
[KS03] Dimitris J. Kavvadias and Elias C. Stavropoulos. Monotone Boolean Dualization is in co-NP[log2(n)]. Information Processing Letters 85(1):1-8. Elsevier, January 2003. 
@article{ipl85(1)-KS,
  author =              {Kavvadias, Dimitris J. and Stavropoulos, Elias C.},
  title =               {Monotone Boolean Dualization is in
                         co-{NP}{\([\log^2(n)]\)}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {85},
  number =              {1},
  pages =               {1-8},
  year =                {2003},
  month =               jan,
}
[KV03] Orna Kupferman and Moshe Y. Vardi. Safraless Decision Procedures. In FOCS'03. IEEE Comp. Soc. Press, October 2003. 
@inproceedings{focs2003-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Safraless Decision Procedures},
  booktitle =           {{P}roceedings of the 44th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'03)},
  acronym =             {{FOCS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2003},
  month =               oct,
}
[KV03] Orna Kupferman and Moshe Y. Vardi. Π2∩Σ2≡ AFMC. In ICALP'03, Lecture Notes in Computer Science 2719, pages 697-713. Springer-Verlag, June 2003. 
@inproceedings{icalp2003-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {{{\(\Pi_2\cap\Sigma_2\equiv \textup{AFMC}\)}}},
  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 =               {697-713},
  year =                {2003},
  month =               jun,
}
[KW03] Detlef Kähler and Thomas Wilke. Program complexity of dynamic LTL model checking. In CSL'03, Lecture Notes in Computer Science 2803, pages 271-284. Springer-Verlag, August 2003. 
@inproceedings{csl2003-KW,
  author =              {K{\"a}hler, Detlef and Wilke, Thomas},
  title =               {Program complexity of dynamic {LTL} model checking},
  editor =              {Baaz, Matthias and Makowsky, Johann A.},
  booktitle =           {{P}roceedings of the 17th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'03)},
  acronym =             {{CSL}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2803},
  pages =               {271-284},
  year =                {2003},
  month =               aug,
  doi =                 {10.1007/978-3-540-45220-1_23},
}
[KWZ+03] Agi Kurucz, Frank Wolter, Michael Zakharyaschev, and Dov M. Gabbay. Many-Dimensional Modal Logics: Theory and Applications. Elsevier, 2003. 
@book{mdml2003-KWZG,
  author =              {Kurucz, Agi and Wolter, Frank and Zakharyaschev,
                         Michael and Gabbay, Dov M.},
  title =               {Many-Dimensional Modal Logics: Theory and
                         Applications},
  publisher =           {Elsevier},
  year =                {2003},
}
[LD03] Cullen Linn and Saumya Debray. Obfuscation of Executable Code to Improve Resistance to Static Disassembly. In CCS'03, pages 290-299. ACM Press, October 2003. 
@inproceedings{ccs2003-LD,
  author =              {Linn, Cullen and Debray, Saumya},
  title =               {Obfuscation of Executable Code to Improve Resistance
                         to Static Disassembly},
  editor =              {Jajodia, Sushil and Atluri, Vijayalakshmi and
                         Jaeger, Trent},
  booktitle =           {{P}roceedings of the 10th {C}onference on {C}omputer
                         and {C}ommunications {S}ecurity ({CCS}'03)},
  acronym =             {{CCS}'03},
  publisher =           {ACM Press},
  pages =               {290-299},
  year =                {2003},
  month =               oct,
}
[Ler03] Jérôme Leroux. Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, December 2003. 
@phdthesis{phd-leroux,
  author =              {Leroux, J{\'e}r{\^o}me},
  title =               {Algorithmique de la v{\'e}rification des
                         syst{\`e}mes {\`a} compteurs. Approximation et
                         acc{\'e}l{\'e}ration. Impl{\'e}mentation de l'outil
                         {FAST}},
  year =                {2003},
  month =               dec,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[LR03] Christof Löding and Philipp Rohde. Solving the Sabotage Game is PSPACE-hard. In MFCS'03, Lecture Notes in Computer Science 2747, pages 531-540. Springer-Verlag, August 2003. 
@inproceedings{mfcs2003-LR,
  author =              {L{\"o}ding, Christof and Rohde, Philipp},
  title =               {Solving the Sabotage Game is {PSPACE}-hard},
  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 =               {531-540},
  year =                {2003},
  month =               aug,
}
[LST03] François Laroussinie, Philippe Schnoebelen, and Mathieu Turuani. On the expressivity and complexity of quantitative branching-time temporal logics. Theoretical Computer Science 297(1-3):297-315. Elsevier, March 2003. 
@article{tcs297(1-3)-LST,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe and Turuani, Mathieu},
  title =               {On the expressivity and complexity of quantitative
                         branching-time temporal logics},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {297},
  number =              {1-3},
  pages =               {297-315},
  year =                {2003},
  month =               mar,
}
[Lug03] Denis Lugiez. Counting and Equality Constraints for Multitree Automata. In FoSSaCS'03, Lecture Notes in Computer Science 2620, pages 328-342. Springer-Verlag, April 2003. 
@inproceedings{fossacs2003-Lug,
  author =              {Lugiez, Denis},
  title =               {Counting and Equality Constraints for Multitree
                         Automata},
  editor =              {Gordon, Andrew D.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'03)},
  acronym =             {{FoSSaCS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2620},
  pages =               {328-342},
  year =                {2003},
  month =               apr,
}
[MBK03] Malik Magdon-Ismail, Costas Busch, and Mukkai S. Krishnamoorthy. Cake-Cutting is not a Piece of Cake. In STACS'03, Lecture Notes in Computer Science 2607, pages 596-607. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-MBK,
  author =              {Magdon{-}Ismail, Malik and Busch, Costas and
                         Krishnamoorthy, Mukkai S.},
  title =               {Cake-Cutting is not a Piece of Cake},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {596-607},
  year =                {2003},
  month =               feb,
}
[MR03] Faron Moller and Alexander Rabinovich. Counting on CTL*: on the expressive power of monadic path logic. Information and Computation 184(1):147-159. Academic Press, July 2003. 
@article{icomp184(1)-MR,
  author =              {Moller, Faron and Rabinovich, Alexander},
  title =               {Counting on {CTL}{\textsuperscript{*}}: on~the
                         expressive power of monadic path logic},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {184},
  number =              {1},
  pages =               {147-159},
  year =                {2003},
  month =               jul,
}
[MW03] Pierre McKenzie and Klaus W. Wagner. The Complexity of Membership Problems for Circuits over Sets of Natural Numbers. In STACS'03, Lecture Notes in Computer Science 2607, pages 571-582. Springer-Verlag, February 2003. 
@inproceedings{stacs2003-MW,
  author =              {McKenzie, Pierre and Wagner, Klaus W.},
  title =               {The Complexity of Membership Problems for Circuits
                         over Sets of Natural Numbers},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {571-582},
  year =                {2003},
  month =               feb,
}
[NS03] Brian Nielsen and Arne Skou. Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer 5(1):59-77. Springer-Verlag, November 2003. 
@article{sttt5(1)-NS,
  author =              {Nielsen, Brian and Skou, Arne},
  title =               {Automated test generation from timed automata},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {5},
  number =              {1},
  pages =               {59-77},
  year =                {2003},
  month =               nov,
  doi =                 {10.1007/s10009-002-0094-1},
}
[Obd03] Jan Obdržálek. Fast Mu-Calculus Model Checking When Tree-Width is Bounded. In CAV'03, Lecture Notes in Computer Science 2725, pages 80-92. Springer-Verlag, July 2003. 
@inproceedings{cav2003-obd,
  author =              {Obdr{\v z}{\'a}lek, Jan},
  title =               {Fast Mu-Calculus Model Checking When Tree-Width is
                         Bounded},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {80-92},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_7},
}
[Odd03] Denis Oddoux. Utilisation des automates alternants pour un model-checking efficace des logiques temporelles linéaires. Thèse de doctorat, Lab. Informatique Algorithmique: Fondements et Applications, Université Paris 7, France, December 2003. 
@phdthesis{phd-oddoux,
  author =              {Oddoux, Denis},
  title =               {Utilisation des automates alternants pour un
                         model-checking efficace des logiques temporelles
                         lin{\'e}aires},
  year =                {2003},
  month =               dec,
  school =              {Lab.~Informatique Algorithmique: Fondements et
                         Applications, Universit{\'e} Paris~7, France},
  type =                {Th\`ese de doctorat},
}
[OW03] Joël Ouaknine and James Worrell. Revisiting Digitization, Robustness, and Decidability for Timed Automata. In LICS'03, pages 198-207. IEEE Comp. Soc. Press, June 2003. 
@inproceedings{lics2003-OW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Revisiting Digitization, Robustness, and
                         Decidability for Timed Automata},
  booktitle =           {{P}roceedings of the 18th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'03)},
  acronym =             {{LICS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {198-207},
  year =                {2003},
  month =               jun,
}
[PSS+03] Matteo Pradella, Pierluigi San Pietro, Paola Spoletini, and Angelo Morzenti. Practical Model Checking of LTL with Past. In ATVA'03. December 2003. 
@inproceedings{atva2003-PSSM,
  author =              {Pradella, Matteo and San{~}Pietro, Pierluigi and
                         Spoletini, Paola and Morzenti, Angelo},
  title =               {Practical Model Checking of {LTL} with Past},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'03)},
  acronym =             {{ATVA}'03},
  year =                {2003},
  month =               dec,
}
[PV03] Nir Piterman and Moshe Y. Vardi. From Bidirectionality to Alternation. Theoretical Computer Science 295(1-3):295-321. Elsevier, February 2003. 
@article{tcs295(1-3)-PV,
  author =              {Piterman, Nir and Vardi, Moshe Y.},
  title =               {From Bidirectionality to Alternation},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {295},
  number =              {1-3},
  pages =               {295-321},
  year =                {2003},
  month =               feb,
}
[QYZ+03] Lili Qiu, Richard Yang, Yin Zhang, and Scott Shenker. On selfish routing in internet-like environments. In SIGCOMM'03, pages 151-162. ACM Press, August 2003. 
@inproceedings{sigcomm2003-QYZS,
  author =              {Qiu, Lili and Yang, Richard and Zhang, Yin and
                         Shenker, Scott},
  title =               {On selfish routing in internet-like environments},
  editor =              {Feldmann, Anja and Zitterbart, Martina and
                         Crowcroft, Jon and Wetherall, David},
  booktitle =           {{P}roceedings of {ACM} {SIGCOMM}~2003 {C}onference
                         on {A}pplications, {T}echnologies, {A}rchitectures,
                         and {P}rotocols for {C}omputer {C}ommunication
                         ({SIGCOMM}'03)},
  acronym =             {{SIGCOMM}'03},
  publisher =           {ACM Press},
  pages =               {151-162},
  year =                {2003},
  month =               aug,
  doi =                 {10.1145/863955.863974},
}
[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,
}
[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},
}
[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,
}
[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},
}
[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,
}
[Saw03] Zdeněk Sawa. Equivalence Checking of Non-flat Systems is EXPTIME-hard. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 237-250. Springer-Verlag, August 2003. 
@inproceedings{concur2003-Saw,
  author =              {Sawa, Zden{\v{e}}k},
  title =               {Equivalence Checking of Non-flat Systems is
                         EXPTIME-hard},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {237-250},
  year =                {2003},
  month =               aug,
}
[SB03] Sanjit A. Seshia and Randal E. Bryant. Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. In CAV'03, Lecture Notes in Computer Science 2725, pages 154-166. Springer-Verlag, July 2003. 
@inproceedings{cav2003-SB,
  author =              {Seshia,Sanjit A. and Bryant, Randal E.},
  title =               {Unbounded, Fully Symbolic Model Checking of Timed
                         Automata using Boolean Methods},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {154-166},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_16},
}
[Sch03] Philippe Schnoebelen. The Complexity of Temporal Logic Model Checking. In AIML'02, pages 481-517. King's College Publications, 2003. 
@inproceedings{aiml2002-Sch,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {The Complexity of Temporal Logic Model Checking},
  editor =              {Balbiani, {\relax Ph}ilippe and Suzuki, Nobu-Yuki
                         and Wolter, Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 4th {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'02)},
  acronym =             {{AIML}'02},
  publisher =           {King's College Publications},
  pages =               {481-517},
  year =                {2003},
  confyear =            {2002},
  confmonth =           {9-10},
}
[Sch03] Philippe Schnoebelen. Oracle Circuits for Branching-Time Model Checking. In ICALP'03, Lecture Notes in Computer Science 2719, pages 790-801. Springer-Verlag, June 2003. 
@inproceedings{icalp2003-Sch,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {Oracle Circuits for Branching-Time Model Checking},
  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 =               {790-801},
  year =                {2003},
  month =               jun,
}
[SKS03] Shoham Shamir, Orna Kupferman, and Eli Shamir. Branching-Depth Hierarchies. In EXPRESS'00, Electronic Notes in Theoretical Computer Science 39(1). Elsevier, February 2003. 
@inproceedings{express2000-SKS,
  author =              {Shamir, Shoham and Kupferman, Orna and Shamir, Eli},
  title =               {Branching-Depth Hierarchies},
  editor =              {Aceto, Luca and Victor, Bjorn},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'00)},
  acronym =             {{EXPRESS}'00},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {39},
  number =              {1},
  year =                {2003},
  month =               feb,
  confyear =            {2000},
  confmonth =           {8},
}
[ST03] Roberto Sebastiani and Stefano Tonetta. "More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. In CHARME'03, Lecture Notes in Computer Science 2860. Springer-Verlag, October 2003. 
@inproceedings{charme2003-ST,
  author =              {Sebastiani, Roberto and Tonetta, Stefano},
  title =               {{"}More Deterministic{"} vs. {"}Smaller{"} B{\"u}chi
                         Automata for Efficient {LTL} Model Checking},
  editor =              {Geist, Daniel and Tronci, Enrico},
  booktitle =           {{P}roceedings of the 12th {C}orrect {H}ardware
                         {D}esign and {V}erification {M}ethods ({CHARME}'03)},
  acronym =             {{CHARME}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2860},
  year =                {2003},
  month =               oct,
}
[Tau03] Heikko Tauriainen. On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata. Licentiate thesis, Helsinki University of Technology, Finland, 2003. 
@mastersthesis{licentiate-tauriainen,
  author =              {Tauriainen, Heikko},
  title =               {On Translating Linear Temporal Logic into
                         Alternating and Nondeterministic Automata},
  year =                {2003},
  school =              {Helsinki University of Technology, Finland},
  type =                {Licentiate thesis},
}
[Tsa03] Boaz Tsaban. Bernoulli Numbers and the Probability of a Birthday Surprise. Discrete Applied Mathematics 127(1):657-663. Elsevier, April 2003. 
@article{dam127(1)-Tsa,
  author =              {Tsaban, Boaz},
  title =               {{B}ernoulli Numbers and the Probability of a
                         Birthday Surprise},
  publisher =           {Elsevier},
  journal =             {Discrete Applied Mathematics},
  volume =              {127},
  number =              {1},
  pages =               {657-663},
  year =                {2003},
  month =               apr,
}
[ZYN03] Sarah Zennou, Manuel Yguel, and Peter Niebert. ELSE: A New Symbolic State Generator for Timed Automata. In FORMATS'03, Lecture Notes in Computer Science 2791, pages 273-280. Springer-Verlag, September 2003. 
@inproceedings{formats2003-ZYN,
  author =              {Zennou, Sarah and Yguel, Manuel and Niebert, Peter},
  title =               {{ELSE}: A~New Symbolic State Generator for Timed
                         Automata},
  editor =              {Larsen, Kim Guldstrand and Niebert, Peter},
  booktitle =           {{R}evised {P}apers of the 1st {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'03)},
  acronym =             {{FORMATS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2791},
  pages =               {273-280},
  year =                {2003},
  month =               sep,
}
List of authors