Monodic fragments of predicate temporal logic
Go to home page | Clare
Dixon's page of related papers
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.
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.
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.
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.
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.
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.
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).
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.
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.