Subclasses of FO(LTL)
In the following, we assume that non-constant function symbols and equality are not allowed. The addition of them can lead to the loss of decidability for any of the subclasses introduced here.
Monadic FO(LTL), proposed by Hodkinson et al. [1] in 2000, is the first non-trivial decidable subclass of FO(LTL). This class contains all sub-formulas beginning with a temporal operator (Since
or Until) have at most one free variable. Thus, we can
talk about objects in the intended domain using the full power of first-order logic; however, temporal operators may be used to describe the development in
time of only one object (two are enough to simulate the behaviour of Turing machines).
The satisfiability problem for formulas in this class can be reduced to fragments of classical two-sorted
first-order logics in which one sort is intended for temporal reasoning. The decidability results also hold for the temporal logics with finite domains.
Remark. FO(LTL) provides only ‘implicit’ access to time: quantification over points in time in the sense of first-order logic is not
permitted, and the only means of expressing temporal properties is by the temporal operators Since
and Until. It turns out that monadic FO(LTL) is weaker than the two-sorted first-order language, where one sort of which refers to points in time and the other to the
first-order domain. For example, the formula $∃t_1 ∃t_2 (t_1 < t_2 ∧ ∀x(P(t_1, x) ↔ P(t_2, x)))$ is not expressible in FO(LTL) over any interesting class of linear time structures [2, 3].
References
1. Decidable fragments of first-order temporal logics.2. Temporal Logic. Part I & Part II. Clarendon Press, Oxford.
3. Temporal connectives versus explicit timestamps in temporal query languages.
No comments:
Post a Comment