Content: Publications

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

In Proc. Workshop on Hybrid Reasoning and Learning (HRL 2018)

Authors:Patrick Koopmann, Benjamin Zarrieß
Type:Article in Conference Proceedings
Publication Date:October 2018
Download:KoopmannZarriess2018.pdf
Conference:Workshop on Hybrid Reasoning and Learning (HRL 2018)

Abstract: Golog programs allow to model complex behaviour of agents by combining primitive actions defined in a Situation Calcu lus 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). However, while complexity upper bounds for Golog programs over DL actions have recently been studied for expressive DLs, 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. We therefore study the verification of metric temporal properties for discrete-timed Golog programs, where actions can be assigned a durations, and provide tight complexity bounds for both expressive and lightweight description logics. Our lower bounds already apply to a very limited fragment of the verification problem, and also close the open complexity bounds for the non-metrical case studied before.

BibTeX
@InProceedings{hybris-a1-timed-golog-2018,
  title =	{{On the Complexity of Verifying Timed Golog Programs over Description Logic Actions}},
  author =	{Patrick Koopmann and Benjamin Zarrieß},
  booktitle =	{Proc. of Workshop on Hybrid Reasoning and Learning (HRL 2018)},
  year =	{2018},
}