This long awaited book gives a thorough account of the mathematical foundations of Temporal Logic, one of the most important areas of logic in computer science.The book, which consists of fifteen chapters, moves on from giving a solid introduction in semantical and axiomatic approaches to temporal logic to covering the central topics of predicate temporal logic, meta-languages, general theories of axiomatization, many dimensional systems, propositionalquantifiers, expressive power, Henkin dimension, temporalization of other logics, and decidability results.Much of the research presented here (...) is frontline in the new results and in the unifying methodology. This is an indispensable reference work for both the pure logician and the theoretical computer scientist. (shrink)

It is shown that the decision problem for the temporal logic with until and since connectives over real-numbers time is PSPACE-complete. This is the most practically useful dense time temporal logic.

In this paper we shall introduce a simple temporal logic suitable for reasoning about the temporal aspects of parallel universes, parallel processes, distributed systems, or multiple agents. We will use a variant of the mosaic method to prove decidability of this logic. We also show that the logic does not have the finite model property. This shows that the mosaic method is sometimes a stronger way of establishing decidability.

We give a Hilbert style axiomatization for the set of formulas in the temporal language with Until and Since which are valid over the real number flow of time. The axiomatization, which is orthodox in the sense of only having the usual temporal rules of inference, is complete with respect to single formulas.

We present a Hilbert style axiomatisation for the set of formulas in the temporal language with F and P which are valid over non-transitive cyclical flows of time. We also give a simpler axiomatisation using the slightly controversial 'irreflexivity rule' and go on to prove the decidability of any temporal logic over cyclical time provided it uses only connectives with first-order tables.

We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.We also add a few axioms to find a sound and complete axiomatisation for the first order temporal logic of Until and Since over rational numbers time.

We introduce a new way of defining metric temporal logic on a real-numbers flow of time. The idea is based on having semantics which allow us to refer to a single universal clock of arbitrary precision in order to impose metric constraints. This gives us a new metric temporal logic which is very expressive, is natural to use, can be applied in very general situations, affords a wide range of useful abbreviations and operators, has a PSPACE decision procedure, and has (...) the promise of being amenable to standard reasoning techniques. Thus it has many advantages over the existing metric temporal logics. We provide a decision procedure via conversion to a non-metric temporal logic, hence doing metric reasoning with no clocks. (shrink)

This paper compares the recently proposed Robust Full Computational Tree Logic to model robustness in concurrent systems with other computational tree logic -based logics. RoCTL* extends CTL* with the addition of the operators Obligatory and Robustly, which quantify over failure-free paths and paths with one more failure respectively. This paper focuses on examining the succinctness and expressiveness of RoCTL* by presenting translations to and from RoCTL*. The core result of this paper is to show that RoCTL* is expressively equivalent to (...) CTL* but is non-elementarily more succinct. That is, RoCTL* does not add any expressive power over CTL*, but can represent some properties using vastly reduced formulae. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula, as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense th.. (shrink)