2001
[LMS01] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model Checking CTL+ and FCTL is hard. In FoSSaCS'01, Lecture Notes in Computer Science 2030, pages 318-331. Springer-Verlag, April 2001.
Abstract

Among the branching-time temporal logics used for the specification and verification of systems, CTL+, FCTL and ECTL+ are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is Δ2p-complete.

@inproceedings{fossacs2001-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking {CTL}{\(^+\)} and {FCTL} is hard},
  editor =              {Honsell, Furio and Miculan, Marino},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'01)},
  acronym =             {{FoSSaCS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2030},
  pages =               {318-331},
  year =                {2001},
  month =               apr,
  doi =                 {10.1007/3-540-45315-6_21},
  abstract =            {Among the branching-time temporal logics used for
                         the specification and verification of systems,
                         CTL\(^+\), FCTL and ECTL\(^+\) are the most notable
                         logics for which the precise computational
                         complexity of model checking is not known. We answer
                         this longstanding open problem and show that model
                         checking these (and some related) logics is
                         \(\Delta_2^p\)-complete.},
}
[AB01] Carlos Areces and Patrick Blackburn. Bringing them all Together. Journal of Logic and Computation 11(5):657-669. Oxford University Press, October 2001. 
@article{jlc11(5)-AB,
  author =              {Areces, Carlos and Blackburn, Patrick},
  title =               {Bringing them all Together},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {11},
  number =              {5},
  pages =               {657-669},
  year =                {2001},
  month =               oct,
}
[AB01] Eugene Asarin and Ahmed Bouajjani. Perturbed Turing machines and hybrid systems. In LICS'01, pages 269-278. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-AB,
  author =              {Asarin, Eugene and Bouajjani, Ahmed},
  title =               {Perturbed {T}uring machines and hybrid systems},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {269-278},
  year =                {2001},
  month =               jun,
}
[AEL+01] Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron A. Peled. Parametric Temporal Logic for "Model Measuring". ACM Transactions on Computational Logic 2(3):388-407. ACM Press, July 2001. 
@article{tocl2(3)-AELP,
  author =              {Alur, Rajeev and Etessami, Kousha and La{~}Torre,
                         Salvatore and Peled, Doron A.},
  title =               {Parametric Temporal Logic for {"}Model Measuring{"}},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {2},
  number =              {3},
  pages =               {388-407},
  year =                {2001},
  month =               jul,
}
[dAH01] Luca de Alfaro and Thomas A. Henzinger. Interface automata. In FSE'01, pages 109-120. ACM Press, September 2001. 
@inproceedings{fse2001-AH,
  author =              {de Alfaro, Luca and Henzinger, Thomas A.},
  title =               {Interface automata},
  booktitle =           {{P}roceedings of the 9th {A}nnual {S}ymposium on
                         {F}oundations of {S}oftware {E}ngineering
                         ({FSE}'01)},
  acronym =             {{FSE}'01},
  publisher =           {ACM Press},
  pages =               {109-120},
  year =                {2001},
  month =               sep,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzinger, and Freddy Y. C. Mang. The Control of Synchronous Systems, Part II. In CONCUR'01, Lecture Notes in Computer Science 2154, pages 566-582. Springer-Verlag, August 2001. 
@inproceedings{concur2001-AHM,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and Mang,
                         Freddy Y. C.},
  title =               {The Control of Synchronous Systems, Part~{II}},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2154},
  pages =               {566-582},
  year =                {2001},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Symbolic Algorithms for Infinite-State Games. In CONCUR'01, Lecture Notes in Computer Science 2154, pages 536-550. Springer-Verlag, August 2001. 
@inproceedings{concur2001-AHM2,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and
                         Majumdar, Rupak},
  title =               {Symbolic Algorithms for Infinite-State Games},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2154},
  pages =               {536-550},
  year =                {2001},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. From Verification to Control: Dynamic Programs for Omega-Regular Objectives. In LICS'01, pages 279-290. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-AHM,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and
                         Majumdar, Rupak},
  title =               {From Verification to Control: Dynamic Programs for
                         Omega-Regular Objectives},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {279-290},
  year =                {2001},
  month =               jun,
}
[AI01] Micah Adler and Neil Immerman. An n! Lower Bound On Formula Size. In LICS'01, pages 197-206. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-AI,
  author =              {Adler, Micah and Immerman, Neil},
  title =               {An {{\(n!\)}} Lower Bound On Formula Size},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {197-206},
  year =                {2001},
  month =               jun,
}
[ALP01] Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. In HSCC'01, Lecture Notes in Computer Science 2034, pages 49-62. Springer-Verlag, March 2001. 
@inproceedings{hscc2001-ALP,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and Pappas,
                         George J.},
  title =               {Optimal paths in weighted timed automata},
  editor =              {Di{~}Benedetto, Maria Domenica and
                         Sangiovani{-}Vincentelli, Alberto L.},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2034},
  pages =               {49-62},
  year =                {2001},
  month =               mar,
  doi =                 {10.1007/3-540-45351-2_8},
}
[ALV01] Roberto Amadio, Denis Lugiez, and Vincent Vanackère. On the Symbolic Reduction of Processes with Cryptographic Functions. Technical Report 4147, INRIA, March 2001. 
@techreport{TR-inria4147,
  author =              {Amadio, Roberto and Lugiez, Denis and Vanack{\`e}re,
                         Vincent},
  title =               {On the Symbolic Reduction of Processes with
                         Cryptographic Functions},
  number =              {4147},
  year =                {2001},
  month =               mar,
  institution =         {INRIA},
}
[AM01] Yasmina Abdeddaïm and Oded Maler. Job-Shop Scheduling Using Timed Automata. In CAV'01, Lecture Notes in Computer Science 2102, pages 478-492. Springer-Verlag, July 2001. 
@inproceedings{cav2001-AM,
  author =              {Abdedda{\"\i}m, Yasmina and Maler, Oded},
  title =               {Job-Shop Scheduling Using Timed Automata},
  editor =              {Berry, G{\'e}rard and Comon, Hubert and Finkel,
                         Alain},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2102},
  pages =               {478-492},
  year =                {2001},
  month =               jul,
}
[AN01] André Arnold and Damian Niwiński. Complete lattices and fixed-point theorems. In Rudiments of μ-calculus, Studies in Logic and the Foundations of Mathematics 146, pages 1-39. North-Holland, 2001. 
@incollection{Rmc2001-ANa,
  author =              {Arnold, Andr{\'e} and Niwi{\'n}ski, Damian},
  title =               {Complete lattices and fixed-point theorems},
  booktitle =           {Rudiments of {\(\mu\)}-calculus},
  publisher =           {North-Holland},
  series =              {Studies in Logic and the Foundations of Mathematics},
  volume =              {146},
  pages =               {1-39},
  chapter =             {1},
  year =                {2001},
}
[ASY01] Eugene Asarin, Gerardo Schneider, and Sergio Yovine. On the Decidability of the Reachability Problem for Planar Differential Inclusions. In HSCC'01, Lecture Notes in Computer Science 2034, pages 89-104. Springer-Verlag, March 2001. 
@inproceedings{hscc2001-ASY,
  author =              {Asarin, Eugene and Schneider, Gerardo and Yovine,
                         Sergio},
  title =               {On the Decidability of the Reachability Problem for
                         Planar Differential Inclusions},
  editor =              {Di{~}Benedetto, Maria Domenica and
                         Sangiovani{-}Vincentelli, Alberto L.},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2034},
  pages =               {89-104},
  year =                {2001},
  month =               mar,
}
[BBF+01] Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre McKenzie. Systems and Software Verification: Model-Checking Techniques and Tools. Springer-Verlag, 2001. 
@book{SSV2001-BBFLPPS,
  author =              {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and
                         Finkel, Alain and Laroussinie, Fran{\c c}ois and
                         Petit, Antoine and Petrucci, Laure and Schnoebelen,
                         {\relax Ph}ilippe and McKenzie, Pierre},
  title =               {Systems and Software Verification: Model-Checking
                         Techniques and Tools},
  publisher =           {Springer-Verlag},
  year =                {2001},
}
[BBS01] Jiří Barnat, Luboš Brim, and Jitka Stříbrná. Distributed LTL Model-Checking in SPIN. In SPIN'01, Lecture Notes in Computer Science 2057, pages 200-216. Springer-Verlag, May 2001. 
@inproceedings{spin2001-BBS,
  author =              {Barnat, Ji{\v r}{\'\i} and Brim, Lubo{\v s} and
                         St{\v r}{\'\i}brn{\'a}, Jitka},
  title =               {Distributed {LTL} Model-Checking in {SPIN}},
  editor =              {Dwyer, Matthew B.},
  booktitle =           {{P}roceedings of the 8th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'01)},
  acronym =             {{SPIN}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2057},
  pages =               {200-216},
  year =                {2001},
  month =               may,
}
[BCK+01] Luboš Brim, Ivana Černa, Pavel Krčál, and Radek Pelánek. Distributed LTL Model Checking Based on Negative Cycle Detection. In FSTTCS'01, Lecture Notes in Computer Science 2245, pages 96-107. Springer-Verlag, December 2001. 
@inproceedings{fsttcs2001-BCKP,
  author =              {Brim, Lubo{\v s} and {\v{C}}erna, Ivana and
                         Kr{\v{c}}{\'a}l, Pavel and Pel{\'a}nek, Radek},
  title =               {Distributed {LTL} Model Checking Based on Negative
                         Cycle Detection},
  editor =              {Hariharan, Ramesh and Mukund, Madhavan and Vinay,
                         V.},
  booktitle =           {{P}roceedings of the 21st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'01)},
  acronym =             {{FSTTCS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2245},
  pages =               {96-107},
  year =                {2001},
  month =               dec,
}
[Bed01] Nicolas Bedon. Logic over Words on Denumerable Ordinals. Journal of Computer and System Sciences 63(3):394-431. Academic Press, November 2001. 
@article{jcss63(3)-Bed,
  author =              {Bedon, Nicolas},
  title =               {Logic over Words on Denumerable Ordinals},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {63},
  number =              {3},
  pages =               {394-431},
  year =                {2001},
  month =               nov,
}
[Bey01] Dirk Beyer. Rabbit: Verification of Real-Time Systems. In RT-TOOLS'01, pages 13-21. August 2001. 
@inproceedings{rttools2001-Bey,
  author =              {Beyer, Dirk},
  title =               {Rabbit: Verification of Real-Time Systems},
  editor =              {Pettersson, Paul and Yovine, Sergio},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on {R}eal-Time
                         {T}ools ({RT-TOOLS}'01)},
  acronym =             {{RT-TOOLS}'01},
  pages =               {13-21},
  year =                {2001},
  month =               aug,
}
[BFH+01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, and Judi Romijn. Efficient Guiding Towards Cost-Optimality in UPPAAL. In TACAS'01, Lecture Notes in Computer Science 2031, pages 174-188. Springer-Verlag, April 2001. 
@inproceedings{tacas2001-BFHLPR,
  author =              {Behrmann, Gerd and Fehnker, Ansgar and Hune, Thomas
                         and Larsen, Kim Guldstrand and Pettersson, Paul and
                         Romijn, Judi},
  title =               {Efficient Guiding Towards Cost-Optimality in UPPAAL},
  editor =              {Margaria, Tiziana and Yi, Wang},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'01)},
  acronym =             {{TACAS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2031},
  pages =               {174-188},
  year =                {2001},
  month =               apr,
}
[BFH+01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimum-Cost Reachability for Priced Timed Automata. In HSCC'01, Lecture Notes in Computer Science 2034, pages 147-161. Springer-Verlag, March 2001. 
@inproceedings{hscc2001-BFHLPRV,
  author =              {Behrmann, Gerd and Fehnker, Ansgar and Hune, Thomas
                         and Larsen, Kim Guldstrand and Pettersson, Paul and
                         Romijn, Judi and Vaandrager, Frits},
  title =               {Minimum-Cost Reachability for Priced Timed Automata},
  editor =              {Di{~}Benedetto, Maria Domenica and
                         Sangiovani{-}Vincentelli, Alberto L.},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2034},
  pages =               {147-161},
  year =                {2001},
  month =               mar,
  doi =                 {10.1007/3-540-45351-2_15},
}
[BG01] Glenn Bruns and Patrice Godefroid. Temporal Logic Query Checking (Extended Abstract). In LICS'01, pages 409-417. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-BG,
  author =              {Bruns, Glenn and Godefroid, Patrice},
  title =               {Temporal Logic Query Checking (Extended Abstract)},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {409-417},
  year =                {2001},
  month =               jun,
}
[BGI+01] Boaz Barak, Oded Goldreich, Rusell Impagliazzo, Steven Rudich, Amit Sahai, Salil Vadhan, and Ke Yang. On the (Im)possibility of Obfuscating Programs. In CRYPTO'01, Lecture Notes in Computer Science 2139, pages 1-18. Springer-Verlag, August 2001. 
@inproceedings{crypto2001-BGIRSVY,
  author =              {Barak, Boaz and Goldreich, Oded and Impagliazzo,
                         Rusell and Rudich, Steven and Sahai, Amit and
                         Vadhan, Salil and Yang, Ke},
  title =               {On the (Im)possibility of Obfuscating Programs},
  editor =              {Kilian, Joe},
  booktitle =           {{P}roceedings of the 21st {A}nnual {I}nternational
                         {C}ryptology {C}onference ({CRYPTO}'01)},
  acronym =             {{CRYPTO}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2139},
  pages =               {1-18},
  year =                {2001},
  month =               aug,
}
[BGI+01] Boaz Barak, Oded Goldreich, Rusell Impagliazzo, Steven Rudich, Amit Sahai, Salil Vadhan, and Ke Yang. On the (Im)possibility of Obfuscating Programs. Research Report 01-057, Electronic Colloquium on Computational Complexity, August 2001. 
@techreport{eccc2001-BGIRSVY,
  author =              {Barak, Boaz and Goldreich, Oded and Impagliazzo,
                         Rusell and Rudich, Steven and Sahai, Amit and
                         Vadhan, Salil and Yang, Ke},
  title =               {On the (Im)possibility of Obfuscating Programs},
  number =              {01-057},
  year =                {2001},
  month =               aug,
  institution =         {Electronic Colloquium on Computational Complexity},
  type =                {Research Report},
}
[BGW01] Nikita Borisov, Ian Goldberg, and Klaus W. Wagner. Intercepting Mobile Communications: The Insecurity of 802.11. In MOBICOM'01, pages 180-189. ACM Press, July 2001. 
@inproceedings{mobicom2001-BGW,
  author =              {Borisov, Nikita and Goldberg, Ian and Wagner, Klaus
                         W.},
  title =               {Intercepting Mobile Communications: The Insecurity
                         of~{\(802.11\)}},
  booktitle =           {{P}roceedings of the 7th {A}nnual {I}nternational
                         {C}onference on {M}obile {C}omputing and
                         {N}etworking ({MOBICOM}'01)},
  acronym =             {{MOBICOM}'01},
  publisher =           {ACM Press},
  pages =               {180-189},
  year =                {2001},
  month =               jul,
}
[BLW01] Benedikt Bollig, Martin Leucker, and Michael Weber. Local Parallel Model Checking for the Alternation Free μ-Calculus. Technical Report AIB-2001-04, Aachener Informatik Berichte, Aachen, Germany, March 2001. 
@techreport{TR-Aachen0104,
  author =              {Bollig, Benedikt and Leucker, Martin and Weber,
                         Michael},
  title =               {Local Parallel Model Checking for the Alternation
                         Free {\(\mu\)}-Calculus},
  number =              {AIB-2001-04},
  year =                {2001},
  month =               mar,
  institution =         {Aachener Informatik Berichte, Aachen, Germany},
  type =                {Technical Report},
}
[BR01] Thomas Ball and Sriram Rajamani. The SLAM toolkit. In CAV'01, Lecture Notes in Computer Science 2102, pages 260-264. Springer-Verlag, July 2001. 
@inproceedings{cav2001-BR,
  author =              {Ball, Thomas and Rajamani, Sriram},
  title =               {The {SLAM} toolkit},
  editor =              {Berry, G{\'e}rard and Comon, Hubert and Finkel,
                         Alain},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2102},
  pages =               {260-264},
  year =                {2001},
  month =               jul,
}
[BS01] Julian C. Bradfield and Colin Stirling. Modal Logics and Mu-Calculi: An Introduction. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka (eds.), Handbook of Process Algebra. Elsevier, 2001. 
@incollection{HPA-BS,
  author =              {Bradfield, Julian C. and Stirling, Colin},
  title =               {Modal Logics and Mu-Calculi: An Introduction},
  editor =              {Bergstra, Jan A. and Ponse, Alban and Smolka, Scott
                         A.},
  booktitle =           {Handbook of Process Algebra},
  publisher =           {Elsevier},
  chapter =             {1.4},
  year =                {2001},
}
[CC01] Sérgio Vale Aguiar Campos and Edmund M. Clarke. The Verus Language: Representing Time Efficiently with BDDs. Theoretical Computer Science 253(1):95-118. Elsevier, February 2001. 
@article{tcs253(1)-CC,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund
                         M.},
  title =               {The {V}erus Language: Representing Time Efficiently
                         with {BDD}s},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {253},
  number =              {1},
  pages =               {95-118},
  year =                {2001},
  month =               feb,
}
[CGJ+01] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Progress on the State Explosion Problem in Model Checking. In Reinhard Wilhelm (eds.), Informatics – 10 Years Back. 10 Years Ahead, Lecture Notes in Computer Science 2000, pages 176-194. Springer-Verlag, 2001. 
@incollection{lncs2000-CGJLV,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Jha, Somesh
                         and Lu, Yuan and Veith, Helmut},
  title =               {Progress on the State Explosion Problem in Model
                         Checking},
  editor =              {Wilhelm, Reinhard},
  booktitle =           {Informatics~-- 10~Years Back. 10~Years Ahead},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2000},
  pages =               {176-194},
  year =                {2001},
}
[CKV01] Hana Chockler, Orna Kupferman, and Moshe Y. Vardi. Coverage Metrics for Temporal Logic Model Checking. In TACAS'01, Lecture Notes in Computer Science 2031, pages 528-542. Springer-Verlag, April 2001. 
@inproceedings{tacas2001-CKV,
  author =              {Chockler, Hana and Kupferman, Orna and Vardi, Moshe
                         Y.},
  title =               {Coverage Metrics for Temporal Logic Model Checking},
  editor =              {Margaria, Tiziana and Yi, Wang},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'01)},
  acronym =             {{TACAS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2031},
  pages =               {528-542},
  year =                {2001},
  month =               apr,
}
[CLS01] Gianfranco Ciardo, Gerald Lüttgen, and Radu Siminiceanu. Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. In TACAS'01, Lecture Notes in Computer Science 2031, pages 328-342. Springer-Verlag, April 2001. 
@inproceedings{tacas2001-CLS,
  author =              {Ciardo, Gianfranco and L{\"u}ttgen, Gerald and
                         Siminiceanu, Radu},
  title =               {Saturation: An Efficient Iteration Strategy for
                         Symbolic State-Space Generation},
  editor =              {Margaria, Tiziana and Yi, Wang},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'01)},
  acronym =             {{TACAS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2031},
  pages =               {328-342},
  year =                {2001},
  month =               apr,
}
[CMR01] Paul Caspi, Christine Mazuet, and Natacha Reynaud-Paligot. About the design of distributed control systems: The quasi-synchronous approach. In SAFECOMP'01, Lecture Notes in Computer Science 2187, pages 215-226. Springer-Verlag, September 2001. 
@inproceedings{safecomp2001-CMR,
  author =              {Caspi, Paul and Mazuet, Christine and
                         Reynaud{-}Paligot, Natacha},
  title =               {About the design of distributed control systems:
                         The~quasi-synchronous approach},
  editor =              {Voges, Udo},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}omputer {S}afety, {R}eliability
                         and {S}ecurity ({SAFECOMP}'01)},
  acronym =             {{SAFECOMP}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2187},
  pages =               {215-226},
  year =                {2001},
  month =               sep,
  doi =                 {10.1007/3-540-45416-0_21},
}
[CMR01] Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discrete Applied Mathematics 108(1-2):23-52. Elsevier, February 2001. 
@article{dam108(1-2)-CMR,
  author =              {Courcelle, Bruno and Makowsky, Johann A. and Rotics,
                         Udi},
  title =               {On the fixed parameter complexity of graph
                         enumeration problems definable in monadic
                         second-order logic},
  publisher =           {Elsevier},
  journal =             {Discrete Applied Mathematics},
  volume =              {108},
  number =              {1-2},
  pages =               {23-52},
  year =                {2001},
  month =               feb,
}
[CRS01] Franck Cassez, Mark D. Ryan, and Pierre-Yves Schobbens. Proving Feature Non-Interaction with Alternating-Time Temporal Logic. In Proceedings of the FIREworks Workshop on Language Constructs for Describing Features, pages 85-104. Springer-Verlag, January 2001. 
@inproceedings{fireworks2000-CRS,
  author =              {Cassez, Franck and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {Proving Feature Non-Interaction with
                         Alternating-Time Temporal Logic},
  editor =              {Gilmore, Stephen D. and Ryan, Mark D.},
  booktitle =           {{P}roceedings of the {FIRE}works {W}orkshop on
                         {L}anguage {C}onstructs for {D}escribing {F}eatures},
  publisher =           {Springer-Verlag},
  pages =               {85-104},
  year =                {2001},
  month =               jan,
  confyear =            {2000},
  confmonth =           {5},
}
[CS01] Edmund M. Clarke and Bernd-Holger Schlingloff. Model Checking. In John Alan Robinson and Andrei Voronkov (eds.), Handbook of Automated Reasoning. Elsevier and MIT Press, 2001. 
@incollection{HARb-2001-24-CS,
  author =              {Clarke, Edmund M. and Schlingloff, Bernd-Holger},
  title =               {Model Checking},
  editor =              {Robinson, John Alan and Voronkov, Andrei},
  booktitle =           {Handbook of Automated Reasoning},
  publisher =           {Elsevier and MIT Press},
  volume =              {2},
  pages =               {1635-1790},
  year =                {2001},
}
[Die01] Henning Dierks. PLC-automata: a new class of implementable real-time automata. Theoretical Computer Science 253(1):61-93. Elsevier, February 2001. 
@article{tcs253(1)-dierks,
  author =              {Dierks, Henning},
  title =               {{PLC}-automata: a new class of implementable
                         real-time automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {253},
  number =              {1},
  pages =               {61-93},
  year =                {2001},
  month =               feb,
}
[Dim01] Cătălin Dima. Real-time automata. Journal of Automata, Languages and Combinatorics 6(1):3-23. 2001. 
@article{jalc6(1)-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Real-time automata},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {6},
  number =              {1},
  pages =               {3-23},
  year =                {2001},
  doi =                 {10.25596/jalc-2001-003},
}
[DSK01] Zhe Dang, Pierluigi San Pietro, and Richard A. Kemmerer. On Presburger Liveness of Discrete Timed Automata. In STACS'01, Lecture Notes in Computer Science 2010, pages 132-143. Springer-Verlag, February 2001. 
@inproceedings{stacs01-DSPK,
  author =              {Dang, Zhe and San{~}Pietro, Pierluigi and Kemmerer,
                         Richard A.},
  title =               {On {P}resburger Liveness of Discrete Timed Automata},
  editor =              {Ferreira, Afonso and Reichel, Horst},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'01)},
  acronym =             {{STACS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2010},
  pages =               {132-143},
  year =                {2001},
  month =               feb,
}
[EJS01] E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model checking for the Mu-calculus and its fragments. Theoretical Computer Science 258(1-2):491-522. Elsevier, May 2001. 
@article{tcs258(1-2)-EJS,
  author =              {Emerson, E. Allen and Jutla, Charanjit S. and
                         Sistla, A. Prasad},
  title =               {On model checking for the Mu-calculus and its
                         fragments},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {258},
  number =              {1-2},
  pages =               {491-522},
  year =                {2001},
  month =               may,
}
[Fre01] Tim French. Decidability of Quantified Propositional Branching Time Logics. In AJCAI'01, Lecture Notes in Computer Science 2256, pages 165-176. Springer-Verlag, December 2001. 
@inproceedings{ajcai2001-Fre,
  author =              {French, Tim},
  title =               {Decidability of Quantified Propositional Branching
                         Time Logics},
  editor =              {Stumptner, Markus and Corbett, Dan and Brooks, Mike},
  booktitle =           {{P}roceedings of the 14th {A}ustralian {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({AJCAI}'01)},
  acronym =             {{AJCAI}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2256},
  pages =               {165-176},
  year =                {2001},
  month =               dec,
  doi =                 {10.1007/3-540-45656-2_15},
}
[FS01] Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata. In RV'01, Electronic Notes in Theoretical Computer Science 55(2). Elsevier, July 2001. 
@inproceedings{rv2001-FS,
  author =              {Finkbeiner, Bernd and Sipma, Henny},
  title =               {Checking Finite Traces using Alternating Automata},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'01)},
  acronym =             {{RV}'01},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {55},
  number =              {2},
  year =                {2001},
  month =               jul,
}
[FS01] Alain Finkel and Philippe Schnoebelen. Well-Structured Transition Systems Everywhere!. Theoretical Computer Science 256(1-2):63-92. Elsevier, April 2001. 
@article{tcs256(1-2)-FS,
  author =              {Finkel, Alain and Schnoebelen, {\relax Ph}ilippe},
  title =               {Well-Structured Transition Systems Everywhere!},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {256},
  number =              {1-2},
  pages =               {63-92},
  year =                {2001},
  month =               apr,
}
[GCO01] Thorsten Gerdsmeier and Rachel Cardell-Oliver. Analysis of Scheduling Behaviour using Generic Timed Automata. In CATS'01, Electronic Notes in Theoretical Computer Science 42. Elsevier, January 2001. 
@inproceedings{cats2001-GC,
  author =              {Gerdsmeier, Thorsten and Cardell-Oliver, Rachel},
  title =               {Analysis of Scheduling Behaviour using Generic Timed
                         Automata},
  editor =              {Fidge, Colin},
  booktitle =           {Computing: The Australasian Theory Symposium
                         ({CATS}'01)},
  acronym =             {{CATS}'01},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {42},
  year =                {2001},
  month =               jan,
}
[Gei01] Marc C.W. Geilen. On the Construction of Monitors for Temporal Logic Properties. In RV'01, Electronic Notes in Theoretical Computer Science 55(2). Elsevier, July 2001. 
@inproceedings{rv2001-Gei,
  author =              {Geilen, Marc C.W.},
  title =               {On the Construction of Monitors for Temporal Logic
                         Properties},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'01)},
  acronym =             {{RV}'01},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {55},
  number =              {2},
  year =                {2001},
  month =               jul,
}
[GO01] Paul Gastin and Denis Oddoux. Fast LTL to Büchi Automata Translation. In CAV'01, Lecture Notes in Computer Science 2102, pages 53-65. Springer-Verlag, July 2001. 
@inproceedings{cav2001-GO,
  author =              {Gastin, Paul and Oddoux, Denis},
  title =               {Fast {LTL} to {B}{\"u}chi Automata Translation},
  editor =              {Berry, G{\'e}rard and Comon, Hubert and Finkel,
                         Alain},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2102},
  pages =               {53-65},
  year =                {2001},
  month =               jul,
}
[Gor01] Valentin Goranko. Coalition Games and Alternating Temporal Logics. In TARK'01, pages 259-272. Morgan Kaufmann Publishers, July 2001. 
@inproceedings{tark2001-Gor,
  author =              {Goranko, Valentin},
  title =               {Coalition Games and Alternating Temporal Logics},
  editor =              {van Benthem, Johan},
  booktitle =           {{P}roceedings of the 8th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'01)},
  acronym =             {{TARK}'01},
  publisher =           {Morgan Kaufmann Publishers},
  pages =               {259-272},
  year =                {2001},
  month =               jul,
}
[GP01] Leszek Gąsieniec and Igor Potapov. Time/Space Efficient Compressed Pattern Matching. In FCT'01, Lecture Notes in Computer Science 2138, pages 138-149. Springer-Verlag, August 2001. 
@inproceedings{fct2001-GP,
  author =              {G{\k a}sieniec, Leszek and Potapov, Igor},
  title =               {Time{\slash}Space Efficient Compressed Pattern
                         Matching},
  editor =              {Freivalds, Rusins},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {S}ymposium on {F}undamentals of {C}omputation
                         {T}heory ({FCT}'01)},
  acronym =             {{FCT}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2138},
  pages =               {138-149},
  year =                {2001},
  month =               aug,
}
[GRS01] Valérie Gouranton, Pierre Réty, and Helmut Seidl. Synchronized Tree Languages Revisited and New Applications. In FoSSaCS'01, Lecture Notes in Computer Science 2030, pages 214-229. Springer-Verlag, April 2001. 
@inproceedings{fossacs2001-GRS,
  author =              {Gouranton, Val{\'e}rie and R{\'e}ty, Pierre and
                         Seidl, Helmut},
  title =               {Synchronized Tree Languages Revisited and New
                         Applications},
  editor =              {Honsell, Furio and Miculan, Marino},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'01)},
  acronym =             {{FoSSaCS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2030},
  pages =               {214-229},
  year =                {2001},
  month =               apr,
}
[HMU01] John Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Pearson, 2001. 
@book{HMU01-IATLC,
  author =              {Hopcroft, John and Motwani, Rajeev and Ullman,
                         Jeffrey D.},
  title =               {Introduction to Automata Theory, Languages, and
                         Computation},
  publisher =           {Pearson},
  year =                {2001},
}
[Hun01] Thomas Hune. Analyzing real-time systems: theory and tools. PhD thesis, University of Aarhus, Denmark, 2001. 
@phdthesis{phd-hune,
  author =              {Hune, Thomas},
  title =               {Analyzing real-time systems: theory and tools},
  year =                {2001},
  school =              {University of Aarhus, Denmark},
}
[KM01] Jarkko Kari and Cristopher Moore. Rectangles and Squares Recognized by Two-dimensional Automata. In STACS'01, Lecture Notes in Computer Science 2010, pages 396-406. Springer-Verlag, February 2001. 
@inproceedings{stacs2001-KM,
  author =              {Kari, Jarkko and Moore, Cristopher},
  title =               {Rectangles and Squares Recognized by Two-dimensional
                         Automata},
  editor =              {Ferreira, Afonso and Reichel, Horst},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'01)},
  acronym =             {{STACS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2010},
  pages =               {396-406},
  year =                {2001},
  month =               feb,
}
[KPV01] Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. Extended Temporal Logic Revisited. In CONCUR'01, Lecture Notes in Computer Science 2154, pages 519-535. Springer-Verlag, August 2001. 
@inproceedings{concur2001-KPV,
  author =              {Kupferman, Orna and Piterman, Nir and Vardi, Moshe
                         Y.},
  title =               {Extended Temporal Logic Revisited},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2154},
  pages =               {519-535},
  year =                {2001},
  month =               aug,
}
[KV01] Orna Kupferman and Moshe Y. Vardi. Model Checking of Safety Properties. Formal Methods in System Design 19(3):291-314. Kluwer Academic, November 2001. 
@article{fmsd19(3)-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Model Checking of Safety Properties},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {19},
  number =              {3},
  pages =               {291-314},
  year =                {2001},
  month =               nov,
}
[KV01] Orna Kupferman and Moshe Y. Vardi. Synthesizing Distributed Systems. In LICS'01, pages 389-398. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Synthesizing Distributed Systems},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {389-398},
  year =                {2001},
  month =               jun,
  doi =                 {10.1109/LICS.2001.932514},
}
[KVW01] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module Checking. Information and Computation 164(2):322-344. Academic Press, January 2001. 
@article{icomp164(2)-KVW,
  author =              {Kupferman, Orna and Vardi, Moshe Y. and Wolper,
                         Pierre},
  title =               {Module Checking},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {164},
  number =              {2},
  pages =               {322-344},
  year =                {2001},
  month =               jan,
}
[La01] Salvatore La Torre. Verification of Reactive Systems and Decision Problems in Temporal Logics. PhD thesis, University of Pennsylvania, 2001. 
@phdthesis{phd-latorre,
  author =              {La{~}Torre, Salvatore},
  title =               {Verification of Reactive Systems and Decision
                         Problems in Temporal Logics},
  year =                {2001},
  school =              {University of Pennsylvania},
}
[LBB+01] Kim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, and Judi Romijn. As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In CAV'01, Lecture Notes in Computer Science 2102, pages 493-505. Springer-Verlag, July 2001. 
@inproceedings{cav2001-LBBFHPR,
  author =              {Larsen, Kim Guldstrand and Behrmann, Gerd and
                         Brinksma, Ed and Fehnker, Ansgar and Hune, Thomas
                         and Pettersson, Paul and Romijn, Judi},
  title =               {As~Cheap as Possible: Efficient Cost-Optimal
                         Reachability for Priced Timed Automata},
  editor =              {Berry, G{\'e}rard and Comon, Hubert and Finkel,
                         Alain},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2102},
  pages =               {493-505},
  year =                {2001},
  month =               jul,
  doi =                 {10.1007/3-540-44585-4_47},
}
[LN01] Salvatore La Torre and Margherita Napoli. Timed tree automata with an application to temporal logic. Acta Informatica 38(2):89-116. Springer-Verlag, 2001. 
@article{acta38(2)-LN,
  author =              {La{~}Torre, Salvatore and Napoli, Margherita},
  title =               {Timed tree automata with an application to temporal
                         logic},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {38},
  number =              {2},
  pages =               {89-116},
  year =                {2001},
}
[Lod01] Christof Löding. Efficient minimization of deterministic weak ω-automata. Information Processing Letters 79(3):105-109. Elsevier, July 2001. 
@article{ipl79(3)-Lod,
  author =              {L{\"o}ding, Christof},
  title =               {Efficient minimization of deterministic weak
                         {\(\omega\)}-automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {79},
  number =              {3},
  pages =               {105-109},
  year =                {2001},
  month =               jul,
}
[LS01] Jan Lunze and Jochen Schröder. State observation and diagnosis of discrete-event systems described by stochastic automata. Discrete Event Dynamic Systems 11(4):319-369. Kluwer Academic, October 2001. 
@article{deds11(4)-LS,
  author =              {Lunze, Jan and Schr{\"o}der, Jochen},
  title =               {State observation and diagnosis of discrete-event
                         systems described by stochastic automata},
  publisher =           {Kluwer Academic},
  journal =             {Discrete Event Dynamic Systems},
  volume =              {11},
  number =              {4},
  pages =               {319-369},
  year =                {2001},
  month =               oct,
  doi =                 {10.1023/A:1011273108731},
}
[LSW01] Carsten Lutz, Ulrike Sattler, and Frank Wolter. Modal Logic and the Two-Variable Fragment. In CSL'01, Lecture Notes in Computer Science 2142, pages 247-261. Springer-Verlag, September 2001. 
@inproceedings{csl2001-LSW,
  author =              {Lutz, Carsten and Sattler, Ulrike and Wolter, Frank},
  title =               {Modal Logic and the Two-Variable Fragment},
  editor =              {Fribourg, Laurent},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'01)},
  acronym =             {{CSL}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2142},
  pages =               {247-261},
  year =                {2001},
  month =               sep,
}
[Pan01] Paritosh K. Pandya. Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. In RT-TOOLS'01. August 2001. 
@inproceedings{rttools2001-Pan,
  author =              {Pandya, Paritosh K.},
  title =               {Specifying and deciding quantified discrete-time
                         duration calculus formulae using {DCVALID}},
  editor =              {Pettersson, Paul and Yovine, Sergio},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on {R}eal-Time
                         {T}ools ({RT-TOOLS}'01)},
  acronym =             {{RT-TOOLS}'01},
  year =                {2001},
  month =               aug,
}
[Pin01] Jean-Éric Pin. Logic on Words. In Gheorghe Păun, Grzegorz Rozenberg, and Arto Salomaa (eds.), Current Trends in Theoretical Computer Science: Entering the 21th Century. World Scientific, 2001. 
@incollection{CTTCS2001-Pin,
  author =              {Pin, Jean-{\'E}ric},
  title =               {Logic on Words},
  editor =              {P{\u a}un, Gheorghe and Rozenberg, Grzegorz and
                         Salomaa, Arto},
  booktitle =           {Current Trends in Theoretical Computer Science:
                         Entering the 21th Century},
  publisher =           {World Scientific},
  pages =               {254-273},
  year =                {2001},
}
[PV01] Nir Piterman and Moshe Y. Vardi. From Bidirectionality to Alternation. In MFCS'01, Lecture Notes in Computer Science 2136, pages 598-610. Springer-Verlag, August 2001. 
@inproceedings{mfcs2001-PV,
  author =              {Piterman, Nir and Vardi, Moshe Y.},
  title =               {From Bidirectionality to Alternation},
  editor =              {Sgall, Ji{\v r}{\'\i} and Pultr, Ales and Kolman,
                         Petr},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'01)},
  acronym =             {{MFCS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2136},
  pages =               {598-610},
  year =                {2001},
  month =               aug,
}
[Rey01] Mark Reynolds. An Axiomatization of Full Computation Tree Logic. Journal of Symbolic Logic 66(3):1011-1057. Association for Symbolic Logic, September 2001. 
@article{jsl66(3)-Rey,
  author =              {Reynolds, Mark},
  title =               {An Axiomatization of Full Computation Tree Logic},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {66},
  number =              {3},
  pages =               {1011-1057},
  year =                {2001},
  month =               sep,
}
[RG01] Muriel Roger and Jean Goubault-Larrecq. Log Auditing through Model-Checking. In CSFW'01, pages 220-236. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{csfw2001-RG,
  author =              {Roger, Muriel and Goubault{-}Larrecq, Jean},
  title =               {Log Auditing through Model-Checking},
  booktitle =           {{P}roceedings of the 14th {IEEE} {C}omputer
                         {S}cience {F}oundations {W}orkshop ({CSFW}'01)},
  acronym =             {{CSFW}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {220-236},
  year =                {2001},
  month =               jun,
}
[RM01] Alexander Rabinovich and Shahar Maoz. An Infinite Hierarchy of Temporal Logics over Branching Time. Information and Computation 171(2):306-332. Academic Press, December 2001. 
@article{icomp171(2)-RM,
  author =              {Rabinovich, Alexander and Maoz, Shahar},
  title =               {An Infinite Hierarchy of Temporal Logics over
                         Branching Time},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {171},
  number =              {2},
  pages =               {306-332},
  year =                {2001},
  month =               dec,
}
[RT01] Michaël Rusinowitch and Mathieu Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. Research Report 4134, LORIA, Nancy, France, March 2001. 
@techreport{inria4134-RT,
  author =              {Rusinowitch, Micha{\"e}l and Turuani, Mathieu},
  title =               {Protocol Insecurity with Finite Number of Sessions
                         is {NP}-complete},
  number =              {4134},
  year =                {2001},
  month =               mar,
  institution =         {LORIA, Nancy, France},
  type =                {Research Report},
}
[Ruf01] Jürgen Ruf. RAVEN: Real-Time Analyzing and Verification Environment. Journal of Universal Computer Science 7(1):89-104. Know-Center, Technische Universität Graz, Austria, January 2001. 
@article{jucs7(1)-Ruf,
  author =              {Ruf, J{\"u}rgen},
  title =               {{RAVEN}: {R}eal-Time Analyzing and Verification
                         Environment},
  publisher =           {Know-Center, Technische Universit{\"a}t Graz,
                         Austria},
  journal =             {Journal of Universal Computer Science},
  volume =              {7},
  number =              {1},
  pages =               {89-104},
  year =                {2001},
  month =               jan,
}
[Rut01] Éric Rutten. A Framework for Using Discrete Control Synthesis in Safe Robotic Programming and Teleoperation. In ICRA'01, pages 4104-4109. IEEE Comp. Soc. Press, May 2001. 
@inproceedings{icra2001-Rut,
  author =              {Rutten, {\'E}ric},
  title =               {A Framework for Using Discrete Control Synthesis in
                         Safe Robotic Programming and Teleoperation},
  booktitle =           {{P}roceedings of the 2001 {IEEE} {I}nternational
                         {C}onference on {R}obotics and {A}utomation
                         ({ICRA}'01)},
  acronym =             {{ICRA}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {4104-4109},
  year =                {2001},
  month =               may,
}
[Sch01] Philippe Schnoebelen. Spécification et Vérification des Systèmes Concurrents. Mémoire d'habilitation, Lab. Spécification & Vérification, ENS Cachan, France, October 2001. 
@phdthesis{hab-schnoebelen,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {Sp{\'e}cification et V{\'e}rification des
                         Syst{\`e}mes Concurrents},
  year =                {2001},
  month =               oct,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {M\'emoire d'habilitation},
}
[SJ01] Zdeněk Sawa and Petr Jančar. P-hardness of Equivalence Testing on Finite State Processes. In SOFSEM'01, Lecture Notes in Computer Science 2234, pages 326-335. Springer-Verlag, November 2001. 
@inproceedings{sofsem2001-SJ,
  author =              {Sawa, Zden{\v{e}}k and Jan{\v c}ar, Petr},
  title =               {{P}-hardness of Equivalence Testing on Finite State
                         Processes},
  editor =              {Pacholski, Leszek and Ruzicka, Peter},
  booktitle =           {{P}roceedings of the 28th {C}onference on {C}urrent
                         {T}rends in {T}heory and {P}ractice of {I}nformatics
                         ({SOFSEM}'01)},
  acronym =             {{SOFSEM}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2234},
  pages =               {326-335},
  year =                {2001},
  month =               nov,
}
[SSS+01] Hiroshi Sakamoto, Shinichi Shimozono, Ayumi Shinohara, and Masayuki Takeda. On the Minimization Problem of Text Compression Scheme by a Reduced Grammar Transform. Technical Report 195, Department of Informatics, Kyushu University, Japan, August 2001. 
@techreport{kyushu-TR195,
  author =              {Sakamoto, Hiroshi and Shimozono, Shinichi and
                         Shinohara, Ayumi and Takeda, Masayuki},
  title =               {On the Minimization Problem of Text Compression
                         Scheme by a Reduced Grammar Transform},
  number =              {195},
  year =                {2001},
  month =               aug,
  institution =         {Department of Informatics, Kyushu University, Japan},
  type =                {Technical Report},
}
[SVD01] Jan Springintveld, Frits Vaandrager, and Pedro R. D'Argenio. Testing timed automata. Theoretical Computer Science 254(1-2):225-257. Elsevier, March 2001. 
@article{tcs254(1-2)-SVD,
  author =              {Springintveld, Jan and Vaandrager, Frits and
                         D{'}Argenio, Pedro R.},
  title =               {Testing timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {254},
  number =              {1-2},
  pages =               {225-257},
  year =                {2001},
  month =               mar,
  doi =                 {10.1016/S0304-3975(99)00134-6},
}
[Tan01] Till Tantau. A Note on the Complexity of the Reachability Problem for Tournaments. Research Report 01-092, Electronic Colloquium on Computational Complexity, 2001. 
@techreport{eccc2001-Tan,
  author =              {Tantau, Till},
  title =               {A Note on the Complexity of the Reachability Problem
                         for Tournaments},
  number =              {01-092},
  year =                {2001},
  institution =         {Electronic Colloquium on Computational Complexity},
  type =                {Research Report},
}
[TY01] Stavros Tripakis and Sergio Yovine. Timing Analysis and Code Generation of Vehicle Control Software using Taxys. In RV'01, Electronic Notes in Theoretical Computer Science 55(2), pages 277-286. Elsevier, July 2001. 
@inproceedings{rv2001-TY,
  author =              {Tripakis, Stavros and Yovine, Sergio},
  title =               {Timing Analysis and Code Generation of Vehicle
                         Control Software using {T}axys},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'01)},
  acronym =             {{RV}'01},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {55},
  number =              {2},
  pages =               {277-286},
  year =                {2001},
  month =               jul,
}
[TY01] Stavros Tripakis and Sergio Yovine. Analysis of Timed Systems Using Time-Abstracting Bisimulations. Formal Methods in System Design 18(1):25-68. Kluwer Academic, January 2001. 
@article{fmsd18(1)-TY,
  author =              {Tripakis, Stavros and Yovine, Sergio},
  title =               {Analysis of Timed Systems Using Time-Abstracting
                         Bisimulations},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {18},
  number =              {1},
  pages =               {25-68},
  year =                {2001},
  month =               jan,
  doi =                 {10.1023/A:1008734703554},
}
[Var01] Moshe Y. Vardi. Branching versus Linear Time: the Final Showdown. In TACAS'01, Lecture Notes in Computer Science 2031, pages 1-22. Springer-Verlag, April 2001. 
@inproceedings{tacas2001-Var,
  author =              {Vardi, Moshe Y.},
  title =               {Branching versus Linear Time: the Final Showdown},
  editor =              {Margaria, Tiziana and Yi, Wang},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'01)},
  acronym =             {{TACAS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2031},
  pages =               {1-22},
  year =                {2001},
  month =               apr,
}
[Vin01] Aymeric Vincent. Synthèse de contrôleurs et stratégies gagnantes dans les jeux de parité. In MSR'01, pages 87-98. Hermès, October 2001. 
@inproceedings{msr2001-Vin,
  author =              {Vincent, Aymeric},
  title =               {Synth{\`e}se de contr{\^o}leurs et strat{\'e}gies
                         gagnantes dans les jeux de parit{\'e}},
  booktitle =           {{A}ctes du 3{\`e}me {C}olloque {F}rancophone sur la
                         {M}od{\'e}lisation des {S}yst{\`e}mes r{\'e}actifs
                         ({MSR}'01)},
  acronym =             {{MSR}'01},
  publisher =           {Herm{\`e}s},
  pages =               {87-98},
  year =                {2001},
  month =               oct,
}
[Wal01] Dan S. Wallach. Copy Protection Technology is Doomed. IEEE Computer 34(10):48-49. IEEE Comp. Soc. Press, October 2001. 
@article{ieeecomp34(10)-Wal,
  author =              {Wallach, Dan S.},
  title =               {Copy Protection Technology is Doomed},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Computer},
  volume =              {34},
  number =              {10},
  pages =               {48-49},
  year =                {2001},
  month =               oct,
}
[Wan01] Farn Wang. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In FORTE'01, IFIP Conference Proceedings 197, pages 235-250. Chapman & Hall, August 2001. 
@inproceedings{forte2001-Wan,
  author =              {Wang, Farn},
  title =               {Symbolic Verification of Complex Real-Time Systems
                         with Clock-Restriction Diagram},
  editor =              {Kim, Myungchul and Chin, Byoungmoon and Kang,
                         Sungwon and Lee, Danhyung},
  booktitle =           {{P}roceedings of the 21st {IFIP} {TC6/WG6.1}
                         {I}nternational {C}onference on {F}ormal
                         {T}echniques for {N}etworked and {D}istributed
                         {S}ystems ({FORTE}'01)},
  acronym =             {{FORTE}'01},
  publisher =           {Chapman \& Hall},
  series =              {IFIP Conference Proceedings},
  volume =              {197},
  pages =               {235-250},
  year =                {2001},
  month =               aug,
}
[Wil01] Thomas Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bulletin of the Belgian Mathematical Society – Simon Stevin 8(2):359-391. Belgian Mathematical Society, 2001. 
@article{bbms8(2)-Wil,
  author =              {Wilke, Thomas},
  title =               {Alternating tree automata, parity games, and modal
                         {{\(\mu\)}}-calculus},
  publisher =           {Belgian Mathematical Society},
  journal =             {Bulletin of the Belgian Mathematical Society~--
                         Simon Stevin},
  volume =              {8},
  number =              {2},
  pages =               {359-391},
  year =                {2001},
}
List of authors