Calculi of temporal logic are widely used in modern computer science. The temporal organization of information flows in the different architectures of laptops, the Internet, or supercomputers would not be possible without appropriate temporal calculi. In the age of digitalization and High-Tech applications, people are often not aware that temporal logic is deeply rooted in the philosophy of modalities. A deep understanding of these roots opens avenues to the modern calculi of temporal logic which have emerged by extension of modal logic with temporal operators.
Computationally, temporal operators can be introduced in different formalisms with increasing complexity such as Basic Modal Logic (BML), Linear-Time Temporal Logic (LTL), Computation Tree Logic (CTL), and Full Computation Tree Logic (CTL*). Proof-theoretically, these formalisms of temporal logic can be interpreted by the sequent calculus of Gentzen, the tableau-based calculus, automata-based calculus, game-based calculus, and dialogue-based calculus with different advantages for different purposes, especially in computer science.
The book culminates in an outlook on trendsetting applications of temporal logics in future technologies such as artificial intelligence and quantum technology. However, it will not be sufficient, as in traditional temporal logic, to start from the everyday understanding of time. Since the 20th century, physics has fundamentally changed the modern understanding of time, which now also determines technology. In temporal logic, we are only just beginning to grasp these differences in proof theory which needs interdisciplinary cooperation of proof theory, computer science, physics, technology, and philosophy.
Author(s): Stefania Centrone, Klaus Mainzer
Edition: 1
Publisher: World Scientific
Year: 2023
Language: English
Pages: 208
Tags: Temporal Logic
Contents
Preface
About the Authors
1. Philosophical Roots of Temporal Logic
1.1. The Concept of Time
1.1.1. Aristotelean temporal logic
1.1.2. Linear and branching temporal logic
1.1.3. Temporal logic of modern physics
1.2. Toward Formal Systems of Temporal Logic
1.2.1. Modo recto and modo obliquo
1.2.2. Intuitionism and the relationship of modalities and temporality
1.2.3. Becker’s modal-logical interpretation of intuitionism
1.2.4. Intuitionism and formal systems of temporal logic
1.2.5. Outlook on temporal logic in computer science
2. Computational Foundations of Temporal Logic
2.1. Basic Modal Logic
2.1.1. Syntax of BML
2.1.2. Semantics of BML
2.1.3. Axiomatic system AxSysBML for BML
2.2. Linear-Time Temporal Logic
2.2.1. Syntax of LTL
2.2.2. Semantics of LTL
2.2.3. Decidability problems of LTL
2.2.4. Axiomatic system AxSysLTL for LTL
2.3. Computation Tree Logic
2.3.1. Temporal logic of reachability
2.3.2. Computation tree logic
2.4. Full Computation Tree Logic
2.4.1. Syntax of CTL*
2.4.2. Semantics of CTL*
2.4.3. Axiomatic system AxSysCTL∗ for CTL∗
2.4.4. Ockhamist CTL*
3. Proof-Theoretical Foundations of Temporal Logic
3.1. Gentzen Calculus and Temporal Logic
3.1.1. Gentzen’s calculus for classical propositional logic in a nutshell
3.1.2. What is a (good) sequent-style calculus?
3.1.3. Sequent-style calculi for TL
3.1.4. Sequent-style calculi for LTL and CTL: A challenge
3.2. Tableaux-Based Calculus and Temporal Logic
3.2.1. What are tableaux?
3.2.2. Basics of tableau construction in basic modal logic
3.2.3. Basics of tableau construction in linear temporal logic
3.3. Automata-Based Calculus and Temporal Logic
3.3.1. What are Büchi automata?
3.3.2. Büchi automata for linear temporal logic
3.3.3. Büchi tree automata for branching-time logic CTL
3.4. Game-Based Calculus and Temporal Logic
3.4.1. Game-based calculus of basis modal logic
3.4.2. Game-based calculus and certification of computer programs
3.4.3. Game-based solution to the model-checking problem for CTL∗
3.4.4. Game-based solution to the satisfiability problem for CTL∗
3.5. Dialogue-Based Constructive Temporal Logic
3.5.1. Dialogue-based introduction of constructive logical operators
3.5.2. Constructive dialogue games
3.5.3. Constructive formal dialogue games
3.5.4. Constructive dialogue-based logic as Gentzen’s intuitionistic calculus G3
3.5.5. Dialogue-based modal logic
3.5.6. Dialogue-based temporal logic
4. Applications and Outlook of Temporal Logic
4.1. Temporal Logic in Artificial Intelligence and Machine Learning
4.1.1. Symbolic AI
4.1.2. Subsymbolic AI
4.1.2.1. Example: Neural networks
4.1.3. Statistical and causal learning
4.1.3.1. Example: Reinforcement learning
4.1.4. Hybrid AI
4.1.5. Reinforcement learning with temporal logic
4.1.6. Policy search in reinforcement learning
4.1.7. Truncated linear temporal logic for reinforcement learning
4.1.7.1. Example: Goal reaching while avoiding obstacles
4.1.7.2. Example: Pick-and-placement tasks of robots
4.1.8. Temporal logic LTL for reinforcement learning
4.2. Temporal Logic in Relativistic Physics
4.2.1. Temporal logic of time frames
4.2.2. Time frames of Minkowskian space-time
4.2.3. Modal and temporal logics for continuous and discrete space-time
4.2.4. Conceptual foundations of general relativity
4.2.5. Temporal logics of general relativity
4.2.6. Temporal logic of black holes
4.3. Temporal Logic in Quantum Computing
4.3.1. Basics of quantum computing
4.3.2. Quantum bits as state vectors of the Bloch sphere
4.3.3. Circuits with quantum operators
4.3.4. No cloning theorem
4.3.5. Unitary transformations
4.3.6. Computation by circuits of a quantum computer
4.3.7. Reading out the results of a quantum computer
4.3.8. Architecture of quantum circuits
4.3.9. What does entanglement mean?
4.3.10. Entanglement and quantum communication
4.3.11. Temporal logic for quantum state transformation
4.4. Societal Impact of Temporal Logic
4.4.1. Generations of quantum technologies
4.4.2. From logical–mathematical foundations to machine learning and quantum technology
References
Index
