On the Complexity of Verifying Timed Golog Programs over Description Logic Actions. Koopmann, P. & Zarriess, B. In Workshop on Hybrid Reasoning and Learning @ KR 2018, pages 9. abstract bibtex 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). 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.
@inproceedings{koopmann_complexity_nodate,
title = {On the {Complexity} of {Verifying} {Timed} {Golog} {Programs} over {Description} {Logic} {Actions}},
abstract = {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). 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.},
language = {en},
booktitle = {Workshop on {Hybrid} {Reasoning} and {Learning} @ {KR} 2018},
author = {Koopmann, Patrick and Zarriess, Benjamin},
keywords = {hrl18},
pages = {9}
}
Downloads: 0
{"_id":"Jq3LyDmcaRCubSZnK","bibbaseid":"koopmann-zarriess-onthecomplexityofverifyingtimedgologprogramsoverdescriptionlogicactions","authorIDs":[],"author_short":["Koopmann, P.","Zarriess, B."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"On the Complexity of Verifying Timed Golog Programs over Description Logic Actions","abstract":"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). 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.","language":"en","booktitle":"Workshop on Hybrid Reasoning and Learning @ KR 2018","author":[{"propositions":[],"lastnames":["Koopmann"],"firstnames":["Patrick"],"suffixes":[]},{"propositions":[],"lastnames":["Zarriess"],"firstnames":["Benjamin"],"suffixes":[]}],"keywords":"hrl18","pages":"9","bibtex":"@inproceedings{koopmann_complexity_nodate,\n\ttitle = {On the {Complexity} of {Verifying} {Timed} {Golog} {Programs} over {Description} {Logic} {Actions}},\n\tabstract = {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). 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.},\n\tlanguage = {en},\n\tbooktitle = {Workshop on {Hybrid} {Reasoning} and {Learning} @ {KR} 2018},\n\tauthor = {Koopmann, Patrick and Zarriess, Benjamin},\n\tkeywords = {hrl18},\n\tpages = {9}\n}\n\n","author_short":["Koopmann, P.","Zarriess, B."],"key":"koopmann_complexity_nodate","id":"koopmann_complexity_nodate","bibbaseid":"koopmann-zarriess-onthecomplexityofverifyingtimedgologprogramsoverdescriptionlogicactions","role":"author","urls":{},"keyword":["hrl18"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/tillhofmann","creationDate":"2019-12-09T14:42:18.245Z","downloads":0,"keywords":["hrl18"],"search_terms":["complexity","verifying","timed","golog","programs","over","description","logic","actions","koopmann","zarriess"],"title":"On the Complexity of Verifying Timed Golog Programs over Description Logic Actions","year":null,"dataSources":["9pYjFWPBodPyDyb7N"]}