Abadir, M.S., Albin, K., Havlicek, J., Krishnamurthy, N., and Martin, A.K. 2003. Formal Verification Successes at Motorola. Formal Methods in System Design, 22(2), 117–123.Google Scholar

Abate, P., Goré, R., and Widmann, F. 2007. One-Pass Tableaux for Computation Tree Logic. Pages 32–46 of: LPA'7. Lecture Notes in Computer Science, vol. 4790. Springer.

Abdou, J., and Keiding, H. 1991. Effectivity Functions in Social Choice Theory. Kluwer.

Abrahamson, K. 1979. Modal Logic of Concurrent Nondeterministic Programs. Pages 21–33 of: International Symposium on Semantics of Concurrent Computation, Evian, France. Lecture Notes in Computer Science, vol. 70. Springer.

Abrahamson, K. 1980. Decidability and Expressiveness of Logics of Programs. Ph.D. thesis, University of Washington.

Accellera Organization, Inc. 2004. Formal Semantics of Accellera Property Specification Language. In Appendix B of http://www.eda.org/vfv/docs/PSL-v1.1.pdf.

Aceto, L., Ingolfsdottir, A., and Srba, J. 2012a. The Algorithmics of Bisimilarity. In: Sangiorgi and Rutten (2012).

Aceto, L., Ingólfsdóttir, A., Levy, P.B., and Sack, J. 2012b. Characteristic Formulae for Fixed-Point Semantics: A General Framework. Mathematical Structures in Computer Science, 22(2), 125–173.Google Scholar

Adler, I.M., and Immerman, N. 2001. An n! Lower Bound on Formula Size. Pages 197–208 of: LIC'1. IEEE.

Ågotnes, T., Goranko, V., and Jamroga, W. 2007. Alternating-Time Temporal Logics with Irrevocable Strategies. Pages 15–24 of: Proceedings of TARK XI.Google Scholar

Ågotnes, T., Goranko, V., and Jamroga, W. 2008. Strategic Commitment and Release in Logics for Multi-Agent Systems (Extended abstract). Tech. rept. IfI-08-01. Clausthal University of Technology.

Aho, A., Hopcroft, J., and Ullman, J. 1974. The Design and Analysis of Computer Algorithms. Addison-Wesley.

Aho, A., Hopcroft, J., and Ullman, J. 1983. Data Structures and Algorithms. Addison- Wesley.

Ajspur, M., and Goranko, V. 2013. Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge. Pages 80–96 of: ICLA 2013.Google Scholar

Alberucci, L., and Facchini, A. 2009. The Modal μ-Calculus over Restricted Classes of Transition Systems. The Journal of Symbolic Logic, 74(4), 1367–1400.Google Scholar

Alpern, B., and Schneider, F. 1987. Recognizing Safety and Liveness. Distributed Computing, 2(3), 117–126.

Alur, R., Henzinger, Th., and Kupferman, O. 1997 (October). Alternating-Time Temporal Logic. Pages 100–109 of: FOC'7.Google Scholar

Alur, R., Henzinger, T.A., Kupferman, O., and Vardi, M. 1998a. Alternating Refinement Relations. Pages 163–178 of: CONCU'8. Lecture Notes in Computer Science, vol. 1466. Springer.

Alur, R., Henzinger, T.A., and Kupferman, O. 1998b. Alternating-Time Temporal Logic. Pages 23–60 of: COMPO'7. Lecture Notes in Computer Science, vol. 1536. Springer.

Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., and Tasiran, S. 1998c. MOCHA: Modularity in Model-Checking. Pages 521–525 of: CA'8. Lecture Notes in Computer Science, vol. 1427. Springer.

Alur, R., Henzinger, Th., and Kupferman, O. 2002. Alternating-Time Temporal Logic. Journal of the Association for Computing Machinery, 49(5), 672–713.Google Scholar

Alur, R., Etessami, K., and Madhusudan, P. 2004. A Temporal Logic of Nested Calls and Returns. Pages 467–481 of: TACA'4. Lecture Notes in Computer Science, vol. 2988. Springer.

Andersen, H.R. 1994a. Model Checking and Boolean Graphs. Theoretical Computer Science, 126(1), 3–30.Google Scholar

Andersen, H.R. 1994b. A Polyadic Modal μ-Calculus. Tech. rept. ID-TR: 1994-195. Dept. of Computer Science, Technical University of Denmark, Copenhagen.

Andréka, H., Németi, I., and van Benthem, J. 1998. Modal Languages and Bounded Fragments of Predicate Logic. Journal of Philosophical Logic, 27(3), 217–274.Google Scholar

Arenas, M., Barceló, P., and Libkin, L. 2011. Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization. Theory of Computing Systems, 49(3), 639–670.Google Scholar

Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., and Zbar, Y. 2002. The ForSpec Temporal Logic: A New Temporal Property Specification Language. Pages 296–311 of: TACA'2. Lecture Notes in Computer Science, vol. 2280. Springer.

Arnold, A. 1994. Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall.

Arnold, A. 1999. The Modal μ-Calculus Alternation Hierarchy Is Strict on Binary Trees. RAIRO – Theoretical Informatics and Applications, 33, 329–339.Google Scholar

Arnold, A., and Nivat, M. 1980. The Metric Space of Infinite Trees. Algebraic And Topological Properties. Fundamenta Informaticae, 3(4), 181–205.Google Scholar

Arnold, A., and Nivat, M. 1982. Comportements de processus. Pages 35–68 of: AFCET.

Arnold, A., and Niwiński, D. 2001. Rudiments of μ-calculus. Elsevier.

Arora, S., and Barak, B. 2009. Computational Complexity – A Modern Approach. Cambridge University Press.

Auffray, Y., and Enjalbert, P. 1989. Modal Theorem Proving An Equational Viewpoint. Pages 441–445 of: IJCA'9.

Baader, F., Calvanese, D., McGuinness, D., Nardi, D., and Patel-Schneider, P. (eds). 2003. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press.

Baier, C., and Katoen, J.P. 2008. Principles of Model Checking. MIT Press.

Banach, S. 1922. Sur les opérations dans les ensembles abstraits et leur application aux équations integrales. Fundamenta Mathematicae, 3, 133–181.Google Scholar

Banieqbal, B., and Barringer, H. 1989. Temporal Logic with Fixed Points. Pages 62–74 of: Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings. Lecture Notes in Computer Science, vol. 398. Springer.

Barringer, H., Kuiper, R., and Pnueli, A. 1986. A Really Abstract Concurrent Model and Its Temporal Logic. Pages 173–183 of: POP'6. ACM.

Bauland, M., Schneider, Th., Schnoor, H., Schnoor, I., and Vollmer, H. 2009. The Complexity of Generalized Satisfiability for Linear Temporal Logic. Logical Methods in Computer Science, 5(1).Google Scholar

Bauland, M., Mundhenk, M., Schneider, Th., Schnoor, H., Schnoor, I., and Vollmer, H. 2011. The Tractability of Model Checking for LTL: The Good, the Bad, and the Ugly Fragments. ACM Transactions on Computational Logic, 12(2), 13.CrossRefGoogle Scholar

Beckmann, A., and Moller, F. 2008. On the complexity of parity games. Pages 237–248 of: Visions of Computer Science – BCS International Academic Conference, Imperial College, London, UK, 22–24 September 2008.

Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., and Rodeh, Y. 2001. The Temporal Logic Sugar. Pages 363–367 of: CA'1. Lecture Notes in Computer Science, vol. 2102. Springer.

Bekić, H. 1984. Programming Languages and Their Definition, Selected Papers. Lecture Notes in Computer Science, vol. 177. Springer.

Ben-Ari, M., Pnueli, A., and Manna, Z. 1981. The Temporal Logic of Branching Time. Pages 164–176 of: POP'1. ACM.

Ben-Ari, M., Pnueli, A., and Manna, Z. 1983. The Temporal Logic of Branching Time. Acta Informatica, 20, 207–226.

Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., and Schnoebelen, Ph. 2001. Systems and Software Verification, Model-Checking Techniques and Tools. Springer.

Bergstra, J.A., and Klop, J.W. 1985. Algebra of Communicating Processes with Abstraction. Theoretical Computer Science, 37, 77–121.Google Scholar

Beth, E.W. 1955. Semantic Entailment and Formal Derivability. Nieuwe Reeks, 18(13), 309–342.Google Scholar

Beth, E.W. 1970. Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic. D. Reidel.

Bhat, G., and Cleaveland, R. 1996a. Efficient Local Model-Checking for Fragments of the Modal μ-Calculus. Pages 107–126 of: TACA'6. Lecture Notes in Computer Science, vol. 1055. Springer.

Bhat, G., and Cleaveland, R. 1996b. Efficient Model Checking via the Equational mu-Calculus. Pages 304–312 of: LIC'6. IEEE.

Bhat, G., Cleaveland, R., and Grumberg, O. 1995. Efficient On-the-Fly Model Checking for CTL*. Pages 388–397 of: LIC'5. IEEE.

Björklund, H., and Vorobyov, S. 2005. Combinatorial Structure and Randomized Subexponential Algorithms for Infinite Games. Theoretical Computer Science, 349(3), 347–360.Google Scholar

Björklund, H., Sandberg, S., and Vorobyov, S.G. 2003. A Discrete Subexponential Algorithm for Parity Games. Pages 663–674 of: STAC'3. Lecture Notes in Computer Science, vol. 2607. Springer.

Blackburn, P., de Rijke, M., and Venema, Y. 2001. Modal Logic. Cambridge University Press.

Blackburn, P., van Benthem, J., and Wolter, F. (eds). 2007. Handbook of Modal Logic. Elsevier.

Boy de la Tour, Th. 1992. An Optimality Result for Clause Form Translation. Journal of Symbolic Computation, 14, 283–301.Google Scholar

Bozzelli, L. 2008. The Complexity of CTL* + Linear Past. Pages 186–200 of: FOSSACS' 08. Lecture Notes in Computer Science, vol. 4962. Springer.

Bradfield, J.C. 1996. The Modal μ-calculus Alternation Hierarchy Is Strict. Pages 233–246 of: CONCU'6. Lecture Notes in Computer Science, vol. 1119. Springer.

Bradfield, J.C. 1998. Simplifying the Modal Mu-Calculus Alternation Hierarchy. Pages 39–49 of: STAC'8. Lecture Notes in Computer Science, vol. 1373. Springer.

Bradfield, J.C. 1999. Fixpoint Alternation: Arithmetic, Transition Systems, and the Binary Tree. RAIRO – Theoretical Informatics and Applications, 33(4/5), 341–356.Google Scholar

Bradfield, J.C., and Stirling, C. 2007. Modal μ-Calculi. In: Blackburn et al. (2007).

Brihaye, Th., Laroussinie, F., Markey, N., and Oreiby, Gh. 2007. Timed Concurrent Game Structures. Pages 445–459 of: CONCU'7. Lecture Notes in Computer Science, vol. 4703. Springer.

Brihaye, Th., Lopes, A. Da Costa, Laroussinie, F., and Markey, N. 2009. ATL with Strategy Contexts and Bounded Memory. Pages 92–106 of: LFC'9. Lecture Notes in Computer Science, vol. 5407. Springer.

Browne, A., Clarke, E.M., Jha, S., Long, D.E., and Marrero, W. 1997. An Improved Algorithm for the Evaluation of Fixpoint Expressions. Theoretical Computer Science, 178(1–2), 237–255.Google Scholar

Browne, M., Clarke, E., and Grumberg, O. 1988. Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science, 59, 115–131.Google Scholar

Bruse, F., Friedmann, O., and Lange, M. 2015. On Guarded Transformation in the μ- Calculus. Logic Journal of the IGPL 23(2), 194–216.Google Scholar

Büchi, J.R. 1962. On a Decision Method in Restricted Second Order Arithmetic. Pages 1–12 of: Congress on Logic, Method, and Philosophy of Science. Stanford University Press.

Bull, R. 1969. On Modal Logic with Propositional Quantifiers. The Journal of Symbolic Logic, 34(2), 257–263.Google Scholar

Bull, R., and Segerberg, K. 1984. Basic Modal Logic. Pages 1–88 of: Gabbay, D.M., and Guenthner, F. (eds), Handbook of Philosophical Logic, Volume II. Reidel.

Bulling, N., Dix, J., and Jamroga, W. 2010. Model Checking Logics of Strategic Ability: Complexity. Pages 125–159 of: Specification and Verification of Multi-Agent Systems. Springer.

Bulling, N., and Jamroga, W. 2014. Comparing Variants of Strategic Ability: How Uncertainty and Memory Influence General Properties of Games. Autonomous Agents and Multi-Agent Systems, 28(3), 474–518.Google Scholar

Burgess, J. 1984. Basic Tense Logic. In: Gabbay and Guenthner (1984).

Bustan, D., and Havlicek, J. 2006. Some Complexity Results for System Verilog Assertions. Pages 205–218 of: CA'6. Lecture Notes in Computer Science, vol. 4144. Springer.

Bustan, D., Fisman, D., and Havlicek, D. 2005. Automata Constructions for PSL. Tech. rept. MCS05-04. The Weizmann Institute of Science.

Cerrito, S., David, A., and Goranko, V. 2014. Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+. Pages 277–291 of: IJCA'4. Lecture Notes in Computer Science, vol. 8562. Springer.

Chagrov, A., and Zakharyaschev, M. 1997. Modal Logic. Clarendon Press.

Chandra, A.K., Kozen, D.C., and Stockmeyer, L.J. 1981. Alternation. Journal of the Association for Computing Machinery, 28(1), 114–133.Google Scholar

Chatterjee, K., Henzinger, T.A., and Piterman, N. 2010. Strategy Logic. Information and Computation, 208(6), 677–693.Google Scholar

Chellas, B. 1980. Modal Logic. Cambridge University Press.

Chen, C.C., and Lin, I.P. 1993. The Computational Complexity of Satisfiability of Temporal Horn Formulas in Propositional Linear-Time Temporal Logic. Information Processing Letters, 45, 131–136.Google Scholar

Clarke, E., and Emerson, E.A. 1981. Design and Synthesis of Synchronisation Skeletons Using Branching Time Temporal Logic. Pages 52–71 of: Workshop on Logics of Programs. Springer.

Clarke, E., Grumberg, O., and Peled, D. 2000. Model Checking. MIT Press.

Clarke, E.M., and Draghicescu, I.A. 1988. Expressibility Results for Linear-Time and Branching-Time Logics. Pages 428–437 of: REX Workshop. Lecture Notes in Computer Science, vol. 354. Springer.

Clarke, E.M., and Schlingloff, B.-H. 2001. Model Checking. Pages 1635–1790 of: Robinson, A., and Voronkov, A. (eds), Handbook of Automated Reasoning. Elsevier.

Clarke, E.M., Emerson, E.A., and Sistla, A.P. 1983 (Jan.). Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. Pages 117–126 of: POP'3.

Clarke, E.M., Emerson, E.A., and Sistla, A.P. 1986. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2), 244–263.Google Scholar

Cleaveland, R. 1989. Tableau-Based Model Checking in the Propositional Mu-Calculus. Acta Informatica, 27(8), 725–747.Google Scholar

Cleaveland, R., and Steffen, B. 1991. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal mu-Calculus. Pages 48–58 of: CA'1. Lecture Notes in Computer Science, vol. 575. Springer.

Comon-Lundh, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., and Tommasi, M. Tree Automata Techniques and Applications. Online book available at: http://tata.gforge.inria.fr.

Cook, S.A. 1971. The Complexity of Theorem-Proving Procedures. Pages 151–158 of: STO'1. ACM.

Copeland, J. 2002. The Genesis of Possible Worlds Semantics. Journal of Philosophical Logic, 31(1), 99–137.Google Scholar

Cristau, J. 2009. Automata and Temporal Logic over Arbitrary Linear Time. Pages 133–144 of: FSTTC'9. LIPIcs, vol. 4. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik.

'gostino, G., and Lenzi, G. 2010. On the μ-Calculus Over Transitive and Finite Transitive Frames. Theoretical Computer Science, 411(50), 4273–4290.Google Scholar

'gostino, G., Montanari, A., and Policriti, A. 1995. A Set-Theoretical Translation Method for Polymodal Logics. Journal of Automated Reasoning, 15, 317–337.Google Scholar

'gostino, M., Gabbay, D.M., Hahnle, R., and Posegga, J. (eds). 1999. Handbook of Tableau Methods. Kluwer Academic.

Dam, M. 1994. CTL* and ECTL* as Fragments of the Modal μ-Calculus. Theoretical Computer Science, 126, 77–96.Google Scholar

David, A. 2013. TATL: Implementation of ATL Tableau-Based Decision Procedure. Pages 97–103 of: TABLEAU'3. Lecture Notes in Computer Science, vol. 8123. Springer.

David, A. 2015. Deciding ATL* Satisfiability by Tableaux. Pages 214–228 of: CAD'5. Lecture Notes in Computer Science, vol. 9195. Springer.

Dawar, A. 2005. How Many First-Order Variables Are Needed on Finite Ordered Structures? Pages 489–520 of: Artëmov, S., Barringer, H., 'vila Garcez, A., Lamb, L., and Woods, J. (eds), We Will Show Them! Essays in Honour of Dov Gabbay, Volume One. College Publications.

Dawar, A., Grädel, E., and Kreutzer, S. 2004. Inflationary Fixed Points in Modal Logics. ACM Transactions on Computational Logic, 5(2), 282–315.Google Scholar

Dax, C., and Lange, M. 2004. Game Over: The Foci Approach to LTL Satisfiability and Model Checking. Pages 33–49 of: GD'4. Electronic Notes in Theoretical Computer Science, vol. 119. Elsevier.

de Bakker, J.W., and de Roever, W.P. 1972. A Calculus for Recursive Program Schemes. In: Nivat, M. (ed), Proc. IRIA Symp. on Automata, Formal Languages and Programming. North-Holland.

de Nivelle, H. 1998. A Resolution Decision Procedure for the Guarded Fragment. Pages 191–204 of: CAD'8. Lecture Notes in Computer Science, vol. 1421. Springer.

de Nivelle, H., and de Rijke, M. 2003. Deciding the Guarded Fragments with Resolution. Journal of Symbolic Computation, 35(1), 21–58.Google Scholar

de Nivelle, H., and Pratt-Hartmann, I. 2001. A Resolution-BasedDecision Procedure for the Two-Variable Fragment with Equality. Pages 211–225 of: IJCA'1. Lecture Notes in Computer Science, vol. 2083. Springer.

Demri, S. 2003. A Polynomial Space Construction of Tree-like Models for Logics with Local Chains of Modal Connectives. Theoretical Computer Science, 300(1–3), 235–258.Google Scholar

Demri, S., and de Nivelle, H. 2005. Deciding Regular Grammar Logics with Converse through First-Order Logic. Journal of Logic, Language, and Information, 14(3), 289–329.Google Scholar

Demri, S., and Gastin, P. 2012. Specification andVerificationUsing Temporal Logics. Pages 457–494 of: Modern Applications of Automata Theory. IISc Research Monographs, vol. 2. World Scientific.

Demri, S., and Goré, R. 1999. Tractable Transformations from Modal Provability Logics into First-Order Logic. Pages 16–30 of: CAD'9. Lecture Notes in Artificial Intelligence, vol. 1632. Springer.

Demri, S., and Lugiez, D. 2010. Complexity of Modal Logics with Presburger Constraints. Journal of Applied Logic, 8(3), 233–252.Google Scholar

Demri, S., and Schnoebelen, Ph. 2002. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation, 174(1), 84–103.Google Scholar

Diekert, V., and Gastin, P. 2008. First-Order Definable Languages. Pages 261–306 of: Logic and Automata: History and Perspectives. Texts in Logic and Games, vol. 2. Amsterdam University Press.

Dima, C., and Tiplea, F.L. 2011. Model-Checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. CoRR, abs/1102.4225.

'ouza, D., and Shankar, P. (eds). 2012. Modern Applications of Automata Theory. IISc Research Monographs Series, no. 2. World Scientific.

Eisner, C., and Fisman, D. 2006. A Practical Introduction to PSL. Springer.

Emerson, E.A. 1983. Alternative Semantics for Temporal Logics. Theoretical Computer Science, 26(1–2), 121–130.Google Scholar

Emerson, E.A. 1990. Temporal and Modal Logics. In: Leeuwen (1990).

Emerson, E.A. 1995. Automated Temporal Reasoning about Reactive Systems. Pages 41–101 of: Banff Higher Order Workshop.

Emerson, E.A., and Clarke, E.M. 1980. Characterizing Correctness Properties of Parallel Programs Using Fixpoints. Pages 169–181 of: ICAL'0. Lecture Notes in Computer Science, vol. 85. Springer.

Emerson, E.A., and Halpern, J.Y. 1982. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. Pages 169–180 of: STO'2. ACM.

Emerson, E.A., and Halpern, J.Y. 1983. ‘Sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time. Pages 127–140 of: POP'3.

Emerson, E.A., and Halpern, J.Y. 1985. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. Journal of Computer and System Sciences, 30, 1–24.Google Scholar

Emerson, E.A., and Halpern, J.Y. 1986. ‘Sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time Temporal Logic. Journal of the Association for Computing Machinery, 33, 151–178.Google Scholar

Emerson, E.A., and Jutla, C.S. 1988. The Complexity of Tree Automata and Logics of Programs (Extended Abstract). Pages 328–337 of: FOC'8. IEEE.

Emerson, E.A., and Jutla, C.S. 1991. Tree Automata, Mu-Calculus and Determinacy (Extended Abstract). Pages 368–377 of: FOC'1. IEEE.

Emerson, E.A., and Jutla, C.S. 2000. The Complexity of Tree Automata and Logics of Programs. SIAM Journal of Computing, 29(1), 132–158.Google Scholar

Emerson, E.A., and Lei, C.-L. 1986 (16–18 June). Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). Pages 267–278 of: LIC'6. IEEE.

Emerson, E.A., and Lei, C.-L. 1987. Modalities for Model Checking: Branching Time Logic Strikes Back. Science of Computer Programming, 8(3), 275–306.Google Scholar

Emerson, E.A., and Sistla, A.P. 1984. Deciding Full Branching Time Logic. Information and Control, 61, 175–201.Google Scholar

Emerson, E.A., Jutla, C.S., and Sistla, A. 2001. On Model-Checking for μ-Calculus and Its Fragments. Theoretical Computer Science, 258(1–2), 491–522.Google Scholar

Etessami, K., Vardi, M.Y., and Wilke, Th. 1997. First-Order Logic with Two Variables and Unary Temporal logics. Pages 228–235 of: LIC'7. IEEE.

Fagin, R., Halpern, J.Y., Moses, Y., and Vardi, M.Y. 1995. Reasoning about Knowledge. MIT Press.

Fernandez, J.-C. 1990. An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming, 13(2–3), 219–236.Google Scholar

Fine, K. 1970. Propositional Quantifiers in Modal Logic. Theoria, 36, 336–346.Google Scholar

Fine, K. 1975. Some Connections between Elementary and Modal Logic. Pages 15–31 of: 3rd Scandinavian Logic Symposium. North-Holland.

Fischer, M., and Ladner, R. 1979. Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences, 18, 194–211.Google Scholar

Fisher, M. 2011. An Introduction to Practical Formal Methods Using Temporal Logic. Wiley.

Fisher, M., Dixon, C., and M., Peim. 2001. Clausal Temporal Resolution. ACM Transactions on Computational Logic, 2(1), 12–56.Google Scholar

Fitting, M. 1972. Tableau Methods of Proof for Modal Logics. Notre Dame Journal of Formal Logic, 18(2), 237–247.Google Scholar

Fitting, M. 1977. A Tableau System for Propositional S5. Notre Dame Journal of Formal Logic, 18(2), 292–294.Google Scholar

Fitting, M. 1983. Proof Methods for Modal and Intuitionistic Logics. D. Reidel.

Fitting, M. 2007. Modal Proof Theory. In: Blackburn et al. (2007).

Fogarty, S., Kupferman, O., Vardi, M.Y., and Wilke, Th. 2011. Unifying Buchi Complementation Constructions. Pages 248–263 of: CS'1. LIPIcs, for Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik.

Francez, N. 1986. Fairness. Springer-Verlag.

Friedmann, O. 2009. An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know It. Pages 145–156 of: LIC'9. IEEE.

Friedmann, O. 2010. The Stevens-Stirling-Algorithm for Solving Parity Games Locally Requires Exponential Time. International Journal of Foundations of Computer Science, 21(3), 277–287.Google Scholar

Friedmann, O. 2011a. An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms. Logical Methods in Computer Science, 7(3).Google Scholar

Friedmann, O. 2011b. Recursive Algorithm for Parity Games Requires Exponential Time. RAIRO – Theoretical Informatics and Applications, 45(4), 449–457.Google Scholar

Friedmann, O. 2013. A Superpolynomial Lower Bound for Strategy Iteration Based on Snare Memorization. Discrete Applied Mathematics, 161(10–11), 1317–1337.Google Scholar

Friedmann, O., and Lange, M. 2009. Solving Parity Games in Practice. Pages 182–196 of: ATV'9. Lecture Notes in Computer Science, vol. 5799. Springer.

Friedmann, O., and Lange, M. 2010. A Solver for Modal Fixpoint Logics. Pages 99–111 of: M4M-6. Lecture Notes in Theoretical Computer Science, 262, 99–111.

Friedmann, O., and Lange, M. 2012. Two Local Strategy Improvement Schemes for Parity Game Solving. International Journal of Foundations of Computer Science, 23(3), 669–685.Google Scholar

Friedmann, O., and Lange, M. 2013. Deciding the Unguarded Modal μ-Calculus. Journal of Applied Non-classical Logics, 23(4), 353–371.Google Scholar

Friedmann, O., Latte, M., and Lange, M. 2013. Satisfiability Games for Branching-Time Logics. Logical Methods in Computer Science, 9(4).Google Scholar

Gabbay, D.M. 1972. A General FiltrationMethod forModal Logics. Journal of Philosophical Logic, 1, 29–34.Google Scholar

Gabbay, D.M. 1976. Investigations in Modal and Tense Logics with Applications. D. Reidel.

Gabbay, D.M. 1981. Expressive Functional Completeness in Tense Logic. Pages 91–117 of: Aspects of Philosophical Logic. Reidel.

Gabbay, D.M. 1989. The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. Pages 409–448 of: Colloquium on Temporal Logic in Specification. Lecture Notes in Computer Science, vol. 398. Springer.

Gabbay, D.M., and Guenthner, F. (eds). 1984. Handbook of Philosophical Logic. Vol. 2. Reidel.

Gabbay, D.M., Pnueli, A., Shelah, S., and Stavi, J. 1980. On the Temporal Analysis of Fairness. Pages 163–173 of: POP'0.

Gabbay, D.M., Hodkinson, I., and Reynolds, M. 1994. Temporal Logic: Mathematical Foundations and Computational Aspects. Oxford University Press.

Gabbay, D.M., Kurucz, A., Wolter, F., and Zakharyaschev, M. 2003. Many-Dimensional Modal Logics: Theory and Practice. Cambridge University Press.

Gale, D., and Stewart, F. 1953. Infinite Games with Perfect Information: Contributions to the Theory of Games. Annals of Mathematics Studies, 28, 245–266.Google Scholar

Ganzinger, H., and de Nivelle, H. 1999. A Superposition Decision Procedure for the Guarded Fragment with Equality. Pages 295–305 of: LIC'9.

Gasquet, O., and Herzig, A. 1994. Translation-Based Deduction Methods for Modal Logics. Pages 399–408 of: IPM'4. Lecture Notes in Computer Science, vol. 945. Springer.

Gastin, P., and Oddoux, D. 2001. Fast LTL to Büchi Automata Translation. Pages 53–65 of: CA'1. Lecture Notes in Computer Science, vol. 2102. Springer.

German, S., and Sistla, A.P. 1992. Reasoning about Systems with Many Processes. Journal of the Association for Computing Machinery, 39(3), 675–735.Google Scholar

Glabbeek, R.J. van. 2001. The Linear Time – Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes. Chap. 1, pages 3–99 of: Handbook of Process Algebra. Elsevier.

Goldblatt, R. 1992. Logics of Time and Computation. 2nd edn. CSLI Lecture Notes, vol. 7. Center for the Study of Language and Information.

Goldblatt, R. 2005. Handbook of the History of Logic. Vol. 7. Elsevier.

Goldreich, O. 2008. Computational Complexity - A Conceptual Perspective. Cambridge University Press.

Goranko, V. 2000. Computation Tree Logics and Temporal Logics with Reference Pointers. Journal of Applied Non-classical Logics, 10(3–4), 221–242.Google Scholar

Goranko, V. 2001. Coalition Games and Alternating Temporal Logics. Pages 259–272 of: TARK VIII. Morgan Kaufmann.

Goranko, V., and Galton, A. 2015. Temporal Logics. Entry in the Stanford Encyclopaedia of Philosophy, http://plato.stanford.edu/entries/logic-temporal/.

Goranko, V., and Jamroga, W. 2004. Comparing Semantics of Logics for Multi-agent Systems. Synthese, 139(2), 241–280.Google Scholar

Goranko, V., and Otto, M. 2007. Model Theory of Modal Logic. In: Blackburn et al. (2007).

Goranko, V., and Shkatov, D. 2009a. Tableau-BasedDecision Procedure for Full Coalitional Multiagent Temporal-Epistemic Logic of Linear Time. Pages 969–976 of: AAMAS 2009. IFAAMAS.

Goranko, V., and Shkatov, D. 2009b. Tableau-Based Decision Procedure for the Full Coalitional Multiagent Logic of Branching Time. In: MALLO'9. CEUR Workshop Proceedings, vol. 494.

Goranko, V., and Shkatov, D. 2009c. Tableau-Based Decision Procedures for Logics of Strategic Ability in Multiagent Systems. ACM Transactions on Computational Logic, 11(1).Google Scholar

Goranko, V., and van Drimmelen, G. 2006. Complete Axiomatization and Decidability of the Alternating-Time Temporal Logic. Theoretical Computer Science, 353, 93–117.Google Scholar

Goranko, V., and Vester, S. 2014. Optimal Decision Procedures for Satisfiability in Fragments of Alternating-Time Temporal Logics. Pages 234–253 of: Advances in Modal Logic, vol. 10. College Publications.

Goranko, V., Kyrilov, A., and Shkatov, D. 2010. Tableau Tool for Testing Satisfiability in LTL: Implementation and Experimental Analysis. Electronic Notes in Theoretical Computer Science, 262, 113–125.Google Scholar

Goré, R. 1991. Semi-analytic Tableaux for Propositional Modal Logics with Applications to Nonmonotonicity. Logique et Analyse, 133–134, 73–104.Google Scholar

Goré, R. 1999. Tableaux Methods for Modal and Temporal Logics. Pages 297–396 of: Handbook of Tableaux Methods. Kluwer.

Goré, R., and Widmann, F. 2009. An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. Pages 437–452 of: CAD'9. Lecture Notes in Computer Science, vol. 5663. Springer.

Goré, R., and Widmann, F. 2010. Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse. Pages 225–239 of: IJCA'0. Lecture Notes in Computer Science, vol. 6173. Springer.

Gough, G. 1984. Decision Procedures for Temporal Logic. M. Phil. thesis, University of Manchester.

Grädel, E. 1999. On the Restraining Power of Guards. The Journal of Symbolic Logic, 64(4), 1719–1742.Google Scholar

Grädel, E. 2002. Model Checking Games. Pages 15–34 of: WOLLI'2. Electronic Notes in Theoretical Computer Science, vol. 67. Elsevier.

Grädel, E., Kolaitis, Ph., and Vardi, M.Y. 1997. On the Decision Problem for Two-Variable First-Order Logic. Bulletin of Symbolic Logic, 3(1), 53–69.Google Scholar

Grädel, E., Thomas, W., and Wilke, Th. (eds). 2002. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science, vol. 2500. Springer.

Grumberg, O., and Kurshan, R. 2001. Which Branching-Time Properties Are Effectively Linear. Journal of Logic and Computation, 11(2), 201–228.Google Scholar

Grumberg, O., and Veith, H. (eds). 2008. 25 Years of Model Checking. Lecture Notes in Computer Science, vol. 5000. Springer.

Gurevich, Y., and Harrington, L. 1982. Trees, Automata and Games. Pages 60–65 of: STO'2. ACM.

Gutierrez, J., Klaedtke, F., and Lange, M. 2014. The μ-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity. Theoretical Computer Science, 560(3), 292–306.Google Scholar

Hafer, T., and Thomas, W. 1987. Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree. Pages 270–279 of: ICAL'7. Lecture Notes in Computer Science, vol. 267. Springer.

Halpern, J.Y. 1995. The Effect of Bounding the Number of Primitive Propositions and the Depth of Nesting on the Complexity of Modal Logic. Artificial Intelligence, 75(2), 361–372.Google Scholar

Halpern, J.Y., and Reif, H. 1983. The Propositional Dynamic Logic of Deterministic,Well- Structured Programs. Theoretical Computer Science, 27, 127–165.Google Scholar

Halpern, J.Y., and Reif, J. 1981. The Propositional Dynamic Logic of Deterministic, Well- Structured Programs. Pages 322–344 of: FOC'1.

Harel, D. 1983. Recurring Dominoes:Making the Highly Undecidable Highly Understandable. Pages 177–194 of: Fundamentals of Computing Theory. Lecture Notes in Computer Science, vol. 158. Springer.

Harel, D. 1985. Recurring Dominoes:Making the Highly Undecidable Highly Understandable. Annals of Discrete Mathematics, 24, 51–72.Google Scholar

Harel, D., Kozen, D.C., and Tiuryn, J. 2000. Dynamic Logic. MIT Press.

Hartmanis, J., and Stearns, R. 1965. On the Computational Complexity of Algorithms. Transactions of the American Mathematical Society, 117, 285–306.Google Scholar

Heljanko, K., Keinänen, M., Lange, M., and Niemelä, I. 2012. Solving Parity Games by a Reduction to SAT. Journal of Computer and System Sciences, 78, 430–440.Google Scholar

Hemaspaandra, E. 1994. Complexity Transfer for Modal Logic (Extended Abstract). Pages 164–173 of: LIC'4. IEEE.

Hemaspaandra, E. 2001. The Complexity of Poor Man's Logic. Journal of Logic and Computation, 11(4), 609–622.Google Scholar

Hennessy, M., and Milner, R. 1980. On Observing Nondeterminism and Concurrency. Pages 299–309 of: ICAL'0. Lecture Notes in Computer Science, vol. 85. Springer.

Hennessy, M., and Milner, R. 1985. Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery, 32(1), 137–161.Google Scholar

Henriksen, J., and Thiagarajan, P. 1999. Dynamic Linear Time Temporal Logic. Annals of Pure and Applied Logic, 96(1–3), 187–207.Google Scholar

Henzinger, Th. A., and Prabhu, V.S. 2006. Timed Alternating-Time Temporal Logic. Pages 1–17 of: FORMAT'6.

Hintikka, J. 1962. Knowledge and Belief. Cornell University Press.

Hoare, C.A.R. 1985. Communicating Sequential Processes. Prentice Hall.

Hodges, W. 2013. Logic and Games. Entry in the Stanford Encyclopaedia of Philosophy, http://plato.stanford.edu/entries/logic-games/.

Hodkinson, I. 1999 (December). Notes on Games in Temporal Logics. Lectures notes for LUATCS Summer School, Johannesburg. Retrieved from http://www.doc.ic.ac.uk/imh/papers/sa.ps.gz.

Hodkinson, I., and Reynolds, M. 2005. Separation – Past, Present, and Future. Pages 117–142 of: Artemov, S., Barringer, H., 'vila Garcez, A., Lamb, L., and Woods, J. (eds), We Will Show Them! (Essays in Honour of Dov Gabbay on his 60th Birthday), vol. 2. College Publications.

Hoek, W. van der, Lomuscio, A., and Wooldridge, M. 2006. On the Complexity of Practical ATL Model Checking. Pages 201–208 of: AAMA'6.

Holzmann, G. 1997. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295.Google Scholar

Hughes, G., and Cresswell, M. 1984. A Companion to Modal Logic. Methuen.

Hughes, G., and Cresswell, M. 1996. A New Introduction to Modal Logic. Routledge.

Huth, M., and Ryan, M. 2000. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.

Iman, S., and Joshi, S. 2004. The e-Hardware Verification Language. Kluwer.

Immerman, N. 1988. Non deterministic Space Is Closed under Complementation. SIAM Journal of Computing, 17, 935–938.Google Scholar

Jamroga, W., and Bulling, N. 2011. Comparing Variants of Strategic Ability. Pages 252–257 of: IJCAI-11.

Jamroga, W., and Dix, J. 2008. Model Checking Abilities of Agents: A Closer Look. Theory of Computing Systems, 42(3), 366–410.Google Scholar

Janin, D., and Walukiewicz, I. 1996. On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic. Pages 263–277 of: CONCUR' 96. Lecture Notes in Computer Science, vol. 1119. Springer.

Johannsen, J., and Lange, M. 2003. CTL+ is Complete for Double Exponential Time. Pages 767 – 775 of: ICAL'3. Lecture Notes in Computer Science, vol. 2719. Springer.

Johnson, D. 2012. A Brief History of NP-Completeness, 1954–2012. Pages 359–376 of: Optimization Stories. DMV. Special volume of Documenta Mathematica.

Jónsson, B., and Tarski, A. 1951. Boolean Algebras with Operators. Part I. American Journal of Mathematics, 73, 891–939.Google Scholar

Jungteerapanich, N. 2009. A Tableau System for theModal μ-Calculus. Pages 220–234 of: TABLEAU'9. Lecture Notes in Computer Science, vol. 5607. Springer.

Jurdziński, M. 1998. Deciding the Winner in Parity Games is in UP n co-UP. Information Processing Letters, 68(3), 119–124.Google Scholar

Jurdziński, M. 2000. Small Progress Measures for Solving Parity Games. Pages 290–301 of: STAC'0. Lecture Notes in Computer Science, vol. 1770. Springer.

Jurdziński, M., Paterson, M., and Zwick, U. 2008. A Deterministic Subexponential Algorithm for Solving Parity Games. SIAM Journal of Computing, 38(4), 1519–1532.Google Scholar

Kähler, D., and Wilke, Th. 2008. Complementation, Disambiguation, and Determinization of Buchi Automata Unified. Pages 724–735 of: ICAL'8. Lecture Notes in Computer Science, vol. 5125. Springer.

Kaivola, R. 1995a. Axiomatising Linear Time Mu-Calculus. Pages 423–437 of: CONCUR ‘95. Lecture Notes in Computer Science, vol. 962. Springer.

Kaivola, R. 1995b. On Modal μ-Calculus and Buchi Tree Automata. Information Processing Letters, 54(1), 17–22.Google Scholar

Kamp, J. 1968. Tense Logic and the Theory of Linear Order. Ph.D. thesis, UCLA.

Kanellakis, P.C., and Smolka, S.A. 1983. CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Pages 228–240 of: POD'3. ACM.

Kanger, S. 1957. Provability in Logic. Stockholm Studies in Philosophy, University of Stockholm. Almqvist and Wiksell.

Karp, R.M. 1972. Reducibility among Combinatorial Problems. Pages 85–103 of: Miller, R.E., and Thatcher, J.W. (eds), Complexity of Computer Computations. Plenum Press.

Keller, R.M. 1976. Formal Verification of Parallel Programs. Communications of the ACM, 19(7), 371–384.Google Scholar

Kesten, Y., Manna, Z., McGuire, H., and Pnueli, A. 1993. A Decision Algorithm for Full Propositional Temporal Logic. Pages 97–109 of: CA'3, Lectures Notes in Computer Science, vol. 697. Springer.

Kindler, E. 1994. Safety and Liveness Properties: A Survey. Bulletin of the European Association of Theoretical Computer Science, 53, 268–272.Google Scholar

Klaedtke, F. 2002. Complementation of Buchi Automata Using Alternation. Pages 61–77 of: Gradel, E., Thomas, W., and Wilke, Th. (eds), Automata, Logics and Infinite Games. Lecture Notes in Computer Science, vol. 2500. Springer.

Klarlund, N. 1991. Progress Measures for Complementation of ω-Automata with Applications to Temporal Logic. Pages 358–367 of: FOC'1. IEEE.

Kozen, D.C. 1976 (June). On Parallelism in Turing Machines. Tech. rept. TR76-282. Department of Computer Science, Cornell University.

Kozen, D.C. 1983. Results on the Propositional μ-Calculus. Theoretical Computer Science, 27, 333–354.Google Scholar

Kozen, D.C. 1988. A Finite Model Theorem for the Propositional μ-Calculus. Studia Logica, 47(3), 233–241.Google Scholar

Kozen, D.C. 2006. Theory of Computation. Texts in Computer Science. Springer.

Kozen, D.C., and Parikh, R. 1983. A Decision Procedure for the Propositional μ-Calculus. Pages 313–325 of: Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 164. Springer.

Kozen, D.C., and Tiuryn, J. 1990. Logics of Programs. In: Leeuwen (1990).

Kracht, M. 1995. Tools and Techniques in Modal Logic. Studies in Logic and the Foundations of Mathematics, vol. 142. Elsevier.

Kripke, S. 1963. Semantical Analysis of Modal Logic I. Normal Modal Propositional Calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 9, 67–96.Google Scholar

Kroger, F. 1987. Temporal Logic of Programs. EATCS Monographs in Computer Science, vol. 8. Springer.

Kroger, F., and Merz, S. 2008. Temporal Logic and State Systems. EATCS Texts in Theoretical Computer Science. Springer.

Kuhtz, L., and Finkbeiner, B. 2009. LTL Path Checking Is Efficiently Parallelizable. Pages 235–246 of: ICAL'9. Lecture Notes in Computer Science, vol. 5556. Springer.

Kupferman, O., and Grumberg, O. 1996. Buy One, Get One Free!!. Journal of Logic and Computation, 6(4), 523–539.Google Scholar

Kupferman, O., and Pnueli, A. 1995. Once and for All. Pages 25–35 of: LIC'5. IEEE Computer Society Press.

Kupferman, O., and Vardi, M.Y. 2001. Weak Alternating Automata Are Not That Weak. ACM Transactions on Computational Logic, 2(3), 408–429.Google Scholar

Kupferman, O., Vardi, M.Y., and Wolper, P. 2000. An Automata-Theoretic Approach to Branching-Time Model Checking. Journal of the Association for Computing Machinery, 47(2), 312–360.Google Scholar

Kupferman, O., Piterman, N., and Vardi, M.Y. 2001 (August). Extended Temporal Logic Revisited. Pages 519–535 of: CONCU'1. Lecture Notes in Computer Science, vol. 2154. Springer.

Kupferman, O., Safra, S., and Vardi, M.Y. 2006. Relating Word and Tree Automata. Annals of Pure and Applied Logic, 138, 126–146.Google Scholar

Kupferman, O., Pnueli, A., and Vardi, M.Y. 2012. Once and for All. Journal of Computer and System Sciences, 78(3), 981–996.Google Scholar

Kučera, A., and Strejček, J. 2005. The Stuttering Principle Revisited. Acta Informatica, 41(7–8), 415–434.Google Scholar

Ladner, R. 1977. The Computational Complexity of Provability in Systems of Modal Propositional Logic. SIAM Journal of Computing, 6(3), 467–480.Google Scholar

Lamport, L. 1977. Proving the Correctness of Multiprocess Programs. IEEE Transactions in Software Engineering, 3(2), 125–143.Google Scholar

Lamport, L. 1980. “Sometime” Is Sometimes “Not Never” – on the Temporal Logic of Programs. Pages 174–185 of: POP'0.

Lange, M. 2002a. Games for Modal and Temporal Logics. Ph.D. thesis, LFCS, Division of Informatics, The University of Edinburgh. Tech. Rep. ECS-LFCS-03-431.

Lange, M. 2002b. Local Model Checking Games for Fixed Point Logic with Chop. Pages 240–254 of: CONCU'2. Lecture Notes in Computer Science, vol. 2421. Springer.

Lange, M. 2005. Solving Parity Games by a Reduction to SAT. In: Proc. Int. Workshop on Games in Design and Verification, GD'5.

Lange, M. 2007. Linear Time Logics around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness. Pages 90–104 of: CONCU'7. Lecture Notes in Computer Science, vol. 4703. Springer.

Lange, M. 2008. A Purely Model-Theoretic Proof of the Exponential Succinctness Gap between CTL+ and CTL. Information Processing Letters, 108(5), 308–312.Google Scholar

Lange, M., and Lozes, E. 2012. Model Checking the Higher-Dimensional Modal μ- Calculus. Pages 39–46 of: FIC'2. Electronic Notes in Theoretical Computer Science, vol. 77. Elsevier.

Lange, M., and Stirling, C. 2000. Model Checking Games for CTL*. Pages 115–125 of: ICT'0.

Lange, M., and Stirling, C. 2001. Focus Games for Satisfiability and Completeness of Temporal Logic. Pages 357–365 of: LIC'1. IEEE.

Lange, M., and Stirling, C. 2002. Model Checking Games for Branching Time Logics. Journal of Logic and Computation, 12(4), 623–639.Google Scholar

Lange, M., Lozes, E., and Guzman, M. Vargas. 2014. Model-Checking Process Equivalences. Theoretical Computer Science, 560, 326–347.Google Scholar

Laroussinie, F. 1994. Logique temporelle avec passé pour la spécification et la vérification des systèmes réactifs. Ph.D. thesis, Institut National Polytechnique de Grenoble.

Laroussinie, F. 1995. About the Expressive Power of CTL Combinators. Information Processing Letters, 54, 343–345.Google Scholar

Laroussinie, F. 2010. Temporal Logics for Games. Bulletin of the European Association of Theoretical Computer Science, 100, 79–98.Google Scholar

Laroussinie, F., and Schnoebelen, Ph. 1995. A Hierarchy of Temporal Logics with Past. Theoretical Computer Science, 148, 303–324.Google Scholar

Laroussinie, F., and Schnoebelen, Ph. 2000. Specification in CTL+Past for Verification in CTL. Information and Computation, 156(1–2), 236–263.Google Scholar

Laroussinie, F., Markey, N., and Schnoebelen, P. 2001. Model Checking CTL+ and FCTL Is Hard. Pages 318–331 of: FOSSAC'1. Lecture Notes in Computer Science, vol. 2030. Springer.

Laroussinie, F., Markey, N., and Schnoebelen, Ph. 2002. Temporal Logic with Forgettable Past. Pages 383–392 of: LIC'2. IEEE.

Laroussinie, F., Markey, N., and Oreiby, G. 2008. On the Expressiveness and Complexity of ATL. Logical Methods in Computer Science, 4(2).Google Scholar

Leeuwen, J. van (ed). 1990. Handbook of Theoretical Computer Science. Vol. B: Formal Models and Semantics. MIT Press.

Lehmann, D., Pnueli, A., and Stavi, J. 1981. Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. Pages 264–277 of: ICAL'1. Lecture Notes in Computer Science, Vol. 115. Springer.

Lemmon, E.J., Scott, D., and Segerberg, K. 1977. An Introduction to Modal Logic: Lemmo' Notes. American Philosophical Quarterly.

Lenzi, G. 1996. A Hierarchy Theorem for the μ-Calculus. Pages 87–97 of: ICAL'6. Lecture Notes in Computer Science, vol. 1099. Springer.

Lewis, H. 1980. Complexity Results for classes of Quantificational formulas. Journal of Computer and System Sciences, 21, 317–353.Google Scholar

Lichtenstein, O., and Pnueli, A. 2000. Propositional Temporal Logics: Decidability and Completeness. Logic Journal of the IGPL, 8(1), 55–85.Google Scholar

Lichtenstein, O., Pnueli, A., and Zuck, L. 1985. The Glory of the Past. Pages 196–218 of: Brooklyn College Conference on Logics of Programs. Lecture Notes in Computer Science, vol. 193. Springer.

Loding, Ch., and Thomas, W. 2000. Alternating Automata and Logics over Infinite Words. Pages 521–535 of: IFIP TCS' 2000. Lecture Notes in Computer Science, vol. 1878. Springer.

Lopes, A. Da Costa, Laroussinie, F., and Markey, N. 2010. ATL with Strategy Contexts: Expressiveness and Model Checking. Pages 120–132 of: FSTTC'0.

Lubarsky, R.S. 1993. μ-Definable Sets of Integers. The Journal of Symbolic Logic, 58(1), 291–313.Google Scholar

Ludwig, W. 1995. A Subexponential Randomized Algorithm for the Simple Stochastic Game Problem. Information and Computation, 117(1), 151–155.Google Scholar

Mader, A. 1997a. Verification ofModal Properties Using Boolean Equation Systems. Ph.D. thesis, Munich, University of Technology.

Mader, A. 1997b. Verification of Modal Properties Using Boolean Equation Systems. Bertz.

Manna, Z., and Pnueli, A. 1979. The Modal Logic of Programs. Pages 385–409 of: ICAL'9. Lecture Notes in Computer Science, vol. 71. Springer.

Manna, Z., and Pnueli, A. 1981. Verification of Concurrent Programs: The Temporal Framework. Pages 215–273 of: Boyer, R., and Moore, J. (eds), The Correctness Problem in Computer Science. Academic Press.

Manna, Z., and Pnueli, A. 1990. A Hierarchy of Temporal Properties. Pages 377–408 of: POD'0. ACM Press.

Manna, Z., and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specifications. Springer.

Manna, Z., and Pnueli, A. 1995. Temporal Verification of Reactive Systems: Safety. Springer.

Markey, N. 2002. Past If for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In: EXPRES'2. Electronic Notes in Theoretical Computer Science, vol. 68. Elsevier.

Markey, N. 2004. Past Is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. Acta Informatica, 40(6–7), 431–458.Google Scholar

Markey, N., and Schnoebelen, Ph. 2003. Model Checking a Path. Pages 251–261 of: CONCUR' 03. Lecture Notes in Computer Science, vol. 2761. Springer.

Marx, M., and Venema, Y. 1997. Multi-dimensional Modal Logic. Applied Logic. Kluwer.

Mateescu, R. 2002. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. Pages 281–295 of: TACA'2. Lecture Notes in Computer Science, vol. 2280. Springer.

McMillan, K. 1993. Symbolic Model Checking. Kluwer Academic.

McNaughton, R. 1993. Infinite Games Played on Finite Graphs. Annals of Pure and Applied Logic, 65(2), 149–184.Google Scholar

Meyer, A.R. 1973. Weak Second Order Theory of Successor Is Not Elementary-Recursive. Tech. rept. MAC TM-38. MIT.

Meyer, A.R. 1975. Weak Monadic Second-Order Theory of Successor Is Not Elementary Recursive. Pages 132–154 of: Logic Colloquium. Lecture Notes in Mathematics, vol. 453. Springer.

Michel, M. 1984. Algebre demachines et logique temporelle. Pages 287–298 of: STAC'4. Lecture Notes in Computer Science, vol. 166. Springer.

Michel, M., and Stefani, J.-B. 1988. Interval Logics and Sequential Transducers. Pages 244–257 of: CAA'8. Lecture Notes in Computer Science, vol. 299. Springer.

Milner, R. 1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer.

Mints, G. 1988. Gentzen-Type and Resolution Rules Part I: Propositional Logic. Pages 198–231 of: International Conference on Computer Logic, Tallinn. Lecture Notes in Computer Science, vol. 417. Springer.

Miyano, S., and Hayashi, T. 1984. Alternating Finite Automata on ω-Words. Theoretical Computer Science, 32(3), 321–330.Google Scholar

Mogavero, F., Murano, A., and Vardi, M.Y. 2010a. Reasoning about Strategies. Pages 133–144 of: FSTTC'0.

Mogavero, F., Murano, A., and Vardi, M.Y. 2010b. Relentful Strategic Reasoning in Alternating-Time Temporal Logic. Pages 371–386 of: LPA'0.

Mogavero, F., Murano, A., Perelli, G., and Vardi, M.Y. 2012. What MakesATL* Decidable? A Decidable Fragment of Strategy Logic. Pages 193–208 of: CONCU'2.

Moller, F., and Rabinovich, A. 2003. Counting on CTL*: On the Expressive Power of Monadic Path Logic. Information and Computation, 184(1), 147–159.Google Scholar

Moore, R.C. 1977. Reasoning about Knowledge and Action. Pages 223–227 of: IJCAI-5.

Morgan, Ch. 1976. Methods for Automated Theorem Proving in Non-classical Logics. IEEE Transactions on Computers, 25(8), 852–862.Google Scholar

Mortimer, M. 1975. On Language with Two Variables. Zeitschrift fürMathematische Logik und Grundlagen der Mathematik, 21, 135–140.Google Scholar

Moschovakis, Y.N. 2006. Notes on Set Theory. 2nd edn. Undergraduate Texts in Mathematics. Springer.

Mostowski, A.W. 1984. Regular Expressions for Infinite Trees and a Standard Form of Automata. Pages 157–168 of: 5th Symp. on Computation Theory. Lecture Notes in Computer Science, vol. 208. Springer.

Mukund, M. 2012. Finite-State Automata on Infinite Inputs. Pages 45–78 of: 'ouza, D., and Shankar, P. (eds), Modern Applications of Automata Theory. IISc Research Monographs Series, vol. 2. World Scientific.

Muller, D.E. 1963. Infinite Sequences and Finite Machines. Pages 3–16 of: 4th IEEE Symposium on Switching Circuit Theory and Logical Design. IEEE.

Muller, D.E., and Schupp, P.E. 1987. Alternating Automata on Infinite Trees. Theoretical Computer Science, 54, 267–276.Google Scholar

Muller, D.E., and Schupp, P.E. 1995. Simulating Alternating Tree Automata by Non deterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141(1–2), 69–107.Google Scholar

Muller, D.E., Saoudi, A., and Schupp, P.E. 1986. Alternating Automata, theWeak Monadic Theory of the Tree and Its Complexity. Pages 275–283 of: ICAL'6. Lecture Notes in Computer Science, vol. 226. Springer.

Muller, D.E., Saoudi, A., and Schupp, P.E. 1988. Weak Alternating Automata Give a Simple Explanation ofWhy Most Temporal and Dynamic Logics Are Decidable in Exponential Time. Pages 422–427 of: LIC'8. IEEE.

Muller-Olm, M. 1999. A Modal Fixpoint Logic with Chop. Pages 510–520 of: STAC'9. Lecture Notes in Computer Science, vol. 1563. Springer.

Nakamura, A., and Ono, H. 1980. On the Size of RefutationKripkeModels for Some Linear Modal and Tense Logics. Studia Logica, 39(4), 325–333.Google Scholar

Nivelle, H. de, Schmidt, R., and Hustadt, U. 2000. Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL, 8(3), 265–292.Google Scholar

Niw'ski, D. 1986. On Fixed-Point Clones. Pages 464–473 of: ICAL'6. Lecture Notes in Computer Science, vol. 226. Springer.

Niw'ski, D. 1997. Fixed Point Characterization of Infinite Behavior of Finite-State Systems. Theoretical Computer Science, 189(1–2), 1–69.Google Scholar

Niw'ski, D. 2002. μ-Calculus via Games. Pages 27–43 of: CS'2. Lecture Notes in Computer Science, vol. 2471. Springer.

Niw'ski, D., and Walukiewicz, I. 1996. Games for themu-Calculus. Theoretical Computer Science, 163(1–2), 99–116.Google Scholar

Nonnengart, A. 1996. Resolution-Based Calculi for Modal and Temporal Logics. Pages 599–612 of: CAD'6. Lecture Notes in Artificial Intelligence, vol. 1104. Springer.

Ohlbach, H.J. 1993. Translation Methods for Non-classical Logics: An Overview. Bulletin of the Interest Group in Propositional and Predicate Logics, 1(1), 69–90.Google Scholar

Ohlbach, H.J., Nonnengart, A., de Rijke, M., and Gabbay, D.M. 2001. Encoding Two- Valued Non-classical Logics in Classical Logic. Pages 1403–1486 of: Handbook of Automated Reasoning. MIT Press.

Ohrstrom, P., and Hasle, P.F. V. 1995. Temporal Logic: From Ancient Ideas to Artificial Intelligence. Springer.

Orłowska, E. 1988. Relational Interpretation of Modal Logics. Pages 443–471 of: Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai 54. North-Holland.

Otto, M. 1999. Bisimulation-Invariant PTIME and Higher-Dimensional μ-Calculus. Theoretical Computer Science, 224(1–2), 237–265.Google Scholar

Paige, R., and Tarjan, R.E. 1987. Three Partition Refinement Algorithms. SIAM Journal of Computing, 16(6), 973–989.Google Scholar

Papadimitriou, C.H. 1994. Computational Complexity. Addison-Wesley.

Park, D. 1970. Fixpoint Induction and Proof of Program Semantics. Pages 59–78 of: Machine Intelligence, vol. 5. Edinburgh University Press.

Park, D. 1981. Concurrency and Automata on Infinite Sequences. Pages 167–183 of: 5th GI Conference on Theoretical Computer Science, Karlsruhe, Germany. Lecture Notes in Computer Science, vol. 104. Springer.

Pauly, M. 2001a. Logic for Social Software. Ph.D. thesis, University of Amsterdam. ILLC Dissertation Series 2001-10.

Pauly, M. 2001b. A Logical Framework for Coalitional Effectivity in Dynamic Procedures. Bulletin of Economic Research, 53(4), 305–324.Google Scholar

Pauly, M. 2002. A Modal Logic for Coalitional Power in Games. Journal of Logic and Computation, 12(1), 149–166.Google Scholar

Pecuchet, J.-P. 1986. On the Complementation of Buchi Automata. Theoretical Computer Science, 47(1), 95–98.Google Scholar

Peled, D., and Wilke, Th. 1997. Stutter-Invariant Temporal Properties Are Expressible without the Next-Time Operator. Information Processing Letters, 63, 243–246.Google Scholar

Perrin, D., and Pin, J.-E. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Elsevier.

Petersson, V., and Vorobyov, S. 2001. A Randomized Subexponential Algorithm for Parity Games. Nordic Journal of Computing, 8(3), 324–345.Google Scholar

Pinchinat, S. 1992. Ordinal Processes in Comparative Concurrency Semantics. Pages 293–305 of: CS'1. Lecture Notes in Computer Science, vol. 626. Springer.

Piterman, N. 2000. Extending Temporal Logic with ω-Automata. M.Phil. thesis, The Weizmann Institute of Science.

Piterman, N. 2006. From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata. Pages 255–264 of: LIC'6. IEEE.

Plotkin, G. 1981. A Structural Approach to Operational Semantics. Tech. report DAIMI FN-19. Aarhus Univ.

Pnueli, A. 1977. The Temporal Logic of Programs. Pages 46–57 of: FOC'7. IEEE.

Pnueli, A. 1979. The Temporal Semantics of Concurrent Programs. Pages 1–20 of: International Symposium on Semantics of Concurrent Computation 1979. Lecture Notes in Computer Science, vol. 70. Springer.

Poizat, B. 1982. Deux ou trois choses que je sais de Ln . The Journal of Symbolic Logic, 47, 641–658.Google Scholar

Popkorn, S. 1992. First Steps in Modal Logic. Cambridge University Press.

Pratt, V. 1979. A Practical Decision Method for Propositional Dynamic Logic. Pages 326–337 of: 10th Annual ACM Symposium on the Theory of Computing. ACM.

Pratt, V. 1980. A Near Optimal Method for Reasoning about Actions. Journal of Computer and System Sciences, 20, 231–254.Google Scholar

Pratt, V.R. 1981. A Decidable mu-Calculus. Pages 421–427 of: FOC'1. IEEE.

Prior, A.N. 1957. Time and Modality. Clarendon Press.

Prior, A.N. 1967. Past, Present and Future. Oxford University Press.

Prior, A.N. 1968. Papers on Time and Tense. University of Oxford Press.

Prior, A.N. 1977. Worlds, Times and Selves. Edited by K., Fine. University of Massachusetts Press.

Puri, A. 1995. Theory of Hybrid Systems and Discrete Event Systems. Ph.D. thesis, University of California, Berkeley.

Queille, J.-P., and Sifakis, J. 1982a. Specification and Verification of Concurrent Systems in CESAR. Pages 337–351 of: FOC'2. IEEE.

Queille, J.-P., and Sifakis, J. 1982b. A Temporal Logic to Deal with Fairness in Transition Systems. Pages 217–225 of: FOC'2. IEEE.

Rabin, M. 1969. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 41, 1–35.Google Scholar

Rabin, M. 1970. Weakly Definable Relations and Special Automata. Pages 1–23 of: Symposium on Mathematical Logic and Foundations of Set Theory. North-Holland.

Rabinovich, A. 2014. A Proof of Kamp's Theorem. Logical Methods in Computer Science, 10(1).Google Scholar

Rescher, N., and Urquhart, A. 1971. Temporal Logic. Springer.

Reynolds, M. 2000. More Past Glories. Pages 229–240 of: LIC'0. IEEE.

Reynolds, M. 2001. An Axiomatization of Full Computation Tree Logic. Journal of Symbolic Logic, 66(3), 1011–1057.Google Scholar

Reynolds, M. 2007. A Tableau for Bundled CTL*. Journal of Logic and Computation, 17(1), 117–132.

Reynolds, M. 2009. A Tableau for CTL*. Pages 403–418 of: F'9. Lecture Notes in Computer Science, vol. 5850, Springer.

Reynolds, M. 2011. A Tableau-Based Decision Procedure for CTL*. Formal Aspects of Computing, 23(6), 739–779.Google Scholar

Reynolds, M. 2013. A Faster Tableau for CTL*. Pages 50–63 of: G and AL'013.

Rich, D.I. 2003. The Evolution of System Verilog. IEEE Design and Test of Computers, 20(4), 82–84.Google Scholar

Rohde, S. 1997. Alternating Automata and the Temporal Logic of Ordinals. Ph.D. thesis, University of Illinois.

Rosenstein, J.G. 1982. Linear Ordering. Academic Press.

Safra, S. 1988. On the Complexity of ω-Automata. Pages 319–327 of: FOC'8. IEEE.

Safra, S. 1989. Complexity of Automata on Infinite Objects. Ph.D. thesis, Weizmann Institute of Science.

Sangiorgi, D. 2009. On the Origins of Bisimulation and Coinduction. ACM Transactions on Programming Languages and Systems (TOPLAS), 31(4).Google Scholar

Sangiorgi, D., and Rutten, J. (eds). 2012. Advanced Topics in Bisimulation and Coinduction. Cambridge Tracts in Theoretical Computer Science, vol. 52. Cambridge University Press.

Sattler, U., and Vardi, M.Y. 2001. The Hybrid μ-Calculus. Pages 76–91 of: IJCA'1. Lecture Notes in Computer Science, vol. 2083. Springer.

Savitch, W.J. 1970. Relationships between Nondeterministic and Deterministic Tape Complexities. Journal of Computer and System Sciences, 4(2), 177–192.Google Scholar

Schewe, S. 2007. Solving Parity Games in Big Steps. Pages 449–460 of: FSTTC'7. Lecture Notes in Computer Science, vol. 4855. Springer.

Schewe, S. 2008a. ATL* Satisfiability is 2 EXPTIME-Complete. Pages 373–385 of: ICAL'8. Lecture Notes in Computer Science, vol. 5126. Springer.

Schewe, S. 2008b. An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games. Pages 369–384 of: CS'8. Lecture Notes in Computer Science, vol. 5213. Springer.

Schewe, S. 2009. Tighter Bounds for the Determinisation of Buchi Automata. Pages 167–181 of: FOSSAC'9. Lecture Notes in Computer Science, vol. 5504. Springer.

Schewe, S., and Finkbeiner, B. 2006. Satisfiability and Finite Model Property for the Alternating-Time mu-Calculus. Pages 591–605 of: CS'6. Lecture Notes in Computer Science, vol. 4207. Springer.

Schneider, K. 2004. Verification of Reactive Systems: Formal Methods and Algorithms. Springer.

Schnoebelen, Ph. 2003. The Complexity of Temporal Logic Model Checking. Pages 393–436 of: AiM'2. Advances in Modal Logic, vol. 4. King's College.

Schobbens, P.-Y. 2004. Alternating-Time Logic with Imperfect Recall. Electronic Notes in Theoretical Computer Science, 85(2), 82–93.Google Scholar

Schwendimann, S. 1998a. Aspects of Computational Logic. Ph.D. thesis, Universitat Bern, Switzerland.

Schwendimann, S. 1998b. A New One-Pass Tableau Calculus for PLTL. Pages 277–291 of: TABLEAU'8. Lecture Notes in Artificial Intelligence, vol. 1397. Springer.

Scott, D. 1962. A Decision Method for Validity of Sentences in Two Variables. The Journal of Symbolic Logic, 27, 377.Google Scholar

Segerberg, K. 1971. An Essay in Classical Modal Logic. Filosofiska Studier 13. University of Uppsala.

Seidl, H. 1996. Fast and Simple Nested Fixpoint. Information Processing Letters, 59(6), 303–308.Google Scholar

Seidl, H., and Neumann, A. 1999. On Guarding Nested Fixpoints. Pages 484–498 of: CS'9. Lecture Notes in Computer Science, vol. 1683. Springer.

Sifakis, J. 1980. Deadlocks and Livelocks in Transition Systems. Pages 587–600 of: MFC'0. Lecture Notes in Computer Science, vol. 88. Springer.

Sistla, A.P. 1983. Theoretical Issues in the Design of Distributed and Concurrent Systems. Ph.D. thesis, Harvard University.

Sistla, A.P., and Clarke, E.M. 1982. The Complexity of Propositional Linear Temporal Logic. Pages 159–168 of: STOC'2. ACM.

Sistla, A.P., and Clarke, E.M. 1985. The Complexity of Propositional Linear Temporal Logics. Journal of the ACM, 32(3), 733–749.Google Scholar

Sistla, A.P., Vardi, M.Y., and Wolper, P. 1987. The Complementation Problem for Buchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49, 217–237.Google Scholar

Slutzki, G. 1987. Alternating Tree Automata. Theoretical Computer Science, 41, 305–318.Google Scholar

Smullyan, R.M. 1968. First-Order Logic. Springer.

Spaan, E. 1993a. Complexity of Modal Logics. Ph.D. thesis, ILLC, Amsterdam University.

Spaan, E. 1993b. The Complexity of Propositional Tense Logics. Pages 287–309 of: de Rijke, M. (ed), Diamonds and Defaults. Series Studies in Pure and Applied Intensional Logic, vol. 229. Kluwer Academic.

Stevens, P., and Stirling, C. 1998. Practical Model-Checking Using Games. Pages 85–101 of: TACAS. Lecture Notes in Computer Science, vol. 1384. Springer.

Stirling, C. 1987. Comparing Linear and Branching Time Temporal Logics. Pages 1–20 of: Banieqbal, B., Barringer, H., and Pnueli, A. (eds), Temporal Logic in Specification. Lecture Notes in Computer Science, vol. 398. Springer.

Stirling, C. 1992. Modal and Temporal Logics. Pages 477–563 of: Handbook of Logic in Computer Science, vol. 2 (Background: Computational Structures). Clarendon Press.

Stirling, C. 1995. Local Model Checking Games. Pages 1–11 of: CONCU'5. Lecture Notes in Computer Science, vol. 962. Springer.

Stirling, C. 1996. Games and Modal Mu-Calculus. Pages 298–312 of: TACA'6. Lecture Notes in Computer Science, vol. 1055. Springer.

Stirling, C. 1999. Bisimulation, Modal Logic and Model Checking Games. Logic Journal of the IGPL, 7(1), 103–124.Google Scholar

Stirling, C. 2001. Modal and Temporal Properties of Processes. Springer.

Stirling, C., and Walker, D. 1989. Local Model Checking in the Modal Mu-Calculus. Pages 369–383 of: TAPSOFT, vol. 1. Lecture Notes in Computer Science, vol. 351. Springer.

Straubing, H. 1994. Finite Automata, Formal Logic, and Circuit Complexity. Progress in Theoretical Computer Science. Birkhauser.

Streett, R.S. 1982. Propositional Dynamic Logic of Looping and Converse Is Elementarily Decidable. Information and Control, 54(1/2), 121–141.Google Scholar

Streett, R.S., and Emerson, E.A. 1984. The Propositional μ-Calculus Is Elementary. Pages 465–472 of: ICAL'4. Lecture Notes in Computer Science, vol. 172. Springer.

Streett, R.S., and Emerson, E.A. 1989. An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus. Information and Computation, 81(3), 249–264.Google Scholar

Sundholm, G. 2001. Systems of Deduction. Pages 1–52 of: Gabbay, D.M., and Guenthner, F. (eds), Handbook of Philosophical Logic, vol. 2. Springer–Science & Business Media, B.V.

Szelepcsenyi, R. 1988. The Method of Forced Enumeration for Nondeterministic Automata. Acta Informatica, 26(3), 279–284.Google Scholar

Tarjan, R.E. 1972. Depth-First Search and Linear Graph Algorithms. SIAM Journal of Computing, 1, 146–160.Google Scholar

Thomas, W. 1990. Automata on Infinite Objects. Pages 133–191 of: van Leeuwen, J. (ed), Handbook of Theoretical Computer Science, Volume B, Formal Models and Semantics. Elsevier.

Thomas, W. 1999. Complementation of Buchi Automata Revisited. Pages 109–122 of: J., Karhumaki et al. (ed), Jewels Are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa. Springer.

Thomason, R.H. 1984. Combinations of Tense and Modality. In: Gabbay and Guenthner (1984).

Troquard, N., and Walther, D. 2012. On Satisfiability of ATL with Strategy Contexts. Pages 398–410 of: JELI'2. Lecture Notes in Artificial Intelligence, vol. 7519. Springer.

van Benthem, J. 1976. Modal Correspondence Theory. Ph.D. thesis, Mathematical Institute, Amsterdam University.

van Benthem, J. 1984. Correspondence Theory. In: Gabbay and Guenthner (1984).

van Benthem, J. 1985. Modal Logic and Classical Logic. Bibliopolis.

van Benthem, J. 1993. The Logic of Time. 2nd edn. Kluwer Academic.

van Benthem, J. 1995. Temporal Logic. Pages 241–351 of: Gabbay, D.M., Hogger, C.J., and Robinson, J.A. (eds), Handbook of Logic in Artificial Intelligence and Logic Programming: Epistemic and Temporal Reasoning, vol. 4. Oxford University Press.

van Benthem, J. 2014. Logic in Games. MIT Press.

van Benthem, J., and Bergstra, J.A. 1995. Logic of Transition Systems. Journal of Logic, Language and Information, 3(4), 247–283.Google Scholar

van Benthem, J., van Eijck, D., and Stebletsova, V. 1993. Modal Logic, Transition Systems and Processes. Tech. rept. CS-R9321. Centrum voor Wiskunde en Informatica, Amsterdam.

van Dalen, D. 2004. Logic and Structure. Springer.

van Drimmelen, G. 2003. Satisfiability in Alternating-Time Temporal Logic. Pages 208–217 of: LIC'3.

van Emde Boas, P. 1997. The Convenience of Tilings. Pages 331–363 of: Complexity, Logic, and Recursion Theory. Lecture Notes in Pure and Applied Mathematics, vol. 187. Marcel Dekker.

Vardi, M.Y. 1988. A Temporal Fixpoint Calculus. Pages 250–259 of: POP'8. ACM.

Vardi, M.Y. 1991. Verification of Concurrent Programs: The Automata-Theoretic Framework. Annals of Pure and Applied Logic, 51(1–2), 79–98.Google Scholar

Vardi, M.Y. 1996. An Automata-Theoretic Approach to Linear Temporal Logic. Pages 238–266 of: Moller, F., and Birtwistle, G. (eds), Logics of Concurrency: Structure versus Automata. Lecture Notes in Computer Science, vol. 1043. Springer.

Vardi, M.Y. 1997. Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. Pages 191–206 of: CAD'7. Lecture Notes in Computer Science, vol. 1249. Springer.

Vardi, M.Y. 2001. Branching vs. Linear Time: Final Showdown. Pages 1–22 of: TACA'1. Lecture Notes in Computer Science, vol. 2031. Springer.

Vardi, M.Y. 2007. Automata-Theoretic Techniques for Temporal Reasoning. Pages 971–990 of: Blackburn, P., Benthem, J. van, and Wolter, F. (eds), Handbook of Modal Logic. Elsevier.

Vardi, M.Y. 2009. From Philosophical to Industrial Logics. Pages 89–115 of: ICL'9. Lecture Notes in Computer Science, vol. 5378. Springer.

Vardi, M.Y., and Stockmeyer, L.J. 1985. Improved Upper and Lower Bounds for Modal Logics of Programs. Pages 240–251 of: STO'5. ACM.

Vardi, M.Y., and Wilke, Th. 2007. Automata: From Logics to Algorithms. Pages 629–736 of: Logic and Automata: History and Perspectives. Texts in Logic and Games, no. 2. Amsterdam University Press.

Vardi, M.Y., and Wolper, P. 1983. Yet Another Process Logic (Preliminary Version). Pages 501–512 of: Logic of Programs. Lecture Notes in Computer Science, vol. 164. Springer.

Vardi, M.Y., and Wolper, P. 1986a. Automata-Theoretic Approach to Automatic Program Verification. Pages 322–331 of: LIC'6. IEEE.

Vardi, M.Y., and Wolper, P. 1986b. Automata-Theoretic Techniques for Modal Logics of Programs. Journal of Computer and System Sciences, 32, 183–221.Google Scholar

Vardi, M.Y., and Wolper, P. 1994. Reasoning about Infinite Computations. Information and Computation, 115, 1–37.Google Scholar

Viswanathan, M., and Viswanathan, R. 2004. A Higher Order Modal Fixed Point Logic. Pages 512–528 of: CONCU'4. Lecture Notes in Computer Science, vol. 3170. Springer.

Voge, J., and Jurdz'ski, M. 2000. A Discrete Strategy Improvement Algorithm for Solving Parity Games. Pages 202–215 of: CA'0. Lecture Notes in Computer Science, vol. 1855. Springer.

Walther, D., Lutz, C., Wolter, F., and Wooldridge, M. 2006. ATL Satisfiability Is Indeed ExpTime-Complete. Journal of Logic and Computation, 16(6), 765–787.Google Scholar

Walther, D., van der Hoek, W., and Wooldridge, W. 2007. Alternating-Time Temporal Logic with Explicit Strategies. Pages 269–278 of: TARK ‘07. ACM.

Walukiewicz, I. 1996. Monadic Second Order Logic on Tree-Like Structures. Pages 401–413 of: STAC'6. Lecture Notes in Computer Science, vol. 1046. Springer.

Walukiewicz, I. 2000. Completeness of Kozen's Axiomatisation of the Propositional μ- Calculus. Information and Computation, 157(1–2), 142–182.Google Scholar

Widmann, F. 2010. Tableaux-Based Decision Procedures for Fixed Point Logics. Ph.D. thesis, Australian National University.

Wilke, Th. 1999. CTL+ Is Exponentially More Succinct than CTL. Pages 110–121 of: FSTTC'9. Lecture Notes in Computer Science, vol. 1999. Springer.

Wolper, P. 1981. Temporal Logic Can Be More Expressive. Pages 340–348 of: FOC'1.

Wolper, P. 1983. Temporal Logic Can Be More Expressive. Information and Control, 56, 72–99.Google Scholar

Wolper, P. 1985. The Tableau Method for Temporal Logic: An Overview. Logique et Analyse, 110–111, 119–136.Google Scholar

Wolper, P. 1989. On the Relation of Programs and Computations to Models of Temporal Logic. Pages 75–123 of: Banieqbal, B., Barringer, H., and Pnueli, A. (eds), Temporal Logic in Specification. Springer.

Wolper, P. 2000. Constructing Automata from Temporal Logic Formulas: A Tutorial. Pages 261–277 of: European Educational Forum: School on Formal Methods and Performance Analysis. Lecture Notes in Computer Science, vol. 2090. Springer.

Zanardo, A. 1996. Branching Time Logic with Quantification over Branches: The Point of View of Modal Logic. The Journal of Symbolic Logic, 61, 1–39.Google Scholar

Zeman, J. 1973. The Lewis-Modal Systems. Clarendon Press.

Zielonka, W. 1998. Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theoretical Computer Science, 200(1–2), 135–183.Google Scholar