Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
  1. Home
  2. Books
  3. Temporal Logics in Computer Science
  • Cited by 53
Publisher:
Cambridge University Press
Online publication date:
October 2016
Print publication year:
2016
Online ISBN:
9781139236119
DOI:
https://doi.org/10.1017/CBO9781139236119
Subjects:
Algorithmics, Complexity, Computer Algebra, Computational Geometry, Computer Science, Logic, Philosophy, Programming Languages and Applied Logic
Series:
Cambridge Tracts in Theoretical Computer Science (58)
Information

Book description

This comprehensive text provides a modern and technically precise exposition of the fundamental theory and applications of temporal logics in computer science. Part I presents the basics of discrete transition systems, including constructions and behavioural equivalences. Part II examines the most important temporal logics for transition systems and Part III looks at their expressiveness and complexity. Finally, Part IV describes the main computational methods and decision procedures for model checking and model building - based on tableaux, automata and games - and discusses their relationships. The book contains a wealth of examples and exercises, as well as an extensive annotated bibliography. Thus, the book is not only a solid professional reference for researchers in the field but also a comprehensive graduate textbook that can be used for self-study as well as for teaching courses.

Reviews

'In summary, the book presents the most important and influential temporal logics, presents their properties, and introduces the most important tools to reason about temporal logics. It strikes a good balance between breadth and depth in coverage …'

Martin Zimmermann Source: MathSciNet

Refine List

Actions for selected content:

Select all | Deselect all
  • View selected items
  • Export citations
  • Download PDF (zip)
  • Save to Kindle
  • Save to Dropbox
  • Save to Google Drive

Save Search

You can save your searches here and later view and run them again in "My saved searches".

Please provide a title, maximum of 40 characters.
Cancel
×

Contents

Contents
References
References
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.
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.
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.
Å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.
Alberucci, L., and Facchini, A. 2009. The Modal μ-Calculus over Restricted Classes of Transition Systems. The Journal of Symbolic Logic, 74(4), 1367–1400.
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.
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.
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.
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.
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.
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.
Arnold, A., and Nivat, M. 1980. The Metric Space of Infinite Trees. Algebraic And Topological Properties. Fundamenta Informaticae, 3(4), 181–205.
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.
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).
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.
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.
Beth, E.W. 1955. Semantic Entailment and Formal Derivability. Nieuwe Reeks, 18(13), 309–342.
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.
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.
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.
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.
Browne, M., Clarke, E., and Grumberg, O. 1988. Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science, 59, 115–131.
Bruse, F., Friedmann, O., and Lange, M. 2015. On Guarded Transformation in the μ- Calculus. Logic Journal of the IGPL 23(2), 194–216.
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.
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.
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.
Chatterjee, K., Henzinger, T.A., and Piterman, N. 2010. Strategy Logic. Information and Computation, 208(6), 677–693.
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.
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.
Cleaveland, R. 1989. Tableau-Based Model Checking in the Propositional Mu-Calculus. Acta Informatica, 27(8), 725–747.
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.
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.
'gostino, G., Montanari, A., and Policriti, A. 1995. A Set-Theoretical Translation Method for Polymodal Logics. Journal of Automated Reasoning, 15, 317–337.
'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.
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.
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.
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.
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.
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.
Demri, S., and Schnoebelen, Ph. 2002. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation, 174(1), 84–103.
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.
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.
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.
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.
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.
Emerson, E.A., and Sistla, A.P. 1984. Deciding Full Branching Time Logic. Information and Control, 61, 175–201.
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.
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.
Fine, K. 1970. Propositional Quantifiers in Modal Logic. Theoria, 36, 336–346.
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.
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.
Fitting, M. 1972. Tableau Methods of Proof for Modal Logics. Notre Dame Journal of Formal Logic, 18(2), 237–247.
Fitting, M. 1977. A Tableau System for Propositional S5. Notre Dame Journal of Formal Logic, 18(2), 292–294.
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.
Friedmann, O. 2011a. An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms. Logical Methods in Computer Science, 7(3).
Friedmann, O. 2011b. Recursive Algorithm for Parity Games Requires Exponential Time. RAIRO – Theoretical Informatics and Applications, 45(4), 449–457.
Friedmann, O. 2013. A Superpolynomial Lower Bound for Strategy Iteration Based on Snare Memorization. Discrete Applied Mathematics, 161(10–11), 1317–1337.
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.
Friedmann, O., and Lange, M. 2013. Deciding the Unguarded Modal μ-Calculus. Journal of Applied Non-classical Logics, 23(4), 353–371.
Friedmann, O., Latte, M., and Lange, M. 2013. Satisfiability Games for Branching-Time Logics. Logical Methods in Computer Science, 9(4).
Gabbay, D.M. 1972. A General FiltrationMethod forModal Logics. Journal of Philosophical Logic, 1, 29–34.
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.
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.
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.
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.
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).
Goranko, V., and van Drimmelen, G. 2006. Complete Axiomatization and Decidability of the Alternating-Time Temporal Logic. Theoretical Computer Science, 353, 93–117.
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.
Goré, R. 1991. Semi-analytic Tableaux for Propositional Modal Logics with Applications to Nonmonotonicity. Logique et Analyse, 133–134, 73–104.
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.
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.
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.
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.
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.
Halpern, J.Y., and Reif, H. 1983. The Propositional Dynamic Logic of Deterministic,Well- Structured Programs. Theoretical Computer Science, 27, 127–165.
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.
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.
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.
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.
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.
Henriksen, J., and Thiagarajan, P. 1999. Dynamic Linear Time Temporal Logic. Annals of Pure and Applied Logic, 96(1–3), 187–207.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Kozen, D.C. 1988. A Finite Model Theorem for the Propositional μ-Calculus. Studia Logica, 47(3), 233–241.
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.
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.
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.
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.
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.
Kupferman, O., Pnueli, A., and Vardi, M.Y. 2012. Once and for All. Journal of Computer and System Sciences, 78(3), 981–996.
Kučera, A., and Strejček, J. 2005. The Stuttering Principle Revisited. Acta Informatica, 41(7–8), 415–434.
Ladner, R. 1977. The Computational Complexity of Provability in Systems of Modal Propositional Logic. SIAM Journal of Computing, 6(3), 467–480.
Lamport, L. 1977. Proving the Correctness of Multiprocess Programs. IEEE Transactions in Software Engineering, 3(2), 125–143.
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.
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.
Lange, M., Lozes, E., and Guzman, M. Vargas. 2014. Model-Checking Process Equivalences. Theoretical Computer Science, 560, 326–347.
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.
Laroussinie, F. 2010. Temporal Logics for Games. Bulletin of the European Association of Theoretical Computer Science, 100, 79–98.
Laroussinie, F., and Schnoebelen, Ph. 1995. A Hierarchy of Temporal Logics with Past. Theoretical Computer Science, 148, 303–324.
Laroussinie, F., and Schnoebelen, Ph. 2000. Specification in CTL+Past for Verification in CTL. Information and Computation, 156(1–2), 236–263.
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).
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.
Lichtenstein, O., and Pnueli, A. 2000. Propositional Temporal Logics: Decidability and Completeness. Logic Journal of the IGPL, 8(1), 55–85.
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.
Ludwig, W. 1995. A Subexponential Randomized Algorithm for the Simple Stochastic Game Problem. Information and Computation, 117(1), 151–155.
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.
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.
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.
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.
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.
Mortimer, M. 1975. On Language with Two Variables. Zeitschrift fürMathematische Logik und Grundlagen der Mathematik, 21, 135–140.
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.
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.
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.
Nivelle, H. de, Schmidt, R., and Hustadt, U. 2000. Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL, 8(3), 265–292.
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.
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.
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.
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.
Paige, R., and Tarjan, R.E. 1987. Three Partition Refinement Algorithms. SIAM Journal of Computing, 16(6), 973–989.
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.
Pauly, M. 2002. A Modal Logic for Coalitional Power in Games. Journal of Logic and Computation, 12(1), 149–166.
Pecuchet, J.-P. 1986. On the Complementation of Buchi Automata. Theoretical Computer Science, 47(1), 95–98.
Peled, D., and Wilke, Th. 1997. Stutter-Invariant Temporal Properties Are Expressible without the Next-Time Operator. Information Processing Letters, 63, 243–246.
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.
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.
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.
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.
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).
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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
Slutzki, G. 1987. Alternating Tree Automata. Theoretical Computer Science, 41, 305–318.
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.
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.
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.
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.
Tarjan, R.E. 1972. Depth-First Search and Linear Graph Algorithms. SIAM Journal of Computing, 1, 146–160.
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.
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.
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.
Vardi, M.Y., and Wolper, P. 1994. Reasoning about Infinite Computations. Information and Computation, 115, 1–37.
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.
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.
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.
Wolper, P. 1985. The Tableau Method for Temporal Logic: An Overview. Logique et Analyse, 110–111, 119–136.
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.
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.

Metrics

Altmetric attention score

Full text views

Total number of HTML views: 0
Total number of PDF views: 0 *
Loading metrics...

Book summary page views

Total views: 0 *
Loading metrics...

* Views captured on Cambridge Core between #date#. This data will be updated every 24 hours.

Usage data cannot currently be displayed.