% The Chicago Journal of Theoretical Computer Science, Volume 1998, Article 2
% Bibliography

@Article{cj98-02-01,
  author =       "M. Abadi and L. Lamport",
  title =        "The Existence of Refinement Mappings",
  journal =      "Theoretical Computer Science",
  volume =       "82",
  number =       "2",
  pages =        "253--284",
  year =         "1991",
}

@InProceedings{cj98-02-02,
  author =       "A. Aziz and V. Singhal and F. Balarin and R. Brayton
                 and A. L. Sangiovanni-Vincentelli",
  title =        "Equivalences for fair {K}ripke Structures",
  booktitle =    "Proceedings of the 21st International Colloquium on Automata, Languages and
                 Programming",
  address =      "Jerusalem, Israel",
  month =        jul,
  year =         "1994",
}

@InProceedings{cj98-02-03,
  author =       "H. R. Andersen and B. Vergauwen",
  title =        "Efficient Checking of Behavioural Relations and Modal
                 Assertions Using Fixed-Point Inversion",
  booktitle =    "Computer Aided Verification, Proceedings of the 7th International
                 Conference",
  series =       "Lecture Notes in Computer Science",
  volume =       "939",
  pages =        "142--154",
  publisher =    "Springer-Verlag",
  address =      "Berlin",
  month =        jul,
  year =         "1995",
}

@InProceedings{cj98-02-04,
  author =       "S. Bensalem and A. Bouajjani and C. Loiseaux and J.
                 Sifakis",
  title =        "Property Preserving Simulations",
  booktitle =    "Proceedings of the 4th Conference on Computer Aided Verification",
  series =       "Lecture Notes in Computer Science",
  volume =       "663",
  publisher =    "Springer-Verlag",
  pages =        "260--273",
  address =      "Berlin",
  month =        jun,
  year =         "1992",
}

@Article{cj98-02-05,
  author =       "M. C. Browne and E. M. Clarke and O. Grumberg",
  title =        "Characterizing finite {K}ripke structures in
                 propositional temporal logic",
  journal =      "Theoretical Computer Science",
  volume =       "59",
  pages =        "115--131",
  year =         "1988",
}

@Article{cj98-02-06,
  author =       "J. Balcazar and J. Gabarro and M. Santha",
  title =        "Deciding bisimilarity is {P}-complete",
  journal =      "Formal Aspects of Computing",
  volume =       "4",
  number =       "6",
  pages =        "638--648",
  year =         "1992",
}

@InProceedings{cj98-02-07,
  author =       "O. Bernholtz and M. Y. Vardi and P. Wolper",
  title =        "An Automata-Theoretic Approach to Branching-Time Model
                 Checking",
  booktitle =    "Computer Aided Verification, Proceedings of the 6th International
                 Conference",
  editor =       "D. L. Dill",
  month =        jun,
  series =       "Lecture Notes in Computer Science",
  volume =       "818",
  year =         "1994",
  publisher =    "Springer-Verlag",
  address =      "Berlin",
  pages =        "142--155",
}

@InProceedings{cj98-02-08,
  author =       "E. M. Clarke and I. A. Draghicescu",
  title =        "Expressibility results for linear-time and
                 branching-time logics",
  booktitle =    "Proceedings of the Workshop on Linear Time, Branching Time, and
                 Partial Order in Logics and Models for Concurrency",
  series =       "Lecture Notes in Computer Science",
  volume =       "354",
  publisher =    "Springer-Verlag",
  address =      "Berlin",
  editors =      "J.W. de Bakker and W.P. de Roever, W.P. and G.
                 Rozenberg",
  year =         "1988",
  pages =        "428--437",
}

@Article{cj98-02-09,
  author =       "E. M. Clarke and I. A. Draghicescu and R. P. Kurshan",
  year =         "1993",
  title =        "A Unified Approach for Showing Language Containment
                 and Equivalence Between Various Types of
                 \(\omega\)-Automata",
  journal =      "Information Processing Letters",
  volume =       "46",
  publisher =    "Elsevier",
  pages =        "301--308",
}

@Article{cj98-02-10,
  author =       "E. M. Clarke and E. A. Emerson and A. P. Sistla",
  title =        "Automatic Verification of Finite-State Concurrent
                 Systems Using Temporal Logic Specifications",
  journal =      "ACM Transactions on Programming Languages and
                 Systems",
  volume =       "8",
  number =       "2",
  pages =        "244--263",
  year =         "1986",
  month =        jan,
}

@Article{cj98-02-11,
  author =       "Y. Choueka",
  title =        "Theories of automata on \(\omega\)-tapes: {A} simplified
                 approach",
  journal =      "Journal of Computer and System Sciences",
  volume =       "8",
  pages =        "117--141",
  year =         "1974",
}

@InProceedings{cj98-02-12,
  author =       "E. A. Emerson and C.-L. Lei",
  title =        "Temporal Model Checking under Generalized Fairness
                 Constraints",
  booktitle =    "Proceedings of the 18th Hawaii International Conference on System
                 Sciences",
  year =         "1985",
  publisher =    "Western Periodicals Company",
  address =      "North Hollywood, CA",
}

@Article{cj98-02-13,
  author =       "E. A. Emerson and C.-L. Lei",
  title =        "Modalities for Model Checking: {B}ranching Time Logic
                 Strikes Back",
  journal =      "Science of Computer Programming",
  volume =       "8",
  year =         "1987",
  pages =        "275--306",
}

@Article{cj98-02-14,
  author =       "E. A. Emerson",
  title =        "Temporal and modal logic",
  journal =      "Handbook of Theoretical Computer Science",
  publisher =    "North Holland",
  editor =       "J. Van Leeuwen",
  pages =        "997--1072",
  year =         "1990",
}

@Book{cj98-02-15,
  author =       "R. Greenlaw and H. J. Hoover and W. L. Ruzzo",
  title =        "Limits of Parallel Computation",
  publisher =    "Oxford University Press",
  year =         "1995",
}

@Book{cj98-02-16,
  author =       "M. Garey and D.~S. Johnson",
  title =        "Computers and Intractability: A Guide to the Theory
                 of {NP}-{C}ompleteness",
  address =      "San Francisco",
  year =         "1979",
  publisher =    "W. Freeman and Co."
}

@Article{cj98-02-17,
  author =       "O. Grumberg and D. E. Long",
  title =        "Model checking and modular verification",
  journal =      "ACM Transactions on Programming Languages and Systems",
  volume =       "16",
  number =       "3",
  pages =        "843--871",
  year =         "1994",
}

@Article{cj98-02-18,
  author =       "L. M. Goldschlager",
  title =        "The monotone and planar circuit value problems are log
                 space complete for {P}",
  journal =      "SIGACT News",
  volume =       "9",
  number =       "2",
  year =         "1977",
  pages =        "25--29",
}

@InProceedings{cj98-02-19,
  author =       "M. R. Henzinger and T. A. Henzinger and P. W. Kopke",
  title =        "Computing simulations on finite and infinite graphs",
  booktitle =    "Proceedings of the 36th Symposium on Foundations of
                 Computer Science",
  publisher =    "IEEE Computer Society Press",
  address =      "Los Alamitos, CA",
  year =         "1995",
  pages =        "453--462",
}

@Book{cj98-02-20,
  author =       "M. Hennessy",
  title =        "Algebraic Theory of Processes",
  publisher =    "MIT Press",
  address =      "Cambridge, MA",
  year =         "1985",
}

@Article{cj98-02-21,
  author =       "N. Immerman",
  title =        "Nondeterministic space is closed under complement",
  journal =      sicomp,
  volume =       "17",
  year =         "1988",
  pages =        "935--938",
}

@Article{cj98-02-22,
  author =       "N. D. Jones",
  title =        "Space-bounded reducibility among combinatorial
                 problems",
  year =         "1975",
  journal =      "Journal of Computer and System Sciences",
  volume =       "11",
  pages =        "68--75",
}

@Article{cj98-02-23,
  author =       "R. M. Keller",
  title =        "Formal verification of parallel programs",
  year =         "1976",
  journal =      "Communications of the {ACM}",
  volume =       "19",
  pages =        "371--384",
}

@Article{cj98-02-24,
  author =       "R. P. Kurshan",
  title =        "Complementing deterministic {B}{\"u}chi automata in
                 polynomial time",
  journal =      "Journal of Computer and System Science",
  volume =       "35",
  pages =        "59--71",
  year =         "1987",
}

@Book{cj98-02-25,
  author =       "R. P. Kurshan",
  title =        "Computer Aided Verification of Coordinating
                 Processes",
  publisher =    "Princeton University Press",
  address =      "Princeton, NJ",
  year =         "1994",
}

@InProceedings{cj98-02-26,
  author =       "O. Lichtenstein and A. Pnueli",
  title =        "Checking that Finite State Concurrent Programs Satisfy
                 their Linear Specification",
  month =        jan,
  year =         "1985",
  booktitle =    "Proceedings of the 12th {ACM} Symposium on Principles
                 of Programming Languages",
  publisher =    "ACM",
  address =      "New York",
  pages =        "97--107",
}

@InProceedings{cj98-02-27,
  author =       "D. Lehman and A. Pnueli and J. Stavi",
  title =        "Impartiality, justice, and fairness---the ethics of
                 concurrent termination",
  booktitle =    "Proceedings of the 8th Colloquium on Automata, Programming, and
                 Languages (ICALP)",
  pages =        "264--277",
  series =       "Lecture Notes in Computer Science",
  volume =       "115",
  publisher =    "Springer-Verlag",
  address =      "Berlin",
  month =        jul,
  year =         "1981",
}

@Article{cj98-02-28,
  author =       "S. S. Lam and A. U. Shankar",
  title =        "Protocol verification via projection",
  journal =      "IEEE Transactions on Software Engineering",
  volume =       "10",
  pages =        "325--342",
  year =         "1984",
}

@InProceedings{cj98-02-29,
  author =       "N. A. Lynch and M. R. Tuttle",
  title =        "Hierarchical correctness proofs for distributed
                 algorithms",
  booktitle =    "Proceedings of the 6th ACM Symposium on Principles of Distributed
                 Computing",
  publisher =    "ACM",
  address =      "New York",
  pages =        "137--151",
  year =         "1987",
}

@InProceedings{cj98-02-30,
  author =       "R. Milner",
  title =        "An Algebraic Definition of Simulation between
                 Programs",
  booktitle =    "Proceedings of the 2nd International Joint Conference
                 on Artificial Intelligence",
  pages =        "481--489",
  month =        sep,
  publisher =    "British Computer Society",
  address =      "London",
  year =         "1971",
}

@Book{cj98-02-31,
  author =       "R. Milner",
  title =        "A Calculus of Communicating Systems",
  year =         "1980",
  volume =       "92",
  series =       "Lecture Notes in Computer Science",
  publisher =    "Springer-Verlag",
  address =      "Berlin",
}

@Book{cj98-02-32,
  author =       "R. Milner",
  title =        "Communication and Concurrency",
  year =         "1989",
  publisher =    "Prentice-Hall",
  address =      "Englewood Cliffs, NJ",
}

@Article{cj98-02-33,
  author =       "R. Milner",
  title =        "Operational and algebraic semantics of concurrent
                 processes",
  journal =      "Handbook of Theoretical Computer Science",
  pages =        "1201--1242",
  year =         "1990",
}

@Book{cj98-02-34,
  author =       "Z. Manna and A. Pnueli",
  title =        "The Temporal Logic of Reactive and Concurrent Systems:
                 Specification",
  year =         "1992",
  publisher =    "Springer-Verlag",
  month =        jan,
  address =      "Berlin",
}

@InProceedings{cj98-02-35,
  author =       "A. R. Meyer and L. J. Stockmeyer",
  title =        "The equivalence problem for regular expressions with
                 squaring requires exponential time",
  booktitle =    "Proceedings of the 13th IEEE Symposium on Switching and Automata
                 Theory",
  year =         "1972",
  pages =        "125--129",
  publisher =    "IEEE Computer Group",
  address =      "New York",
}

@Article{cj98-02-36,
  author =       "D. A. Plaisted",
  title =        "Complete Problems in the First-order Predicate
                 Calculus",
  journal =      "Journal of Computer and System Sciences",
  volume =       "29",
  number =       "1",
  pages =        "8--35",
  year =         "1984",
}

@InProceedings{cj98-02-37,
  author =       "A. Pnueli",
  title =        "Linear and branching structures in the semantics and
                 logics of reactive systems",
  booktitle =    "Proceedings of the 12th International Colloquium on Automata, Languages and
                 Programming",
  series =       "Lecture Notes in Computer Science",
  pages =        "15--32",
  publisher =    "Springer-Verlag",
  address =      "Berlin",
  year =         "1985",
}

@InProceedings{cj98-02-38,
  author =       "S. Safra",
  title =        "On the Complexity of \(\omega\)-Automata",
  month =        oct,
  year =         "1988",
  booktitle =    "Proceedings of the 29th {IEEE} Symposium on
                 Foundations of Computer Science",
  pages =        "319--327",
  publisher =    "IEEE Computer Society Press",
  address =      "Los Alamitos, CA"
}

@InProceedings{cj98-02-39,
  author =       "S. Safra",
  title =        "Exponential Determinization for \(\omega\)-Automata with
                 Strong-Fairness Acceptance Condition",
  month =        may,
  year =         "1992",
  booktitle =    "Proceedings of the 24th {ACM} Symposium on Theory of
                 Computing",
  publisher =    "ACM",
  address =      "New York",
}

@Article{cj98-02-40,
  author =       "A. P. Sistla and E. M. Clarke",
  title =        "The complexity of propositional linear temporal
                 logic",
  journal =      "Journal of the ACM",
  volume =       "32",
  year =         "1985",
  pages =        "733--749",
}

@Article{cj98-02-41,
  author =       "R. Szelepcsinyi",
  title =        "The Method of Forced Enumeration for Nondeterministic
                 Automata",
  journal =      "Acta Informatica",
  volume =       "26",
  pages =        "279--284",
  year =         "1988",
}

@Article{cj98-02-42,
  author =       "A. P. Sistla and M. Y. Vardi and P. Wolper",
  title =        "The Complementation Problem for {B}{\"u}chi Automata
                 with Applications to Temporal Logic",
  journal =      "Theoretical Computer Science",
  volume =       "49",
  pages =        "217--237",
  year =         "1987",
}

@Article{cj98-02-43,
  author =       "W. Thomas",
  title =        "Automata on infinite objects",
  journal =      "Handbook of Theoretical Computer Science",
  publisher =    "North Holland",
  editor =       "J. Van Leeuwen",
  pages =        "165--191",
  year =         "1990",
}

@InProceedings{cj98-02-44,
  author =       "M. Y. Vardi and P. Wolper",
  title =        "An Automata-Theoretic Approach to Automatic Program
                 Verification",
  booktitle =    "Proceedings of the First Symposium on Logic in Computer Science",
  pages =        "322--331",
  year =         "1986",
  month =        jun,
  publisher =    "IEEE Computer Society Press",
  address =      "Los Alamitos, CA",
}

@Article{cj98-02-45,
  author =       "M. Y. Vardi and P. Wolper",
  title =        "Reasoning about Infinite Computations",
  journal =      "Information and Computation",
  volume =       "115",
  number =       "1",
  year =         "1994",
  month =        nov,
  pages =        "1--37",
}