We investigate the computational behaviour of
‘two-dimen\-sional’ propositional temporal logics over (\nat
,<) (with and without the next-time operator \nxt) that
are capable of reasoning about states with transitive
relations. Such logics are known to be undecidable (even
\Pi^1_1-complete) if the domains of states with those
relations are assumed to be constant. Motivated by
applications in the areas of temporal description logic and
specification & verification of hybrid systems, in this
paper we analyse the computational impact of allowing the
domains of states to expand. We show that over finite
expanding domains (with an arbitrary, tree-like, quasi-order,
or linear transitive relation) the logics are recursively
enumerable, but undecidable. If these finite domains
eventually become constant then the resulting \nxt-free
logics are decidable (but not in primitive recursive time);
on the other hand, when equipped with \nxt they are not
even recursively enumerable. Finally, we show that temporal
logics over infinite expanding domains as above are
undecidable even for the language with the sole temporal
operator ‘eventually.’ The proofs are based on Kruskal’s tree
theorem and reductions of reachability problems for lossy
channel systems.
×