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...

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Boris Konev, Frank Wolter, Michael Zakharyaschev
• Keywords: Automated Reasoning, CADE 2005, Linear Transitive Relation, Lossy Channel Systems, Primitive Recursive Time