Thus, the Ockhamist truth of an atomic proposition depends both on the time instant and on the possible future on which it is considered. In general, not all histories in the temporal frame may be of interest, and in order to define Ockhamist type semantics it suffices to consider rich enough families of histories, called a bundles.
We say that a formula of OBTL is bundled tree valid BT-valid if it is true on every branch of every bundled tree model. We note that, as proved in Zanardo et al. In such frames, branches are abstract primitive entities and the relations between branches that correspond to the modal and temporal operators in OBTL are explicitly given as part of the definition of the model. Visually, these are horizontal slices through the bundle of all histories. On the other hand, it turns out that bundled tree validity is strictly weaker than the Ockhamist validity, i. All these intermediate histories may belong to the bundle, while the limit history may not be in it.
Thus, to completely axiomatize Ockhamist validity we must add axioms that capture the limit closure property of complete bundled trees. Reynolds proposed complete axiomatic systems for OBTL for both BT-validity and Ockhamist validity, assuming instant-based atomic propositions. Several extensions and variations of OBTL have been proposed and studied. For instance, Brown and Goranko extend the language of OBTL with a modality for an alternative branch and a special sort of fan-variables representing all histories stemming from one instant, and axiomatise the resulting logic.
Another extension along similar lines is Ciuni and Zanardo For more related results, see also Thomason , Zanardo ; , Reynolds ; Complete finitary axiomatisation of Peircean temporal logic for BT-validity has been obtained by Burgess using a version of the Irreflexivity rule IRR, and Zanardo without using such a rule, but with infinitely many axioms, including a very complex axiom schema. See Reynolds for more details.
Branching time logics are much used in computer science. They are variations of the Peircean and Ockhamist logics presented above, but essentially restricted to the class of trees where every history has the order type of the natural numbers. Such trees, called computation trees , are naturally obtained as tree unfoldings of discrete transition systems, hence they naturally represent the tree of all infinite computations arising in such systems. The most popular branching time logics used in computer science are:. The logic CTL became widely used owing to its good computational properties with regard to model checking , which has linear complexity both in the size of the input formula and in the size of the input model as a finite transition system.
For references and further details, see Emerson and Stirling For completeness proofs of versions of this axiomatic system for CTL, see Goldblatt and Emerson We note that all logics mentioned in this section have the finite model property and are decidable. Proofs of decidability of the respective logics can be found e.
While the technical reductions between instant-based and interval based models can be used to reconcile different philosophical and ontological standpoints, they do not resolve the main semantic issue arising when developing logical formalisms for capturing temporal reasoning, viz. The possible natural answers to this question lead to three reasonable alternatives, respectively giving rise to point-based logics discussed above, interval-based logics , and mixed, two-sorted logics , where points and intervals are considered as separate sorts on a par and formulae for both sorts are constructed.
We will only discuss here purely interval-based temporal logics, while for a recent study and technical exploration of the two-sorted approach we refer to Balbiani et al. There have been various proposals and developments of interval-based temporal logics. However, some quite non-trivial decidable cases of fragments of HS have been identified. This interpretation has been fruitfully explored to relate various technical results, such as undecidability, between spatial and interval logics, see e. Lastly, a few words about the relationships between the expressiveness of the languages of interval temporal logics and first-order logic.
It was shown in Bresolin et al. So far we have discussed the traditional hierarchy of temporal logics, but there are numerous alternative developments which do not fit this hierarchy, and yet can be useful formalisms for various applications. We briefly present some of them here.
logic. In fact, propositional temporal logics are an extension of We will summarize important results on decidability, axiomatizability, . that in linear temporal logics each time point is followed by only one operators are included in the syntax PSPACE-completeness is PhD thesis, University of. Udine. This is a timed extension of LTL. [Koy90] Koymans. . Tense logic and the theory of linear order (PhD Thesis UCLA ). [GPSS80] Gabbay .. The reachability problem is decidable (and PSPACE-complete) for timed automata [AD94].
A notable development, enriching the traditional framework of temporal logics, is to incorporate features of first-order logic to produce a family of so-called hybrid logics , that blend together the language and metalanguage of temporal logic. Hybrid logics are very expressive, yet they often preserve the good computational properties of standard temporal logic. See more details and references e. Metric temporal logics go back to Prior, too. We can define the general, non-metric operators respectively by.
For more on metric and layered temporal logics see Montanari and Montanari and Policriti For metric neighborhood interval logics see Bresolin et al. Various real-time extensions of temporal logics have also been proposed and studied, for instance by adding:. Such real-time extensions are usually very expressive and often lead to logics with undecidable decision problems. For further details see Alur and Henzinger ; ; , as well as Reynolds ; on the real-time linear temporal logic RTL and the survey Konur Propositional temporal logics can be extended with quantifiers over atomic propositions, see Rescher and Urquhart , Chapter XIX.
Semantically, these quantify over all valuations of the atomic propositions, so they are monadic second-order quantifiers. The resulting languages are very expressive and the respective logics are usually undecidable, often not even recursively axiomatizable. Some complete axiomatic systems for quantified propositional temporal logics have been designed, see Kesten and Pnueli and French and Reynolds for QPTL with and without past operators, also providing proofs of decidability. Logics are often used to reason about dynamically changing structures or aspects of the world.
It is therefore very natural to consider the evolution over time of such structures by adding a temporal dimension to them. This leads to the idea of adding a temporal dimension to a logic designed to reason about such models, that is to enrich the logical language with temporal operators suitable for reasoning about the evolution of the models over time. A prime example is first-order temporal logic, discussed in Section 8. Various modal logics can also be naturally temporalized and the relations between time and modality is one of the central questions in the philosophical study of modal logic.
The study of historical necessity is another important example of philosophical analysis of a modality from temporal logic perspective. From a technical viewpoint, there are several ways of combining models and logical systems and, in particular, of temporalising a logic : products, fusions, etc.
Some generic questions of transfer of logical properties , such as axiomatisations, completeness, decidability, etc. Decidability, for instance, is usually preserved in fusions, while it is often lost in products of logical systems. For general discussion and study of temporalizing logical systems and properties of temporised logics, see Finger and Gabbay ; , Finger et al.
Here we only briefly present and discuss some of the most popular cases of temporalized logical systems. Temporal Logic is obtained by adding the tense operators to an existing logic; above this was tacitly assumed to be the classical Propositional Calculus.
Other temporal-logical systems are obtained by taking different logical bases. Of obvious interest is tensed predicate logic, where the tense operators are added to classical First-order Predicate Calculus. This enables us to express important distinctions concerning the logic of time and existence. For example, the statement A philosopher will be a king can be interpreted in several different ways, such as. The interpretation of such formulae is not unproblematic, however. The problem concerns the domain of quantification. These problems are related to the so-called Barcan formulae of modal logic, a temporal analogue of which is.
Temporal first-order logics are typically highly undecidable. Few axiomatizable, and even fewer decidable, natural fragments of first-order temporal logics have been identified and investigated so far, including notably the monodic fragment , see Hodkinson et al. Temporal-epistemic logics combine temporal and multi-agent logics of knowledge. These were developed in various ways during the s, with a unifying study by Halpern and Vardi , who considered a variety of 96 temporal-epistemic logics with semantics based on so-called interpreted systems : sets of runs in a transition system with epistemic indistinguishability relations on the state space for each agent.
The variety is based on six parameters: number of agents one or many , the language with or without common knowledge, linear or branching time, etc. For further detail see Halpern and Vardi , Fagin et al.
Temporal reasoning is an important aspect of reasoning about agency. In particular, a temporal dimension has gradually been introduced explicitly into the STIT models and logics; for a recent account see Lorrini , which gives formal semantics and complete axiomatisations of temporal STIT logics. They have subsequently become a very popular logical framework for strategic reasoning in multiagent systems.
So, the one-step single-agent strategic operator in ATL is technically very similar to the stit operator of Belnap and Perloff, Even though the latter are quite more expressive languages, they generally preserving the good computational properties of the former. For further details see Alur et al. Space and time are intimately related in the physical world, and have become inseparable in modern physical theories.
Combined logical reasoning about space-time has been actively evolving over the past decades, particularly in the context of Artificial Intelligence, spatio-temporal databases, ontologies and constraint networks. The main focus of recent research is on logical characterisation of spatio-temporal models, expressiveness and computational complexity Kontchakov et al.
Description logics are very close to modal logics. They involve concepts unary predicates and roles binary predicates and are used to describe various ontologies and the relations between concepts in them. For further detail see e. Baader and Lutz Description logics can naturally be temporalized in various ways, see Artale and Franconi , Wolter and Zakharyaschev , and Lutz et al.
Temporal logical reasoning can naturally be build on, or combined with, various non-classical logical systems resulting, for instance, in many-valued temporal logics Rescher and Urquhart , Chapter XVIII , intuitionistic temporal logics Ewald , constructive and paraconsistent temporal logics Kamide and Wansing ; , probabilistic temporal logics Hart and Sharir ; Konur , etc. Extensive research and numerous publications over the past 50 years have developed a variety of logical deduction systems and decision methods for the temporal logics mentioned here and many more.
Hilbert style axiomatic systems have been the most commonly developed logical deduction systems for temporal logics. Besides, many complete systems of semantic tableaux , sequent calculi , and resolution-based systems have been developed for various temporal logics. It is beyond the scope and space of this entry to provide any comprehensive account of these, so here we only list some general references on deductive systems for temporal logics, in addition to the more specific references mentioned elsewhere in this text: Rescher and Urquhart , Burgess , Goldblatt , Emerson , Gabbay et al.
Particularly efficient and practically useful are the tableaux-based methods for deciding satisfiability.