% The Chicago Journal of Theoretical Computer Science, Volume 1995, Article 3
% Bibliography

cj9@article{cj95-03-1,
  author={B. Alpern and F. B. Schneider},
  title={Recognizing Safety and Liveness},
  journal={Distributed Computing},
  year={1987},
  volume={2},
  pages={117--126}
}

@article{cj95-03-2,
  author={B. Alpern and F. B. Schneider},
  title={Verifying Temporal Properties without Temporal Logic},
  journal={ACM Transactions on Programming Languages and Systems},
  year={1989},
  volume={11},
  number={1},
  pages={147--167},
  month={January}
}

@article{cj95-03-3,
  author={K. R. Apt and E.-R. Olderog},
  title={Proof Rules and Transformations Dealing with Fairness},
  journal={Science of Computer Programming},
  year={1983},
  volume={3},
  pages={65--100}
}

@article{cj95-03-4,
  author={K. R. Apt and A. Pnueli and J. Stavi},
  title={Fair termination revisited with delay},
  journal={Theoretical Computer Science},
  year={1984},
  volume={33},
  pages={65--84}
}

@article{cj95-03-5,
  title={Fair Termination with Cruel Schedulers},
  author={I. Dayan and D. Harel},
  journal={Fundamenta Informatica},
  year={1986},
  volume={9},
  pages={1--12}
}

@inproceedings{cj95-03-6,
  author={E. A. Emerson and C. S. Jutla},
  title={Complexity of Tree Automata and Logics of Programs},
  booktitle={Proceedings of the 29th Symposium on Foundations of
		  Computer Science},
  year={1988},
  pages={328--337},
  organization={Institute of Electrical and Electronics Engineers},
  address={Los Alamitos, CA}
}

@inproceedings{cj95-03-7,
  author={E. A. Emerson and C. S. Jutla},
  title={Tree automata, mu-calculus and determinacy},
  booktitle={Proceedings of the 32nd Symposium on Foundations of
		  Computer Science, San Juan, Puerto Rico},
  year={1991},
  pages={368--377},
  organization={Institute of Electrical and Electronics Engineers},
  address={Los Alamitos, CA}
}

@book{cj95-03-8,
  author={N. Francez},
  title={Fairness},
  publisher={Springer-Verlag},
  address={Berlin, Heidelberg},
  year={1986}
}

@inproceedings{cj95-03-9,
  author={N. Francez and D. Kozen},
  title={Generalized Fair Termination},
  booktitle={Proceedings of the 11th Symposium on Principles of
		  Programming Languages, Salt Lake City},
  year={1984},
  pages={46--53},
  organization={Association for Computing Machinery},
  month={January}
}

@article{cj95-03-10,
  author={O. Grumberg and N. Francez and J. A. {Ma\-kow\-sky} and
                  de Roever, W. P.},
  title={A proof rule for fair termination of guarded commands},
  journal={Information and Control},
  year={1985},
  volume={66},
  number={1/2},
  pages={83--102}
}

@inproceedings{cj95-03-11,
  author={Y. Gurevich and L. Harrington},
  title={Trees, automata, and games},
  booktitle={Proceedings of the 14th Symposium on Theory of Computing},
  pages={60--65},
  year={1982},
  organization={Association for Computing Machinery}
}

@inproceedings{cj95-03-12,
  author={B. Jonsson},
  title={Modular Verification of Asynchronous Networks},
  booktitle={Proceedings of the 6th Symposium on the Principles of 
			Distributed Computing},
  year={1987},
  pages={152--166},
  organization={Association for Computing Machinery}
}

@phdthesis{cj95-03-13,
  author={N. Klarlund},
  title={Progress Measures and Finite Arguments for  Infinite Computations},
  school={Cornell University},
  year={1990},
  month={August},
  note={Available as Technical Report TR-1153}
}

@techreport{cj95-03-14,
  author={N. Klarlund},
  title={Verification Conditions for $\omega$-automata and
		  Applications to Fairness},
  institution={Cornell University},
  year={1990},
  month={February},
  number={TR-1080}
}

@inproceedings{cj95-03-15,
  author={N. Klarlund},
  title={Liminf Progress Measures},
  booktitle={Mathematical Foundations of Programming Semantics, 7th
		  International Conference, March 1991},
  series={Lecture Notes in Computer Science},
  volume={598},
  year={1992},
  editor={S. Brookes and M. Main and A. Melton, A. and M. Mislove and
		  D. Schmidt},
  pages={477--491},
  publisher={Springer-Verlag},
  address={Berlin, Heidelberg}
}

@inproceedings{cj95-03-16,
  author={N. Klarlund},
  title={Progress Measures for Complementation of $\omega$-Automata
		  with Applications to Temporal Logic},
  booktitle={Proceedings of the 32nd Symposium on Foundations of
		  Computer Science, San Juan, Puerto Rico},
  year={1991},
  organization={Institute of Electrical and Electronics Engineers},
  address={Los Alamitos, CA},
  pages={358--367}
}

@inproceedings{cj95-03-17,
  author={N. Klarlund},
  title={Progress Measures and Stack Assertions for Fair Termination},
  booktitle={Proceedings of the 11th Symposium on Principles of Distributed
	Computing, Vancouver},
  year={1992},
  organization={Institute of Electrical and Electronics Engineers},
  address={Los Alamitos, CA},
  pages={229--240}
}

@inproceedings{cj95-03-18,
  author={N. Klarlund},
  title={The Limit View of Infinite Computations},
  booktitle={Proceedings CONCUR '94: Concurrency Theory},
  series={Lecture Notes in Computer Science},
  volume={836},
  pages={351--368},
  publisher={Springer-Verlag},
  address={Berlin, Heidelberg},
  year={1994}
}

@article{cj95-03-19,
  author={N. Klarlund},
  title={Progress measures, immediate determinacy, and a subset
		construction for tree automata},
  journal={Journal of Pure and Applied Logic},
  year={1994},
  volume={69},
  pages={243--268},
  publisher={Elsevier Science Publishers B.V. (North-Holland)},
  address={Amsterdam, Holland},
  note={A preliminary version appeared in \emph{Proceedings of the 7th
		  Symposium on Logic in Computer Science}, 1992}
}

@inproceedings{cj95-03-20,
  author={N. Klarlund and D. Kozen},
  title={Rabin measures and their applications to fairness and
		  automata theory},
  booktitle={Proceedings of the 6th Symposium on Logic in Computer
		  Science},
  pages={256--265},
  organization={Institute of Electrical and Electronics Engineers},
  address={Los Alamitos, CA},
  year={1991}
}

@inproceedings{cj95-03-21,
  author={D. Lehmann and A. Pnueli and J. Stavi},
  title={Impartiality, Justice and Fairness: the Ethics of Concurrent
		  Termination},
  booktitle={Proceedings of the 8th Colloquium on Automata, Language,
		  and Programming}, 
  series={Lecture Notes in Computer Science},
  volume={115},
  year={1981},
  publisher={Springer-Verlag},
  address={Berlin, Heidelberg},
  pages={264--277}
}

@techreport{cj95-03-22,
  author={M. G. Main},
  title={Complete Proof Rules for Strong Fairness and Strong
		  Extreme-Fairness},
  institution={Department of Computer Science, University of Colorado},
  year={1989},
  number={CU-CS-447-89}
}

@article{cj95-03-23,
  author={Z. Manna and A. Pnueli},
  title={Adequate proof principles  for invariance and liveness
		  properties of concurrent programs},
  journal={Science of Computer Programming},
  year={1984},
  volume={4},
  number={3},
  pages={257--290}
}

@inproceedings{cj95-03-24,
  author={Z. Manna and A. Pnueli},
  title={Specification and Verification of Concurrent Programs by
		  $\forall$-automata},
  booktitle={Proceedings of the 14th Symposium on Principles of
		  Programming Languages, Munich, West Germany},
  year={1987},
  pages={1--12},
  organization={Association for Computing Machinery}
}

@article{cj95-03-25,
  author={R. McNaughton},
  title={Testing and generating infinite sequences by a finite automaton},
  journal={Information and Control},
  volume={9},
  year={1966},
  pages={521--530}
}

@inproceedings{cj95-03-26,
  author={A. W. Mostowski},
  title={Regular expressions for infinite trees and a standard form of
		  automata},
  booktitle={Computation Theory, Proceedings of the 5th Symposium},
  series={Lecture Notes in Computer Science},
  volume={208},
  year={1984},
  pages={157--168},
  publisher={Springer-Verlag},
  address={Berlin, Heidelberg}
}

@article{cj95-03-27,
  author={S. Owicki and L. Lamport},
  title={Proving Liveness of concurrent programs},
  journal={ACM Transactions on Programming Languages and Systems},
  year={1982},
  volume={4},
  number={3},
  pages={455--495}
}

@article{cj95-03-28,
  author={M. O. Rabin},
  title={Decidability of second-order theories and automata on infinite
		  trees},
  journal={Transactions of the American Mathematical Society},
  year={1969},
  volume={141},
  pages={1--35}
}

@article{cj95-03-29,
  author={R. Rinat and N. Francez and O. Grumberg},
  title={Infinite trees, markings and well-foundedness},
  journal={Information and Computation},
  year={1988},
  volume={79},
  pages={131--154}
}

@book{cj95-03-30,
  author={Rogers, Jr., Hartley},
  title={Theory of Recursive Functions and Effective Computability},
  publisher={McGraw-Hill Book Company},
  year={1967},
  address={New York, NY},
}

@inproceedings{cj95-03-31,
  author={S. Safra},
  title={On Complexity of $\omega$-automata},
  booktitle={Proceedings of the 29th Symposium on Foundations of Computer
		  Science},
  year={1988},
  pages={319--327},
  organization={Institute of Electrical and Electronics Engineers}
}

@techreport{cj95-03-32,
  author={A. P. Sistla},
  title={On Using Automata in the Verification of Concurrent Programs},
  institution={Computer and Intelligent Systems Laboratory, GTE
		  Laboratories Inc},
  year={1987}
}

@article{cj95-03-33,
  author={F. A. Stomp and de Roever, W. P. and  R. T. Gerth},
  title={The $\mu$-Calculus as an Assertion-Language for Fairness Arguments},
  journal={Information and Computation},
  year={1989},
  volume={82},
  pages={278--322}
}

@article{cj95-03-34,
  author={M. Vardi},
  title={ Verification of Concurrent Programs: The Automata-Theoretic
		  Framework},
  journal={Annals of Pure and Applied Logic},
  volume={51},
  year={1991},
  pages={79--98}
}

@techreport{cj95-03-35,
  author={M. Vardi},
  title={Rank Predicates vs.\ progress measures in concurrent-program
		  verification},
  institution={IBM Research Division},
  year={1994},
  number={RJ 9879}
}