% 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",
}