1997
[ABK+97] Eugene Asarin, Marius Bozga, Alain Kerbrat, Oded Maler, Amir Pnueli, and Anne Rasse. Data-Structures for the Verification of Timed Automata. In HART'97, Lecture Notes in Computer Science 1201, pages 346-360. Springer-Verlag, March 1997. 
@inproceedings{hart1997-ABKMPR,
  author =              {Asarin, Eugene and Bozga, Marius and Kerbrat, Alain
                         and Maler, Oded and Pnueli, Amir and Rasse, Anne},
  title =               {Data-Structures for the Verification of Timed
                         Automata},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {346-360},
  year =                {1997},
  month =               mar,
}
[ABO97] Eric Allender, Robert Beals, and Mitsunori Ogihara. The Complexity of Matrix Rank and Feasible Systems of Linear Equations. Technical Report 97-40, Rutgers University, New Jersey, USA, September 1997. 
@techreport{TR-DIMACS9740,
  author =              {Allender, Eric and Beals, Robert and Ogihara,
                         Mitsunori},
  title =               {The Complexity of Matrix Rank and Feasible Systems
                         of Linear Equations},
  number =              {97-40},
  year =                {1997},
  month =               sep,
  institution =         {Rutgers University, New Jersey, USA},
}
[ACH97] Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. Computing Accumulated Delays in Real Time Systems. Formal Methods in System Design 11(2):137-155. Kluwer Academic, August 1997. 
@article{fmsd11(2)-ACH,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Henzinger,
                         Thomas A.},
  title =               {Computing Accumulated Delays in Real Time Systems},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {11},
  number =              {2},
  pages =               {137-155},
  year =                {1997},
  month =               aug,
}
[ACM97] Eugene Asarin, Paul Caspi, and Oded Maler. A Kleene Theorem for Timed Automata. In LICS'97, pages 160-171. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{lics1997-ACM,
  author =              {Asarin, Eugene and Caspi, Paul and Maler, Oded},
  title =               {A {K}leene Theorem for Timed Automata},
  booktitle =           {{P}roceedings of the 12th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'97)},
  acronym =             {{LICS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {160-171},
  year =                {1997},
  month =               jun,
}
[AHK97] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. In FOCS'97, pages 100-109. IEEE Comp. Soc. Press, October 1997. 
@inproceedings{focs1997-AHK,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Temporal Logic},
  booktitle =           {{P}roceedings of the 38th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'97)},
  acronym =             {{FOCS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {100-109},
  year =                {1997},
  month =               oct,
}
[All97] Eric Allender. Making Computation Count: Arithmetic Circuits in the Nineties. SIGACT News 28(4):2-15. ACM Press, December 1997. 
@article{sigact-news28(4)-All,
  author =              {Allender, Eric},
  title =               {Making Computation Count: Arithmetic Circuits in the
                         Nineties},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {28},
  number =              {4},
  pages =               {2-15},
  year =                {1997},
  month =               dec,
}
[BDL+97] Joshua Berman, Arthur Drisko, François Lemieux, Cristopher Moore, and Denis Thérien. Circuit and Expressions with Non-Associative Gates. In CoCo'97, pages 193-203. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{coco1997-BDLMT,
  author =              {Berman, Joshua and Drisko, Arthur and Lemieux,
                         Fran{\c c}ois and Moore, Cristopher and Th{\'e}rien,
                         Denis},
  title =               {Circuit and Expressions with Non-Associative Gates},
  booktitle =           {{P}roceedings of the 12th {A}nnual {IEEE}
                         {C}onference on {C}omputational {C}omplexity
                         ({CoCo}'97)},
  acronym =             {{CoCo}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {193-203},
  year =                {1997},
  month =               jun,
}
[BLM+97] David A. Mix Barrington, Chi-Jen Lu, Peter Bro Miltersen, and Sven Skyum. On Uniformity Within NC1. Research Report 97-044, Electronic Colloquium on Computational Complexity, September 1997. 
@techreport{eccc1997-BLMS,
  author =              {Barrington, David A. Mix and Lu, Chi-Jen and
                         Miltersen, Peter Bro and Skyum, Sven},
  title =               {On Uniformity Within {{\(\mathit{NC}^1\)}}},
  number =              {97-044},
  year =                {1997},
  month =               sep,
  institution =         {Electronic Colloquium on Computational Complexity},
  type =                {Research Report},
}
[BMP+97] Martin Beaudry, Pierre McKenzie, Pierre Péladeau, and Denis Thérien. Finite Monoids: From Word to Circuit Evaluation. SIAM Journal on Computing 26(1):138-152. Society for Industrial and Applied Math., February 1997. 
@article{siamcomp26(1)-BMPT,
  author =              {Beaudry, Martin and McKenzie, Pierre and
                         P{\'e}ladeau, Pierre and Th{\'e}rien, Denis},
  title =               {Finite Monoids: From Word to Circuit Evaluation},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {26},
  number =              {1},
  pages =               {138-152},
  year =                {1997},
  month =               feb,
}
[BTY97] Ahmed Bouajjani, Stavros Tripakis, and Sergio Yovine. On-the-Fly Symbolic Model Checking for Real-Time Systems. In RTSS'97, pages 25-35. IEEE Comp. Soc. Press, December 1997. 
@inproceedings{rts1997-BTY,
  author =              {Bouajjani, Ahmed and Tripakis, Stavros and Yovine,
                         Sergio},
  title =               {On-the-Fly Symbolic Model Checking for Real-Time
                         Systems},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'97)},
  acronym =             {{RTSS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {25-35},
  year =                {1997},
  month =               dec,
}
[Bus97] Samuel R. Buss. ALOGTIME Algorithm for Tree Isomorphism, Comparison, and Canonization. In KGC'97, Lecture Notes in Computer Science 1289, pages 18-33. Springer-Verlag, August 1997. 
@inproceedings{kgc1997-Bus,
  author =              {Buss, Samuel R.},
  title =               {{ALOGTIME} Algorithm for Tree Isomorphism,
                         Comparison, and Canonization},
  editor =              {Gottlob, Georg and Leitsch, Alexander and Mundici,
                         Daniele},
  booktitle =           {{P}roceedings of the 5th {K}urt {G}{\"o}del
                         {C}olloquium ({KGC}'97)},
  acronym =             {{KGC}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1289},
  pages =               {18-33},
  year =                {1997},
  month =               aug,
}
[CGH97] Edmund M. Clarke, Orna Grumberg, and Kiyoharu Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design 10(1):47-71. Kluwer Academic, February 1997. 
@article{fmsd10(1)-CGH,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Hamaguchi,
                         Kiyoharu},
  title =               {Another Look at {LTL} Model Checking},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {10},
  number =              {1},
  pages =               {47-71},
  year =                {1997},
  month =               feb,
}
[CJ97] Hubert Comon and Florent Jacquemard. Ground Reducibility is EXPTIME-Complete. In LICS'97, pages 26-34. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{lics1997-CJ,
  author =              {Comon, Hubert and Jacquemard, Florent},
  title =               {Ground Reducibility is {EXPTIME}-Complete},
  booktitle =           {{P}roceedings of the 12th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'97)},
  acronym =             {{LICS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {26-34},
  year =                {1997},
  month =               jun,
}
[CM97] Stephen A. Cook and David G. Mitchell. Finding Hard Instances of the Satisfiability Problem: A Survey. In Ding-zhu Du, Jun Gu, and Panos M. Pardalos (eds.), Satisfiability Problem: Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 35, pages 1-17. American Mathematical Society, October 1997. 
@incollection{dimacs35-CM,
  author =              {Cook, Stephen A. and Mitchell, David G.},
  title =               {Finding Hard Instances of the Satisfiability
                         Problem: A Survey},
  editor =              {Du, Ding-zhu and Gu, Jun and Pardalos, Panos M.},
  booktitle =           {Satisfiability Problem: Theory and Applications},
  publisher =           {American Mathematical Society},
  series =              {DIMACS Series in Discrete Mathematics and
                         Theoretical Computer Science},
  volume =              {35},
  pages =               {1-17},
  year =                {1997},
  month =               oct,
}
[Cou97] Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In Grzegorz Rozenberg (eds.), Handbook of Graph Grammars. World Scientific, 1997. 
@incollection{handbookGG1997-Cou,
  author =              {Courcelle, Bruno},
  title =               {The expression of graph properties and graph
                         transformations in monadic second-order logic},
  editor =              {Rozenberg, Grzegorz},
  booktitle =           {Handbook of Graph Grammars},
  publisher =           {World Scientific},
  pages =               {313-400},
  year =                {1997},
}
[CP97] Yi-Liang Chen and Gregory Provan. Modeling and Diagnosis of Timed Discrete Event Systems – A Factory Automation Example. In ACC'97, pages 31-36. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{acc1997-CP,
  author =              {Chen, Yi-Liang and Provan, Gregory},
  title =               {Modeling and Diagnosis of Timed Discrete Event
                         Systems~-- A~Factory Automation Example},
  booktitle =           {Proceedings of the 1997 American Control Conference
                         ({ACC}'97)},
  acronym =             {{ACC}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {31-36},
  year =                {1997},
  month =               jun,
  doi =                 {10.1109/ACC.1997.611749},
}
[CTL97] Christian Collberg, Clark Thomborson, and Douglas Low. A Taxonomy of Obfuscating Transformations. Technical Report 148, Department of Computer Science, University of Auckland, New Zealand, July 1997. 
@techreport{tr148-CTL,
  author =              {Collberg, Christian and Thomborson, Clark and Low,
                         Douglas},
  title =               {A Taxonomy of Obfuscating Transformations},
  number =              {148},
  year =                {1997},
  month =               jul,
  institution =         {Department of Computer Science, University of
                         Auckland, New Zealand},
  type =                {Technical Report},
}
[DJW97] Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How Much Memory is Needed to Win Infinite Games. In LICS'97, pages 99-110. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{lics1997-DJW,
  author =              {Dziembowski, Stefan and Jurdzi{\'n}ski, Marcin and
                         Walukiewicz, Igor},
  title =               {How Much Memory is Needed to Win Infinite Games},
  booktitle =           {{P}roceedings of the 12th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'97)},
  acronym =             {{LICS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {99-110},
  year =                {1997},
  month =               jun,
}
[vEB97] Peter van Emde Boas. The convenience of tiling. In Andrea Sorbi (eds.), Complexity, Logic and Recursion Theory, Lecture Notes in Pure and Applied Mathematics 187, pages 331-363. Marcel Dekker Inc., February 1997. 
@incollection{lnpam187-Emd,
  author =              {van Emde Boas, Peter},
  title =               {The convenience of tiling},
  editor =              {Sorbi, Andrea},
  booktitle =           {Complexity, Logic and Recursion Theory},
  publisher =           {Marcel Dekker Inc.},
  series =              {Lecture Notes in Pure and Applied Mathematics},
  volume =              {187},
  pages =               {331-363},
  year =                {1997},
  month =               feb,
}
[ET97] E. Allen Emerson and Richard J. Trefler. Generalized Quantitative Temporal Reasoning. In TAPSOFT'97, Lecture Notes in Computer Science 1214, pages 189-200. Springer-Verlag, April 1997. 
@inproceedings{tapsoft1997-ET,
  author =              {Emerson, E. Allen and Trefler, Richard J.},
  title =               {Generalized Quantitative Temporal Reasoning},
  editor =              {Bidoit, Michel and Dauchet, Max},
  booktitle =           {{P}roceedings of the 7th {I}nternational {J}oint
                         {C}onference {CAAP}{\slash}{FASE} on {T}heory and
                         {P}ractice of {S}oftware {D}evelopment
                         ({TAPSOFT}'97)},
  acronym =             {{TAPSOFT}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1214},
  pages =               {189-200},
  year =                {1997},
  month =               apr,
}
[EVW97] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. In LICS'97, pages 228-235. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{lics1997-EVW,
  author =              {Etessami, Kousha and Vardi, Moshe Y. and Wilke,
                         Thomas},
  title =               {First-Order Logic with Two Variables and Unary
                         Temporal Logic},
  booktitle =           {{P}roceedings of the 12th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'97)},
  acronym =             {{LICS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {228-235},
  year =                {1997},
  month =               jun,
}
[FV97] Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer-Verlag, 1997. 
@book{CMDP-FV97,
  author =              {Filar, Jerzy and Vrieze, Koos},
  title =               {Competitive {M}arkov decision processes},
  publisher =           {Springer-Verlag},
  year =                {1997},
}
[GHJ97] Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan. Robust Timed Automata. In HART'97, Lecture Notes in Computer Science 1201, pages 331-345. Springer-Verlag, March 1997. 
@inproceedings{hart1997-GHJ,
  author =              {Gupta, Vineet and Henzinger, Thomas A. and
                         Jagadeesan, Radha},
  title =               {Robust Timed Automata},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {331-345},
  year =                {1997},
  month =               mar,
}
[GR97] Dora Giammarresi and Antonio Restivo. Two-dimensional Languages. In Grzegorz Rozenberg and Arto Salomaa (eds.), Handbook of Formal Languages. Springer-Verlag, 1997. 
@incollection{HFL1997(3)-GR,
  author =              {Giammarresi, Dora and Restivo, Antonio},
  title =               {Two-dimensional Languages},
  editor =              {Rozenberg, Grzegorz and Salomaa, Arto},
  booktitle =           {Handbook of Formal Languages},
  publisher =           {Springer-Verlag},
  volume =              {3},
  pages =               {215-267},
  year =                {1997},
}
[HHW97] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A Model-Checker for Hybrid Systems. International Journal on Software Tools for Technology Transfer 1(1-2):110-122. Springer-Verlag, October 1997. 
@article{sttt1(1-2)-HHW,
  author =              {Henzinger, Thomas A. and Ho, Pei-Hsin and
                         Wong{-}Toi, Howard},
  title =               {{H}y{T}ech: A~Model-Checker for Hybrid Systems},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {1},
  number =              {1-2},
  pages =               {110-122},
  year =                {1997},
  month =               oct,
}
[HK97] Thomas A. Henzinger and Orna Kupferman. From Quantity to Quality. In HART'97, Lecture Notes in Computer Science 1201, pages 48-62. Springer-Verlag, March 1997. 
@inproceedings{hart1997-HK,
  author =              {Henzinger, Thomas A. and Kupferman, Orna},
  title =               {From Quantity to Quality},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {48-62},
  year =                {1997},
  month =               mar,
}
[Hol97] Gerard J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5):279-295. IEEE Comp. Soc. Press, May 1997. 
@article{tse23(5)-Hol,
  author =              {Holzmann, Gerard J.},
  title =               {The Model Checker {SPIN}},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Software Engineering},
  volume =              {23},
  number =              {5},
  pages =               {279-295},
  year =                {1997},
  month =               may,
}
[HSL+97] Klaus Havelund, Arne Skou, Kim Guldstrand Larsen, and Kristian Lund. Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. In RTSS'97, pages 2-13. IEEE Comp. Soc. Press, December 1997. 
@inproceedings{rts1997-HSLL,
  author =              {Havelund, Klaus and Skou, Arne and Larsen, Kim
                         Guldstrand and Lund, Kristian},
  title =               {Formal Modelling and Analysis of an
                         Audio{\slash}Video Protocol: An Industrial Case
                         Study Using {U}ppaal},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'97)},
  acronym =             {{RTSS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {2-13},
  year =                {1997},
  month =               dec,
}
[HW97] Harald Hempel and Gerd Wechsung. The Operators min and max on the Polynomial Hierarchy. Technical Report TR97-025, Electronic Colloquium on Computational Complexity, May 1997. 
@techreport{ECCC-TR97-025-HW,
  author =              {Hempel, Harald and Wechsung, Gerd},
  title =               {The Operators min and max on the Polynomial
                         Hierarchy},
  number =              {TR97-025},
  year =                {1997},
  month =               may,
  institution =         {Electronic Colloquium on Computational Complexity},
  type =                {Technical Report},
}
[JGB97] Predrag Janičić, Ian Green, and Alan Bundy. A Comparison of Decision Procedures in Presburger Arithmetic. In LIRA'97, pages 91-101. September 1997. 
@inproceedings{lira1997-JGB,
  author =              {Jani{\v c}i{\'c}, Predrag and Green, Ian and Bundy,
                         Alan},
  title =               {A Comparison of Decision Procedures in {P}resburger
                         Arithmetic},
  editor =              {To{\v s}i{\'c}, Ratko and Budimac, Zoran},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {L}ogic and {C}omputer {S}cience
                         ({LIRA}'97)},
  acronym =             {{LIRA}'97},
  pages =               {91-101},
  year =                {1997},
  month =               sep,
}
[JLM97] Birgit Jenner, Klaus-Jörn Lange, and Pierre McKenzie. Tree Isomorphism and Some Other Complete Problems for Deterministic Logspace. Technical Report 1059, DIRO, Université de Montréal, Canada, March 1997. 
@techreport{diro1-59-JLM,
  author =              {Jenner, Birgit and Lange, Klaus-J{\"o}rn and
                         McKenzie, Pierre},
  title =               {Tree Isomorphism and Some Other Complete Problems
                         for Deterministic Logspace},
  number =              {1059},
  year =                {1997},
  month =               mar,
  institution =         {DIRO, Universit{\'e} de Montr{\'e}al, Canada},
  type =                {Technical Report},
}
[Kai97] Roope Kaivola. Using Automata to Characterise Fixed Point Temporal Logics. PhD thesis, School of Informatics, University of Edinburgh, UK, July 1997. 
@phdthesis{phd-kaivola,
  author =              {Kaivola, Roope},
  title =               {Using Automata to Characterise Fixed Point Temporal
                         Logics},
  year =                {1997},
  month =               jul,
  school =              {School of Informatics, University of Edinburgh, UK},
  type =                {{PhD} thesis},
}
[KLL+97] Kåre J. Kristoffersen, François Laroussinie, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. In TAPSOFT'97, Lecture Notes in Computer Science 1214, pages 565-579. Springer-Verlag, April 1997. 
@inproceedings{tapsoft1997-KLLPY,
  author =              {Kristoffersen, K{\aa}re J. and Laroussinie, Fran{\c
                         c}ois and Larsen, Kim Guldstrand and Pettersson,
                         Paul and Yi, Wang},
  title =               {A Compositional Proof of a Real-Time Mutual
                         Exclusion Protocol},
  editor =              {Bidoit, Michel and Dauchet, Max},
  booktitle =           {{P}roceedings of the 7th {I}nternational {J}oint
                         {C}onference {CAAP}{\slash}{FASE} on {T}heory and
                         {P}ractice of {S}oftware {D}evelopment
                         ({TAPSOFT}'97)},
  acronym =             {{TAPSOFT}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1214},
  pages =               {565-579},
  year =                {1997},
  month =               apr,
}
[KRS97] Marek Karpinski, Wojciech Rytter, and Ayumi Shinohara. An Efficient Pattern-Matching Algorithm for Strings with Short Description. Nordic Journal of Computing 4(2):172-186. Publishing Association Nordic Journal of Computing, 1997. 
@article{njc4(2)-KRS,
  author =              {Karpinski, Marek and Rytter, Wojciech and Shinohara,
                         Ayumi},
  title =               {An Efficient Pattern-Matching Algorithm for Strings
                         with Short Description},
  publisher =           {Publishing Association Nordic Journal of Computing},
  journal =             {Nordic Journal of Computing},
  volume =              {4},
  number =              {2},
  pages =               {172-186},
  year =                {1997},
}
[KV97] Orna Kupferman and Moshe Y. Vardi. Weak Alternating Automata Are Not That Weak. In ISTCS'97, pages 147-158. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{istcs1997-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Weak Alternating Automata Are Not That Weak},
  booktitle =           {{P}roceedings of the 5th {I}srael {S}ymposium on
                         {T}heory of {C}omputing {S}ystems ({ISTCS}'97)},
  acronym =             {{ISTCS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {147-158},
  year =                {1997},
  month =               jun,
}
[KV97] Orna Kupferman and Moshe Y. Vardi. Module Checking Revisited. In CAV'97, Lecture Notes in Computer Science 1254, pages 36-47. Springer-Verlag, June 1997. 
@inproceedings{cav1997-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Module Checking Revisited},
  editor =              {Grumberg, Orna},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'97)},
  acronym =             {{CAV}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1254},
  pages =               {36-47},
  year =                {1997},
  month =               jun,
}
[LLP+97] Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Efficient verification of real-time systems: compact data structure and state-space reduction. In RTSS'97, pages 14-24. IEEE Comp. Soc. Press, December 1997. 
@inproceedings{rtss1997-LLPY,
  author =              {Larsen, Kim Guldstrand and Larsson, Fredrik and
                         Pettersson, Paul and Yi, Wang},
  title =               {Efficient verification of real-time systems: compact
                         data structure and state-space reduction},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'97)},
  acronym =             {{RTSS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {14-24},
  year =                {1997},
  month =               dec,
}
[LPY97] Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer 1(1-2):134-152. Springer-Verlag, October 1997. 
@article{sttt1(1-2)-LPY,
  author =              {Larsen, Kim Guldstrand and Pettersson, Paul and Yi,
                         Wang},
  title =               {{\textsc{Uppaal}} in a nutshell},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {1},
  number =              {1-2},
  pages =               {134-152},
  year =                {1997},
  month =               oct,
}
[MO97] Dieter van Melkebeek and Mitsunori Ogihara. Sparse Hard Sets for P. In Ding-zhu Du and Ker-I Ko (eds.), Advances in Algorithms, Languages and Complexity. Kluwer Academic, 1997. 
@incollection{AALC1997-MO,
  author =              {Melkebeek, Dieter van and Ogihara, Mitsunori},
  title =               {Sparse Hard Sets for~{P}},
  editor =              {Du, Ding-zhu and Ko, Ker-I},
  booktitle =           {Advances in Algorithms, Languages and Complexity},
  publisher =           {Kluwer Academic},
  pages =               {191-208},
  year =                {1997},
}
[MS97] Oded Maler and Ludwig Staiger. On Syntactic Congruences fpr ω-languages. Theoretical Computer Science 183(1):93-112. Elsevier, August 1997. 
@article{tcs183(1)-MS,
  author =              {Maler, Oded and Staiger, Ludwig},
  title =               {On Syntactic Congruences fpr {\(\omega\)}-languages},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {183},
  number =              {1},
  pages =               {93-112},
  year =                {1997},
  month =               aug,
}
[MST97] Masamichi Miyazaki, Ayumi Shinohara, and Masayuki Takeda. An Improved Pattern-Matching Algorithm for Strings in Terms of Straight-Line Programs. In CPM'97, Lecture Notes in Computer Science 1264, pages 1-11. Springer-Verlag, June 1997. 
@inproceedings{cpm1997-MST,
  author =              {Miyazaki, Masamichi and Shinohara, Ayumi and Takeda,
                         Masayuki},
  title =               {An Improved Pattern-Matching Algorithm for Strings
                         in Terms of Straight-Line Programs},
  booktitle =           {{P}roceedings of the 8th {A}nnual {S}ymposium on
                         {C}ombinatorial {P}attern {M}atching ({CPM}'97)},
  acronym =             {{CPM}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1264},
  pages =               {1-11},
  year =                {1997},
  month =               jun,
}
[Niw97] Damian Niwiński. Fixed point characterization of infinite behavior of finite-state systems. Theoretical Computer Science 189(1-2):1-69. Elsevier, December 1997. 
@article{tcs189(1-2)-Niw,
  author =              {Niwi{\'n}ski, Damian},
  title =               {Fixed point characterization of infinite behavior of
                         finite-state systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {189},
  number =              {1-2},
  pages =               {1-69},
  year =                {1997},
  month =               dec,
  doi =                 {10.1016/S0304-3975(97)00039-X},
}
[PI97] Sushant Patnaik and Neil Immerman. Dyn-FO: A Parallel, Dynamic Complexity Class. Journal of Computer and System Sciences 55(2):199-209. Academic Press, October 1997. 
@article{jcss55(2)-PI,
  author =              {Patnaik, Sushant and Immerman, Neil},
  title =               {Dyn-{FO}: A~Parallel, Dynamic Complexity Class},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {55},
  number =              {2},
  pages =               {199-209},
  year =                {1997},
  month =               oct,
  doi =                 {10.1006/jcss.1997.1520},
}
[PW97] Doron A. Peled and Thomas Wilke. Stutter-Invariant Temporal Properties are Expressible Without the Next-time Operator. Information Processing Letters 63(5):243-246. Elsevier, 1997. 
@article{ipl63(5)-PW,
  author =              {Peled, Doron A. and Wilke, Thomas},
  title =               {Stutter-Invariant Temporal Properties are
                         Expressible Without the Next-time Operator},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {63},
  number =              {5},
  pages =               {243-246},
  year =                {1997},
}
[RK97] Jürgen Ruf and Thomas Kropf. A New Algorithm for Discrete Timed Symbolic Model Checking. In HART'97, Lecture Notes in Computer Science 1201, pages 18-32. Springer-Verlag, March 1997. 
@inproceedings{hart1997-RK,
  author =              {Ruf, J{\"u}rgen and Kropf, {\relax Th}omas},
  title =               {A New Algorithm for Discrete Timed Symbolic Model
                         Checking},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {18-32},
  year =                {1997},
  month =               mar,
}
[Roh97] Scott Rohde. Alternating automata and the temporal logic of ordinals. PhD thesis, University of Illinois, 1997. 
@phdthesis{phd-rohde,
  author =              {Rohde, Scott},
  title =               {Alternating automata and the temporal logic of
                         ordinals},
  year =                {1997},
  school =              {University of Illinois},
}
[RS97] Jean-François Raskin and Pierre-Yves Schobbens. State Clock Logic: A Decidable Real-Time Logic. In HART'97, Lecture Notes in Computer Science 1201, pages 33-47. Springer-Verlag, March 1997. 
@inproceedings{hart1997-RS,
  author =              {Raskin, Jean-Fran{\c c}ois and Schobbens,
                         Pierre-Yves},
  title =               {State Clock Logic: A~Decidable Real-Time Logic},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {33-47},
  year =                {1997},
  month =               mar,
}
[Sip97] Michael Sipser. Introduction to the theory of computation. PWS Publishing Company, 1997. 
@book{Sip97-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {PWS Publishing Company},
  year =                {1997},
}
[Tak97] Masayuki Takeda. Pattern Maching Machine for Text Compressed Using Finite State Model. Technical Report DOI-TR-142, Dept. of Informatics, Kyushu University, Fukuoka, Japan, October 1997. 
@techreport{DOI-TR-142,
  author =              {Takeda, Masayuki},
  title =               {Pattern Maching Machine for Text Compressed Using
                         Finite State Model},
  number =              {DOI-TR-142},
  year =                {1997},
  month =               oct,
  institution =         {Dept. of Informatics, Kyushu University, Fukuoka,
                         Japan},
  type =                {Technical Report},
}
[Tho97] Wolfgang Thomas. Automata Theory on Tress and Partial Orders. In TAPSOFT'97, Lecture Notes in Computer Science 1214, pages 20-38. Springer-Verlag, April 1997. 
@inproceedings{tapsoft1997-Tho,
  author =              {Thomas, Wolfgang},
  title =               {Automata Theory on Tress and Partial Orders},
  editor =              {Bidoit, Michel and Dauchet, Max},
  booktitle =           {{P}roceedings of the 7th {I}nternational {J}oint
                         {C}onference {CAAP}{\slash}{FASE} on {T}heory and
                         {P}ractice of {S}oftware {D}evelopment
                         ({TAPSOFT}'97)},
  acronym =             {{TAPSOFT}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1214},
  pages =               {20-38},
  year =                {1997},
  month =               apr,
}
[Tho97] Wolfgang Thomas. Languages, Automata and Logics. In Grzegorz Rozenberg and Arto Salomaa (eds.), Handbook of Formal Languages. Springer-Verlag, 1997. 
@incollection{HFL1997(3)-Tho,
  author =              {Thomas, Wolfgang},
  title =               {Languages, Automata and Logics},
  editor =              {Rozenberg, Grzegorz and Salomaa, Arto},
  booktitle =           {Handbook of Formal Languages},
  publisher =           {Springer-Verlag},
  volume =              {3},
  pages =               {389-455},
  year =                {1997},
}
[Var97] Moshe Y. Vardi. Alternating Automata: Checking Truth and Validity for Temporal Logics. In CADE'97, Lecture Notes in Artificial Intelligence 1249, pages 191-206. Springer-Verlag, July 1997. 
@inproceedings{cade1997-Var,
  author =              {Vardi, Moshe Y.},
  title =               {Alternating Automata: Checking Truth and Validity
                         for Temporal Logics},
  editor =              {McCune, William},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {A}utomated {D}eduction ({CADE}'97)},
  acronym =             {{CADE}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {1249},
  pages =               {191-206},
  year =                {1997},
  month =               jul,
}
[Vea97] Margus Veanes. On Computational Complexity of Basic Decision Problems of Finite Tree Automata. Technical Report 133, Uppsala Programming Methodology and Artificial Intelligence Laboratory, Sweden, January 1997. 
@techreport{upmail-133-Vea,
  author =              {Veanes, Margus},
  title =               {On Computational Complexity of Basic Decision
                         Problems of Finite Tree Automata},
  number =              {133},
  year =                {1997},
  month =               jan,
  institution =         {Uppsala Programming Methodology and Artificial
                         Intelligence Laboratory, Sweden},
  type =                {Technical Report},
}
[Wei97] Volker Weispfenning. Complexity and Uhiformity of Elimination in Presburger Arithmetic. In ISSAC'97, pages 48-53. ACM Press, July 1997. 
@inproceedings{issac1997-Wei,
  author =              {Weispfenning, Volker},
  title =               {Complexity and Uhiformity of Elimination in
                         {P}resburger Arithmetic},
  editor =              {K{\"u}chlin, Wolfgang},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {S}ymbolic and {A}lgebraic
                         {C}omputation ({ISSAC}'97)},
  acronym =             {{ISSAC}'97},
  publisher =           {ACM Press},
  pages =               {48-53},
  year =                {1997},
  month =               jul,
}
[Yov97] Sergio Yovine. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer 1(1-2):123-133. Springer-Verlag, October 1997. 
@article{sttt1(1-2)-Yov,
  author =              {Yovine, Sergio},
  title =               {Kronos: A verification tool for real-time systems},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {1},
  number =              {1-2},
  pages =               {123-133},
  year =                {1997},
  month =               oct,
}
List of authors