2000
[Mar00] Nicolas Markey. Complexité de la logique temporelle avec passé. Rapport de DEA, Lab. Spécification & Vérification, ENS Cachan, France, June 2000. 
@mastersthesis{dea2000-Mar,
  author =              {Markey, Nicolas},
  title =               {Complexit{\'e} de la logique temporelle avec
                         pass{\'e}},
  year =                {2000},
  month =               jun,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Rapport de~{DEA}},
}
[AAB00] Aurore Annichini, Eugene Asarin, and Ahmed Bouajjani. Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In CAV'00, Lecture Notes in Computer Science 1855, pages 419-434. Springer-Verlag, July 2000. 
@inproceedings{cav2000-AAB,
  author =              {Annichini, Aurore and Asarin, Eugene and Bouajjani,
                         Ahmed},
  title =               {Symbolic Techniques for Parametric Reasoning about
                         Counter and Clock Systems},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {419-434},
  year =                {2000},
  month =               jul,
}
[ABE00] Parosh Aziz Abdulla, Per Bjesse, and Niklas Eén. Symbolic Reachability Analysis based on SAT Solvers. In TACAS'00, Lecture Notes in Computer Science 1785, pages 411-425. Springer-Verlag, March 2000. 
@inproceedings{tacas2000-ABE,
  author =              {Abdulla, Parosh Aziz and Bjesse, Per and E{\'e}n,
                         Niklas},
  title =               {Symbolic Reachability Analysis based on {SAT}
                         Solvers},
  editor =              {Graf, Susanne and Schwartzbach, Michael I.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'00)},
  acronym =             {{TACAS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1785},
  pages =               {411-425},
  year =                {2000},
  month =               mar,
}
[ABM00] Carlos Areces, Patrick Blackburn, and Maarten Marx. The Computational Complexity of Hybrid Temporal Logics. Logic Journal of the IGPL 8(5):653-679. Oxford University Press, September 2000. 
@article{jigpl8(5)-ABM,
  author =              {Areces, Carlos and Blackburn, Patrick and Marx,
                         Maarten},
  title =               {The Computational Complexity of Hybrid Temporal
                         Logics},
  publisher =           {Oxford University Press},
  journal =             {Logic Journal of the IGPL},
  volume =              {8},
  number =              {5},
  pages =               {653-679},
  year =                {2000},
  month =               sep,
}
[AG00] Carme Àlvarez and Raymond Greenlaw. A Compendium of Problems Complete for Symmetric Logarithmic Space. Computational Complexity 9(2):123-145. Birkhäuser, 2000. 
@article{cc9(2)-AG,
  author =              {{\`A}lvarez, Carme and Greenlaw, Raymond},
  title =               {A Compendium of Problems Complete for Symmetric
                         Logarithmic Space},
  publisher =           {Birkh{\"a}user},
  journal =             {Computational Complexity},
  volume =              {9},
  number =              {2},
  pages =               {123-145},
  year =                {2000},
}
[AGS00] Karine Altisen, Gregor Gößler, and Joseph Sifakis. A Methodology for the Construction of Scheduled Systems. In FTRTFT'00, Lecture Notes in Computer Science 1926, pages 106-120. Springer-Verlag, September 2000. 
@inproceedings{ftrtft2000-AGS,
  author =              {Altisen, Karine and G{\"o}{\ss}ler, Gregor and
                         Sifakis, Joseph},
  title =               {A Methodology for the Construction of Scheduled
                         Systems},
  editor =              {Joseph, Mathai},
  booktitle =           {{P}roceedings of the 6th {F}ormal {T}echniques in
                         {R}eal-Time and {F}ault-Tolerant {S}ystems
                         ({FTRTFT}'00)},
  acronym =             {{FTRTFT}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1926},
  pages =               {106-120},
  year =                {2000},
  month =               sep,
}
[dAH00] Luca de Alfaro and Thomas A. Henzinger. Concurrent Omera-Regular Games. In LICS'00, pages 141-154. IEEE Comp. Soc. Press, June 2000. 
@inproceedings{lics2000-AH,
  author =              {de Alfaro, Luca and Henzinger, Thomas A.},
  title =               {Concurrent Omera-Regular Games},
  booktitle =           {{P}roceedings of the 15th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'00)},
  acronym =             {{LICS}'00},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {141-154},
  year =                {2000},
  month =               jun,
  doi =                 {10.1109/LICS.2000.855763},
}
[dAH+00] Luca de Alfaro, Thomas A. Henzinger, and Freddy Y. C. Mang. The Control of Synchronous Systems. In CONCUR'00, Lecture Notes in Computer Science 1877, pages 458-473. Springer-Verlag, August 2000. 
@inproceedings{concur2000-AHM,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and Mang,
                         Freddy Y. C.},
  title =               {The Control of Synchronous Systems},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1877},
  pages =               {458-473},
  year =                {2000},
  month =               aug,
}
[AHR00] Myla Archer, Constance L. Heitmeyer, and Elvinia Riccobene. Using TAME to prove invariants of automata models: Two case studies. In FMSP'00, pages 25-36. ACM Press, August 2000. 
@inproceedings{fmsp2000-AHR,
  author =              {Archer, Myla and Heitmeyer, Constance L. and
                         Riccobene, Elvinia},
  title =               {Using {TAME} to prove invariants of automata models:
                         Two~case studies},
  editor =              {Heimdahl, Mats Per Erik},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {F}ormal
                         {M}ethods in {S}oftware {P}ractice ({FMSP}'00)},
  acronym =             {{FMSP}'00},
  publisher =           {ACM Press},
  pages =               {25-36},
  year =                {2000},
  month =               aug,
  doi =                 {10.1145/349360.351127},
}
[AIP+00] Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. RAIRO – Theoretical Informatics and Applications 34(6):565-584. EDP Sciences, 2000. 
@article{rairo-tia34(6)-AIPP,
  author =              {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna and
                         Pedersen, Mikkel Lykke and Poulsen, Jan},
  title =               {Characteristic Formulae for Timed Automata},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Theoretical Informatics and Applications},
  volume =              {34},
  number =              {6},
  pages =               {565-584},
  year =                {2000},
  doi =                 {10.1051/ita:2000131},
}
[ASS+00] Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. Model-checking continous-time Markov chains. ACM Transactions on Computational Logic 1(1):162-170. ACM Press, July 2000. 
@article{tocl1(1)-ASSB,
  author =              {Aziz, Adnan and Sanwal, Kumud and Singhal, Vigyan
                         and Brayton, Robert K.},
  title =               {Model-checking continous-time {M}arkov chains},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {1},
  number =              {1},
  pages =               {162-170},
  year =                {2000},
  month =               jul,
  doi =                 {10.1145/343369.343402},
}
[BD00] Béatrice Bérard and Catherine Dufourd. Timed Automata and Additive Clock Constraints. Information Processing Letters 75(1-2):1-7. Elsevier, July 2000. 
@article{ipl75(1-2)-BD,
  author =              {B{\'e}rard, B{\'e}atrice and Dufourd, Catherine},
  title =               {Timed Automata and Additive Clock Constraints},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {75},
  number =              {1-2},
  pages =               {1-7},
  year =                {2000},
  month =               jul,
}
[Ber00] Gérard Berry. The foundations of Esterel. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte (eds.), Proof, Language, and Interaction – Essays in Honour of Robin Milner. MIT Press, 2000. 
@incollection{PLI2000-Ber,
  author =              {Berry, G{\'e}rard},
  title =               {The foundations of {E}sterel},
  editor =              {Plotkin, Gordon D. and Stirling, Colin and Tofte,
                         Mads},
  booktitle =           {Proof, Language, and Interaction~-- Essays in Honour
                         of {R}obin {M}ilner},
  publisher =           {MIT Press},
  pages =               {425-454},
  year =                {2000},
}
[BHK00] Steven Bradley, William Henderson, and David Kendall. Using Timed Automata for Response Time Analysis and Distributed Real-Time Systems. In WRTP'99, pages 143-148. Pergamon Press, January 2000. 
@inproceedings{wrtp1999-BHK,
  author =              {Bradley, Steven and Henderson, William and Kendall,
                         David},
  title =               {Using Timed Automata for Response Time Analysis and
                         Distributed Real-Time Systems},
  editor =              {Frigeri, Alceu Heinke and Halang, Wolfgang A. and
                         Son, Sang H.},
  booktitle =           {{P}roceedings of the 24th {IFAC}/{IFIP} {W}orkshop
                         on {R}eal-{T}ime {P}rogramming ({WRTP}'99)},
  acronym =             {{WRTP}'99},
  publisher =           {Pergamon Press},
  pages =               {143-148},
  year =                {2000},
  month =               jan,
  confyear =            {1999},
  confmonth =           {5},
}
[Bla00] Patrick Blackburn. Representations, Reasoning and Relational Structures: a Hybrid Logic Manifesto. Logic Journal of the IGPL 8(3):339-365. Oxford University Press, May 2000. 
@article{jigpl8(3)-Bla,
  author =              {Blackburn, Patrick},
  title =               {Representations, Reasoning and Relational
                         Structures: a Hybrid Logic Manifesto},
  publisher =           {Oxford University Press},
  journal =             {Logic Journal of the IGPL},
  volume =              {8},
  number =              {3},
  pages =               {339-365},
  year =                {2000},
  month =               may,
}
[BM00] Ed Brinksma and Angelika Mader. Verification and Optimization of a PLC Control Schedule. In SPIN'00, Lecture Notes in Computer Science 1885, pages 73-92. Springer-Verlag, August 2000. 
@inproceedings{spin2000-BM,
  author =              {Brinksma, Ed and Mader, Angelika},
  title =               {Verification and Optimization of a {PLC} Control
                         Schedule},
  editor =              {Havelund, Klaus and Penix, John and Viser, Willem},
  booktitle =           {{P}roceedings of the 7th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'00)},
  acronym =             {{SPIN}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1885},
  pages =               {73-92},
  year =                {2000},
  month =               aug,
}
[BMM+00] Jean-Camille Birget, Stuart W. Margolis, John C. Meakin, and Pascal Weil. PSPACE-Completeness of Certain Algorithmic Problems on the Subgroups of Free Groups. Theoretical Computer Science 242(1-2):247-281. Elsevier, July 2000. 
@article{tcs242(1-2)-BMMW,
  author =              {Birget, Jean-Camille and Margolis, Stuart W. and
                         Meakin, John C. and Weil, Pascal},
  title =               {{PSPACE}-Completeness of Certain Algorithmic
                         Problems on the Subgroups of Free Groups},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {242},
  number =              {1-2},
  pages =               {247-281},
  year =                {2000},
  month =               jul,
}
[CC00] Hubert Comon and Véronique Cortier. Flatness is not Weakness. In CSL'00, Lecture Notes in Computer Science 1862, pages 262-276. Springer-Verlag, August 2000. 
@inproceedings{csl2000-CC,
  author =              {Comon, Hubert and Cortier, V{\'e}ronique},
  title =               {Flatness is not Weakness},
  editor =              {Clote, Peter and Schwichtenberg, Helmut},
  booktitle =           {{P}roceedings of the 14th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'00)},
  acronym =             {{CSL}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1862},
  pages =               {262-276},
  year =                {2000},
  month =               aug,
}
[CCG+00] Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A New Symbolic Model Checker. International Journal on Software Tools for Technology Transfer 2(4):410-425. Springer-Verlag, March 2000. 
@article{sttt2(4)-CCGR,
  author =              {Cimatti, Alessandro and Clarke, Edmund M. and
                         Giunchiglia, Fausto and Roveri, Marco},
  title =               {{NuSMV}: A New Symbolic Model Checker},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {2},
  number =              {4},
  pages =               {410-425},
  year =                {2000},
  month =               mar,
}
[CGJ+00] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-Guided Abstraction Refinement. In CAV'00, Lecture Notes in Computer Science 1855, pages 154-169. Springer-Verlag, July 2000. 
@inproceedings{cav2000-CGJLV,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Jha, Somesh
                         and Lu, Yuan and Veith, Helmut},
  title =               {Counterexample-Guided Abstraction Refinement},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {154-169},
  year =                {2000},
  month =               jul,
  doi =                 {10.1007/10722167_15},
}
[CGP00] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. MIT Press, 2000. 
@book{MC2000-CGP,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Peled,
                         Doron A.},
  title =               {Model checking},
  publisher =           {MIT Press},
  year =                {2000},
}
[Cha00] William Chan. Temporal-Logic Queries. In CAV'00, Lecture Notes in Computer Science 1855, pages 450-463. Springer-Verlag, July 2000. 
@inproceedings{cav2000-Cha,
  author =              {Chan, William},
  title =               {Temporal-Logic Queries},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {450-463},
  year =                {2000},
  month =               jul,
}
[CL00] Franck Cassez and Kim Guldstrand Larsen. The Impressive Power of Stopwatches. In CONCUR'00, Lecture Notes in Computer Science 1877, pages 138-152. Springer-Verlag, August 2000. 
@inproceedings{concur2000-CL,
  author =              {Cassez, Franck and Larsen, Kim Guldstrand},
  title =               {The Impressive Power of Stopwatches},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1877},
  pages =               {138-152},
  year =                {2000},
  month =               aug,
  doi =                 {10.1007/3-540-44618-4_12},
}
[De00] Sergio De Agostino. Erratum to "P-complete Problems in Data Compression". Theoretical Computer Science 234(1-2):325-326. Elsevier, March 2000. 
@article{tcs234(1-2)-Dea,
  author =              {De{~}Agostino, Sergio},
  title =               {Erratum to {"}{P}-complete Problems in Data
                         Compression{"}},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {234},
  number =              {1-2},
  pages =               {325-326},
  year =                {2000},
  month =               mar,
}
[DG00] Volker Diekert and Paul Gastin. LTL is Expressively Complete for Mazurkiewicz Traces. In ICALP'00, Lecture Notes in Computer Science 1853, pages 211-222. Springer-Verlag, July 2000. 
@inproceedings{icalp2000-DG,
  author =              {Diekert, Volker and Gastin, Paul},
  title =               {{LTL} is Expressively Complete for {M}azurkiewicz
                         Traces},
  editor =              {Montanari, Ugo and Rolim, Jos\'e D. P. and Welzl,
                         Emo},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'00)},
  acronym =             {{ICALP}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1853},
  pages =               {211-222},
  year =                {2000},
  month =               jul,
}
[DH00] Giovanna D'Agostino and Marco Hollenberg. Logical Questions Concerning the μ-Calculus: Interpolation, Lyndon and łoś-Tarski. Journal of Symbolic Logic 65(1):310-332. Association for Symbolic Logic, March 2000. 
@article{jsl65(1)-DH,
  author =              {D{'}Agostino, Giovanna and Hollenberg, Marco},
  title =               {Logical Questions Concerning the
                         {{\(\mu\)}}-Calculus: Interpolation, Lyndon and
                         {\L}o{\'s}-Tarski},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {65},
  number =              {1},
  pages =               {310-332},
  year =                {2000},
  month =               mar,
  doi =                 {10.2307/2586539},
}
[Dim00] Cătălin Dima. Real-Time Automata and the Kleene Algebra of Sets of Real Numbers. In STACS'00, Lecture Notes in Computer Science 1770, pages 279-289. Springer-Verlag, March 2000. 
@inproceedings{stacs2000-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Real-Time Automata and the {K}leene Algebra of Sets
                         of Real Numbers},
  editor =              {Reichel, Horst and Tison, Sophie},
  booktitle =           {{P}roceedings of the 17th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'00)},
  acronym =             {{STACS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1770},
  pages =               {279-289},
  year =                {2000},
  month =               mar,
}
[EK00] E. Allen Emerson and Vineet Kahlon. Reducing Model Checking of the Many to the Few. In CADE'00, Lecture Notes in Artificial Intelligence 1831, pages 236-254. Springer-Verlag, June 2000. 
@inproceedings{cade2000-EK,
  author =              {Emerson, E. Allen and Kahlon, Vineet},
  title =               {Reducing Model Checking of the Many to the~Few},
  editor =              {McAllester, David},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {A}utomated {D}eduction ({CADE}'00)},
  acronym =             {{CADE}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {1831},
  pages =               {236-254},
  year =                {2000},
  month =               jun,
  doi =                 {10.1007/10721959_19},
}
[Ete00] Kousha Etessami. A Note on a Question of Peled and Wilke Regarding Stutter-Invariant LTL. Information Processing Letters 75(6):261-263. Elsevier, November 2000. 
@article{ipl75(6)-Ete,
  author =              {Etessami, Kousha},
  title =               {A Note on a Question of {P}eled and {W}ilke
                         Regarding Stutter-Invariant {LTL}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {75},
  number =              {6},
  pages =               {261-263},
  year =                {2000},
  month =               nov,
}
[EW00] Kousha Etessami and Thomas Wilke. An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraïssé Game for Temporal Logic. Information and Computation 160(1-2):88-108. Academic Press, July 2000. 
@article{icomp160(1-2)-EW,
  author =              {Etessami, Kousha and Wilke, Thomas},
  title =               {An Until Hierarchy and Other Applications of an
                         Ehrenfeucht-Fra{\"i}ss{\'e} Game for Temporal Logic},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {160},
  number =              {1-2},
  pages =               {88-108},
  year =                {2000},
  month =               jul,
}
[FS00] Alain Finkel and Grégoire Sutre. Decidability of Reachability Problems for Classes of Two-Counter Automata. In STACS'00, Lecture Notes in Computer Science 1770, pages 346-357. Springer-Verlag, March 2000. 
@inproceedings{stacs2000-FS,
  author =              {Finkel, Alain and Sutre, Gr{\'e}goire},
  title =               {Decidability of Reachability Problems for Classes of
                         Two-Counter Automata},
  editor =              {Reichel, Horst and Tison, Sophie},
  booktitle =           {{P}roceedings of the 17th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'00)},
  acronym =             {{STACS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1770},
  pages =               {346-357},
  year =                {2000},
  month =               mar,
}
[Gor00] Valentin Goranko. Temporal Logics of Computations. In ESSLLI'00. August 2000. 
@inproceedings{esslli2000-Gor,
  author =              {Goranko, Valentin},
  title =               {Temporal Logics of Computations},
  booktitle =           {{P}roceedings of the 12th {E}uropean {S}ummer
                         {S}chool in {L}ogic, {L}anguage and {I}nformation
                         ({ESSLLI}'00)},
  acronym =             {{ESSLLI}'00},
  year =                {2000},
  month =               aug,
}
[GRS00] Valérie Gouranton, Pierre Réty, and Helmut Seidl. Synchronized Tree Languages Revisited and New Applications. Research Report 2000-16, Lab. Informatique Fondamentale d'Orléans, France, 2000. 
@techreport{lifo-2000-16-GRS,
  author =              {Gouranton, Val{\'e}rie and R{\'e}ty, Pierre and
                         Seidl, Helmut},
  title =               {Synchronized Tree Languages Revisited and New
                         Applications},
  number =              {2000-16},
  year =                {2000},
  institution =         {Lab.~Informatique Fondamentale d'Orl{\'e}ans,
                         France},
  type =                {Research Report},
}
[HCC+00] Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, and Fausto Giunchiglia. Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. Science of Computer Programming 36(1):53-64. Elsevier, January 2000. 
@article{scp36(1)-HCCCG,
  author =              {Hartonas{-}Garmhausen, Vicky and Campos, S{\'e}rgio
                         Vale Aguiar and Cimatti, Alessandro and Clarke,
                         Edmund M. and Giunchiglia, Fausto},
  title =               {Verification of a Safety-Critical Railway
                         Interlocking System with Real-Time Constraints},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {36},
  number =              {1},
  pages =               {53-64},
  year =                {2000},
  month =               jan,
}
[HR00] Thomas A. Henzinger and Jean-François Raskin. Robust Undecidability of Timed and Hybrid Systems. In HSCC'00, Lecture Notes in Computer Science 1790, pages 145-159. Springer-Verlag, March 2000. 
@inproceedings{hscc2000-HR,
  author =              {Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Robust Undecidability of Timed and Hybrid Systems},
  editor =              {Lynch, Nancy and Krogh, Bruce H.},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'00)},
  acronym =             {{HSCC}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1790},
  pages =               {145-159},
  year =                {2000},
  month =               mar,
  doi =                 {10.1007/3-540-46430-1_15},
}
[HTS+00] Masahiro Hirao, Masayuki Takeda, Ayumi Shinohara, and Setsuo Arikawa. Faster Fully Compressed Pattern Matching Algorithm for a Subclass of Straight-Line Programs. Technical Report DOI-TR-169, Dept. of Informatics, Kyushu University, Fukuoka, Japan, January 2000. 
@techreport{DOI-TR-169-HTSA,
  author =              {Hirao, Masahiro and Takeda, Masayuki and Shinohara,
                         Ayumi and Arikawa, Setsuo},
  title =               {Faster Fully Compressed Pattern Matching Algorithm
                         for a Subclass of Straight-Line Programs},
  number =              {DOI-TR-169},
  year =                {2000},
  month =               jan,
  institution =         {Dept. of Informatics, Kyushu University, Fukuoka,
                         Japan},
  type =                {Technical Report},
}
[Jur00] Marcin Jurdziński. Small Progress Measures for Solving Parity Games. In STACS'00, Lecture Notes in Computer Science 1770, pages 290-301. Springer-Verlag, March 2000. 
@inproceedings{stacs2000-Jur,
  author =              {Jurdzi{\'n}ski, Marcin},
  title =               {Small Progress Measures for Solving Parity Games},
  editor =              {Reichel, Horst and Tison, Sophie},
  booktitle =           {{P}roceedings of the 17th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'00)},
  acronym =             {{STACS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1770},
  pages =               {290-301},
  year =                {2000},
  month =               mar,
}
[KMP00] Yonit Kesten, Zohar Manna, and Amir Pnueli. Verifying Clocked Transition Systems. Acta Informatica 36(11):837-912. Springer-Verlag, 2000. 
@article{acta36(11)-KMP,
  author =              {Kesten, Yonit and Manna, Zohar and Pnueli, Amir},
  title =               {Verifying Clocked Transition Systems},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {36},
  number =              {11},
  pages =               {837-912},
  year =                {2000},
}
[KMT+00] Orna Kupferman, Parthasarathy Madhusudan, P. S. Thiagarajan, and Moshe Y. Vardi. Open Systems in Reactive Environments: Control and Synthesis. In CONCUR'00, Lecture Notes in Computer Science 1877, pages 92-107. Springer-Verlag, August 2000. 
@inproceedings{concur2000-KMTV,
  author =              {Kupferman, Orna and Madhusudan, Parthasarathy and
                         Thiagarajan, P. S. and Vardi, Moshe Y.},
  title =               {Open Systems in Reactive Environments: Control and
                         Synthesis},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1877},
  pages =               {92-107},
  year =                {2000},
  month =               aug,
}
[KV00] Orna Kupferman and Moshe Y. Vardi. An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. In CAV'00, Lecture Notes in Computer Science 1855, pages 36-52. Springer-Verlag, July 2000. 
@inproceedings{cav2000-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {An Automata-Theoretic Approach to Reasoning about
                         Infinite-State Systems},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {36-52},
  year =                {2000},
  month =               jul,
}
[KVW00] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An Automata-Theoretic Approach to Branching-Time Model-Checking. Journal of the ACM 47(2):312-360. ACM Press, March 2000. 
@article{jacm47(2)-KVW,
  author =              {Kupferman, Orna and Vardi, Moshe Y. and Wolper,
                         Pierre},
  title =               {An Automata-Theoretic Approach to Branching-Time
                         Model-Checking},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {47},
  number =              {2},
  pages =               {312-360},
  year =                {2000},
  month =               mar,
}
[LN00] Salvatore La Torre and Margherita Napoli. A Decidable Dense Branching-time Temporal Logic. In FSTTCS'00, Lecture Notes in Computer Science 1974, pages 139-150. Springer-Verlag, December 2000. 
@inproceedings{fsttcs2000-LN,
  author =              {La{~}Torre, Salvatore and Napoli, Margherita},
  title =               {A Decidable Dense Branching-time Temporal Logic},
  editor =              {Kapoor, Sanjiv and Prasad, Sanjiva},
  booktitle =           {{P}roceedings of the 20th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'00)},
  acronym =             {{FSTTCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1974},
  pages =               {139-150},
  year =                {2000},
  month =               dec,
}
[LS00] François Laroussinie and Philippe Schnoebelen. Specification in CTL+Past for Verification in CTL. Information and Computation 156(1-2):236-263. Academic Press, January 2000. 
@article{icomp156(1-2)-LS,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {Specification in {CTL}+{P}ast for Verification in
                         {CTL}},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {156},
  number =              {1-2},
  pages =               {236-263},
  year =                {2000},
  month =               jan,
}
[LS00] François Laroussinie and Philippe Schnoebelen. The State-Explosion Problem from Trace to Bisimulation Equivalence. In FoSSaCS'00, Lecture Notes in Computer Science 1784, pages 192-207. Springer-Verlag, March 2000. 
@inproceedings{fossacs2000-LS,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {The State-Explosion Problem from Trace to
                         Bisimulation Equivalence},
  editor =              {Tiuryn, Jerzy},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'00)},
  acronym =             {{FoSSaCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1784},
  pages =               {192-207},
  year =                {2000},
  month =               mar,
  doi =                 {10.1007/3-540-46432-8_13},
}
[LST00] François Laroussinie, Philippe Schnoebelen, and Mathieu Turuani. On the Expressive and Complexity of Quantitative Branching-Time Temporal Logics. In LATIN'00, Lecture Notes in Computer Science 1776, pages 437-446. Springer-Verlag, April 2000. 
@inproceedings{latin2000-LST,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe and Turuani, Mathieu},
  title =               {On the Expressive and Complexity of Quantitative
                         Branching-Time Temporal Logics},
  editor =              {Gonnet, Gastn H. and Panario, Daniel and Viola,
                         Alfredo},
  booktitle =           {{P}roceedings of the 4th {L}atin {A}merican
                         {S}ymposium on {T}heoretical {IN}formatics
                         ({LATIN}'00)},
  acronym =             {{LATIN}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1776},
  pages =               {437-446},
  year =                {2000},
  month =               apr,
}
[LT00] Christof Löding and Wolfgang Thomas. Alternating Automata and Logics over Infinite Words. In IFIPTCS'00, Lecture Notes in Computer Science 1872, pages 521-535. Springer-Verlag, August 2000. 
@inproceedings{ifiptcs2000-LT,
  author =              {L{\"o}ding, Christof and Thomas, Wolfgang},
  title =               {Alternating Automata and Logics over Infinite Words},
  editor =              {van Leeuwen, Jan and Watanabe, Osamu and Hagiya,
                         Masami and Mosses, Peter D. and Ito, Takayasu},
  booktitle =           {{E}xploring {N}ew {F}rontiers of {T}heoretical
                         {I}nformatics~--- {P}roceedings of the 1st {IFIP}
                         {I}nternational {C}onference on {T}heoretical
                         {C}omputer {S}cience ({IFIPTCS}'00)},
  acronym =             {{IFIPTCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1872},
  pages =               {521-535},
  year =                {2000},
  month =               aug,
}
[Mai00] Monika Maidl. The Common Fragment of CTL and LTL. In FOCS'00, pages 643-652. IEEE Comp. Soc. Press, November 2000. 
@inproceedings{focs2000-Mai,
  author =              {Maidl, Monika},
  title =               {The Common Fragment of {CTL} and~{LTL}},
  booktitle =           {{P}roceedings of the 41st {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'00)},
  acronym =             {{FOCS}'00},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {643-652},
  year =                {2000},
  month =               nov,
}
[Mal00] Oded Maler. Systèmes discrets, temporisés et hybrides. Mémoire d'habilitation, Université Joseph Fourier, Grenoble, France, May 2000. 
@phdthesis{hab-maler,
  author =              {Maler, Oded},
  title =               {Syst{\`e}mes discrets, temporis{\'e}s et hybrides},
  year =                {2000},
  month =               may,
  institution =         {Universit{\'e} Joseph Fourier, Grenoble, France},
  school =              {Universit{\'e} Joseph Fourier, Grenoble, France},
  type =                {M\'emoire d'habilitation},
}
[Man00] Panagiotis Manolios. Mu-Calculus Model-Checking. In Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore (eds.), Computer Aided Reasoning: ACL2 Case Studies. Kluwer Academic, June 2000. 
@incollection{CAR-ACL2CS-Man,
  author =              {Manolios, Panagiotis},
  title =               {Mu-Calculus Model-Checking},
  editor =              {Kaufmann, Matt and Manolios, Panagiotis and Moore,
                         J. Strother},
  booktitle =           {Computer Aided Reasoning: {ACL2} Case Studies},
  publisher =           {Kluwer Academic},
  pages =               {93-111},
  year =                {2000},
  month =               jun,
}
[Mil00] Joseph S. Miller. Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata. In HSCC'00, Lecture Notes in Computer Science 1790, pages 296-310. Springer-Verlag, March 2000. 
@inproceedings{hscc2000-Mil,
  author =              {Miller, Joseph S.},
  title =               {Decidability and Complexity Results for Timed
                         Automata and Semi-linear Hybrid Automata},
  editor =              {Lynch, Nancy and Krogh, Bruce H.},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'00)},
  acronym =             {{HSCC}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1790},
  pages =               {296-310},
  year =                {2000},
  month =               mar,
}
[MS00] Zohar Manna and Henny Sipma. Alternating the Temporal Picture for Safety. In ICALP'00, Lecture Notes in Computer Science 1853, pages 429-450. Springer-Verlag, July 2000. 
@inproceedings{icalp2000-MS,
  author =              {Manna, Zohar and Sipma, Henny},
  title =               {Alternating the Temporal Picture for Safety},
  editor =              {Montanari, Ugo and Rolim, Jos\'e D. P. and Welzl,
                         Emo},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'00)},
  acronym =             {{ICALP}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1853},
  pages =               {429-450},
  year =                {2000},
  month =               jul,
}
[Odd00] Denis Oddoux. Génération efficace d'automates de Büchi à partir de formules LTL. Mémoire de D.E.A., Lab. Informatique Algorithmique: Fondements et Applications, Université Paris 7, France, June 2000. 
@mastersthesis{dea-oddoux,
  author =              {Oddoux, Denis},
  title =               {G{\'e}n{\'e}ration efficace d'automates de
                         {B}{\"u}chi {\`a} partir de formules {LTL}},
  year =                {2000},
  month =               jun,
  school =              {Lab.~Informatique Algorithmique: Fondements et
                         Applications, Universit{\'e} Paris~7, France},
  type =                {M\'emoire de D.E.A.},
}
[Pur00] Anuj Puri. Dynamical Properties of Timed Systems. Discrete Event Dynamic Systems 10(1-2):87-113. Kluwer Academic, January 2000. 
@article{deds10(1-2)-Pur,
  author =              {Puri, Anuj},
  title =               {Dynamical Properties of Timed Systems},
  publisher =           {Kluwer Academic},
  journal =             {Discrete Event Dynamic Systems},
  volume =              {10},
  number =              {1-2},
  pages =               {87-113},
  year =                {2000},
  month =               jan,
  doi =                 {10.1023/A:1008387132377},
}
[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,
}
[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,
}
[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,
}
[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},
}
[SB00] Fabio Somenzi and Roderick Bloem. Efficient Büchi Automata from LTL Formulae. In CAV'00, Lecture Notes in Computer Science 1855, pages 248-263. Springer-Verlag, July 2000. 
@inproceedings{cav2000-SB,
  author =              {Somenzi, Fabio and Bloem, Roderick},
  title =               {Efficient {B}{\"u}chi Automata from {LTL} Formulae},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {248-263},
  year =                {2000},
  month =               jul,
}
[TH00] Heikko Tauriainen and Keijo Heljanko. Testing SPIN's LTL Formula Conversion into Büchi Automata with Randomly Generated Input. In SPIN'00, Lecture Notes in Computer Science 1885, pages 54-72. Springer-Verlag, August 2000. 
@inproceedings{spin2000-TH,
  author =              {Tauriainen, Heikko and Heljanko, Keijo},
  title =               {Testing {SPIN}'s {LTL} Formula Conversion into
                         {B}{\"u}chi Automata with Randomly Generated Input},
  editor =              {Havelund, Klaus and Penix, John and Viser, Willem},
  booktitle =           {{P}roceedings of the 7th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'00)},
  acronym =             {{SPIN}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1885},
  pages =               {54-72},
  year =                {2000},
  month =               aug,
}
[Wal00] Igor Walukiewicz. Model Checking CTL Properties of Pushdown Systems. In FSTTCS'00, Lecture Notes in Computer Science 1974, pages 127-138. Springer-Verlag, December 2000. 
@inproceedings{fsttcs2000-Wal,
  author =              {Walukiewicz, Igor},
  title =               {Model Checking {CTL} Properties of Pushdown Systems},
  editor =              {Kapoor, Sanjiv and Prasad, Sanjiva},
  booktitle =           {{P}roceedings of the 20th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'00)},
  acronym =             {{FSTTCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1974},
  pages =               {127-138},
  year =                {2000},
  month =               dec,
}
[Wol00] Pierre Wolper. Constructing Automata from Temporal Logic Formulas: A Tutorial. In Lectures on Formal Methods and Performance Analysis – Revised Lectures of the 1st EEF/Euro Summer School on Trends in Computer Science, Lecture Notes in Computer Science 2090, pages 261-277. Springer-Verlag, July 2000. 
@inproceedings{eef2000-Wol,
  author =              {Wolper, Pierre},
  title =               {Constructing Automata from Temporal Logic Formulas:
                         A Tutorial},
  editor =              {Brinksma, Ed and Hermanns, Holger and Katoen,
                         Joost-Pieter},
  booktitle =           {{L}ectures on {F}ormal {M}ethods and {P}erformance
                         {A}nalysis~-- {R}evised {L}ectures of the 1st
                         {EEF}/{E}uro {S}ummer {S}chool on {T}rends in
                         {C}omputer {S}cience},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2090},
  pages =               {261-277},
  year =                {2000},
  month =               jul,
}
List of authors