Monodic fragments of predicate temporal logic

Go to home page   |   Clare Dixon's page of related papers

Decidable fragments of first-order temporal logics

Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev
Ann. Pure. Appl. Logic 106 (2000) 85-134.
Copyright Elsevier Science BV 2000.  doi: 10.1016/S0168-0072(00)00018-X
In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable.  We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic.  This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning.  Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains.  We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps.

Monodic packed fragment with equality is decidable

Ian Hodkinson
Studia Logica 72 (2002) 185-197.
This paper proves decidability of satisfiability of sentences of the monodic packed fragment of first-order temporal logic with equality and connectives Until and Since, in models with various flows of time and  domains of arbitrary cardinality. It also proves decidability over models with finite domains, over flows of time including the real order.

Monodic fragments of first-order temporal logics: 2000--2001 A.D.

I Hodkinson, F Wolter, M Zakharyaschev
In R. Nieuwenhuis and A. Voronkov, editors, Logic for Programming, Artificial Intelligence and Reasoning, number 2250 of LNAI, Springer, 2001, pages 1-23.
The aim of this paper is to summarize and analyze some results obtained in 2000--2001 about decidable and undecidable fragments of various first-order temporal logics, give some applications in the field of knowledge representation and reasoning, and attract the attention of the `temporal community' to a number of interesting open problems.

Decidable and undecidable fragments of first-order branching temporal logics

I Hodkinson, F Wolter, M Zakharyaschev
Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 393--402.
The link is to the draft version (17 pages)
In this paper we analyze the decision problem for fragments of first-order extensions of branching time temporal logics such as computational tree logics CTL and CTL* or Prior's Ockhamist logic of historical necessity. On the one hand, we show that the one-variable fragments of logics like first-order CTL* - such as the product of propositional CTL* with simple propositional modal logic S5, or even the one-variable bundled first-order temporal logic with sole temporal operator `some time in the future' - are undecidable.  On the other hand, it is proved that by restricting applications of first-order quantifiers to state (i.e., path-independent) formulas, and applications of temporal operators and path quantifiers to formulas with at most one free variable, we can obtain decidable fragments.  The same arguments show decidability of `non-local' propositional CTL*, in which truth values of propositional atoms depends on the history as well as the current time.  The positive decidability results can serve as a unifying framework for devising expressive and effective time-dependent knowledge representation formalisms, e.g., temporal description or spatio-temporal logics.

On non-local propositional and one-variable quantified CTL*

S Bauer, I Hodkinson, F Wolter, M Zakharyaschev
(This link is to the full version.  Abbreviated version in Proc. TIME'02, IEEE Inc., pp2-9.)
Here we prove decidability of the so-called weak one-variable fragment of first-order CTL*, in which quantifiers are not restricted to state formulas, but only the next-time operator may be applied to open formulas, while all other temporal operators and path quantifiers are applicable only to sentences. To obtain this result, we first show decidability of the non-local version of propositional CTL*, where truth values of atoms may depend on the branch of evaluation, and then reduce the weak one-variable fragment to this logic.

On Non-local Propositional and Weak Monodic Quantified CTL*

S Bauer, I Hodkinson, F Wolter, M Zakharyaschev
Journal of Logic and Computation 14 (2004) pp 3-22.
In this paper we prove decidability of two kinds of branching time temporal logics. First we show that the non-local version of propositional PCTL*, in which truth values of atoms may depend on the branch of evaluation, is decidable. Then we use this result to establish decidability of various fragments of quantified PCTL*, where the next-time operator can be applied only to formulas with at most one free variable, all other temporal operators and path quantifiers are applicable only to sentences, and the first-order constructs follow the pattern of any of several decidable fragments of first-order logic.

On the computational complexity of decidable fragments of first-order linear temporal logics

Ian Hodkinson, Roman Kontchakov, Agi Kurucz, Frank Wolter, Michael Zakharyaschev
Proc. TIME-ICTL 2003 (M Reynolds and A Sattar, eds.), IEEE, 2003, pp. 91-98.
We study the complexity of some fragments of first-order temporal logic over natural numbers time.  The one-variable fragment of linear first-order temporal logic even with sole temporal operator Box is EXPSPACE-complete (this solves an open problem of Halpern and Vardi).  So are the one-variable, two-variable and monadic monodic fragments with Until and Since.  If we add the operators X^n (tomorrow^n), with n given in binary, the fragments become 2EXPSPACE-complete. The packed monodic fragment has the same complexity as its pure first-order part - 2EXPTIME-complete.  Over rationals and real numbers time as well as over arbitrary strict linear orders, we obtain EXPSPACE lower bounds (which solves an open problem of Reynolds).

Complexity of monodic guarded fragments over linear and real time

I Hodkinson
Ann. Pure Appl. Logic 138 (2006) 94-125.
We show that the satisfiability problem for the monodic guarded and packed fragments with equality and arbitrary first-order domains over linear time, dense linear time, rational numbers time, and some other classes of linear flows of time, is 2Exptime-complete.  We then show that with finite first-order domains, these fragments are also 2Exptime-complete over real numbers 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.

First-order temporal logic with fixpoint operators over the natural numbers

Konstantinos Mamouras
Distinguished MSc project, 2009, done under my supervision.
We show that the satisfiability problem formonodic first-order linear time temporal logic with temporal fixpoint operators and no equality over the flow of the natural numbers is in EXPSPACE (2EXPTIME), if the purely first-order part of the language is restricted to a fragment of first-order logic that lies in EXPSPACE (2EXPTIME). The same upper complexity bound holds for the finite satisfiability problem. For the monodic packed fragment with equality we show 2EXPTIME-completeness and EXPSPACE-completeness for the bounded-variable or bounded-arity case. We also consider the monodic guarded and loosely guarded fragments with temporal fixpoints as well as domain-side least fixpoints and show 2EXPTIME-completeness (EXPSPACE-completeness for the bounded-variable or bounded-arity case) of the satisfiability problem over arbitrary domains.