Temporal Logics

Temporal Logics are a rich variety of logical systems designed for formalising reasoning about time, and about events and changes in the world over time. These systems differ by the ontological assumptions made about the nature of time in the associated models, by the logical languages involving various operators for composing temporalized expressions, and by the formal logical semantics adopted for capturing the precise intended meaning of these temporal operators. Temporal logics have found a wide range of applications as formal frameworks for temporal knowledge representation and reasoning in artificial intelligence, and as tools for formal specification, analysis, and verification of properties of computer programs and systems. This Element aims at providing both a panoramic view on the landscape of the variety of temporal logics and closer looks at some of their most interesting and important landmarks. Cover Title Page Imprints Page Temporal Logics Contents Preface 1 Temporal Reasoning and Logics: Introduction and a Brief Historical Overview 1.1 What Is Time? 1.2 What Is Temporal Logic? 1.3 Origins and Antiquity: Zeno’s Paradoxes and Sea-Battles 1.4 Time, Necessity, and Determinism: Diodorus Cronus’ Master Argument 1.5 Medieval Times: Determinism versus Free Will 1.6 Precursors to Temporal Logic 1.7 The Birth of Temporal Logic: Prior and Post-Prior Some References 2 The Variety of Models of Time 2.1 Instant-Based Models of Time and Their Properties 2.2 Interval-Based Models of Time 2.3 Instant-Based versus Interval-Based Models of Time Some References 3 Prior’s Basic Systems of Temporal Logic 3.1 Prior’s Tense Operators 3.2 Semantics of TL 3.3 Standard Translation of TL into First-Order Logic 3.4 Tense Logic and McTaggart’s time series 3.5 Axiomatic System K[sub(t)] for TL 3.6 Expressing Temporal Properties in TL: Extensions of K[sub(t)] Some References 4 Temporal Logics for Linear Time 4.1 Adding the Nexttime Operator 4.2 Adding Since and Until 4.3 Axiomatic Systems for Since and Until 4.4 The Linear Time Temporal Logic (LTL) 4.4.1 Formal Language and Expressing Properties in LTL 4.4.2 Formal Semantics of LTL 4.4.3 Axiomatic System for LTL and Variations Some References 5 Reasoning about Non-determinism: Models and Logics for Branching Time 5.1 Prior’s Formal Reconstruction of Diodorus Cronus’ Master Argument 5.2 Lavenham’s Deterministic Argument Formalised 5.3 Prior’s Theory of Branching Time 5.4 Tree-Like Models for Branching Time: Bundled Trees 5.5 Logics for Branching Time Structures with the Basic Priorian Semantics Some References 6 The Peircean Branching Time Logic PBTL 6.1 Language, Models, and Semantics of PBTL 6.2 Some Validities and Non-validities of PBTL 6.3 Axiomatic Systems for PBTL 6.4 Computation Tree Logic CTL 6.4.1 The Language and Semantics of CTL 6.4.2 Unfoldings and Semantics of CTL on Kripke Models 6.4.3 Extension of the Semantics of LTL to Kripke Models 6.4.4 A Sound and Complete Axiomatic System for CTL Some References 7 The Ockhamist Branching Time Logic OBTL 7.1 Language and Models for OBTL 7.2 Expressing Temporal Statements in OBTL 7.3 Formal Semantics of OBTL 7.3.1 Ockhamist Truth on a Branch in an OBTL Model 7.3.2 Some Validities and Non-validities of OBTL 7.3.3 Ockhamist Validity versus Bundled Trees Validity 7.4 Embedding PBTL into OBTL 7.5 Full Computation Tree Logic CTL* 7.6 Axiomatic Systems for Ockhamist Validity 7.7 Some Variations of Branching Time Semantics 7.8 Aristotle’s ‘Sea-Battle Tomorow’ Revisited in Branching Time Models Some References 8 First-Order Temporal Logics 8.1 Existence and Quantification in Time 8.2 Preliminaries: First-Order Relational Structures and Languages 8.3 The Language and Models of FOTL 8.4 Semantics of FOTL 8.4.1 Variable Assignments and Truth of FOTL Formulae 8.4.2 Varying and Constant Domain Semantics 8.4.3 Temporal Barcan Formulae 8.5 Eternalist Quantification and Constant Domain Semantics 8.5.1 On Validities and Non-validities in Constant Domain Semantics 8.5.2 An Axiomatic System for the Eternalist Semantics 8.6 Presentist Quantification and Varying Domain Semantics 8.6.1 The Barcan Formulae and Varying Domain Semantics 8.6.2 An Axiomatic System for Presentist Semantics 8.7 The Existence Predicate 8.8 On Proper Names, Definite Descriptions, Rigid and Non-rigid Designations 8.9 On Technical Results for First-Order Temporal Logics Some References 9 Variations, Extensions, and Applications of Temporal Logics 9.1 Interval Temporal Logics 9.2 Hybrid, Metric, and Real-Time Temporal Logics 9.3 Combining Temporal and Other Logics 9.4 On Logical Deduction and Decision Methods for Temporal Logics 9.5 On Applications of Temporal Logics 9.5.1 Temporal Logics in Computer Science 9.5.2 Temporal Logics in Artificial Intelligence 9.5.3 Temporal Logics in Natural Language Semantics and Linguistics Some References 9.6 Finally, on What Is Not in the Element Epilogue: Past, Present, and Future of Temporal Logics References Acknowledgements