@proceedings(DBLP:conf/lfcs/2009,
 editor       = "Sergei N. Art{\"e}mov and Anil Nerode",
 year         = "2009",
 title        = "Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "5407",
 publisher    = "Springer",
 url          = "http://dx.doi.org/10.1007/978-3-540-92687-0",
)
@inproceedings(DBLP:conf/cav/BernholtzVW94,
 author       = "Orna Bernholtz and Moshe Y. Vardi and Pierre Wolper",
 year         = "1994",
 title        = "An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract)",
 editor       = "David L. Dill",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "818",
 publisher    = "Springer",
 pages        = "142--155",
 url          = "http://dx.doi.org/10.1007/3-540-58179-0_50",
)
@article(+emhal86,
 author       = "E. Emerson and J. Halpern",
 year         = "1986",
 title        = "`{S}ometimes' and `not never' revisited",
 journal      = "J. ACM",
 volume       = "33",
 url          = "http://dx.doi.org/10.1145/4904.4999",
)
@inproceedings(EJ88,
 author       = "E. Emerson and C. Jutla",
 year         = "1988",
 title        = "Complexity of Tree Automata and Modal Logics of Programs",
 booktitle    = "29th IEEE Foundations of Computer Science, Proceedings",
 publisher    = "IEEE",
)
@article(+emsi,
 author       = "E. Emerson and A. Sistla",
 year         = "1984",
 title        = "Deciding full branching time logic",
 journal      = "Inf. and Control",
 volume       = "61",
 pages        = "175 -- 201",
 url          = "http://dx.doi.org/10.1016/S0019-9958(84)80047-9",
)
@incollection(Eme90,
 author       = "E.A. Emerson",
 year         = "1990",
 title        = "Temporal and modal logic",
 editor       = "J. van Leeuwen",
 booktitle    = "Hbk of Th. Comp. Sci.",
 vol. = "B",
 publisher    = "Elsevier",
)
@inproceedings(FLL10,
 author       = "O. Friedmann and M. Latte and M. Lange",
 year         = "2010",
 title        = "A Decision Procedure for {CTL*} Based on Tableaux and Automata.",
 booktitle    = "IJCAR'10",
 pages        = "331--345",
 url          = "http://dx.doi.org/10.1007/978-3-642-14203-1_28",
)
@inproceedings(DBLP:conf/lfcs/GorankoS09,
 author       = "Valentin Goranko and Dmitry Shkatov",
 year         = "2009",
 title        = "Tableau-Based Procedure for Deciding Satisfiability in the Full Coalitional Multiagent Epistemic Logic",
 editor       = "Art{\"e}mov and Nerode",
 pages        = "197--213",
 url          = "http://dx.doi.org/10.1007/978-3-540-92687-0_14",
)
@inproceedings(DBLP:conf/focs/KupfermanV05,
 author       = "Orna Kupferman and Moshe Y. Vardi",
 year         = "2005",
 title        = "Safraless Decision Procedures",
 booktitle    = "FOCS",
 publisher    = "IEEE Computer Society",
 pages        = "531--542",
 url          = "http://doi.ieeecomputersociety.org/10.1109/SFCS.2005.66",
)
@inproceedings(Lange00modelchecking,
 author       = "M. Lange and C. Stirling",
 year         = "2000",
 title        = "Model Checking Games for CTL*",
 booktitle    = "In ICTL'00",
 pages        = "115--125",
)
@article(DBLP:journals/entcs/McCabe-Dansted11,
 author       = "J. McCabe-Dansted",
 year         = "2011",
 title        = "A Rooted Tableau for BCTL",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "278",
 pages        = "145--158",
 url          = "http://dx.doi.org/10.1016/j.entcs.2011.10.012",
)
@inproceedings(DBLP:conf/concur/MogaveroMPV12,
 author       = "Fabio Mogavero and Aniello Murano and Giuseppe Perelli and Moshe Y. Vardi",
 year         = "2012",
 title        = "What Makes {ATL}* Decidable? A Decidable Fragment of Strategy Logic",
 editor       = "Maciej Koutny and Irek Ulidowski",
 booktitle    = "CONCUR",
 series       = "Lecture Notes in Computer Science",
 volume       = "7454",
 publisher    = "Springer",
 pages        = "193--208",
 url          = "http://dx.doi.org/10.1007/978-3-642-32940-1_15",
)
@inproceedings(Pnu77,
 author       = "A. Pnueli",
 year         = "1977",
 title        = "The temporal logic of programs",
 booktitle    = "Proceedings of the Eighteenth Symposium on Foundations of Computer Science",
 pages        = "46--57",
 note         = "Providence, RI",
)
@article(Rey:ctlstar,
 author       = "M. Reynolds",
 year         = "2001",
 title        = "An Axiomatization of Full Computation Tree Logic",
 journal      = "J.S.L.",
 volume       = "66",
 number       = "3",
 pages        = "1011--1057",
)
@techreport(Rey:fasttablong,
 author       = "M. Reynolds",
 year         = "May, 2013",
 title        = "A Faster Tableau for {CTL*}, Long Version",
 type         = "Technical Report",
 institution  = "CSSE, UWA",
 url          = "{http://www.csse.uwa.edu.au/~mark/research/Online/quicktab/}",
 note         = "Implemented reasoner also available here.",
)
@inproceedings(Rey:startabFM,
 author       = "Mark Reynolds",
 year         = "2009",
 title        = "A Tableau for {CTL*}",
 editor       = "Ana Cavalcanti and Dennis Dams",
 booktitle    = "FM 2009: Eindhoven, 2009. Proc.",
 series       = "Lecture Notes in Computer Science",
 volume       = "5850",
 publisher    = "Springer",
 pages        = "403--418",
 url          = "http://dx.doi.org/10.1007/978-3-642-05089-3_26",
)
@article(Rey:startab,
 author       = "M. Reynolds",
 year         = "2011",
 title        = "A tableau-based decision procedure for {CTL*}",
 journal      = "J. Formal Aspects of Comp.",
 pages        = "1--41",
 url          = "http://dx.doi.org/10.1007/s00165-011-0193-4",
)
@inproceedings(VaS85,
 author       = "M. Vardi and L. Stockmeyer",
 year         = "1985",
 title        = "Improved Upper and Lower Bounds for Modal Logics of Programs",
 booktitle    = "17th ACM Symp. on Theory of Computing, Proceedings",
 publisher    = "ACM",
 pages        = "240--251",
 url          = "http://dx.doi.org/10.1145/22145.22173",
)