Temporal Logics over Transitive States

12 years 12 months ago
Temporal Logics over Transitive States
Abstract. We investigate the computational behaviour of `two-dimensional' propositional temporal logics over (N, <) (with and without the next-time operator ?) that are capable of reasoning about states with transitive relations. Such logics are known to be undecidable (even 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 ?-free logics are decidable (but not in primitive recursive time); on the other hand, when equipped with ? they are not even recursively enumerable. Finally, we sho...
Boris Konev, Frank Wolter, Michael Zakharyaschev
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Boris Konev, Frank Wolter, Michael Zakharyaschev
Comments (0)