On the Complexity of Verifying Timed Golog Programs over Description Logic Actions: Extended Version

Golog programs allow to model complex behaviour of agents by combining primitive actions defined in a Situation Calculus theory using imperative and non-deterministic programming language constructs. In general, verifying temporal properties of Golog programs is undecidable. One way to establish decidability is to restrict the logic used by the program to a Description Logic (DL), for which recently some complexity upper bounds for verification problem have been established. However, so far it was open whether these results are tight, and lightweight DLs such as EL have not been studied at all. Furthermore, these results only apply to a setting where actions do not consume time, and the properties to be verified only refer to the timeline in a qualitative way. In a lot of applications, this is an unrealistic assumption. In this work, we study the verification problem for timed Golog programs, in which actions can be assigned differing durations, and temporal properties are specified in a metric branching time logic. This allows to annotate temporal properties with time intervals over which they are evaluated, to specify for example that some property should hold for at least n time units, or should become specified within some specified time window. We establish tight complexity bounds of the verification problem for both expressive and lightweight DLs. Our lower bounds already apply to a very limited fragment of the verification problem, and close open complexity bounds for the non-metrical cases studied before