We show that the satisfiability problem for the monodic guarded, loosely guarded, and packed fragments of first-order temporal logic with equality is 2Exptime-complete for structures with arbitrary first-order domains, over linear time, dense linear time, rational number time, and some other classes of linear flows of time. We then show that for structures with finite first-order domains, these fragments are also 2Exptime-complete over real number time and hence over most of the commonly used linear flows of time, including the natural (...) numbers, integers, rationals, and any first-order definable class of linear flows of time. (shrink)

We define the logic FOTLT(n), to be a monadic monodic fragment of first-order linear temporal logic, with 2n propositions representing the read and write steps of n two-step concurrent database transactions and a time-dependent predicate representing queries giving the sets of data items accessed by those read and write steps at given points in time. The models of FOTLT(n) contain interleaved sequences of the steps of infinitely many occurrences of the n transactions accessing unlimited data over time. A property of (...) serializability is specified for FOTLT(n) formulae. We show that the serializability problem for FOTLT(n) formulae is decidable. (shrink)

We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are well-designed to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger LTL. Related formalisms are also briefly presented.

As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order (...) fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented. (shrink)

We study term modal logics, where modalities can be indexed by variables that can be quantified over. We suggest that these logics are appropriate for reasoning about systems of unboundedly many reasoners and define a notion of bisimulation which preserves propositional fragment of term modal logics. Also we show that the propositional fragment is already undecidable but that its monodic fragment is decidable, and expressive enough to include interesting assertions.